Proofreading pass through Chapter 3

src/InductiveTypes.v

@@ -104,7 +104,7 @@ Theorem unit_singleton : forall x : unit, x = tt.
 ]]
 *)
 
-  (** ...which we can discharge trivially. *)
+  (** %\noindent{}%...which we can discharge trivially. *)
 
   reflexivity.
 Qed.
@@ -160,13 +160,13 @@ Definition e2u (e : Empty_set) : unit := match e with end.
 
 %\medskip%
 
-Moving up the ladder of complexity, we can define the booleans:%\index{Gallina terms!bool}\index{Gallina terms!true}\index{Gallina terms!false}% *)
+Moving up the ladder of complexity, we can define the Booleans:%\index{Gallina terms!bool}\index{Gallina terms!true}\index{Gallina terms!false}% *)
 
 Inductive bool : Set :=
 | true
 | false.
 
-(** We can use less vacuous pattern matching to define boolean negation.%\index{Gallina terms!negb}% *)
+(** We can use less vacuous pattern matching to define Boolean negation.%\index{Gallina terms!negb}% *)
 
 Definition negb (b : bool) : bool :=
   match b with
@@ -209,7 +209,7 @@ Restart.
 Qed.
 (* end thide *)
 
-(** Another theorem about booleans illustrates another useful tactic.%\index{tactics!discriminate}% *)
+(** Another theorem about Booleans illustrates another useful tactic.%\index{tactics!discriminate}% *)
 
 Theorem negb_ineq : forall b : bool, negb b <> b.
 (* begin thide *)
@@ -217,7 +217,7 @@ Theorem negb_ineq : forall b : bool, negb b <> b.
 Qed.
 (* end thide *)
 
-(** [discriminate] is used to prove that two values of an inductive type are not equal, whenever the values are formed with different constructors.  In this case, the different constructors are [true] and [false].
+(** The [discriminate] tactic is used to prove that two values of an inductive type are not equal, whenever the values are formed with different constructors.  In this case, the different constructors are [true] and [false].
 
 At this point, it is probably not hard to guess what the underlying induction principle for [bool] is. *)
 
@@ -305,7 +305,7 @@ We can start out by using computation to simplify the goal as far as we can.%\in
 
   rewrite IHn.
 
-(** ...we get a trivial conclusion [S n = S n]. *)
+(** %\noindent{}%...we get a trivial conclusion [S n = S n]. *)
 
   reflexivity.
 
@@ -599,7 +599,6 @@ Check even_list_mut.
        (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->
        (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) ->
        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}% *)
@@ -635,7 +634,13 @@ Inductive pformula : Set :=
 | Falsehood : pformula
 | Conjunction : pformula -> pformula -> pformula.
 
