'make doc' works with 8.2

Makefile

@@ -43,6 +43,7 @@ latex/cpdt.pdf: latex/cpdt.dvi
 	cd latex ; pdflatex cpdt
 
 html: Makefile $(VS) src/toc.html
+	mkdir -p html
 	cd src ; coqdoc $(VS_DOC) \
 		--glob-from ../$(GLOBALS) \
 		-d ../html

src/Coinductive.v

@@ -28,6 +28,8 @@ We spent some time in the last chapter discussing the Curry-Howard isomorphism,
 
 Fixpoint bad (u : unit) : P := bad u.
 
+]]
+
 This would leave us with [bad tt] as a proof of [P].
 
 There are also algorithmic considerations that make universal termination very desirable.  We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules.  Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps.  It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem.
@@ -95,6 +97,9 @@ The restriction for co-inductive types shows up as the %\textit{%#<i>#guardednes
 
 [[
 CoFixpoint looper : stream nat := looper.
+
+]]
+
 [[
 Error:
 Recursive definition of looper is ill-formed.
@@ -102,6 +107,8 @@ In environment
 looper : stream nat
 
 unguarded recursive call in "looper"
+]]
+
 *)
 
 
@@ -145,6 +152,8 @@ Section map'.
     match s with
       | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s))
     end.
+
+    ]]
    *)
 
   (** We get another error message about an unguarded recursive call.  This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls.  The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion.
@@ -201,7 +210,9 @@ Theorem ones_eq : stream_eq ones ones'.
   assumption.
   (** [[
 
-Proof completed. *)
+Proof completed.
+
+]] *)
 
   (** Unfortunately, we are due for some disappointment in our victory lap. *)
 
@@ -214,7 +225,9 @@ Recursive definition of ones_eq is ill-formed.
 In environment
 ones_eq : stream_eq ones ones'
 
-unguarded recursive call in "ones_eq" *)
+unguarded recursive call in "ones_eq"
+
+]] *)
 
   (** Via the Curry-Howard correspondence, the same guardedness condition applies to our co-inductive proofs as to our co-inductive data structures.  We should be grateful that this proof is rejected, because, if it were not, the same proof structure could be used to prove any co-inductive theorem vacuously, by direct appeal to itself!
 
@@ -223,6 +236,8 @@ unguarded recursive call in "ones_eq" *)
      [[
 Guarded.
 
+]]
+
      Running [Guarded] here gives us the same error message that we got when we tried to run [Qed].  In larger proofs, [Guarded] can be helpful in detecting problems %\textit{%#<i>#before#</i>#%}% we think we are ready to run [Qed].
      
      We need to start the co-induction by applying one of [stream_eq]'s constructors.  To do that, we need to know that both arguments to the predicate are [Cons]es.  Informally, this is trivial, but [simpl] is not able to help us. *)
@@ -312,7 +327,9 @@ Theorem ones_eq' : stream_eq ones ones'.
   cofix; crush.
   (** [[
 
-  Guarded. *)
+  Guarded.
+
+  ]] *)
 Abort.
 (* end thide *)
 

src/DataStruct.v

@@ -56,6 +56,8 @@ Section ilist.
         end
     end.
 
+    ]]
+
     We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [index] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return].
 
     [[
@@ -76,6 +78,8 @@ Section ilist.
         end
     end.
 
+    ]]
+
     Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls'].  We need to use [match] annotations to make the relationship explicit.  Unfortunately, the usual trick of postponing argument binding will not help us here.  We need to match on both [ls] and [idx]; one or the other must be matched first.  To get around this, we apply a trick that we will call "the convoy pattern," introducing a new function and applying it immediately, to satisfy the type checker.
 
     [[
@@ -96,6 +100,8 @@ Section ilist.
         end ls'
     end.
 
+    ]]
+
     There is just one problem left with this implementation.  Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination.  We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
 
   Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
@@ -433,6 +439,8 @@ Section fhlist.
         end
     end.
 
+    ]]
+
     Only one problem remains.  The expression [fst mls] is not known to have the proper type.  To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
 
   Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
@@ -542,6 +550,8 @@ Section tree.
   | Leaf : A -> tree
   | Node : forall n, filist tree n -> tree.
 
+  ]]
+
 [[
 
 Error: Non strictly positive occurrence of "tree" in

src/Equality.v

@@ -177,6 +177,8 @@ Section fhlist_map.
 
     destruct a0.
 
+    ]]
+
     [[
 User error: Cannot solve a second-order unification problem
 ]]
@@ -187,6 +189,8 @@ User error: Cannot solve a second-order unification problem
 
     assert (a0 = refl_equal _).
 
