# HG changeset patch # User Adam Chlipala # Date 1349192080 14400 # Node ID 0df6dde807abc93f70cea02464698ffa9a1eb8f1 # Parent b36876d4611e73d082da3b2ecdcf3a010b5b099e Batch of changes based on proofreader feedback diff -r b36876d4611e -r 0df6dde807ab src/InductiveTypes.v --- a/src/InductiveTypes.v Wed Sep 26 16:35:35 2012 -0400 +++ b/src/InductiveTypes.v Tue Oct 02 11:34:40 2012 -0400 @@ -334,7 +334,7 @@ | NNil : nat_list | NCons : nat -> nat_list -> nat_list. -(** Recursive definitions are straightforward extensions of what we have seen before. *) +(** Recursive definitions over [nat_list] are straightforward extensions of what we have seen before. *) Fixpoint nlength (ls : nat_list) : nat := match ls with @@ -625,7 +625,7 @@ (* 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). *) +(** 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). *) Fixpoint pformulaDenote (f : pformula) : Prop := match f with @@ -641,7 +641,7 @@ | And : formula -> formula -> formula | Forall : (nat -> formula) -> formula. -(** Our kinds of formulas are equalities between naturals, conjunction, and universal quantification over natural numbers. We avoid needing to include a notion of "variables" in our type, by using Coq functions to encode quantification. For instance, here is the encoding of [forall x : nat, x = x]:%\index{Vernacular commands!Example}% *) +(** Our kinds of formulas are equalities between naturals, conjunction, and universal quantification over natural numbers. We avoid needing to include a notion of "variables" in our type, by using Coq functions to encode the syntax of quantification. For instance, here is the encoding of [forall x : nat, x = x]:%\index{Vernacular commands!Example}% *) Example forall_refl : formula := Forall (fun x => Eq x x). @@ -732,85 +732,74 @@ (** As we have emphasized a few times already, Coq proofs are actually programs, written in the same language we have been using in our examples all along. We can get a first sense of what this means by taking a look at the definitions of some of the %\index{induction principles}%induction principles we have used. A close look at the details here will help us construct induction principles manually, which we will see is necessary for some more advanced inductive definitions. *) -Print unit_ind. +Print nat_ind. (** %\vspace{-.15in}%[[ - unit_ind = - fun P : unit -> Prop => unit_rect P - : forall P : unit -> Prop, P tt -> forall u : unit, P u +nat_ind = +fun P : nat -> Prop => nat_rect P + : forall P : nat -> Prop, + P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n ]] -We see that this induction principle is defined in terms of a more general principle, [unit_rect]. The <> stands for "recursion principle," and the <> at the end stands for [Type]. *) +We see that this induction principle is defined in terms of a more general principle, [nat_rect]. The <> stands for "recursion principle," and the <> at the end stands for [Type]. *) -Check unit_rect. +Check nat_rect. (** %\vspace{-.15in}% [[ - unit_rect - : forall P : unit -> Type, P tt -> forall u : unit, P u +nat_rect + : forall P : nat -> Type, + P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n ]] -The principle [unit_rect] gives [P] type [unit -> Type] instead of [unit -> Prop]. [Type] is another universe, like [Set] and [Prop]. In fact, it is a common supertype of both. Later on, we will discuss exactly what the significances of the different universes are. For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop]. We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [unit] automatically: *) +The principle [nat_rect] gives [P] type [nat -> Type] instead of [nat -> Prop]. This [Type] is another universe, like [Set] and [Prop]. In fact, it is a common supertype of both. Later on, we will discuss exactly what the significances of the different universes are. For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop]. We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [nat] automatically: *) -Print unit_rec. +Print nat_rec. (** %\vspace{-.15in}%[[ - unit_rec = - fun P : unit -> Set => unit_rect P - : forall P : unit -> Set, P tt -> forall u : unit, P u +nat_rec = +fun P : nat -> Set => nat_rect P + : forall P : nat -> Set, + P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n ]] -This is identical to the definition for [unit_ind], except that we have substituted [Set] for [Prop]. For most inductive types [T], then, we get not just induction principles [T_ind], but also %\index{recursion principles}%recursion principles [T_rec]. We can use [T_rec] to write recursive definitions without explicit [Fixpoint] recursion. For instance, the following two definitions are equivalent: *) +This is identical to the definition for [nat_ind], except that we have substituted [Set] for [Prop]. For most inductive types [T], then, we get not just induction principles [T_ind], but also %\index{recursion principles}%recursion principles [T_rec]. We can use [T_rec] to write recursive definitions without explicit [Fixpoint] recursion. For instance, the following two definitions are equivalent: *) -Definition always_O (u : unit) : nat := - match u with - | tt => O +Fixpoint plus_recursive (n : nat) : nat -> nat := + match n with + | O => fun m => m + | S n' => fun m => S (plus_recursive n' m) end. -Definition always_O' (u : unit) : nat := - unit_rec (fun _ : unit => nat) O u. +Definition plus_rec : nat -> nat -> nat := + nat_rec (fun _ : nat => nat -> nat) (fun _ => O) (fun _ r m => S (r m)). -(** Going even further down the rabbit hole, [unit_rect] itself is not even a primitive. It is a functional program that we can write manually. *) +(** Going even further down the rabbit hole, [nat_rect] itself is not even a primitive. It is a functional program that we can write manually. *) -Print unit_rect. +Print nat_rect. (** %\vspace{-.15in}%[[ - unit_rect = - fun (P : unit -> Type) (f : P tt) (u : unit) => - match u as u0 return (P u0) with - | tt => f +nat_rect = +fun (P : nat -> Type) (f : P O) (f0 : forall n : nat, P n -> P (S n)) => +fix F (n : nat) : P n := + match n as n0 return (P n0) with + | O => f + | S n0 => f0 n0 (F n0) end - : forall P : unit -> Type, P tt -> forall u : unit, P u + : forall P : nat -> Type, + P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n ]] -The only new wrinkle here is the annotations on the [match] expression. This is a%\index{dependent pattern matching}% _dependently typed_ pattern match, because the _type_ of the expression depends on the _value_ being matched on. Of course, for this example, the dependency is degenerate; the value being matched on has type [unit], so it may only take on a single known value, [tt]. We will meet more involved examples later, especially in Part II of the book. +The only new wrinkle heres are, first, an anonymous recursive function definition, using the %\index{Gallina terms!fix}%[fix] keyword of Gallina (which is like [fun] with recursion supported); and, second, the annotations on the [match] expression. This is a%\index{dependent pattern matching}% _dependently typed_ pattern match, because the _type_ of the expression depends on the _value_ being matched on. We will meet more involved examples later, especially in Part II of the book. -%\index{type inference}%Type inference for dependent pattern matching is undecidable, which can be proved by reduction from %\index{higher-order unification}%higher-order unification%~\cite{HOU}%. Thus, we often find ourselves needing to annotate our programs in a way that explains dependencies to the type checker. In the example of [unit_rect], we have an %\index{Gallina terms!as}%[as] clause, which binds a name for the discriminee; and a %\index{Gallina terms!return}%[return] clause, which gives a way to compute the [match] result type as a function of the discriminee. +%\index{type inference}%Type inference for dependent pattern matching is undecidable, which can be proved by reduction from %\index{higher-order unification}%higher-order unification%~\cite{HOU}%. Thus, we often find ourselves needing to annotate our programs in a way that explains dependencies to the type checker. In the example of [nat_rect], we have an %\index{Gallina terms!as}%[as] clause, which binds a name for the discriminee; and a %\index{Gallina terms!return}%[return] clause, which gives a way to compute the [match] result type as a function of the discriminee. -To prove that [unit_rect] is nothing special, we can reimplement it manually. *) +To prove that [nat_rect] is nothing special, we can reimplement it manually. *) -Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) := - match u return P u with - | tt => f +Fixpoint nat_rect' (P : nat -> Type) + (HO : P O) + (HS : forall n, P n -> P (S n)) (n : nat) := + match n return P n with + | O => HO + | S n' => HS n' (nat_rect' P HO HS n') end. -(* begin hide *) -(* begin thide *) -Definition foo := nat_rect. -(* end thide *) -(* end hide *) - -(** We can check the implementation [nat_rect] as well: *) - -Print nat_rect. -(** %\vspace{-.15in}% [[ - nat_rect = - fun (P : nat -> Type) (f : P O) (f0 : forall n : nat, P n -> P (S n)) => - fix F (n : nat) : P n := - match n as n0 return (P n0) with - | O => f - | S n0 => f0 n0 (F n0) - end - : forall P : nat -> Type, - P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n - ]] - -Now we have an actual recursive definition. Expressions starting with %\index{Gallina terms!fix}%[fix] are anonymous forms of [Fixpoint], just as [fun] expressions stand for anonymous non-recursive functions. Beyond that, the syntax of [fix] mirrors that of [Fixpoint]. We can understand the definition of [nat_rect] better by reimplementing [nat_ind] using sections. *) +(** We can understand the definition of [nat_rect] better by reimplementing [nat_ind] using sections. *) Section nat_ind'. (** First, we have the property of natural numbers that we aim to prove. *) diff -r b36876d4611e -r 0df6dde807ab src/Predicates.v --- a/src/Predicates.v Wed Sep 26 16:35:35 2012 -0400 +++ b/src/Predicates.v Tue Oct 02 11:34:40 2012 -0400 @@ -380,7 +380,7 @@ Theorem exist1 : exists x : nat, x + 1 = 2. (* begin thide *) (** remove printing exists *) - (** We can start this proof with a tactic %\index{tactics!exists}%[exists], which should not be confused with the formula constructor shorthand of the same name. (In the PDF version of this document, the reverse %`%#'#E#'#%'% appears instead of the text "exists" in formulas.) *) + (** We can start this proof with a tactic %\index{tactics!exists}%[exists], which should not be confused with the formula constructor shorthand of the same name. %In the version of this document that you are reading, the reverse ``E'' appears instead of the text ``exists'' in formulas.% *) exists 1. diff -r b36876d4611e -r 0df6dde807ab staging/updates.rss --- a/staging/updates.rss Wed Sep 26 16:35:35 2012 -0400 +++ b/staging/updates.rss Tue Oct 02 11:34:40 2012 -0400 @@ -13,6 +13,14 @@ Batch of changes based on proofreader feedback + Tue, 2 Oct 2012 11:34:17 EDT + http://adam.chlipala.net/cpdt/ + adamc@csail.mit.edu + Thanks to everyone who is helping with the final proofreading! + + + + Batch of changes based on proofreader feedback Wed, 26 Sep 2012 16:31:01 EDT http://adam.chlipala.net/cpdt/ adamc@csail.mit.edu