-(** A key distinction here is between, for instance, the _syntax_ [Truth] and its _semantics_ [True].  We can make the semantics explicit with a recursive function.  This function uses the infix operator %\index{Gallina operators!/\textbackslash}%[/\], which desugars to uses of the type family %\index{Gallina terms!and}%[and] from the standard library.  The family [and] implements conjunction, the [Prop] Curry-Howard analogue of the usual pair type from functional programming (which is the type family %\index{Gallina terms!prod}%[prod] in Coq's standard library). *)
+(* begin hide *)
+(* begin thide *)
+Definition prod' := prod.
+(* end thide *)
+(* end hide *)
+
+(** A key distinction here is between, for instance, the _syntax_ [Truth] and its _semantics_ [True].  We can make the semantics explicit with a recursive function.  This function uses the infix operator %\index{Gallina operators!/\textbackslash}%[/\], which desugared to uses of the type family %\index{Gallina terms!and}%[and] from the standard library.  The family [and] implements conjunction, the [Prop] Curry-Howard analogue of the usual pair type from functional programming (which is the type family %\index{Gallina terms!prod}%[prod] in Coq's standard library). *)
 
 Fixpoint pformulaDenote (f : pformula) : Prop :=
   match f with
@@ -989,7 +994,7 @@ In addition to the definition of [and] itself, we get information on %\index{imp
 
 %\medskip%
 
-Now we create a section for our induction principle, following the same basic plan as in the last section of this chapter. *)
+Now we create a section for our induction principle, following the same basic plan as in the previous section of this chapter. *)
 
 Section nat_tree_ind'.
   Variable P : nat_tree -> Prop.
@@ -1163,7 +1168,7 @@ This is the point in the proof where we apply some creativity.  We define a func
 
   Definition toProp (b : bool) := if b then True else False.
 
-(** It is worth recalling the difference between the lowercase and uppercase versions of truth and falsehood: [True] and [False] are logical propositions, while [true] and [false] are boolean values that we can case-analyze.  We have defined [toProp] such that our conclusion of [False] is computationally equivalent to [toProp false].  Thus, the %\index{tactics!change}%[change] tactic will let us change the conclusion to [toProp false].  The general form [change e] replaces the conclusion with [e], whenever Coq's built-in computation rules suffice to establish the equivalence of [e] with the original conclusion. *)
+(** It is worth recalling the difference between the lowercase and uppercase versions of truth and falsehood: [True] and [False] are logical propositions, while [true] and [false] are Boolean values that we can case-analyze.  We have defined [toProp] such that our conclusion of [False] is computationally equivalent to [toProp false].  Thus, the %\index{tactics!change}%[change] tactic will let us change the conclusion to [toProp false].  The general form [change e] replaces the conclusion with [e], whenever Coq's built-in computation rules suffice to establish the equivalence of [e] with the original conclusion. *)
 
   change (toProp false).
 (** %\vspace{-.15in}%[[
@@ -1172,7 +1177,7 @@ This is the point in the proof where we apply some creativity.  We define a func
    toProp false
 ]]
 
-Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side the equality with the lefthand side.%\index{tactics!rewrite}% *)
+Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side of the equality with the lefthand side.%\index{tactics!rewrite}% *)
 
   rewrite <- H.
 (** %\vspace{-.15in}%[[

src/MoreDep.v

@@ -199,7 +199,7 @@ Inductive exp : type -> Set :=
 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.
 
-(** We have a standard algebraic datatype [type], defining a type language of naturals, booleans, and product (pair) types.  Then we have the indexed inductive type [exp], where the argument to [exp] tells us the encoded type of an expression.  In effect, we are defining the typing rules for expressions simultaneously with the syntax.
+(** We have a standard algebraic datatype [type], defining a type language of naturals, Booleans, and product (pair) types.  Then we have the indexed inductive type [exp], where the argument to [exp] tells us the encoded type of an expression.  In effect, we are defining the typing rules for expressions simultaneously with the syntax.
 
    We can give types and expressions semantics in a new style, based critically on the chance for _type-level computation_. *)
 
@@ -235,7 +235,7 @@ Definition sumboool := sumbool.
 (* end thide *)
 (* end hide *)
 
-(** Despite the fancy type, the function definition is routine.  In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype.  The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case.  Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type.  Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns.
+(** Despite the fancy type, the function definition is routine.  In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype.  The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case.  Remember that [eq_nat_dec] has a rich dependent type, rather than a simple Boolean type.  Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple Boolean from the [sumbool] that [eq_nat_dec] returns.
 
    We can implement our old favorite, a constant folding function, and prove it correct.  It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so.  Unsurprisingly, a first attempt leads to a type error.
 [[

src/Predicates.v

@@ -849,7 +849,7 @@ Abort.
 (* begin hide *)
 (* In-class exercises *)
 
-(* EX: Define a type [prop] of simple boolean formulas made up only of truth, falsehood, binary conjunction, and binary disjunction.  Define an inductive predicate [holds] that captures when [prop]s are valid, and define a predicate [falseFree] that captures when a [prop] does not contain the "false" formula.  Prove that every false-free [prop] is valid. *)
+(* EX: Define a type [prop] of simple Boolean formulas made up only of truth, falsehood, binary conjunction, and binary disjunction.  Define an inductive predicate [holds] that captures when [prop]s are valid, and define a predicate [falseFree] that captures when a [prop] does not contain the "false" formula.  Prove that every false-free [prop] is valid. *)
 
 (* begin thide *)
 Inductive prop : Set :=

src/StackMachine.v

@@ -550,7 +550,7 @@ Inductive tbinop : type -> type -> type -> Set :=
 
 (** The definition of [tbinop] is different from [binop] in an important way.  Where we declared that [binop] has type [Set], here we declare that [tbinop] has type [type -> type -> type -> Set].  We define [tbinop] as an _indexed type family_.  Indexed inductive types are at the heart of Coq's expressive power; almost everything else of interest is defined in terms of them.
 
-The inuitive explanation of [tbinop] is that a [tbinop t1 t2 t] is a binary operator whose operands should have types [t1] and [t2], and whose result has type [t].  For instance, constructor [TLt] (for less-than comparison of numbers) is assigned type [tbinop Nat Nat Bool], meaning the operator's arguments are naturals and its result is boolean.  The type of [TEq] introduces a small bit of additional complication via polymorphism: we want to allow equality comparison of any two values of any type, as long as they have the _same_ type.
+The inuitive explanation of [tbinop] is that a [tbinop t1 t2 t] is a binary operator whose operands should have types [t1] and [t2], and whose result has type [t].  For instance, constructor [TLt] (for less-than comparison of numbers) is assigned type [tbinop Nat Nat Bool], meaning the operator's arguments are naturals and its result is Boolean.  The type of [TEq] introduces a small bit of additional complication via polymorphism: we want to allow equality comparison of any two values of any type, as long as they have the _same_ type.
 
 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.
 
@@ -574,7 +574,7 @@ Definition typeDenote (t : type) : Set :=
     | Bool => bool
   end.
 
-(** It can take a few moments to come to terms with the fact that [Set], the type of types of programs, is itself a first-class type, and that we can write functions that return [Set]s.  Past that wrinkle, the definition of [typeDenote] is trivial, relying on the [nat] and [bool] types from the Coq standard library.  We can interpret binary operators by relying on standard-library equality test functions [eqb] and [beq_nat] for booleans and naturals, respectively, along with a less-than test [leb]: *)
+(** It can take a few moments to come to terms with the fact that [Set], the type of types of programs, is itself a first-class type, and that we can write functions that return [Set]s.  Past that wrinkle, the definition of [typeDenote] is trivial, relying on the [nat] and [bool] types from the Coq standard library.  We can interpret binary operators by relying on standard-library equality test functions [eqb] and [beq_nat] for Booleans and naturals, respectively, along with a less-than test [leb]: *)
 
 Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
   : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=

src/Subset.v

@@ -459,7 +459,7 @@ Definition eq_nat_dec' (n m : nat) : {n = m} + {n <> m}.
   decide equality.
 Defined.
 
-(** Curious readers can verify that the [decide equality] version extracts to the same OCaml code as our more manual version does.  That OCaml code had one undesirable property, which is that it uses <<Left>> and <<Right>> constructors instead of the boolean values built into OCaml.  We can fix this, by using Coq's facility for mapping Coq inductive types to OCaml variant types.%\index{Vernacular commands!Extract Inductive}% *)
+(** Curious readers can verify that the [decide equality] version extracts to the same OCaml code as our more manual version does.  That OCaml code had one undesirable property, which is that it uses <<Left>> and <<Right>> constructors instead of the Boolean values built into OCaml.  We can fix this, by using Coq's facility for mapping Coq inductive types to OCaml variant types.%\index{Vernacular commands!Extract Inductive}% *)
 
 Extract Inductive sumbool => "bool" ["true" "false"].
 Extraction eq_nat_dec'.
@@ -492,7 +492,7 @@ let rec eq_nat_dec' n m0 =
 
 (** %\smallskip%
 
-We can build "smart" versions of the usual boolean operators and put them to good use in certified programming.  For instance, here is a [sumbool] version of boolean "or." *)
+We can build "smart" versions of the usual Boolean operators and put them to good use in certified programming.  For instance, here is a [sumbool] version of Boolean "or." *)
 
 (* EX: Write a function that decides if an element belongs to a list. *)