Everything compiles in Coq 8.3pl1

Makefile

-MODULES_NODOC := Axioms Tactics MoreSpecif DepList
+MODULES_NODOC := Tactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality Generic Universes Match Reflection \

src/Axioms.v

-(* Copyright (c) 2008, 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/
- *)
-
-(* Additional axioms not in the Coq standard library *)
-
-Set Implicit Arguments.
-
-Axiom ext_eq : forall (A : Type) (B : A -> Type)
-  (f g : forall x, B x),
-  (forall x, f x = g x)
-  -> f = g.
-
-Theorem ext_eq_Set : forall (A : Set) (B : A -> Set)
-  (f g : forall x, B x),
-  (forall x, f x = g x)
-  -> f = g.
-  intros.
-  rewrite (ext_eq _ _ _ H); reflexivity.
-Qed.
-
-Theorem ext_eq_forall : forall (A : Type)
-  (f g : A -> Set),
-  (forall x, f x = g x)
-  -> @eq Type (forall x, f x) (forall x, g x).
-  intros.
-  rewrite (ext_eq _ _ _ H); trivial.
-Qed.
-
-Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
-  || apply ext_eq_forall); intro.
-
-
-Theorem eta : forall (A B : Type) (f : A -> B),
-  (fun x => f x) = f.
-  intros; ext_eq; trivial.
-Qed.

src/AxiomsImpred.v

-(* Copyright (c) 2008, 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/
- *)
-
-(* Additional axioms not in the Coq standard library, including those that need impredicativity *)
-
-Set Implicit Arguments.
-
-Require Import Axioms.
-Export Axioms.
-
-Theorem ext_eq_forall_Set : forall (A : Type)
-  (f g : A -> Set),
-  (forall x, f x = g x)
-  -> @eq Set (forall x, f x) (forall x, g x).
-  intros.
-  rewrite (ext_eq _ _ _ H); trivial.
-Qed.
-
-Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
-  || apply ext_eq_forall || apply ext_eq_forall_Set); intro.

src/Equality.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -159,7 +159,9 @@ Section fhlist_map.
 (* begin thide *)
     induction ls; crush.
 
