Batch of changes based on proofreader feedback

src/GeneralRec.v

@@ -853,7 +853,7 @@ Theorem cassociativity : forall A B C (m : comp A) (f : A -> comp B) (g : B -> c
 Qed.
 (* end hide *)
 
-(** Not only can we define the Fibonacci function with the new monad, but even our running example of merge sort becomes definable.  By shadowing our previous notation for "bind,", we can write almost exactly the same code as in our previous [mergeSort'] definition, but with less syntactic clutter. *)
+(** Not only can we define the Fibonacci function with the new monad, but even our running example of merge sort becomes definable.  By shadowing our previous notation for "bind," we can write almost exactly the same code as in our previous [mergeSort'] definition, but with less syntactic clutter. *)
 
 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)).
 

src/InductiveTypes.v

@@ -60,16 +60,11 @@ Check (fun _ : False => I).
 Check (fun x : False => x).
 (** [: False -> False] *)
 
-(** %\smallskip{}%In fact, [False] implies anything, and we can take advantage of this fact with an odd looking [match] expression that has no branches.  Since there are no rules for deducing [False], there are no cases to consider! *)
-
-Check (fun x : False => match x with end : True).
-(** [: False -> True] *)
-
 (** %\smallskip{}%Every one of these example programs whose type looks like a logical formula is a%\index{proof term}% _proof term_.  We use that name for any Gallina term of a logical type, and we will elaborate shortly on what makes a type logical.
 
-In the rest of this chapter, we will introduce different ways of defining types.  Every example type can be interpreted alternatively as a type of programs or %\index{proposition}%propositions (i.e., formulas or theorem statements).
+In the rest of this chapter, we will introduce different ways of defining types.  Every example type can be interpreted alternatively as a type of programs or proofs.
 
-One of the first types we introduce will be [bool], with constructors [true] and [false].  Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false].  One glib answer is that [True] and [False] are types, but [true] and [false] are not.  A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false].  This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool].  Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that.  We ought to be glad that we have no algorithm for deciding mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like most any properties of general-purpose programs. *)
+One of the first types we introduce will be [bool], with constructors [true] and [false].  Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false].  One glib answer is that [True] and [False] are types, but [true] and [false] are not.  A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false].  This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool].  Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that.  We ought to be glad that we have no algorithm for deciding mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like almost any interesting property of general-purpose programs. *)
 
 
 (** * Enumerations *)
@@ -253,15 +248,7 @@ Definition pred (n : nat) : nat :=
     | S n' => n'
   end.
 
-(** We can prove theorems by case analysis: *)
-
-Theorem S_isZero : forall n : nat, isZero (pred (S (S n))) = false.
-(* begin thide *)
-  destruct n; reflexivity.
-Qed.
-(* end thide *)
-
-(** We can also now get into genuine inductive theorems.  First, we will need a recursive function, to make things interesting.%\index{Gallina terms!plus}% *)
+(** We can prove theorems by case analysis with [destruct] as for simpler inductive types, but we can also now get into genuine inductive theorems.  First, we will need a recursive function, to make things interesting.%\index{Gallina terms!plus}% *)
 
 Fixpoint plus (n m : nat) : nat :=
   match n with
@@ -287,7 +274,7 @@ Theorem n_plus_O : forall n : nat, plus n O = n.
 
   reflexivity.
 
