Stub out new chapter

Makefile

 MODULES_NODOC := CpdtTactics MoreSpecif DepList
 MODULES_PROSE := Intro
-MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
+MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive GeneralRec Subset \
 	MoreDep DataStruct Equality Generic Universes LogicProg Match Reflection \
 	Large
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)

latex/cpdt.tex

@@ -40,6 +40,7 @@ The license text is available at:
 \include{InductiveTypes.v}
 \include{Predicates.v}
 \include{Coinductive.v}
+\include{GeneralRec.v}
 \include{Subset.v}
 \include{MoreDep.v}
 \include{DataStruct.v}

src/DepList.v

@@ -7,7 +7,7 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-(* Dependent list types presented in Chapter 8 *)
+(* Dependent list types presented in Chapter 9 *)
 
 Require Import Arith List CpdtTactics.
 

src/GeneralRec.v

+(* Copyright (c) 2006, 2011, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import List.
+
+Require Import CpdtTactics.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\chapter{General Recursion}% *)
+

src/Generic.v

@@ -77,7 +77,7 @@ Section denote.
 
   Definition constructorDenote (c : constructor) :=
     nonrecursive c -> ilist T (recursive c) -> T.
-  (** We write that a constructor is represented as a function returning a [T].  Such a function takes two arguments, which pack together the non-recursive and recursive arguments of the constructor.  We represent a tuple of all recursive arguments using the length-indexed list type [ilist] that we met in Chapter 7. *)
+  (** We write that a constructor is represented as a function returning a [T].  Such a function takes two arguments, which pack together the non-recursive and recursive arguments of the constructor.  We represent a tuple of all recursive arguments using the length-indexed list type [ilist] that we met in Chapter 8. *)
 
   Definition datatypeDenote := hlist constructorDenote.
   (** Finally, the evidence for type [T] is a heterogeneous list, including a constructor denotation for every constructor encoding in a datatype encoding.  Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *)

src/Intro.v

@@ -75,7 +75,7 @@ A language with %\textit{%#<i>#dependent types#</i>#%}% may include references t
 
 %\index{ACL2}%ACL2 and %\index{HOL}%HOL lack dependent types outright.  %\index{PVS}%PVS and %\index{Twelf}%Twelf each supports a different strict subset of Coq's dependent type language.  Twelf's type language is restricted to a bare-bones, monomorphic lambda calculus, which places serious restrictions on how complicated %\textit{%#<i>#computations inside types#</i>#%}% can be.  This restriction is important for the soundness argument behind Twelf's approach to representing and checking proofs.
 
-In contrast, %\index{PVS}%PVS's dependent types are much more general, but they are squeezed inside the single mechanism of %\textit{%#<i>#subset types#</i>#%}%, where a normal type is refined by attaching a predicate over its elements.  Each member of the subset type is an element of the base type that satisfies the predicate.  Chapter 6 of this book introduces that style of programming in Coq, while the remaining chapters of Part II deal with features of dependent typing in Coq that go beyond what PVS supports.
+In contrast, %\index{PVS}%PVS's dependent types are much more general, but they are squeezed inside the single mechanism of %\textit{%#<i>#subset types#</i>#%}%, where a normal type is refined by attaching a predicate over its elements.  Each member of the subset type is an element of the base type that satisfies the predicate.  Chapter 7 of this book introduces that style of programming in Coq, while the remaining chapters of Part II deal with features of dependent typing in Coq that go beyond what PVS supports.
 
 Dependent types are not just useful because they help you express correctness properties in types.  Dependent types also often let you write certified programs %\textit{%#<i>#without writing anything that looks like a proof#</i>#%}%.  Even with subset types, which for many contexts can be used to express any relevant property with enough acrobatics, the human driving the proof assistant usually has to build some proofs explicitly.  Writing formal proofs is hard, so we want to avoid it as far as possible, so dependent types are invaluable.
 
@@ -225,6 +225,8 @@ Inductive Predicates & \texttt{Predicates.v} \\
 \hline
 Infinite Data and Proofs & \texttt{Coinductive.v} \\
 \hline
+General Recursion & \texttt{GeneralRec.v} \\
+\hline
 Subset Types and Variations & \texttt{Subset.v} \\
 \hline
 More Dependent Types & \texttt{MoreDep.v} \\

src/Large.v

@@ -284,7 +284,7 @@ Qed.
 
    Before we are ready to update our proofs, we need to write them in the first place.  While fully-automated scripts are most robust to changes of specification, it is hard to write every new proof directly in that form.  Instead, it is useful to begin a theorem with exploratory proving and then gradually refine it into a suitable automated form.
 
-   Consider this theorem from Chapter 7, which we begin by proving in a mostly manual way, invoking [crush] after each steop to discharge any low-hanging fruit.  Our manual effort involves choosing which expressions to case-analyze on. *)
+   Consider this theorem from Chapter 8, which we begin by proving in a mostly manual way, invoking [crush] after each steop to discharge any low-hanging fruit.  Our manual effort involves choosing which expressions to case-analyze on. *)
 
 (* begin hide *)
 Require Import MoreDep.

src/MoreDep.v

@@ -350,7 +350,7 @@ User error: e1 is used in hypothesis e
 
     Coq gives us another cryptic error message.  Like so many others, this one basically means that Coq is not able to build some proof about dependent types.  It is hard to generate helpful and specific error messages for problems like this, since that would require some kind of understanding of the dependency structure of a piece of code.  We will encounter many examples of case-specific tricks for recovering from errors like this one.
 
-    For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book [CpdtTactics] module.  General elimination/inversion of dependently typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed.  The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq.  In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dep_destruct]'s implementation in Ltac, but for now, we treat it as a useful black box.  (In Chapter 11, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *)
+    For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book [CpdtTactics] module.  General elimination/inversion of dependently typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed.  The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq.  In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dep_destruct]'s implementation in Ltac, but for now, we treat it as a useful black box.  (In Chapter 12, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *)
   
   dep_destruct (cfold e1).
 