-    (** Part of our single remaining subgoal is:
+    (** In Coq 8.2, one subgoal remains at this point.  Coq 8.3 has added some tactic improvements that enable [crush] to complete all of both inductive cases.  To introduce the basics of reasoning about equality, it will be useful to review what was necessary in Coq 8.2
+
+       Part of our single remaining subgoal is:
 
        [[
   a0 : a = elm
@@ -195,18 +197,22 @@ The term "refl_equal ?98" has type "?98 = ?98"
 
     Is it time to throw in the towel?  Luckily, the answer is %``%#"#no.#"#%''%  In this chapter, we will see several useful patterns for proving obligations like this.
 
-    For this particular example, the solution is surprisingly straightforward.  [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments. *)
+    For this particular example, the solution is surprisingly straightforward.  [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
 
+    [[
     case a0.
-    (** [[
+
   ============================
    f a1 = f a1
  
    ]]
 
-    It seems that [destruct] was trying to be too smart for its own good. *)
+    It seems that [destruct] was trying to be too smart for its own good.
 
+    [[
     reflexivity.
+ 
+    ]] *)
   Qed.
 (* end thide *)
 
@@ -605,8 +611,7 @@ Section fhapp'.
   (* EX: Prove [fhapp] associativity using [JMeq]. *)
 
 (* begin thide *)
-  Theorem fhapp_ass' : forall ls1 ls2 ls3
-    (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
+  Theorem fhapp_ass' : forall ls1 ls2 ls3 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
     fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
     induction ls1; crush.
 
@@ -614,16 +619,11 @@ Section fhapp'.
 
        [[
   ============================
-   (a0,
-   fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b
-     (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) ==
-   (a0,
-   fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3)
-     (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
+   (a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
  
        ]]
 
-       It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial.
+       It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial.  Here is what happens when we try that in Coq 8.2:
 
        [[
     rewrite IHls1.
@@ -633,6 +633,8 @@ Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
  
        ]]
 
+       Coq 8.3 currently gives an error message about an uncaught exception.  Perhaps that will be fixed soon.  In any case, it is educational to consider a more explicit approach.
+
        We see that [JMeq] is not a silver bullet.  We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts.  Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type.  That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument.
 
        We can get around this problem by another multiple use of [generalize].  We want to bring into the goal the proper instance of the inductive hypothesis, and we also want to generalize the two relevant uses of [fhapp]. *)

src/Extensional.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import String List.
 
-Require Import Axioms Tactics DepList.
+Require Import Tactics DepList.
 
 Set Implicit Arguments.
 (* end hide *)

src/Hoas.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -8,9 +8,9 @@
  *)
 
 (* begin hide *)
-Require Import Eqdep String List.
+Require Import Eqdep String List FunctionalExtensionality.
 
-Require Import Axioms Tactics.
+Require Import Tactics.
 
 Set Implicit Arguments.
 (* end hide *)
@@ -727,7 +727,7 @@ Ltac my_crush :=
                   | ?F = ?G =>
                     let ec := equate_conj F G in
                       let var := fresh "var" in
-                        assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
+                        assert ec; [ intuition; unfold Exp; extensionality var;
                             assert (H' : F var = G var); try congruence;
                               match type of H' with
                                 | ?X = ?Y =>

src/Intensional.v

-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2008-2009, 2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -8,9 +8,9 @@
  *)
 
 (* begin hide *)
-Require Import Arith Eqdep List.
+Require Import Arith Eqdep List FunctionalExtensionality.
 
-Require Import Axioms DepList Tactics.
+Require Import DepList Tactics.
 
 Set Implicit Arguments.
 (* end hide *)
@@ -178,7 +178,7 @@ Definition Phoasify t (e : DeBruijn.exp nil t) : Phoas.Exp t :=
 
 Theorem phoasify_sound : forall G t (e : DeBruijn.exp G t) s,
   Phoas.expDenote (phoasify e s) = DeBruijn.expDenote e s.
-  induction e; crush; ext_eq; crush.
+  induction e; crush; (let x := fresh in extensionality x); crush.
 Qed.
 
 (** We can prove that any output of [Phoasify] is well-formed, in a sense strong enough to let us avoid asserting last chapter's axiom. *)
@@ -420,7 +420,7 @@ Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t),
   -> forall ts (w : wf ts e1) s,
     G = makeG' s
     -> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2.
-  induction 1; crush; ext_eq; crush.
+  induction 1; crush; (let x := fresh in extensionality x); crush.
 Qed.
 
 (** In the usual way, we wrap [dbify_sound] into the final soundness theorem, formally establishing the expressive equivalence of PHOAS and de Bruijn index terms. *)

src/Interps.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -8,9 +8,9 @@
  *)
 
 (* begin hide *)
-Require Import String List.
+Require Import String List FunctionalExtensionality.
 
-Require Import Axioms Tactics.
+Require Import Tactics.
 
 Set Implicit Arguments.
 (* end hide *)
@@ -191,7 +191,7 @@ Module STLC.
 (* begin thide *)
   Lemma cfold_correct : forall t (e : exp _ t),
     expDenote (cfold e) = expDenote e.
-    induction e; crush; try (ext_eq; crush);
+    induction e; crush; try (let x := fresh in extensionality x; crush);
       repeat (match goal with
                 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
               end; crush).
@@ -484,7 +484,7 @@ Module PSLC.
 
   Lemma cfold_correct : forall t (e : exp _ t),
     expDenote (cfold e) = expDenote e.
-    induction e; crush; try (ext_eq; crush);
+    induction e; crush; try (let x := fresh in extensionality x; crush);
       repeat (match goal with
                 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
                 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E

src/Match.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -988,7 +988,7 @@ Section t7.
     -> P v2 u2
     -> P (f v1 v2) (g u1 u2).
 
-  Theorem t6 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2).
+  Theorem t7 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2).
     intros; do 2 insterKeep H1;
       repeat match goal with
                | [ H : ex _ |- _ ] => destruct H

src/MoreDep.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -875,7 +875,7 @@ Section split.
 
   (** [split'] is the workhorse behind [split].  It searches through the possible ways of splitting [s] into two pieces, checking the two predicates against each such pair.  [split'] progresses right-to-left, from splitting all of [s] into the first piece to splitting all of [s] into the second piece.  It takes an extra argument, [n], which specifies how far along we are in this search process. *)
 
-  Definition split' (n : nat) : n <= length s
+  Definition split' : forall n : nat, n <= length s
     -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
     + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}.
     refine (fix F (n : nat) : n <= length s
@@ -1094,8 +1094,8 @@ Section dec_star.
 
     (** Now we come to [dec_star''] itself.  It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split'].  The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *)
 
-    Definition dec_star'' (l : nat)
-      : {exists l', S l' <= l
+    Definition dec_star'' : forall l : nat,
+      {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)
@@ -1137,7 +1137,7 @@ Section dec_star.
 
   (** The work of [dec_star''] is nested inside another linear search by [dec_star'], which provides the final functionality we need, but for arbitrary suffixes of [s], rather than just for [s] overall. *)
   
-  Definition dec_star' (n n' : nat) : length s - n' <= n
+  Definition dec_star' : forall n n' : nat, length s - n' <= n
     -> {star P (substring n' (length s - n') s)}
     + {~ star P (substring n' (length s - n') s)}.
     refine (fix F (n n' : nat) : length s - n' <= n
@@ -1181,7 +1181,7 @@ Hint Resolve app_cong.
 
 (** With these helper functions completed, the implementation of our [matches] function is refreshingly straightforward.  We only need one small piece of specific tactic work beyond what [crush] does for us. *)
 
-Definition matches P (r : regexp P) s : {P s} + {~ P s}.
+Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
   refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
     match r with
       | Char ch => string_dec s (String ch "")

src/Reflection.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -68,7 +68,7 @@ Local Open Scope partial_scope.
 (** We bring into scope some notations for the [partial] type.  These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *)
 
 (* begin thide *)
-Definition check_even (n : nat) : [isEven n].
+Definition check_even : forall n : nat, [isEven n].
   Hint Constructors isEven.
 
   refine (fix F (n : nat) : [isEven n] :=
@@ -462,9 +462,9 @@ Section my_tauto.
 
   (** 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]. *)
 
-  Definition forward (f : formula) (known : set index) (hyp : formula)
-    (cont : forall known', [allTrue known' -> formulaDenote atomics f])
-    : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f].
+  Definition forward : forall (f : formula) (known : set index) (hyp : formula)
+    (cont : forall known', [allTrue known' -> formulaDenote atomics f]),
+    [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f].
     refine (fix F (f : formula) (known : set index) (hyp : formula)
       (cont : forall known', [allTrue known' -> formulaDenote atomics f])
       : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] :=
@@ -482,8 +482,8 @@ Section my_tauto.
 
   (** A [backward] function implements analysis of the final goal.  It calls [forward] to handle implications. *)
 
-  Definition backward (known : set index) (f : formula)
-    : [allTrue known -> formulaDenote atomics f].
+  Definition backward : forall (known : set index) (f : formula),
+    [allTrue known -> formulaDenote atomics f].
     refine (fix F (known : set index) (f : formula)
       : [allTrue known -> formulaDenote atomics f] :=
       match f with
@@ -498,7 +498,7 @@ Section my_tauto.
 
   (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *)
 
-  Definition my_tauto (f : formula) : [formulaDenote atomics f].
+  Definition my_tauto : forall f : formula, [formulaDenote atomics f].
     intro; refine (Reduce (backward nil f)); crush.
   Defined.
 End my_tauto.

src/Subset.v

-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -226,7 +226,7 @@ let pred_strong3 = function
 
 We have managed to reach a type that is, in a formal sense, the most expressive possible for [pred].  Any other implementation of the same type must have the same input-output behavior.  However, there is still room for improvement in making this kind of code easier to write.  Here is a version that takes advantage of tactic-based theorem proving.  We switch back to passing a separate proof argument instead of using a subset type for the function's input, because this leads to cleaner code. *)
 
-Definition pred_strong4 (n : nat) : n > 0 -> {m : nat | n = S m}.
+Definition pred_strong4 : forall n : nat, n > 0 -> {m : nat | n = S m}.
   refine (fun n =>
     match n with
       | O => fun _ => False_rec _ _
@@ -296,7 +296,7 @@ Eval compute in pred_strong4 two_gt0.
 Notation "!" := (False_rec _ _).
 Notation "[ e ]" := (exist _ e _).
 
-Definition pred_strong5 (n : nat) : n > 0 -> {m : nat | n = S m}.
+Definition pred_strong5 : forall n : nat, n > 0 -> {m : nat | n = S m}.
   refine (fun n =>
     match n with
       | O => fun _ => !
@@ -356,7 +356,7 @@ Notation "'Reduce' x" := (if x then Yes else No) (at level 50).
 
 Now we can write [eq_nat_dec], which compares two natural numbers, returning either a proof of their equality or a proof of their inequality. *)
 
-Definition eq_nat_dec (n m : nat) : {n = m} + {n <> m}.
+Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}.
   refine (fix f (n m : nat) : {n = m} + {n <> m} :=
     match n, m with
       | O, O => Yes
@@ -528,7 +528,7 @@ Notation "[[ x ]]" := (Found _ x _).
 
 (** Now our next version of [pred] is trivial to write. *)
 
-Definition pred_strong7 (n : nat) : {{m | n = S m}}.
+Definition pred_strong7 : forall n : nat, {{m | n = S m}}.
   refine (fun n =>
     match n with
       | O => ??
@@ -567,7 +567,7 @@ Notation "[[[ x ]]]" := (inleft _ [x]).
 
 (** Now we are ready to give the final version of possibly-failing predecessor.  The [sumor]-based type that we use is maximally expressive; any implementation of the type has the same input-output behavior. *)
 
-Definition pred_strong8 (n : nat) : {m : nat | n = S m} + {n = 0}.
+Definition pred_strong8 : forall n : nat, {m : nat | n = S m} + {n = 0}.
   refine (fun n =>
     match n with
       | O => !!
@@ -604,7 +604,7 @@ Notation "x <- e1 ; e2" := (match e1 with
 
    This notation is very helpful for composing richly-typed procedures.  For instance, here is a very simple implementation of a function to take the predecessors of two naturals at once. *)
 
-Definition doublePred (n1 n2 : nat) : {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
+Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
   refine (fun n1 n2 =>
     m1 <- pred_strong7 n1;
     m2 <- pred_strong7 n2;
@@ -623,8 +623,8 @@ Notation "x <-- e1 ; e2" := (match e1 with
 
 (** printing * $\times$ *)
 
-Definition doublePred' (n1 n2 : nat)
-  : {p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}
+Definition doublePred' : forall n1 n2 : nat,
+  {p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}
   + {n1 = 0 \/ n2 = 0}.
   refine (fun n1 n2 =>
     m1 <-- pred_strong8 n1;
@@ -676,7 +676,7 @@ Notation "e1 ;; e2" := (if e1 then e2 else ??)
 (** With that notation defined, we can implement a [typeCheck] function, whose code is only more complex than what we would write in ML because it needs to include some extra type annotations.  Every [[[e]]] expression adds a [hasType] proof obligation, and [crush] makes short work of them when we add [hasType]'s constructors as hints. *)
 (* end thide *)
 
-Definition typeCheck (e : exp) : {{t | hasType e t}}.
+Definition typeCheck : forall e : exp, {{t | hasType e t}}.
 (* begin thide *)
   Hint Constructors hasType.
 
@@ -813,7 +813,7 @@ Qed.
 (** Now we can define the type-checker.  Its type expresses that it only fails on untypable expressions. *)
 
 (* end thide *)
-Definition typeCheck' (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t}.
+Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~ hasType e t}.
 (* begin thide *)
   Hint Constructors hasType.
   (** We register all of the typing rules as hints. *)

src/Tactics.v

-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -126,13 +126,19 @@ Ltac un_done :=
            | [ H : done _ |- _ ] => clear H
          end.
 
+Require Import JMeq.
+
 Ltac crush' lemmas invOne :=
   let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
     let rewriter := autorewrite with cpdt in *;
       repeat (match goal with
-                | [ H : _ |- _ ] => (rewrite H; [])
+                | [ H : ?P |- _ ] =>
+                  match P with
+                    | context[JMeq] => fail 1
+                    | _ => (rewrite H; [])
                       || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
                         || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
+                  end
               end; autorewrite with cpdt in *)
     in (sintuition; rewriter;
         match lemmas with