+    ]]
+
     [[
 The term "refl_equal ?98" has type "?98 = ?98"
  while it is expected to have type "a = elm"
@@ -256,6 +260,8 @@ end
     (** [[
 
     simple destruct pf.
+
+    ]]
     
       [[
 
@@ -282,6 +288,8 @@ User error: Cannot solve a second-order unification problem
     (** [[
 
     simple destruct pf.
+
+    ]]
     
       [[
 
@@ -299,6 +307,8 @@ User error: Cannot solve a second-order unification problem
         | refl_equal => refl_equal _
       end.
 
+      ]]
+
      [[
 
 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
@@ -380,6 +390,8 @@ Section fhapp.
     (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
     fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
 
+    ]]
+
      [[
 
 The term
@@ -415,6 +427,8 @@ The term
        [[
     case pf.
 
+    ]]
+
        [[
 
 User error: Cannot solve a second-order unification problem
@@ -454,6 +468,8 @@ User error: Cannot solve a second-order unification problem
 
     rewrite (UIP_refl _ _ pf).
 
+    ]]
+
        [[
 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
  while it is expected to have type "?556 = ?556"
@@ -645,6 +661,8 @@ Section fhapp'.
 
     rewrite IHls1.
 
+    ]]
+
        [[
 
 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
@@ -764,6 +782,8 @@ Qed.
 
    Theorem S_eta : S = (fun n => S n).
 
+   ]]
+
    Unfortunately, this theorem is not provable in CIC without additional axioms.  None of the definitional equality rules force function equality to be %\textit{%#<i>#extensional#</i>#%}%.  That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal.  We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *)
 
 (* begin thide *)

src/InductiveTypes.v

@@ -63,6 +63,9 @@ Qed.
 (** It seems kind of odd to write a proof by induction with no inductive hypotheses.  We could have arrived at the same result by beginning the proof with: [[
 
   destruct x.
+
+]]
+
 ...which corresponds to "proof by case analysis" in classical math.  For non-recursive inductive types, the two tactics will always have identical behavior.  Often case analysis is sufficient, even in proofs about recursive types, and it is nice to avoid introducing unneeded induction hypotheses.
 
 What exactly %\textit{%#<i>#is#</i>#%}% the induction principle for [unit]?  We can ask Coq: *)
@@ -666,6 +669,8 @@ Definition uhoh (t : term) : term :=
     | _ => t
   end.
 
+]]
+
 Using an informal idea of Coq's semantics, it is easy to verify that the application [uhoh (Abs uhoh)] will run forever.  This would be a mere curiosity in OCaml and Haskell, where non-termination is commonplace, though the fact that we have a non-terminating program without explicit recursive function definitions is unusual.
 
 For Coq, however, this would be a disaster.  The possibility of writing such a function would destroy all our confidence that proving a theorem means anything.  Since Coq combines programs and proofs in one language, we would be able to prove every theorem with an infinite loop.
@@ -943,6 +948,8 @@ Section nat_tree_ind'.
       | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest)
     end.
 
+  ]]
+
   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. *)
 
   Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=

src/Match.v

@@ -89,6 +89,8 @@ End forall_and.
       | [ H : forall x, ?P x /\ _ |- _ ] => apply (proj1 (H X))
     end.
 
+    ]]
+
    [[
 User error: Bound head variable
    ]]
@@ -450,6 +452,8 @@ Section firstorder'.
 
     completer'.
 
+    ]]
+
     Coq loops forever at this point.  What went wrong? *)
   Abort.
 (* end thide *)
@@ -475,6 +479,8 @@ Theorem t1' : forall x : nat, x = x.
     | [ |- forall x, ?P ] => trivial
   end.
 
+  ]]
+
     [[
 User error: No matching clauses for match goal
     ]] *)
@@ -503,6 +509,8 @@ Ltac length ls :=
     | _ :: ls' => S (length ls')
   end.
 
+  ]]
+
    [[
 Error: The reference ls' was not found in the current environment
    ]]
@@ -516,6 +524,8 @@ Ltac length ls :=
     | _ :: ?ls' => S (length ls')
   end.
 
+  ]]
+
 [[
 Error: The reference S was not found in the current environment
 ]]

src/Predicates.v

@@ -73,6 +73,7 @@ We have also already seen the definition of [True].  For a demonstration of a lo
   (** [[
 
 Inductive False : Prop :=
+
 ]] *)
 
   (** We can conclude anything from [False], doing case analysis on a proof of [False] in the same way we might do case analysis on, say, a natural number.  Since there are no cases to consider, any such case analysis succeeds immediately in proving the goal. *)

src/Reflection.v

@@ -118,6 +118,8 @@ Theorem even_255 : isEven 255.
 
   prove_even_reflective.
 
