Commit 453fc375 authored by Adam Chlipala's avatar Adam Chlipala

Batch of changes based on proofreader feedback

parent 78fc804e
...@@ -334,7 +334,7 @@ Inductive nat_list : Set := ...@@ -334,7 +334,7 @@ Inductive nat_list : Set :=
| NNil : nat_list | NNil : nat_list
| NCons : nat -> nat_list -> 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 := Fixpoint nlength (ls : nat_list) : nat :=
match ls with match ls with
...@@ -625,7 +625,7 @@ Definition prod' := prod. ...@@ -625,7 +625,7 @@ Definition prod' := prod.
(* end thide *) (* end thide *)
(* end hide *) (* 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 := Fixpoint pformulaDenote (f : pformula) : Prop :=
match f with match f with
...@@ -641,7 +641,7 @@ Inductive formula : Set := ...@@ -641,7 +641,7 @@ Inductive formula : Set :=
| And : formula -> formula -> formula | And : formula -> formula -> formula
| Forall : (nat -> 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). Example forall_refl : formula := Forall (fun x => Eq x x).
...@@ -732,85 +732,74 @@ Nonetheless, the basic insight of HOAS is a very useful one, and there are ways ...@@ -732,85 +732,74 @@ Nonetheless, the basic insight of HOAS is a very useful one, and there are ways
(** 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. *) (** 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}%[[ (** %\vspace{-.15in}%[[
unit_ind = nat_ind =
fun P : unit -> Prop => unit_rect P fun P : nat -> Prop => nat_rect P
: forall P : unit -> Prop, P tt -> forall u : unit, P u : 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 <<rec>> stands for "recursion principle," and the <<t>> at the end stands for [Type]. *) We see that this induction principle is defined in terms of a more general principle, [nat_rect]. The <<rec>> stands for "recursion principle," and the <<t>> at the end stands for [Type]. *)
Check unit_rect. Check nat_rect.
(** %\vspace{-.15in}% [[ (** %\vspace{-.15in}% [[
unit_rect nat_rect
: 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 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}%[[ (** %\vspace{-.15in}%[[
unit_rec = nat_rec =
fun P : unit -> Set => unit_rect P fun P : nat -> Set => nat_rect P
: forall P : unit -> Set, P tt -> forall u : unit, P u : 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 := Fixpoint plus_recursive (n : nat) : nat -> nat :=
match u with match n with
| tt => O | O => fun m => m
| S n' => fun m => S (plus_recursive n' m)
end. end.
Definition always_O' (u : unit) : nat := Definition plus_rec : nat -> nat -> nat :=
unit_rec (fun _ : unit => nat) O u. 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}%[[ (** %\vspace{-.15in}%[[
unit_rect = nat_rect =
fun (P : unit -> Type) (f : P tt) (u : unit) => fun (P : nat -> Type) (f : P O) (f0 : forall n : nat, P n -> P (S n)) =>
match u as u0 return (P u0) with fix F (n : nat) : P n :=
| tt => f match n as n0 return (P n0) with
| O => f
| S n0 => f0 n0 (F n0)
end 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) := Fixpoint nat_rect' (P : nat -> Type)
match u return P u with (HO : P O)
| tt => f (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. end.
(* begin hide *) (** We can understand the definition of [nat_rect] better by reimplementing [nat_ind] using sections. *)
(* 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. *)
Section nat_ind'. Section nat_ind'.
(** First, we have the property of natural numbers that we aim to prove. *) (** First, we have the property of natural numbers that we aim to prove. *)
......
...@@ -380,7 +380,7 @@ We will see more about Coq's program extraction facility in a later chapter. Ho ...@@ -380,7 +380,7 @@ We will see more about Coq's program extraction facility in a later chapter. Ho
Theorem exist1 : exists x : nat, x + 1 = 2. Theorem exist1 : exists x : nat, x + 1 = 2.
(* begin thide *) (* begin thide *)
(** remove printing exists *) (** 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. exists 1.
......
...@@ -11,6 +11,14 @@ ...@@ -11,6 +11,14 @@
<webMaster>adam@chlipala.net</webMaster> <webMaster>adam@chlipala.net</webMaster>
<docs>http://blogs.law.harvard.edu/tech/rss</docs> <docs>http://blogs.law.harvard.edu/tech/rss</docs>
<item>
<title>Batch of changes based on proofreader feedback</title>
<pubDate>Tue, 2 Oct 2012 11:34:17 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> <item>
<title>Batch of changes based on proofreader feedback</title> <title>Batch of changes based on proofreader feedback</title>
<pubDate>Wed, 26 Sep 2012 16:31:01 EDT</pubDate> <pubDate>Wed, 26 Sep 2012 16:31:01 EDT</pubDate>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment