Batch of changes based on proofreader feedback

src/Coinductive.v

@@ -57,7 +57,7 @@ CoInductive evilStream := Nil.
 
 (** The definition is surprisingly simple.  Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive].  We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite.
 
-   How do we write down a stream constant?  Obviously simple application of constructors is not good enough, since we could only denote finite objects that way.  Rather, whereas recursive definitions were necessary to _use_ values of recursive inductive types effectively, here we find that we need%\index{co-recursive definitions}% _co-recursive definitions_ to _build_ values of co-inductive types effectively.
+   How do we write down a stream constant?  Obviously, simple application of constructors is not good enough, since we could only denote finite objects that way.  Rather, whereas recursive definitions were necessary to _use_ values of recursive inductive types effectively, here we find that we need%\index{co-recursive definitions}% _co-recursive definitions_ to _build_ values of co-inductive types effectively.
 
    We can define a stream consisting only of zeroes.%\index{Vernacular commands!CoFixpoint}% *)
 
@@ -191,11 +191,13 @@ CoFixpoint bad : stream nat := tl (Cons 0 bad).
 
 Imagine that Coq had accepted our definition, and consider how we might evaluate [approx bad 1].  We would be trying to calculate the first element in the stream [bad].  However, it is not hard to see that the definition of [bad] "begs the question": unfolding the definition of [tl], we see that we essentially say "define [bad] to equal itself"!  Of course such an equation admits no single well-defined solution, which does not fit well with the determinism of Gallina reduction.
 
-Since Coq can be considered to check definitions after inlining and simplification of previously defined identifiers, the basic guardedness condition rules out our definition of [bad].  Such an inlining reduces [bad] to:
+Coq's complete rule for co-recursive definitions includes not just the basic guardedness condition, but also a requirement about where co-recursive calls may occur.  In particular, a co-recursive call must be a direct argument to a constructor, _nested only inside of other constructor calls or [fun] or [match] expressions_.  In the definition of [bad], we erroneously nested the co-recursive call inside a call to [tl], and we nested inside a call to [interleave] in the definition of [map'].
+
+Coq helps the user out a little by performing the guardedness check after using computation to simplify terms.  For instance, any co-recursive function definition can be expanded by inserting extra calls to an identity function, and this change preserves guardedness.  However, in other cases computational simplification can reveal why definitions are dangerous.  Consider what happens when we inline the definition of [tl] in [bad]:
 [[
 CoFixpoint bad : stream nat := bad.
 ]]
-This is the same looping definition we rejected earlier.  A similar inlining process reveals the way that Coq saw our failed definition of [map']:
+This is the same looping definition we rejected earlier.  A similar inlining process reveals an alternate view on our failed definition of [map']:
 [[
 CoFixpoint map' (s : stream A) : stream B :=
   match s with
@@ -384,7 +386,7 @@ Theorem ones_eq' : stream_eq ones ones'.
   *)
 Abort.
 
-(** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness.  One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case.  Alternatively, there are tricks that can be played with "hiding" the co-inductive hypothesis.
+(** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness.  A correct proof strategy for a theorem like this usually starts by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case.  Alternatively, there are tricks that can be played with "hiding" the co-inductive hypothesis.
 
    %\medskip%
 
@@ -404,7 +406,7 @@ Definition hd A (s : stream A) : A :=
 Section stream_eq_coind.
   Variable A : Type.
   Variable R : stream A -> stream A -> Prop.
-  (** This relation generalizes the theorem we want to prove, characterizing exactly which two arguments to [stream_eq] we want to consider. *)
+  (** This relation generalizes the theorem we want to prove, defining a set of pairs of streams that we must eventually prove contains the particular pair we care about. *)
 
   Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
   Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).
@@ -494,7 +496,7 @@ Eval simpl in approx fact_slow 5.
      : list nat
 ]]
 
-Now, to prove that the two versions are equivalent, it is helpful to prove (and add as a proof hint) a quick lemma about the computational behavior of [fact]. *)
+Now, to prove that the two versions are equivalent, it is helpful to prove (and add as a proof hint) a quick lemma about the computational behavior of [fact].  (I intentionally skip explaining its proof at this point.) *)
 
 (* begin thide *)
 Lemma fact_def : forall x n,
@@ -547,7 +549,7 @@ Qed.
 
 (** We close the chapter with a quick motivating example for more complex uses of co-inductive types.  We will define a co-inductive semantics for a simple imperative programming language and use that semantics to prove the correctness of a trivial optimization that removes spurious additions by 0.  We follow the technique of%\index{co-inductive big-step operational semantics}% _co-inductive big-step operational semantics_ %\cite{BigStep}%.
 
-   We define a suggestive synonym for [nat], as we will consider programs with infinitely many variables, represented as [nat]s. *)
+   We define a suggestive synonym for [nat], as we will consider programs over infinitely many variables, represented as [nat]s. *)
 
 Definition var := nat.
 
@@ -578,7 +580,7 @@ Inductive cmd : Set :=
 | Seq : cmd -> cmd -> cmd
 | While : exp -> cmd -> cmd.
 
