Mercurial > cpdt > repo

changeset 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents cbf2f74a5130
children 3f4576f15130
files Makefile src/Coinductive.v src/DataStruct.v src/Equality.v src/InductiveTypes.v src/Match.v src/Predicates.v src/Reflection.v src/StackMachine.v
diffstat 9 files changed, 95 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/Makefile	Fri Nov 06 10:52:43 2009 -0500
+++ b/Makefile	Fri Nov 06 12:15:05 2009 -0500
@@ -43,6 +43,7 @@
 	cd latex ; pdflatex cpdt
 
 html: Makefile $(VS) src/toc.html
+	mkdir -p html
 	cd src ; coqdoc $(VS_DOC) \
 		--glob-from ../$(GLOBALS) \
 		-d ../html
--- a/src/Coinductive.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Coinductive.v	Fri Nov 06 12:15:05 2009 -0500
@@ -28,6 +28,8 @@
 
 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 @@
 
 [[
 CoFixpoint looper : stream nat := looper.
+
+]]
+
 [[
 Error:
 Recursive definition of looper is ill-formed.
@@ -102,6 +107,8 @@
 looper : stream nat
 
 unguarded recursive call in "looper"
+]]
+
 *)
 
 
@@ -145,6 +152,8 @@
     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 @@
   assumption.
   (** [[
 
-Proof completed. *)
+Proof completed.
+
+]] *)
 
   (** Unfortunately, we are due for some disappointment in our victory lap. *)
 
@@ -214,7 +225,9 @@
 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 @@
      [[
 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 @@
   cofix; crush.
   (** [[
 
-  Guarded. *)
+  Guarded.
+
+  ]] *)
 Abort.
 (* end thide *)
 
--- a/src/DataStruct.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/DataStruct.v	Fri Nov 06 12:15:05 2009 -0500
@@ -56,6 +56,8 @@
         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 @@
         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 @@
         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 @@
         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 @@
   | Leaf : A -> tree
   | Node : forall n, filist tree n -> tree.
 
+  ]]
+
 [[
 
 Error: Non strictly positive occurrence of "tree" in
--- a/src/Equality.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Equality.v	Fri Nov 06 12:15:05 2009 -0500
@@ -177,6 +177,8 @@
 
     destruct a0.
 
+    ]]
+
     [[
 User error: Cannot solve a second-order unification problem
 ]]
@@ -187,6 +189,8 @@
 
     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 @@
     (** [[
 
     simple destruct pf.
+
+    ]]
     
       [[
 
@@ -282,6 +288,8 @@
     (** [[
 
     simple destruct pf.
+
+    ]]
     
       [[
 
@@ -299,6 +307,8 @@
         | 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 @@
     (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 @@
        [[
     case pf.
 
+    ]]
+
        [[
 
 User error: Cannot solve a second-order unification problem
@@ -454,6 +468,8 @@
 
     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 @@
 
     rewrite IHls1.
 
+    ]]
+
        [[
 
 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
@@ -764,6 +782,8 @@
 
    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 *)
--- a/src/InductiveTypes.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/InductiveTypes.v	Fri Nov 06 12:15:05 2009 -0500
@@ -63,6 +63,9 @@
 (** 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 @@
     | _ => 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 @@
       | 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 :=
--- a/src/Match.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Match.v	Fri Nov 06 12:15:05 2009 -0500
@@ -89,6 +89,8 @@
       | [ H : forall x, ?P x /\ _ |- _ ] => apply (proj1 (H X))
     end.
 
+    ]]
+
    [[
 User error: Bound head variable
    ]]
@@ -450,6 +452,8 @@
 
     completer'.
 
+    ]]
+
     Coq loops forever at this point.  What went wrong? *)
   Abort.
 (* end thide *)
@@ -475,6 +479,8 @@
     | [ |- forall x, ?P ] => trivial
   end.
 
+  ]]
+
     [[
 User error: No matching clauses for match goal
     ]] *)
@@ -503,6 +509,8 @@
     | _ :: ls' => S (length ls')
   end.
 
+  ]]
+
    [[
 Error: The reference ls' was not found in the current environment
    ]]
@@ -516,6 +524,8 @@
     | _ :: ?ls' => S (length ls')
   end.
 
+  ]]
+
 [[
 Error: The reference S was not found in the current environment
 ]]
--- a/src/Predicates.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Predicates.v	Fri Nov 06 12:15:05 2009 -0500
@@ -73,6 +73,7 @@
   (** [[
 
 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. *)
--- a/src/Reflection.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Reflection.v	Fri Nov 06 12:15:05 2009 -0500
@@ -118,6 +118,8 @@
 
   prove_even_reflective.
 
+  ]]
+
   [[
 
 User error: No matching clauses for match goal
@@ -129,6 +131,8 @@
 
   exact (partialOut (check_even 255)).
 
+  ]]
+
   [[
 
   Error: The term "partialOut (check_even 255)" has type
@@ -633,12 +637,19 @@
   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 @@
                   end ]
       end.
 
+]]
+
 #</ol>#%\end{enumerate}%
 #</li>#
    
--- a/src/StackMachine.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/StackMachine.v	Fri Nov 06 12:15:05 2009 -0500
@@ -73,6 +73,8 @@
     | Times => mult
   end.
 
+]]
+
 In this example, we could also omit all of the type annotations, arriving at:
 
 [[
@@ -82,6 +84,8 @@
     | 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 @@
 (** 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 @@
 *)
 
   unfold compile.
-
 (** [[
-
  n : nat
  s : stack
  p : list instr
@@ -289,9 +287,7 @@
 ]] *)
 
   unfold expDenote.
-
 (** [[
-
  n : nat
  s : stack
  p : list instr
@@ -463,6 +459,8 @@
 [[
 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 @@
       end
   end.
 
+]]
+
 The Coq type-checker complains that:
 
 [[