Batch of changes based on proofreader feedback

src/Coinductive.v

@@ -617,8 +617,7 @@ Section evalCmd_coind.
     cofix; intros; destruct c.
     rewrite (AssignCase H); constructor.
     destruct (SeqCase H) as [? [? ?]]; econstructor; eauto.
-    destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst;
-      [ econstructor | econstructor 4 ]; eauto.
+    destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto.
   Qed.
 End evalCmd_coind.
 
@@ -644,13 +643,12 @@ Fixpoint optCmd (c : cmd) : cmd :=
 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e.
   induction e; crush;
     repeat (match goal with
-              | [ |- context[match ?E with Const _ => _ | Var _ => _
-                               | Plus _ _ => _ end] ] => destruct E
+              | [ |- context[match ?E with Const _ => _ | _ => _ end] ] => destruct E
               | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
             end; crush).
 Qed.
 
-Hint Rewrite optExp_correct .
+Hint Rewrite optExp_correct.
 
 (** The final theorem is easy to establish, using our co-induction principle and a bit of Ltac smarts that we leave unexplained for now.  Curious readers can consult the Coq manual, or wait for the later chapters of this book about proof automation.  At a high level, we show inclusions between behaviors, going in both directions between original and optimized programs. *)
 

src/DataStruct.v

@@ -74,7 +74,7 @@ Section ilist.
         end
     end.
     ]]
-    %\vspace{-.15in}%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'].  In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic.  We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A].  We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically.  Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern.  As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
+    %\vspace{-.15in}%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'].  In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic.  We are told that the [Nil] case body has type [match X with | O => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A].  We can see that setting [X] to [O] resolves the conflict, but Coq is not yet smart enough to do this unification automatically.  Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern.  As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
 
     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 the convoy pattern that we met last chapter.  This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables.
     [[
@@ -623,7 +623,7 @@ Qed.
 
 Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat),
   (forall idx, f1 idx >= f2 idx)
-  -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
+  -> rifoldr plus O f1 >= rifoldr plus O f2.
   Hint Resolve plus_ge.
 
   induction n; crush.

staging/updates.rss

@@ -11,6 +11,14 @@
 <webMaster>adam@chlipala.net</webMaster>
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
+<item>
+        <title>Batch of changes based on proofreader feedback</title>
+        <pubDate>Sun, 11 Nov 2012 18:16:46 EST</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>
         <title>Batch of changes based on proofreader feedback</title>
         <pubDate>Thu, 25 Oct 2012 08:40:19 EDT</pubDate>