-(** We could define an inductive relation to characterize the results of command evaluation.  However, such a relation would not capture _nonterminating_ executions.  With a co-inductive relation, we can capture both cases.  The parameters of the relation are an initial state, a command, and a final state.  A program that does not terminate in a particular initial state is related to _any_ final state. *)
+(** We could define an inductive relation to characterize the results of command evaluation.  However, such a relation would not capture _nonterminating_ executions.  With a co-inductive relation, we can capture both cases.  The parameters of the relation are an initial state, a command, and a final state.  A program that does not terminate in a particular initial state is related to _any_ final state.  For more realistic languages than this one, it is often possible for programs to _crash_, in which case a semantics would generally relate their executions to no final states; so relating safely non-terminating programs to all final states provides a crucial distinction. *)
 
 CoInductive evalCmd : vars -> cmd -> vars -> Prop :=
 | EvalAssign : forall vs v e, evalCmd vs (Assign v e) (set vs v (evalExp vs e))

src/InductiveTypes.v

@@ -20,7 +20,7 @@ Set Implicit Arguments.
 
 \chapter{Introducing Inductive Types}% *)
 
-(** In a sense, CIC is built from just two relatively straightforward features: function types and inductive types.  From this modest foundation, we can prove effectively all of the theorems of math and carry out effectively all program verifications, with enough effort expended.  This chapter introduces induction and recursion for functional programming in Coq.  Most of our examples reproduce functionality from the Coq standard library, and we have tried to copy the standard library's choices of identifiers, where possible, so many of the definitions here are already available in the default Coq environment.
+(** In a sense, CIC is built from just two relatively straightforward features: function types and inductive types.  From this modest foundation, we can prove effectively all of the theorems of math and carry out effectively all program verifications, with enough effort expended.  This chapter introduces induction and recursion for functional programming in Coq.  Most of our examples reproduce functionality from the Coq standard library, and I have tried to copy the standard library's choices of identifiers, where possible, so many of the definitions here are already available in the default Coq environment.
 
 The last chapter took a deep dive into some of the more advanced Coq features, to highlight the unusual approach that I advocate in this book.  However, from this point on, we will rewind and go back to basics, presenting the relevant features of Coq in a more bottom-up manner.  A useful first step is a discussion of the differences and relationships between proofs and programs in Coq. *)
 
@@ -64,7 +64,7 @@ Check (fun x : False => x).
 
 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 almost any interesting property 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 our formalized version of 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 *)
@@ -76,7 +76,7 @@ The singleton type [unit] is an inductive type:%\index{Gallina terms!unit}\index
 Inductive unit : Set :=
   | tt.
 
-(** This vernacular command defines a new inductive type [unit] whose only value is [tt], as we can see by checking the types of the two identifiers: *)
+(** This vernacular command defines a new inductive type [unit] whose only value is [tt].  We can verify the types of the two identifiers we introduce: *)
 
 Check unit.
 (** [unit : Set] *)
@@ -322,7 +322,7 @@ Theorem S_inj : forall n m : nat, S n = S m -> n = m.
 Qed.
 (* end thide *)
 
-(** The [injection] tactic refers to a premise by number, adding new equalities between the corresponding arguments of equated terms that are formed with the same constructor.  We end up needing to prove [n = m -> n = m], so it is unsurprising that a tactic named [trivial] is able to finish the proof.
+(** The [injection] tactic refers to a premise by number, adding new equalities between the corresponding arguments of equated terms that are formed with the same constructor.  We end up needing to prove [n = m -> n = m], so it is unsurprising that a tactic named [trivial] is able to finish the proof.  This tactic attempts a variety of single proof steps, drawn from a user-specified database that we will later see how to extend.
 
 There is also a very useful tactic called %\index{tactics!congruence}%[congruence] that can prove this theorem immediately.  The [congruence] tactic generalizes [discriminate] and [injection], and it also adds reasoning about the general properties of equality, such as that a function returns equal results on equal arguments.  That is, [congruence] is a%\index{theory of equality and uninterpreted functions}% _complete decision procedure for the theory of equality and uninterpreted functions_, plus some smarts about inductive types.
 
@@ -368,12 +368,14 @@ Check nat_list_ind.
 
 %\medskip%
 
-In general, we can implement any "tree" types as inductive types.  For example, here are binary trees of naturals. *)
+In general, we can implement any "tree" type as an inductive type.  For example, here are binary trees of naturals. *)
 
 Inductive nat_btree : Set :=
 | NLeaf : nat_btree
 | NNode : nat_btree -> nat -> nat_btree -> nat_btree.
 
+(** Here are two functions whose intuitive explanations are not so important.  The first one computes the size of a tree, and the second performs some sort of splicing of one tree into the leftmost available leaf node of another. *)
+
 Fixpoint nsize (tr : nat_btree) : nat :=
   match tr with
     | NLeaf => S O
@@ -401,7 +403,7 @@ Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2)
 Qed.
 (* end thide *)
 
-(** It is convenient that these proofs go through so easily, but it is useful to check that the tree induction principle works as usual. *)
+(** It is convenient that these proofs go through so easily, but it is still useful to look into the details of what happened, by checking the statement of the tree induction principle. *)
 
 Check nat_btree_ind.
 (** %\vspace{-.15in}% [[
@@ -505,7 +507,7 @@ Check list_ind.
        forall l : list T, P l
 ]]
 
-Thus, even though we just saw that [T] is added as an extra argument to the constructor [Cons], there is no quantifier for [T] in the type of the inductive case like there is for each of the other arguments. *)
+Thus, even though we just saw that [T] is added as an extra argument to the constructor [Cons], the inductive case in the type of [list_ind] (i.e., the third line of the type) includes no quantifier for [T], even though all of the other arguments are quantified explicitly.  Parameters in other inductive definitions are treated similarly in stating induction principles. *)
 
 
 (** * Mutually Inductive Types *)