+  ]]
+
   [[
 
 User error: No matching clauses for match goal
@@ -129,6 +131,8 @@ User error: No matching clauses for match goal
 
   exact (partialOut (check_even 255)).
 
+  ]]
+
   [[
 
   Error: The term "partialOut (check_even 255)" has type
@@ -633,12 +637,19 @@ To work with rational numbers, import module [QArith] and use [Open Local Scope
   Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1
     -> z + (8 # 1) * x == 20 # 1
     -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1.
+
+    ]]
+
 [[
 
     intros; reflectContext; assumption.
+
+    ]]
 [[
   Qed.
 
+]]
+
   Your solution can work in any way that involves reflecting syntax and doing most calculation with a Gallina function.  These hints outline a particular possible solution.  Throughout, the [ring] tactic will be helpful for proving many simple facts about rationals, and tactics like [rewrite] are correctly overloaded to work with rational equality [==].
 
 %\begin{enumerate}%#<ol>#
@@ -680,6 +691,8 @@ To work with rational numbers, import module [QArith] and use [Open Local Scope
                   end ]
       end.
 
+]]
+
 #</ol>#%\end{enumerate}%
 #</li>#
    

src/StackMachine.v

@@ -73,6 +73,8 @@ Definition binopDenote : binop -> nat -> nat -> nat := fun (b : binop) =>
     | Times => mult
   end.
 
+]]
+
 In this example, we could also omit all of the type annotations, arriving at:
 
 [[
@@ -82,6 +84,8 @@ Definition binopDenote := fun b =>
     | Times => mult
   end.
 
+]]
+
 Languages like Haskell and ML have a convenient %\textit{%#<i>#principal typing#</i>#%}% property, which gives us strong guarantees about how effective type inference will be.  Unfortunately, Coq's type system is so expressive that any kind of "complete" type inference is impossible, and the task even seems to be hard heuristically in practice.  Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language.
 
 This is as good a time as any to mention the preponderance of different languages associated with Coq.  The theoretical foundation of Coq is a formal system called the %\textit{%#<i>#Calculus of Inductive Constructions (CIC)#</i>#%}%, which is an extension of the older %\textit{%#<i>#Calculus of Constructions (CoC)#</i>#%}%.  CIC is quite a spartan foundation, which is helpful for proving metatheory but not so helpful for real development.  Still, it is nice to know that it has been proved that CIC enjoys properties like %\textit{%#<i>#strong normalization#</i>#%}%, meaning that every program (and, more importantly, every proof term) terminates; and %\textit{%#<i>#relative consistency#</i>#%}% with systems like versions of Zermelo Fraenkel set theory, which roughly means that you can believe that Coq proofs mean that the corresponding propositions are "really true," if you believe in set theory.
@@ -107,17 +111,13 @@ Fixpoint expDenote (e : exp) : nat :=
 (** It is convenient to be able to test definitions before starting to prove things about them.  We can verify that our semantics is sensible by evaluating some sample uses. *)
 
 Eval simpl in expDenote (Const 42).
-(** [[
-= 42 : nat
-]] *)
+(** [= 42 : nat] *)
+
 Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)).
-(** [[
-= 4 : nat
-]] *)
+(** [= 4 : nat] *)
+
 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
-(** [[
-= 28 : nat
-]] *)
+(** [= 28 : nat] *)
 
 (** ** Target Language *)
 
@@ -277,9 +277,7 @@ To progress further, we need to use the definitions of some of the functions app
 *)
 
   unfold compile.
-
 (** [[
-
  n : nat
  s : stack
  p : list instr
@@ -289,9 +287,7 @@ To progress further, we need to use the definitions of some of the functions app
 ]] *)
 
   unfold expDenote.
-
 (** [[
-
  n : nat
  s : stack
  p : list instr
@@ -463,6 +459,8 @@ Now we can apply a similar sequence of tactics to that that ended the proof of t
 [[
 Proof completed.
 
+]]
+
 And there lies our first proof.  Already, even for simple theorems like this, the final proof script is unstructured and not very enlightening to readers.  If we extend this approach to more serious theorems, we arrive at the unreadable proof scripts that are the favorite complaints of opponents of tactic-based proving.  Fortunately, Coq has rich support for scripted automation, and we can take advantage of such a scripted tactic (defined elsewhere) to make short work of this lemma.  We abort the old proof attempt and start again.
 *)
 
@@ -709,6 +707,8 @@ Definition tinstrDenote ts ts' (i : tinstr ts ts') (s : vstack ts) : vstack ts'
       end
   end.
 
+]]
+
 The Coq type-checker complains that:
 
 [[