-(** Our second subgoal is more work and also demonstrates our first inductive hypothesis.
+(** Our second subgoal requires more work and also demonstrates our first inductive hypothesis.
 
 [[
   n : nat
@@ -489,11 +476,9 @@ Section list.
 (* end thide *)
 End list.
 
-(* begin hide *)
 Implicit Arguments Nil [T].
-(* end hide *)
 
-(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  We verify that this has happened using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
+(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  With an [Implicit Arguments]%~\index{Vernacular commands!Implicit Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter.  We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
 
 Print list.
 (** %\vspace{-.15in}% [[
@@ -627,7 +612,7 @@ Qed.
 
 (** * Reflexive Types *)
 
-(** A kind of inductive type called a _reflexive type_ is defined in terms of functions that have the type being defined as their range.  One very useful class of examples is in modeling variable binders.  Our example will be an encoding of the syntax of first-order logic.  Since the idea of syntactic encodings of logic may require a bit of acclimation, let us first consider a simpler formula type for a subset of propositional logic. *)
+(** A kind of inductive type called a _reflexive type_ includes at least one constructor that takes as an argument _a function returning the same type we are defining_.  One very useful class of examples is in modeling variable binders.  Our example will be an encoding of the syntax of first-order logic.  Since the idea of syntactic encodings of logic may require a bit of acclimation, let us first consider a simpler formula type for a subset of propositional logic.  We are not yet using a reflexive type, but later we will extend the example reflexively. *)
 
 Inductive pformula : Set :=
 | Truth : pformula
@@ -704,7 +689,7 @@ Focusing on the [Forall] case, which comes third, we see that we are allowed to
 
 %\medskip%
 
-Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in %\index{Haskell}%Haskell and %\index{ML}%ML.  This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes.  In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness.  Reflexive types provide our first good example of such a case.
+Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in %\index{Haskell}%Haskell and %\index{ML}%ML.  This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes.  In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness.  Reflexive types provide our first good example of such a case; only some of them are legal.
 
 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of %\index{lambda calculus}%lambda calculus.  Indeed, the function-based representation technique that we just used, called%\index{higher-order abstract syntax}\index{HOAS|see{higher-order abstract syntax}}% _higher-order abstract syntax_ (HOAS)%~\cite{HOAS}%, is the representation of choice for lambda calculi in %\index{Twelf}%Twelf and in many applications implemented in Haskell and ML.  Let us try to import that choice to Coq: *)
 (* begin hide *)
@@ -800,7 +785,7 @@ The only new wrinkle here is the annotations on the [match] expression.  This is
 To prove that [unit_rect] is nothing special, we can reimplement it manually. *)
 
 Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) :=
-  match u with
+  match u return P u with
     | tt => f
   end.
 
@@ -810,9 +795,7 @@ Definition foo := nat_rect.
 (* end thide *)
 (* end hide *)
 
-(** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms.
-
-We can check the implementation [nat_rect] as well: *)
+(** We can check the implementation [nat_rect] as well: *)
 
 Print nat_rect.
 (** %\vspace{-.15in}% [[

src/LogicProg.v

@@ -406,7 +406,7 @@ Example three_minus_four_zero : exists x, 1 + x = 0.
 Finished transaction in 0. secs (0.004u,0.s)
 >>
 
-This [eauto] fails to prove the goal, but it least it takes substantially less than the 2 seconds required above! *)
+This [eauto] fails to prove the goal, but at least it takes substantially less than the 2 seconds required above! *)
 
 Abort.
 (* end thide *)

src/Predicates.v

@@ -373,6 +373,8 @@ We will see more about Coq's program extraction facility in a later chapter.  Ho
     ex_intro : forall x : A, P x -> ex P
     ]]
 
+  (Note that here, as always, each [forall] quantifier has the largest possible scope, so that the type of [ex_intro] could also be written [forall x : A, (P x -> ex P)].)
+
   The family [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s.  We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x].  As usual, there are tactics that save us from worrying about the low-level details most of the time.  We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic.  For our purposes, it is. *)
 
 Theorem exist1 : exists x : nat, x + 1 = 2.
@@ -519,7 +521,7 @@ Theorem isZero_contra' : isZero 1 -> 2 + 2 = 5.
  
    ]]
 
-   What on earth happened here?  Internally, [destruct] replaced [1] with a fresh variable, and, trying to be helpful, it also replaced the occurrence of [1] within the unary representation of each number in the goal.  This has the net effect of decrementing each of these numbers. *)
+   What on earth happened here?  Internally, [destruct] replaced [1] with a fresh variable, and, trying to be helpful, it also replaced the occurrence of [1] within the unary representation of each number in the goal.  Then, within the [O] case of the proof, we replace the fresh variable with [O].  This has the net effect of decrementing each of these numbers. *)
 
 Abort.
 

src/StackMachine.v

@@ -42,7 +42,7 @@ A note for readers following along in the PDF version: %\index{coqdoc}%coqdoc su
 
 %\medskip%
 
-Now we are ready to say what these programs mean.  We will do this by writing an %\index{interpreters}%interpreter that can be thought of as a trivial operational or denotational semantics.  (If you are not familiar with these semantic techniques, no need to worry; we will stick to "common sense" constructions.)%\index{Vernacular commands!Definition}% *)
+Now we are ready to say what programs in our expression language mean.  We will do this by writing an %\index{interpreters}%interpreter that can be thought of as a trivial operational or denotational semantics.  (If you are not familiar with these semantic techniques, no need to worry; we will stick to "common sense" constructions.)%\index{Vernacular commands!Definition}% *)
 
 Definition binopDenote (b : binop) : nat -> nat -> nat :=
   match b with
@@ -187,13 +187,12 @@ Eval simpl in progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2))
 (** We are ready to prove that our compiler is implemented correctly.  We can use a new vernacular command [Theorem] to start a correctness proof, in terms of the semantics we defined earlier:%\index{Vernacular commands!Theorem}% *)
 
 Theorem compile_correct : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