@@ -586,13 +588,23 @@ Check even_list_mut.
        forall e : even_list, P e
 ]]
 
-This is the principle we wanted in the first place.  There is one more wrinkle left in using it: the [induction] tactic will not apply it for us automatically.  It will be helpful to look at how to prove one of our past examples without using [induction], so that we can then generalize the technique to mutual inductive types.%\index{tactics!apply}% *)
+This is the principle we wanted in the first place.
+
+The [Scheme] command is for asking Coq to generate particular induction schemes that are mutual among a set of inductive types (possibly only one such type, in which case we get a normal induction principle).  In a sense, it generalizes the induction scheme generation that goes on automatically for each inductive definition.  Future Coq versions might make that automatic generation smarter, so that [Scheme] is needed in fewer places.  In a few sections, we will see how induction principles are derived theorems in Coq, so that there is not actually any need to build in _any_ automatic scheme generation.
+
+There is one more wrinkle left in using the [even_list_mut] induction principle: the [induction] tactic will not apply it for us automatically.  It will be helpful to look at how to prove one of our past examples without using [induction], so that we can then generalize the technique to mutual inductive types.%\index{tactics!apply}% *)
 
 Theorem n_plus_O' : forall n : nat, plus n O = n.
+  apply nat_ind.
+  (** Here we use [apply], which is one of the most essential basic tactics.  When we are trying to prove fact [P], and when [thm] is a theorem whose conclusion can be made to match [P] by proper choice of quantified variable values, the invocation [apply thm] will replace the current goal with one new goal for each premise of [thm].
+
+     This use of [apply] may seem a bit _too_ magical.  To better see what is going on, we use a variant where we partially apply the theorem [nat_ind] to give an explicit value for the predicate that gives our induction hypothesis. *)
+
+  Undo.
   apply (nat_ind (fun n => plus n O = n)); crush.
 Qed.
 
