Incorporate PC's comments on InductiveTypes

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. *)
+(** 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. *)
 
 
 (** * Enumerations *)
@@ -118,7 +118,7 @@ Inductive bool : Set :=
 
 (** We can use less vacuous pattern matching to define boolean negation. *)
 
-Definition not (b : bool) : bool :=
+Definition negb (b : bool) : bool :=
   match b with
     | true => false
     | false => true
@@ -126,12 +126,12 @@ Definition not (b : bool) : bool :=
 
 (** An alternative definition desugars to the above: *)
 
-Definition not' (b : bool) : bool :=
+Definition negb' (b : bool) : bool :=
   if b then false else true.
 
-(** We might want to prove that [not] is its own inverse operation. *)
+(** We might want to prove that [negb] is its own inverse operation. *)
 
-Theorem not_inverse : forall b : bool, not (not b) = b.
+Theorem negb_inverse : forall b : bool, negb (negb b) = b.
 (* begin thide *)
   destruct b.
 
@@ -141,12 +141,12 @@ Theorem not_inverse : forall b : bool, not (not b) = b.
 2 subgoals
   
   ============================
-   not (not true) = true
+   negb (negb true) = true
 ]]
 
 [[
 subgoal 2 is:
- not (not false) = false
+ negb (negb false) = false
  
 ]]
 
@@ -163,7 +163,7 @@ Qed.
 
 (** Another theorem about booleans illustrates another useful tactic. *)
 
-Theorem not_ineq : forall b : bool, not b <> b.
+Theorem negb_ineq : forall b : bool, negb b <> b.
 (* begin thide *)
   destruct b; discriminate.
 Qed.
@@ -936,7 +936,7 @@ Section nat_tree_ind'.
 
   ]]
 
-  Coq rejects this definition, saying "Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest."  The term "nested inductive type" hints at the solution to the problem.  Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *)
+  Coq rejects this definition, saying "Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest."  There is no deep theoretical reason why this program should be rejected; Coq applies incomplete termination-checking heuristics, and it is necessary to learn a few of the most important rules.  The term "nested inductive type" hints at the solution to this particular problem.  Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *)
 
   Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
     match tr with

src/Intro.v

@@ -180,7 +180,7 @@ The source code to the book is also freely available at:
 
 There, you can find all of the code appearing in this book, with prose interspersed in comments, in exactly the order that you find in this document.  You can step through the code interactively with your chosen graphical Coq interface.  The code also has special comments indicating which parts of the chapters make suitable starting points for interactive class sessions, where the class works together to construct the programs and proofs.  The included Makefile has a target %\texttt{%#<tt>#templates#</tt>#%}% for building a fresh set of class template files automatically from the book source.
 
-I believe that a good graphical interface to Coq is crucial for using it productively.  I use the %Proof General\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}}%#<a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a># mode for Emacs, which supports a number of other proof assistants besides Coq.  There is also the standalone 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] command, which CoqIDE does not support.  It would be bad form to leave [Abort] 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.
+I believe that a good graphical interface to Coq is crucial for using it productively.  I use the %Proof General\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}}%#<a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a># mode for Emacs, which supports a number of other proof assistants besides Coq.  There is also the standalone 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 [Restart] 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.
 
 The next chapter will introduce Coq with some simple examples, and the chapter starts with step-by-step instructions on getting set up to run the book chapters interactively, assuming that you have Coq and Proof General installed.
 *)

src/StackMachine.v

@@ -19,7 +19,9 @@ Set Implicit Arguments.
 (** %\chapter{Some Quick Examples}% *)
 
 
-(** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq version 8.2pl2, though parts may work with other versions.
+(** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  This chapter is not meant to give full explanations of the features that are employed.  Rather, it is meant more as an advertisement of what is possible.  Later chapters will introduce all of the concepts in bottom-up fashion.
+
+I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq version 8.2pl2, though parts may work with other versions.
 
 To set up your Proof General environment to process the source to this chapter, a few simple steps are required.
 
@@ -606,10 +608,10 @@ Definition typeDenote (t : type) : Set :=
 We need to define one auxiliary function, implementing a boolean binary "less-than" operator, which only appears in the standard library with a type fancier than what we are prepared to deal with here.  The code is entirely standard and ML-like, with the one caveat being that the Coq [nat] type uses a unary representation, where [O] is zero and [S n] is the successor of [n].
 *)
 
-Fixpoint lt (n1 n2 : nat) : bool :=
+Fixpoint lessThan (n1 n2 : nat) : bool :=
   match n1, n2 with
     | O, S _ => true
-    | S n1', S n2' => lt n1' n2'
+    | S n1', S n2' => lessThan n1' n2'
     | _, _ => false
   end.
 
@@ -623,7 +625,7 @@ Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
     | TTimes => mult
     | TEq Nat => beq_nat
     | TEq Bool => eqb
-    | TLt => lt
+    | TLt => lessThan
   end.
 
 (** 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 %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks.  In each branch of the [match], we need to use branch-specific information about the indices to [tbinop].  General type inference that takes such information into account is undecidable, so it is often necessary to write annotations, like we see above on the line with [match].
@@ -642,7 +644,7 @@ Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
     | TTimes => mult
     | TEq Nat => beq_nat
     | TEq Bool => eqb
-    | TLt => lt
+    | TLt => lessThan
   end.
 
 (**