# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1333059052 14400
# Node ID 31fa03bc0f1801dafaf3970197514ddfd1410506
# Parent  e23d41ae63be71a92cba48d118a986192a662c5a
Get it to build with Coq 8.4

diff -r e23d41ae63be -r 31fa03bc0f18 src/GeneralRec.v
--- a/src/GeneralRec.v	Thu Mar 29 17:15:14 2012 -0400
+++ b/src/GeneralRec.v	Thu Mar 29 18:10:52 2012 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2006, 2011, Adam Chlipala
+(* Copyright (c) 2006, 2011-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -346,6 +346,11 @@
 
 Require Import Max.
 
+Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n.
+  induction n; destruct m; simpl; intuition;
+    specialize (IHn m); intuition.
+Qed.
+
 Ltac max := intros n m; generalize (max_spec_le n m); crush.
 
 Lemma max_1 : forall n m, max n m >= n.
diff -r e23d41ae63be -r 31fa03bc0f18 src/Intro.v
--- a/src/Intro.v	Thu Mar 29 17:15:14 2012 -0400
+++ b/src/Intro.v	Thu Mar 29 18:10:52 2012 -0400
@@ -183,7 +183,7 @@
 (** ** Installation and Emacs Set-Up *)
 
 (**
-At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq version 8.3pl2, though parts may work with other versions.
+At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.3pl2 and 8.4 beta, though parts may work with other versions.
 
 %\index{Proof General|(}%To set up your Proof General environment to process the source to this chapter, a few simple steps are required.
 
diff -r e23d41ae63be -r 31fa03bc0f18 src/MoreDep.v
--- a/src/MoreDep.v	Thu Mar 29 17:15:14 2012 -0400
+++ b/src/MoreDep.v	Thu Mar 29 18:10:52 2012 -0400
@@ -558,13 +558,13 @@
 Definition balance1 n (a : rtree n) (data : nat) c2 :=
   match a in rtree n return rbtree c2 n
     -> { c : color & rbtree c (S n) } with
-    | RedNode' _ _ _ t1 y t2 =>
-      match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
+    | RedNode' _ c0 _ t1 y t2 =>
+      match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
         -> { c : color & rbtree c (S n) } with
         | RedNode _ a x b => fun c d =>
           {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
         | t1' => fun t2 =>
-          match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
+          match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
             -> { c : color & rbtree c (S n) } with
             | RedNode _ b x c => fun a d =>
               {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
@@ -581,13 +581,13 @@
 
 Definition balance2 n (a : rtree n) (data : nat) c2 :=
   match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
-    | RedNode' _ _ _ t1 z t2 =>
-      match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
+    | RedNode' _ c0 _ t1 z t2 =>
+      match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
         -> { c : color & rbtree c (S n) } with
         | RedNode _ b y c => fun d a =>
           {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
         | t1' => fun t2 =>
-          match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
+          match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
             -> { c : color & rbtree c (S n) } with
             | RedNode _ c z' d => fun b a =>
               {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
@@ -1132,7 +1132,11 @@
       + {forall l', S l' <= l
         -> ~ P (substring n (S l') s)
         \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
-      match l with
+      match l return {exists l', S l' <= l
+        /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
+      + {forall l', S l' <= l
+        -> ~ P (substring n (S l') s)
+        \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} with
         | O => _
         | S l' =>
           (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
@@ -1186,13 +1190,10 @@
     end.
   Defined.
 
-  (** Finally, we have [dec_star].  It has a straightforward implementation.  We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star].  The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
+  (** Finally, we have [dec_star], defined by straightforward reduction from [dec_star']. *)
 
   Definition dec_star : {star P s} + {~ star P s}.
-    refine (match s return _ with
-              | "" => Reduce (dec_star' (n := length s) 0 _)
-              | _ => Reduce (dec_star' (n := length s) 0 _)
-            end); crush.
+    refine (Reduce (dec_star' (n := length s) 0 _)); crush.
   Defined.
 End dec_star.
 
@@ -1226,22 +1227,22 @@
 
 (* begin hide *)
 Example hi := Concat (Char "h"%char) (Char "i"%char).
-Eval simpl in matches hi "hi".
-Eval simpl in matches hi "bye".
+Eval hnf in matches hi "hi".
+Eval hnf in matches hi "bye".
 
 Example a_b := Or (Char "a"%char) (Char "b"%char).
-Eval simpl in matches a_b "".
-Eval simpl in matches a_b "a".
-Eval simpl in matches a_b "aa".
-Eval simpl in matches a_b "b".
+Eval hnf in matches a_b "".
+Eval hnf in matches a_b "a".
+Eval hnf in matches a_b "aa".
+Eval hnf in matches a_b "b".
 (* end hide *)
 
-(** Many regular expression matching problems are easy to test.  The reader may run each of the following queries to verify that it gives the correct answer. *)
+(** Many regular expression matching problems are easy to test.  The reader may run each of the following queries to verify that it gives the correct answer.  We use evaluation strategy %\index{tactics!hnf}%[hnf] to reduce each term to %\index{head-normal form}\emph{%#<i>#head-normal form#</i>#%}%, where the datatype constructor used to build its value is known. *)
 
 Example a_star := Star (Char "a"%char).
-Eval simpl in matches a_star "".
-Eval simpl in matches a_star "a".
-Eval simpl in matches a_star "b".
-Eval simpl in matches a_star "aa".
+Eval hnf in matches a_star "".
+Eval hnf in matches a_star "a".
+Eval hnf in matches a_star "b".
+Eval hnf in matches a_star "aa".
 
 (** Evaluation inside Coq does not scale very well, so it is easy to build other tests that run for hours or more.  Such cases are better suited to execution with the extracted OCaml code. *)
diff -r e23d41ae63be -r 31fa03bc0f18 src/Subset.v
--- a/src/Subset.v	Thu Mar 29 17:15:14 2012 -0400
+++ b/src/Subset.v	Thu Mar 29 18:10:52 2012 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2011, Adam Chlipala
+(* Copyright (c) 2008-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -566,7 +566,7 @@
 
 Definition pred_strong7 : forall n : nat, {{m | n = S m}}.
   refine (fun n =>
-    match n with
+    match n return {{m | n = S m}} with
       | O => ??
       | S n' => [|n'|]
     end); trivial.
@@ -725,7 +725,7 @@
   Hint Constructors hasType.
 
   refine (fix F (e : exp) : {{t | hasType e t}} :=
-    match e with
+    match e return {{t | hasType e t}} with
       | Nat _ => [|TNat|]
       | Plus e1 e2 =>
         t1 <- F e1;
@@ -872,7 +872,7 @@
   (** Finally, the implementation of [typeCheck] can be transcribed literally, simply switching notations as needed. *)
 
   refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} :=
-    match e with
+    match e return {t : type | hasType e t} + {forall t, ~ hasType e t} with
       | Nat _ => [||TNat||]
       | Plus e1 e2 =>
         t1 <-- F e1;
diff -r e23d41ae63be -r 31fa03bc0f18 staging/index.html
--- a/staging/index.html	Thu Mar 29 17:15:14 2012 -0400
+++ b/staging/index.html	Thu Mar 29 18:10:52 2012 -0400
@@ -39,11 +39,11 @@
 <div class="project">
 <h2>Status</h2>
 
-<p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, and then again on January 14, 2011 to support Coq 8.3.  On August 25, 2011, I've started passes through all chapters, with an eye toward getting ready both for <a href="http://stellar.mit.edu/S/course/6/fa11/6.892/">my fall class</a> and publication by MIT Press.  I'm adding bibliographic references, index entries, and additional exercises, along with the usual tweaks and improvements.</p>
+<p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, then again on January 14, 2011 to support Coq 8.3, and then again on March 29, 2012 to support Coq 8.4 beta.  On August 25, 2011, I started passes through all chapters, with an eye toward getting ready both for <a href="http://stellar.mit.edu/S/course/6/fa11/6.892/">my fall class</a> and publication by MIT Press.  I'm adding bibliographic references and index entries, along with the usual tweaks and improvements.</p>
 
 <p>The current version is effectively a beta release.  It is intended to be consistent, self-contained, and useful, both for individual study and for introductory theorem-proving classes aimed at students with ML or Haskell experience and with basic familiarity with programming language theory.</p>
 
-<p>The main omissions have to do with some supporting resources that I didn't get around to implementing when I used this book for a course.  Some suggested exercises are present, but only at points where I was looking to assign an exercise in the course.  Some chapters are lacking the annotations used to build reduced versions of their source code, where some definitions and proofs have been elided; the course instructor can step through such a file, guiding class participants in filling in the omitted code.</p>
+<p>The main omissions have to do with some supporting resources that I didn't get around to implementing when I used this book for a course.  Some suggested exercises are present (now only in a supplementary file), but only at points where I was looking to assign an exercise in the course.  Some chapters are lacking the annotations used to build reduced versions of their source code, where some definitions and proofs have been elided; the course instructor can step through such a file, guiding class participants in filling in the omitted code.</p>
 
 <p>Previous versions included a final Part on programming language semantics in particular.  I have decided to separate that part out.  I plan to put it up as a supplementary resource eventually; for now it is simply removed.  (It remains present in the <a href="repo">Mercurial</a> history.)</p>
 </div>
diff -r e23d41ae63be -r 31fa03bc0f18 staging/updates.rss
--- a/staging/updates.rss	Thu Mar 29 17:15:14 2012 -0400
+++ b/staging/updates.rss	Thu Mar 29 18:10:52 2012 -0400
@@ -12,6 +12,13 @@
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
 <item>
+        <title>Update to work with Coq 8.4 beta (and keep working with 8.3pl2)</title>
+        <pubDate>Thu, 29 Mar 2012 18:10:00 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+</item>
+
+<item>
         <title>Two new tricks useful in proof by reflection</title>
         <pubDate>Thu, 29 Mar 2012 17:12:01 EDT</pubDate>
         <link>http://adam.chlipala.net/cpdt/</link>