-(** From this example, we can see that [induction] is not magic.  It only does some bookkeeping for us to make it easy to apply a theorem, which we can do directly with the [apply] tactic.  We apply not just an identifier but a partial application of it, specifying the predicate we mean to prove holds for all naturals.
+(** From this example, we can see that [induction] is not magic.  It only does some bookkeeping for us to make it easy to apply a theorem, which we can do directly with the [apply] tactic.
 
 This technique generalizes to our mutual example: *)
 
@@ -905,25 +917,29 @@ End formula_ind'.
 (** Suppose we want to extend our earlier type of binary trees to trees with arbitrary finite branching.  We can use lists to give a simple definition. *)
 
 Inductive nat_tree : Set :=
-| NLeaf' : nat_tree
 | NNode' : nat -> list nat_tree -> nat_tree.
 
 (** This is an example of a%\index{nested inductive type}% _nested_ inductive type definition, because we use the type we are defining as an argument to a parameterized type family.  Coq will not allow all such definitions; it effectively pretends that we are defining [nat_tree] mutually with a version of [list] specialized to [nat_tree], checking that the resulting expanded definition satisfies the usual rules.  For instance, if we replaced [list] with a type family that used its parameter as a function argument, then the definition would be rejected as violating the positivity restriction.
 
 Like we encountered for mutual inductive types, we find that the automatically generated induction principle for [nat_tree] is too weak. *)
 
+(* begin hide *)
+(* begin thide *)
+Check Forall.
+(* end thide *)
+(* end hide *)
+
 Check nat_tree_ind.
 (** %\vspace{-.15in}% [[
   nat_tree_ind
      : forall P : nat_tree -> Prop,
-       P NLeaf' ->
        (forall (n : nat) (l : list nat_tree), P (NNode' n l)) ->
        forall n : nat_tree, P n
 ]]
 
-There is no command like [Scheme] that will implement an improved principle for us.  In general, it takes creativity to figure out how to incorporate nested uses of different type families.  This is roughly the same creativity employed in the traditional task of strengthening an induction hypothesis.  Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem.
+There is no command like [Scheme] that will implement an improved principle for us.  In general, it takes creativity to figure out _good_ ways to incorporate nested uses of different type families.  Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem.
 
-First, we will need an auxiliary definition, characterizing what it means for a property to hold of every element of a list. *)
+Many induction principles for types with nested used of [list] could benefit from a unified predicate capturing the idea that some property holds of every element in a list.  By defining this generic predicate once, we facilitate reuse of library theorems about it.  (Here, we are actually duplicating the standard library's [Forall] predicate, with a different implementation, for didactic purposes.) *)
 
 Section All.
   Variable T : Set.
@@ -971,7 +987,6 @@ Now we create a section for our induction principle, following the same basic pl
 Section nat_tree_ind'.
   Variable P : nat_tree -> Prop.
 
-  Hypothesis NLeaf'_case : P NLeaf'.
   Hypothesis NNode'_case : forall (n : nat) (ls : list nat_tree),
     All P ls -> P (NNode' n ls).
 
@@ -986,7 +1001,6 @@ Section nat_tree_ind'.
   %\vspace{-.15in}%[[
   Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
     match tr with
-      | NLeaf' => NLeaf'_case
       | NNode' n ls => NNode'_case n ls (list_nat_tree_ind ls)
     end
 
@@ -1007,12 +1021,11 @@ Section nat_tree_ind'.
 
   Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
     match tr with
-      | NLeaf' => NLeaf'_case
       | NNode' n ls => NNode'_case n ls
         ((fix list_nat_tree_ind (ls : list nat_tree) : All P ls :=
           match ls with
             | Nil => I
-            | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest)
+            | Cons tr' rest => conj (nat_tree_ind' tr') (list_nat_tree_ind rest)
           end) ls)
     end.
 
@@ -1043,7 +1056,6 @@ Fixpoint sum (ls : list nat) : nat :=
 
 Fixpoint ntsize (tr : nat_tree) : nat :=
   match tr with
-    | NLeaf' => S O
     | NNode' _ trs => S (sum (map ntsize trs))
   end.
 
@@ -1051,7 +1063,6 @@ Fixpoint ntsize (tr : nat_tree) : nat :=
 
 Fixpoint ntsplice (tr1 tr2 : nat_tree) : nat_tree :=
   match tr1 with
-    | NLeaf' => NNode' O (Cons tr2 Nil)
     | NNode' n Nil => NNode' n (Cons tr2 Nil)
     | NNode' n (Cons tr trs) => NNode' n (Cons (ntsplice tr tr2) trs)
   end.

src/Intro.v

@@ -16,7 +16,7 @@
 
 We would all like to have programs check that our programs are correct.  Due in no small part to some bold but unfulfilled promises in the history of computer science, today most people who write software, practitioners and academics alike, assume that the costs of formal program verification outweigh the benefits.  The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science.  Beyond the convincing, I also want to provide a handbook on practical engineering of certified programs with the Coq proof assistant.  Almost every subject covered is also relevant to interactive computer theorem-proving in general, such as for traditional mathematical theorems.  In fact, I hope to demonstrate how verified programs are useful as building blocks in all sorts of formalizations.
 
-Research into mechanized theorem proving began around the 1970s, and some of the earliest practical work involved Nqthm%~\cite{Nqthm}\index{Nqthm}%, the "Boyer-Moore Theorem Prover," which was used to prove such theorems as correctness of a complete hardware and software stack%~\cite{Piton}%.  ACL2%~\cite{CAR}\index{ACL2}%, Nqthm's successor, has seen significant industry adoption, for instance, by AMD to verify correctness of floating-point division units%~\cite{AMD}%.
+Research into mechanized theorem proving began in the second half of the 20th century, and some of the earliest practical work involved Nqthm%~\cite{Nqthm}\index{Nqthm}%, the "Boyer-Moore Theorem Prover," which was used to prove such theorems as correctness of a complete hardware and software stack%~\cite{Piton}%.  ACL2%~\cite{CAR}\index{ACL2}%, Nqthm's successor, has seen significant industry adoption, for instance, by AMD to verify correctness of floating-point division units%~\cite{AMD}%.
 
 Around the beginning of the 21st century, the pace of progress in practical applications of interactive theorem proving accelerated significantly.  Several well-known formal developments have been carried out in Coq, the system that this book deals with.  In the realm of pure mathematics, Georges Gonthier built a machine-checked proof of the four color theorem%~\cite{4C}%, a mathematical problem first posed more than a hundred years before, where the only previous proofs had required trusting ad-hoc software to do brute-force checking of key facts.  In the realm of program verification, Xavier Leroy led the CompCert project to produce a verified C compiler back-end%~\cite{CompCert}% robust enough to use with real embedded software.
 
@@ -130,7 +130,7 @@ On the other hand, Agda, Epigram, and similar tools have less implementation bag
 (**
 In comparisons with its competitors, Coq is often derided for promoting unreadable proofs.  It is very easy to write proof scripts that manipulate proof goals imperatively, with no structure to aid readers.  Such developments are nightmares to maintain, and they certainly do not manage to convey "why the theorem is true" to anyone but the original author.  One additional (and not insignificant) purpose of this book is to show why it is unfair and unproductive to dismiss Coq based on the existence of such developments.
 
-I will go out on a limb and guess that the reader is a fan of some programming language, and that he may even have been involved in teaching that language to undergraduates.  I want to propose an analogy between two attitudes: coming to a negative conclusion about Coq after reading common Coq developments in the wild, and coming to a negative conclusion about Your Favorite Language after looking at the programs undergraduates write in it in the first week of class.  The pragmatics of mechanized proving and program verification have been under serious study for much less time than the pragmatics of programming have been.  The computer theorem proving community is still developing the key insights that correspond to those that programming texts and instructors impart to their students, to help those students get over that critical hump where using the language stops being more trouble than it is worth.  Most of the insights for Coq are barely even disseminated among the experts, let alone set down in a tutorial form.  I hope to use this book to go a long way towards remedying that.
+I will go out on a limb and guess that the reader is a fan of some programming language and may even have been involved in teaching that language to undergraduates.  I want to propose an analogy between two attitudes: coming to a negative conclusion about Coq after reading common Coq developments in the wild, and coming to a negative conclusion about Your Favorite Language after looking at the programs undergraduates write in it in the first week of class.  The pragmatics of mechanized proving and program verification have been under serious study for much less time than the pragmatics of programming have been.  The computer theorem proving community is still developing the key insights that correspond to those that programming texts and instructors impart to their students, to help those students get over that critical hump where using the language stops being more trouble than it is worth.  Most of the insights for Coq are barely even disseminated among the experts, let alone set down in a tutorial form.  I hope to use this book to go a long way towards remedying that.
 
 If I do that job well, then this book should be of interest even to people who have participated in classes or tutorials specifically about Coq.  The book should even be useful to people who have been using Coq for years but who are mystified when their Coq developments prove impenetrable by colleagues.  The crucial angle in this book is that there are "design patterns" for reliably avoiding the really grungy parts of theorem proving, and consistent use of these patterns can get you over the hump to the point where it is worth your while to use Coq to prove your theorems and certify your programs, even if formal verification is not your main concern in a project.  We will follow this theme by pursuing two main methods for replacing manual proofs with more understandable artifacts: dependently typed functions and custom Ltac decision procedures.
 *)
@@ -159,19 +159,19 @@ There, you can find all of the code appearing in this book, with prose intersper
 
 A traditional printed version of the book is slated to appear from MIT Press in the future.  The online versions will remain available at no cost even after the printed book is released, and I intend to keep the source code up-to-date with bug fixes and compatibility changes to track new Coq releases.
 
-%\index{graphical interfaces to Coq}%I believe that a good graphical interface to Coq is crucial for using it productively.  I use the %\index{Proof General}%{{http://proofgeneral.inf.ed.ac.uk/}Proof General} mode for Emacs, which supports a number of other proof assistants besides Coq.  There is also the standalone %\index{CoqIDE}%CoqIDE program developed by the Coq team.  I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor, and CoqIDE has had a good number of crashes and other annoying bugs in recent history, though I hear that it is improving.  In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it.  The one issue with CoqIDE, regarding running through the book source, is that I will sometimes begin a proof attempt but cancel it with the Coq [Abort] or #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Restart%}%#</span></span># commands, which CoqIDE does not support.  It would be bad form to leave such commands lying around in a real, finished development, but I find these commands helpful in writing single source files that trace a user's thought process in designing a proof.
+%\index{graphical interfaces to Coq}%I believe that a good graphical interface to Coq is crucial for using it productively.  I use the %\index{Proof General}%{{http://proofgeneral.inf.ed.ac.uk/}Proof General} mode for Emacs, which supports a number of other proof assistants besides Coq.  There is also the standalone %\index{CoqIDE}%CoqIDE program developed by the Coq team.  I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor.  In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it.  The one issue with CoqIDE, regarding running through the book source, is that I will sometimes begin a proof attempt but cancel it with the Coq [Abort] or #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Restart%}%#</span></span># commands, which CoqIDE does not support.  It would be bad form to leave such commands lying around in a real, finished development, but I find these commands helpful in writing single source files that trace a user's thought process in designing a proof.
 *)
 
 (** ** Reading This Book *)
 
 (**
-For experts in functional programming or formal methods, learning to use Coq is not hard, in a sense.  The Coq manual%~\cite{CoqManual}% and the textbook by Bertot and Cast%\'%eran%~\cite{CoqArt}% have helped many people become productive Coq users.  However, I believe that the best ways to manage significant Coq developments are far from settled.  In this book, I mean to propose my own techniques, and, rather than treating them as advanced material for a final chapter or two, I employ them from the very beginning.  After a first chapter showing off what can be done with dependent types, I retreat into simpler programming styles for the first part of the book.  I adopt the other main thrust of the book, Ltac proof automation, more or less from the very start of the technical exposition.
+For experts in functional programming or formal methods, learning to use Coq is not hard, in a sense.  The Coq manual%~\cite{CoqManual}%, the textbook by Bertot and Cast%\'%eran%~\cite{CoqArt}%, and Pierce et al.'s %\emph{%Software Foundations%}\footnote{\url{http://www.cis.upenn.edu/~bcpierce/sf/}}% have helped many people become productive Coq users.  However, I believe that the best ways to manage significant Coq developments are far from settled.  In this book, I mean to propose my own techniques, and, rather than treating them as advanced material for a final chapter or two, I employ them from the very beginning.  After a first chapter showing off what can be done with dependent types, I retreat into simpler programming styles for the first part of the book.  I adopt the other main thrust of the book, Ltac proof automation, more or less from the very start of the technical exposition.
 
 Some readers have suggested that I give multiple recommended reading orders in this introduction, targeted at people with different levels of Coq expertise.  It is certainly true that Part I of the book devotes significant space to basic concepts that most Coq users already know quite well.  However, as I am introducing these concepts, I am also developing my preferred automated proof style, so I think even the chapters on basics are worth reading for experienced Coq hackers.
 
 Readers with no prior Coq experience can ignore the preceding discussion!  I hope that my heavy reliance on proof automation early on will seem like the most natural way to go, such that you may wonder why others are spending so much time entering sequences of proof steps manually.
 
-Coq is a very complex system, with many different commands driven more by pragmatic concerns than by any overarching aesthetic principle.  When I use some construct for the first time, I try to give a one-sentence intuition for what it accomplishes, but I leave the details to the Coq reference manual%~\cite{CoqManual}%.  I expect that readers interested in complete understandings will be consulting that manual frequently; in that sense, this book is not meant to be completely standalone.  I often use constructs in code snippets without first introducing them at all, but explanations should always follow in the prose paragraphs immediately after the offending snippets.
+Coq is a very complex system, with many different commands driven more by pragmatic concerns than by any overarching aesthetic principle.  When I use some construct for the first time, I try to give a one-sentence intuition for what it accomplishes, but I leave the details to the Coq reference manual%~\cite{CoqManual}%.  I expect that readers interested in complete understanding will be consulting that manual frequently; in that sense, this book is not meant to be completely standalone.  I often use constructs in code snippets without first introducing them at all, but explanations should always follow in the prose paragraphs immediately after the offending snippets.
 
 Previous versions of the book included some suggested exercises at the ends of chapters.  Since then, I have decided to remove the exercises and focus on the main book exposition.  Especially in the domain of interactive theorem proving, keeping exercises at the proper difficulty level is a lot of work, I have learned!  My advice to readers is to learn to use Coq by getting started applying it in their own real projects, rather than focusing on artificial exercises.
 *)

src/Predicates.v

@@ -56,7 +56,7 @@ With that perspective in mind, this chapter is sort of a mirror image of the las
 
 (** * Propositional Logic *)
 
-(** Let us begin with a brief tour through the definitions of the connectives for propositional logic.  We will work within a Coq section that provides us with a set of propositional variables.  In Coq parlance, these are just terms of type [Prop.] *)
+(** Let us begin with a brief tour through the definitions of the connectives for propositional logic.  We will work within a Coq section that provides us with a set of propositional variables.  In Coq parlance, these are just variables of type [Prop]. *)
 
 Section Propositional.
   Variables P Q R : Prop.
@@ -101,7 +101,7 @@ We have also already seen the definition of [True].  For a demonstration of a lo
 (* begin thide *)
     intro.
 
-    (** At this point, we have an inconsistent hypothesis [2 + 2 = 5], so the specific conclusion is not important.  We use the %\index{tactics!elimtype}%[elimtype] tactic to state a proposition, telling Coq that we wish to construct a proof of the new proposition and then prove the original goal by case analysis on the structure of the new auxiliary proof.  Since [False] has no constructors, [elimtype False] simply leaves us with the obligation to prove [False]. *)
+    (** At this point, we have an inconsistent hypothesis [2 + 2 = 5], so the specific conclusion is not important.  We use the %\index{tactics!elimtype}%[elimtype] tactic.  For a full description of it, see the Coq manual.  For our purposes, we only need the variant [elimtype False], which lets us replace any conclusion formula with [False], because any fact follows from an inconsistent context. *)
 
     elimtype False.
     (** [[
@@ -294,7 +294,7 @@ subgoal 2 is
 (* end thide *)
   Qed.
 
-  (** Sometimes propositional reasoning forms important plumbing for the proof of a theorem, but we still need to apply some other smarts about, say, arithmetic.  The tactic %\index{tactics!intuition}%[intuition] is a generalization of [tauto] that proves everything it can using propositional reasoning.  When some goals remain, it uses propositional laws to simplify them as far as possible.  Consider this example, which uses the list concatenation operator [++] from the standard library. *)
+  (** Sometimes propositional reasoning forms important plumbing for the proof of a theorem, but we still need to apply some other smarts about, say, arithmetic.  The tactic %\index{tactics!intuition}%[intuition] is a generalization of [tauto] that proves everything it can using propositional reasoning.  When some further facts must be established to finish the proof, [intuition] uses propositional laws to simplify them as far as possible.  Consider this example, which uses the list concatenation operator %\coqdocnotation{%#<tt>#++#</tt>#%}% from the standard library. *)
 
   Theorem arith_comm : forall ls1 ls2 : list nat,
     length ls1 = length ls2 \/ length ls1 + length ls2 = 6
@@ -350,10 +350,12 @@ End Propositional.
 
 (** * What Does It Mean to Be Constructive? *)
 
-(** One potential point of confusion in the presentation so far is the distinction between [bool] and [Prop].  The datatype [bool] is built from two values [true] and [false], while [Prop] is a more primitive type that includes among its members [True] and [False].  Why not collapse these two concepts into one, and why must there be more than two states of mathematical truth?
+(** One potential point of confusion in the presentation so far is the distinction between [bool] and [Prop].  The datatype [bool] is built from two values [true] and [false], while [Prop] is a more primitive type that includes among its members [True] and [False].  Why not collapse these two concepts into one, and why must there be more than two states of mathematical truth, [True] and [False]?
 
 The answer comes from the fact that Coq implements%\index{constructive logic}% _constructive_ or%\index{intuitionistic logic|see{constructive logic}}% _intuitionistic_ logic, in contrast to the%\index{classical logic}% _classical_ logic that you may be more familiar with.  In constructive logic, classical tautologies like [~ ~ P -> P] and [P \/ ~ P] do not always hold.  In general, we can only prove these tautologies when [P] is%\index{decidability}% _decidable_, in the sense of %\index{computability|see{decidability}}%computability theory.  The Curry-Howard encoding that Coq uses for [or] allows us to extract either a proof of [P] or a proof of [~ P] from any proof of [P \/ ~ P].  Since our proofs are just functional programs which we can run, a general %\index{law of the excluded middle}%law of the excluded middle would give us a decision procedure for the halting problem, where the instantiations of [P] would be formulas like "this particular Turing machine halts."
 
+A similar paradoxical situation would result if every proposition evaluated to either [True] or [False].  Evaluation in Coq is decidable, so we would be limiting ourselves to decidable propositions only.
+
 Hence the distinction between [bool] and [Prop].  Programs of type [bool] are computational by construction; we can always run them to determine their results.  Many [Prop]s are undecidable, and so we can write more expressive formulas with [Prop]s than with [bool]s, but the inevitable consequence is that we cannot simply "run a [Prop] to determine its truth."
 
 Constructive logic lets us define all of the logical connectives in an aesthetically appealing way, with orthogonal inductive definitions.  That is, each connective is defined independently using a simple, shared mechanism.  Constructivity also enables a trick called%\index{program extraction}% _program extraction_, where we write programs by phrasing them as theorems to be proved.  Since our proofs are just functional programs, we can extract executable programs from our final proofs, which we could not do as naturally with classical proofs.
@@ -375,7 +377,9 @@ We will see more about Coq's program extraction facility in a later chapter.  Ho
 
   (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. *)
+  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.
+
+  Here is an example of a theorem statement with existential quantification.  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.
 (* begin thide *)
@@ -809,7 +813,7 @@ Qed.
 
 (** We write the proof in a way that avoids the use of local variable or hypothesis names, using the %\index{tactics!match}%[match] tactic form to do pattern-matching on the goal.  We use unification variables prefixed by question marks in the pattern, and we take advantage of the possibility to mention a unification variable twice in one pattern, to enforce equality between occurrences.  The hint to rewrite with [plus_n_Sm] in a particular direction saves us from having to figure out the right place to apply that theorem, and we also take critical advantage of a new tactic, %\index{tactics!eauto}%[eauto].
 
-The [crush] tactic uses the tactic [intuition], which, when it runs out of tricks to try using only propositional logic, by default tries the tactic [auto], which we saw in an earlier example.  The [auto] tactic attempts %\index{Prolog}%Prolog-style logic programming, searching through all proof trees up to a certain depth that are built only out of hints that have been registered with [Hint] commands.  (See Chapter 13 for a first-principles introduction to what we mean by "Prolog-style logic programming.")  Compared to Prolog, [auto] places an important restriction: it never introduces new unification variables during search.  That is, every time a rule is applied during proof search, all of its arguments must be deducible by studying the form of the goal.  This restriction is relaxed for [eauto], at the cost of possibly exponentially greater running time.  In this particular case, we know that [eauto] has only a small space of proofs to search, so it makes sense to run it.  It is common in effectively automated Coq proofs to see a bag of standard tactics applied to pick off the "easy" subgoals, finishing with [eauto] to handle the tricky parts that can benefit from ad-hoc exhaustive search.
+The [crush] tactic uses the tactic [intuition], which, when it runs out of tricks to try using only propositional logic, by default tries the tactic [auto], which we saw in an earlier example.  For now, think of [eauto] as a potentially more expensive version of [auto] that considers more possible proofs; see Chapter 13 for more detail.  The quick summary is that [eauto] considers applying a lemma even when the form of the current goal doesn not uniquely determine the values of all of the lemma's quantified variables.
 
 The original theorem now follows trivially from our lemma. *)
 

src/StackMachine.v

@@ -148,7 +148,7 @@ Fixpoint progDenote (p : prog) (s : stack) : option stack :=
 
 (** ** Translation *)
 
-(** Our compiler itself is now unsurprising.  The list concatenation operator %\index{Gallina operators!++}%[++] comes from the Coq standard library. *)
+(** Our compiler itself is now unsurprising.  The list concatenation operator %\index{Gallina operators!++}\coqdocnotation{%#<tt>#++#</tt>#%}% comes from the Coq standard library. *)
 
 Fixpoint compile (e : exp) : prog :=
   match e with
@@ -303,7 +303,7 @@ We only need to unfold the first occurrence of [progDenote] to prove the goal.
  
 ]]
 
-This last [unfold] has left us with an anonymous fixpoint version of [progDenote], which will generally happen when unfolding recursive definitions.  Note that Coq has automatically renamed the [fix] arguments [p] and [s] to [p0] and [s0], to avoid clashes with our local free variables.  There is also a subterm [None (A:=stack)], which has an annotation specifying that the type of the term ought to be [option stack].  This is phrased as an explicit instantiation of a named type parameter [A] from the definition of [option].
+This last [unfold] has left us with an anonymous recursive definition of [progDenote] (similarly to how [fun] or "lambda" constructs in general allow anonymous non-recursive functions), which will generally happen when unfolding recursive definitions.  Note that Coq has automatically renamed the [fix] arguments [p] and [s] to [p0] and [s0], to avoid clashes with our local free variables.  There is also a subterm [None (A:=stack)], which has an annotation specifying that the type of the term ought to be [option stack].  This is phrased as an explicit instantiation of a named type parameter [A] from the definition of [option].
 
 Fortunately, in this case, we can eliminate the complications of anonymous recursion right away, since the structure of the argument ([iConst n :: nil) ++ p] is known, allowing us to simplify the internal pattern match with the [simpl] tactic, which applies the same reduction strategy that we used earlier with [Eval] (and whose details we still postpone).%\index{tactics!simpl}%
 *)
@@ -390,7 +390,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}% *)
+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}%  (Here and elsewhere, it is possible to tell the difference between inputs and outputs to Coq by periods at the ends of the inputs.) *)
 
 Check app_assoc_reverse.
 (** %\vspace{-.15in}%[[
@@ -587,8 +587,7 @@ Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
 
 (** This function has just a few differences from the denotation functions we saw earlier.  First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote].  Second, we need to perform a genuine%\index{dependent pattern matching}% _dependent pattern match_, where the necessary _type_ of each case body depends on the _value_ that has been matched.  At this early stage, we will not go into detail on the many subtle aspects of Gallina that support dependent pattern-matching, but the subject is central to Part II of the book.
 
-The same tricks suffice to define an expression denotation function in an unsurprising way:
-*)
+The same tricks suffice to define an expression denotation function in an unsurprising way.  Note that the [type] arguments to the [TBinop] constructor must be included explicitly in pattern-matching, but here we write underscores because we do not need to refer to those arguments directly. *)
 
 Fixpoint texpDenote t (e : texp t) : typeDenote t :=
   match e with

src/Subset.v

@@ -107,7 +107,7 @@ The term [zgtz pf] fails to type-check.  Somehow the type checker has failed to
 
 In this case, we must use a [return] annotation to declare the relationship between the _value_ of the [match] discriminee and the _type_ of the result.  There is no annotation that lets us declare a relationship between the discriminee and the type of a variable that is already in scope; hence, we delay the binding of [pf], so that we can use the [return] annotation to express the needed relationship.
 
-We are lucky that Coq's heuristics infer the [return] clause (specifically, [return n > 0 -> nat]) for us in this case. *)
+We are lucky that Coq's heuristics infer the [return] clause (specifically, [return n > 0 -> nat]) for us in the definition of [pred_strong1], leading to the following elaborated code: *)
 
 Definition pred_strong1' (n : nat) : n > 0 -> nat :=
   match n return n > 0 -> nat with
@@ -139,6 +139,8 @@ let pred_strong1 = function
 
 (** The proof argument has disappeared!  We get exactly the OCaml code we would have written manually.  This is our first demonstration of the main technically interesting feature of Coq program extraction: proofs are erased systematically.
 
+%\medskip%
+
 We can reimplement our dependently typed [pred] based on%\index{subset types}% _subset types_, defined in the standard library with the type family %\index{Gallina terms!sig}%[sig]. *)
 
 (* begin hide *)
@@ -389,7 +391,7 @@ Inductive sumbool (A : Prop) (B : Prop) : Set :=
     left : A -> {A} + {B} | right : B -> {A} + {B}
 ]]
 
-We can define some notations to make working with [sumbool] more convenient. *)
+Here, the constructors of [sumbool] have types written in terms of a registered notation for [sumbool], such that the result type of each constructor desugars to [sumbool A B].  We can define some notations of our own to make working with [sumbool] more convenient. *)
 
 Notation "'Yes'" := (left _ _).
 Notation "'No'" := (right _ _).
@@ -638,7 +640,7 @@ Eval compute in pred_strong8 0.
 
 (** * Monadic Notations *)
 
-(** We can treat [maybe] like a monad%~\cite{Monads}\index{monad}\index{failure monad}%, in the same way that the Haskell <<Maybe>> type is interpreted as a failure monad.  Our [maybe] has the wrong type to be a literal monad, but a "bind"-like notation will still be helpful. *)
+(** We can treat [maybe] like a monad%~\cite{Monads}\index{monad}\index{failure monad}%, in the same way that the Haskell <<Maybe>> type is interpreted as a failure monad.  Our [maybe] has the wrong type to be a literal monad, but a "bind"-like notation will still be helpful.  %Note that the notation definition uses an ASCII \texttt{<-}, while later code uses (in this rendering) a nicer left arrow $\leftarrow$.% *)
 
 Notation "x <- e1 ; e2" := (match e1 with
                              | Unknown => ??
@@ -661,7 +663,7 @@ Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd
 Defined.
 (* end thide *)
 
-(** We can build a [sumor] version of the "bind" notation and use it to write a similarly straightforward version of this function.  %The operator rendered here as $\longleftarrow$ is noted in the source as a less-than character followed by two hyphens.% *)
+(** We can build a [sumor] version of the "bind" notation and use it to write a similarly straightforward version of this function.  %Again, the notation definition exposes the ASCII syntax with an operator \texttt{<-{}-}, while the later code uses a nicer long left arrow $\longleftarrow$.% *)
 
 Notation "x <-- e1 ; e2" := (match e1 with
                                | inright _ => !!
@@ -896,7 +898,7 @@ Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~
         [||TBool||]
     end); clear F; crush' tt hasType; eauto.
 
-  (** We clear [F], the local name for the recursive function, to avoid strange proofs that refer to recursive calls that we never make.  The [crush] variant %\index{tactics!crush'}%[crush'] helps us by performing automatic inversion on instances of the predicates specified in its second argument.  Once we throw in [eauto] to apply [hasType_det] for us, we have discharged all the subgoals. *)
+  (** We clear [F], the local name for the recursive function, to avoid strange proofs that refer to recursive calls that we never make.  Such a step is usually warranted when defining a recursive function with [refine].  The [crush] variant %\index{tactics!crush'}%[crush'] helps us by performing automatic inversion on instances of the predicates specified in its second argument.  Once we throw in [eauto] to apply [hasType_det] for us, we have discharged all the subgoals. *)
 (* 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>Mon, 8 Oct 2012 16:04:09 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>Batch of changes based on proofreader feedback</title>
         <pubDate>Tue, 2 Oct 2012 11:34:17 EDT</pubDate>