-(* begin hide *)
-Abort.
-(* end hide *)
 (* begin thide *)
 
 (** Though a pencil-and-paper proof might clock out at this point, writing "by a routine induction on [e]," it turns out not to make sense to attack this proof directly.  We need to use the standard trick of%\index{strengthening the induction hypothesis}% _strengthening the induction hypothesis_.  We do that by proving an auxiliary lemma, using the command [Lemma] that is a synonym for [Theorem], conventionally used for less important theorems that appear in the proofs of primary theorems.%\index{Vernacular commands!Lemma}% *)
 
+Abort.
+
 Lemma compile_correct' : forall e p s,
   progDenote (compile e ++ p) s = progDenote p (expDenote e :: s).
 
@@ -393,7 +392,7 @@ We start out the same way as before, introducing new free variables and unfoldin
 
 What we need is the associative law of list concatenation, which is available as a theorem [app_assoc_reverse] in the standard library.%\index{Vernacular commands!Check}% *)
 
-Check app_assoc.
+Check app_assoc_reverse.
 (** %\vspace{-.15in}%[[
 app_assoc_reverse
      : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
@@ -554,7 +553,7 @@ The intuitive explanation of [tbinop] is that a [tbinop t1 t2 t] is a binary ope
 
 ML and Haskell have indexed algebraic datatypes.  For instance, their list types are indexed by the type of data that the list carries.  However, compared to Coq, ML and Haskell 98 place two important restrictions on datatype definitions.
 
-First, the indices of the range of each data constructor must be type variables bound at the top level of the datatype definition.  There is no way to do what we did here, where we, for instance, say that [TPlus] is a constructor building a [tbinop] whose indices are all fixed at [Nat].  %\index{generalized algebraic datatypes}\index{GADTs|see{generalized algebraic datatypes}}% _Generalized algebraic datatypes_ (GADTs)%~\cite{GADT}% are a popular feature in %\index{GHC Haskell}%GHC Haskell and other languages that removes this first restriction.
+First, the indices of the range of each data constructor must be type variables bound at the top level of the datatype definition.  There is no way to do what we did here, where we, for instance, say that [TPlus] is a constructor building a [tbinop] whose indices are all fixed at [Nat].  %\index{generalized algebraic datatypes}\index{GADTs|see{generalized algebraic datatypes}}% _Generalized algebraic datatypes_ (GADTs)%~\cite{GADT}% are a popular feature in %\index{GHC Haskell}%GHC Haskell, OCaml 4, and other languages that removes this first restriction.
 
 The second restriction is not lifted by GADTs.  In ML and Haskell, indices of types must be types and may not be _expressions_.  In Coq, types may be indexed by arbitrary Gallina terms.  Type indices can live in the same universe as programs, and we can compute with them just like regular programs.  Haskell supports a hobbled form of computation in type indices based on %\index{Haskell}%multi-parameter type classes, and recent extensions like type functions bring Haskell programming even closer to "real" functional programming with types, but, without dependent typing, there must always be a gap between how one programs with types and how one programs normally.
 *)

src/Subset.v

@@ -519,17 +519,17 @@ End In_dec.
 Eval compute in In_dec eq_nat_dec 2 (1 :: 2 :: nil).
 (** %\vspace{-.15in}% [[
      = Yes
-     : {In 2 (1 :: 2 :: nil)} + {~ In 2 (1 :: 2 :: nil)}
+     : {In 2 (1 :: 2 :: nil)} + { ~ In 2 (1 :: 2 :: nil)}
      ]]
      *)
 
 Eval compute in In_dec eq_nat_dec 3 (1 :: 2 :: nil).
 (** %\vspace{-.15in}% [[
      = No
-     : {In 3 (1 :: 2 :: nil)} + {~ In 3 (1 :: 2 :: nil)}
+     : {In 3 (1 :: 2 :: nil)} + { ~ In 3 (1 :: 2 :: nil)}
      ]]
 
-[In_dec] has a reasonable extraction to OCaml. *)
+The [In_dec] function has a reasonable extraction to OCaml. *)
 
 Extraction In_dec.
 (* end thide *)

staging/updates.rss

@@ -11,6 +11,14 @@
 <webMaster>adam@chlipala.net</webMaster>
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
+<item>
+        <title>Batch of changes based on proofreader feedback</title>
+        <pubDate>Wed, 26 Sep 2012 16:31:01 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+        <description>Thanks to everyone who is helping with the final proofreading!</description>
+</item>
+
 <item>
         <title>Ready for final proofreading</title>
         <pubDate>Thu, 30 Aug 2012 08:31:25 EDT</pubDate>