src/MoreSpecif.v

@@ -7,7 +7,7 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-(* Types and notations presented in Chapter 6 *)
+(* Types and notations presented in Chapter 7 *)
 
 Set Implicit Arguments.
 

src/Predicates.v

@@ -52,7 +52,7 @@ Print True.
   ]]
 *)
 
-(** Recall that [unit] is the type with only one value, and [True] is the proposition that always holds.  Despite this superficial difference between the two concepts, in both cases we can use the same inductive definition mechanism.  The connection goes further than this.  We see that we arrive at the definition of [True] by replacing [unit] by [True], [tt] by [I], and [Set] by [Prop].  The first two of these differences are superficial changes of names, while the third difference is the crucial one for separating programs from proofs.  A term [T] of type [Set] is a type of programs, and a term of type [T] is a program.  A term [T] of type [Prop] is a logical proposition, and its proofs are of type [T].  Chapter 11 goes into more detail about the theoretical differences between [Prop] and [Set].  For now, we will simply follow common intuitions about what a proof is.
+(** Recall that [unit] is the type with only one value, and [True] is the proposition that always holds.  Despite this superficial difference between the two concepts, in both cases we can use the same inductive definition mechanism.  The connection goes further than this.  We see that we arrive at the definition of [True] by replacing [unit] by [True], [tt] by [I], and [Set] by [Prop].  The first two of these differences are superficial changes of names, while the third difference is the crucial one for separating programs from proofs.  A term [T] of type [Set] is a type of programs, and a term of type [T] is a program.  A term [T] of type [Prop] is a logical proposition, and its proofs are of type [T].  Chapter 12 goes into more detail about the theoretical differences between [Prop] and [Set].  For now, we will simply follow common intuitions about what a proof is.
 
 The type [unit] has one value, [tt].  The type [True] has one proof, [I].  Why distinguish between these two types?  Many people who have read about Curry-Howard in an abstract context and not put it to use in proof engineering answer that the two types in fact %\textit{%#<i>#should not#</i>#%}% be distinguished.  There is a certain aesthetic appeal to this point of view, but I want to argue that it is best to treat Curry-Howard very loosely in practical proving.  There are Coq-specific reasons for preferring the distinction, involving efficient compilation and avoidance of paradoxes in the presence of classical math, but I will argue that there is a more general principle that should lead us to avoid conflating programming and proving.
 

src/Reflection.v

@@ -460,7 +460,7 @@ Section my_tauto.
 
   Local Open Scope partial_scope.
 
-  (** Now we can write a function [forward] which implements deconstruction of hypotheses.  It has a dependent type, in the style of Chapter 6, guaranteeing correctness.  The arguments to [forward] are a goal formula [f], a set [known] of atomic formulas that we may assume are true, a hypothesis formula [hyp], and a success continuation [cont] that we call when we have extended [known] to hold new truths implied by [hyp]. *)
+  (** Now we can write a function [forward] which implements deconstruction of hypotheses.  It has a dependent type, in the style of Chapter 7, guaranteeing correctness.  The arguments to [forward] are a goal formula [f], a set [known] of atomic formulas that we may assume are true, a hypothesis formula [hyp], and a success continuation [cont] that we call when we have extended [known] to hold new truths implied by [hyp]. *)
 
   Definition forward : forall (f : formula) (known : set index) (hyp : formula)
     (cont : forall known', [allTrue known' -> formulaDenote atomics f]),

src/Universes.v

@@ -612,7 +612,7 @@ Print proof_irrelevance.
   *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
   ]]
 
-  This axiom asserts that any two proofs of the same proposition are equal.  If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable.  However, equality is a stronger notion than logical equivalence.  Recall this example function from Chapter 6. *)
+  This axiom asserts that any two proofs of the same proposition are equal.  If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable.  However, equality is a stronger notion than logical equivalence.  Recall this example function from Chapter 7. *)
 
 (* begin hide *)
 Lemma zgtz : 0 > 0 -> False.

src/toc.html

@@ -9,6 +9,7 @@
 <li><a href="InductiveTypes.html">Introducing Inductive Types</a>
 <li><a href="Predicates.html">Inductive Predicates</a>
 <li><a href="Coinductive.html">Infinite Data and Proofs</a>
+<li><a href="GeneralRec.html">General Recursion</a>
 <li><a href="Subset.html">Subset Types and Variations</a>
 <li><a href="MoreDep.html">More Dependent Types</a>
 <li><a href="DataStruct.html">Dependent Data Structures</a>