Mercurial > cpdt > repo

changeset 426:5f25705a10ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 18:10:26 -0400
parents 6ed5ee4845e4
children 5e6b76ca14de
files src/DataStruct.v src/Equality.v src/Exercises.v src/GeneralRec.v src/Large.v src/MoreDep.v src/Predicates.v src/Reflection.v src/Subset.v src/Universes.v
diffstat 10 files changed, 101 insertions(+), 92 deletions(-) [+]
line wrap: on
line diff
--- a/src/DataStruct.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/DataStruct.v	Wed Jul 25 18:10:26 2012 -0400
@@ -32,7 +32,7 @@
   | Nil : ilist O
   | Cons : forall n, A -> ilist n -> ilist (S n).
 
-  (** We might like to have a certified function for selecting an element of an [ilist] by position.  We could do this using subset types and explicit manipulation of proofs, but dependent types let us do it more directly.  It is helpful to define a type family %\index{Gallina terms!fin}%[fin], where [fin n] is isomorphic to [{m : nat | m < n}].  The type family name stands for %``%#"#finite.#"#%''% *)
+  (** We might like to have a certified function for selecting an element of an [ilist] by position.  We could do this using subset types and explicit manipulation of proofs, but dependent types let us do it more directly.  It is helpful to define a type family %\index{Gallina terms!fin}%[fin], where [fin n] is isomorphic to [{m : nat | m < n}].  The type family name stands for "finite." *)
 
   (* EX: Define a function [get] for extracting an [ilist] element by position. *)
 
@@ -160,6 +160,10 @@
 *)
 (* end thide *)
 
+(* begin hide *)
+Definition map' := map.
+(* end hide *)
+
 (** Our [get] function is also quite easy to reason about.  We show how with a short example about an analogue to the list [map] function. *)
 
 Section ilist_map.
@@ -172,7 +176,7 @@
       | Cons _ x ls' => Cons (f x) (imap ls')
     end.
 
-  (** It is easy to prove that [get] %``%#"#distributes over#"#%''% [imap] calls. *)
+  (** It is easy to prove that [get] "distributes over" [imap] calls. *)
 
 (* EX: Prove that [get] distributes over [imap]. *)
 
@@ -188,7 +192,7 @@
 
 (** * Heterogeneous Lists *)
 
-(** Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type.  With fancy type systems, we can partially lift this requirement.  We can index a list type with a %``%#"#type-level#"#%''% list that explains what type each element of the list should have.  This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Coq. *)
+(** Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type.  With fancy type systems, we can partially lift this requirement.  We can index a list type with a "type-level" list that explains what type each element of the list should have.  This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Coq. *)
 
 Section hlist.
   Variable A : Type.
@@ -215,7 +219,7 @@
   | MFirst : forall ls, member (elm :: ls)
   | MNext : forall x ls, member ls -> member (x :: ls).
 
-  (** Because the element [elm] that we are %``%#"#searching for#"#%''% in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable.  In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too.  The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations.
+  (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable.  In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too.  The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations.
 
      We can use [member] to adapt our definition of [get] to [hlist]s.  The same basic [match] tricks apply.  In the [MCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match].  We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
 
@@ -370,7 +374,7 @@
 
 (** * Recursive Type Definitions *)
 
-(** %\index{recursive type definition}%There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above.  Because Coq supports %``%#"#type-level computation,#"#%''% we can redo our inductive definitions as _recursive_ definitions. *)
+(** %\index{recursive type definition}%There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above.  Because Coq supports "type-level computation," we can redo our inductive definitions as _recursive_ definitions. *)
 
 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
 
@@ -434,7 +438,7 @@
       | x :: ls' => (x = elm) + fmember ls'
     end%type.
 
-  (** The definition of [fmember] follows the definition of [ffin].  Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail.  While for [index] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for.  We express that with a sum type whose left branch is the appropriate equality proposition.  Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
+  (** The definition of [fmember] follows the definition of [ffin].  Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail.  While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for.  We express that with a sum type whose left branch is the appropriate equality proposition.  Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
 
      We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
 
@@ -459,7 +463,7 @@
       | _ :: ls' => fun mls idx =>
         match idx with
           | inl pf => match pf with
-                        | refl_equal => fst mls
+                        | eq_refl => fst mls
                       end
           | inr idx' => fhget ls' (snd mls) idx'
         end
@@ -467,13 +471,17 @@
 
   (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker.  Exactly why this works can be seen by studying the definition of equality. *)
 
+  (* begin hide *)
+  Definition foo := (@eq, @eq_refl).
+  (* end hide *)
+
   Print eq.
   (** %\vspace{-.15in}% [[
-Inductive eq (A : Type) (x : A) : A -> Prop :=  refl_equal : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
  
 ]]
 
-In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument.  The type of the constructor [refl_equal] shows that [y] can only ever be instantiated to [x].  Thus, within a pattern-match with [refl_equal], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
+In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument.  The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x].  Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
 (* end thide *)
 
 End fhlist.
@@ -638,7 +646,7 @@
 
 (** ** Another Interpreter Example *)
 
-(** We develop another example of variable-arity constructors, in the form of optimization of a small expression language with a construct like Scheme's %\texttt{%#<tt>#cond#</tt>#%}%.  Each of our conditional expressions takes a list of pairs of boolean tests and bodies.  The value of the conditional comes from the body of the first test in the list to evaluate to [true].  To simplify the %\index{interpreters}%interpreter we will write, we force each conditional to include a final, default case. *)
+(** We develop another example of variable-arity constructors, in the form of optimization of a small expression language with a construct like Scheme's <<cond>>.  Each of our conditional expressions takes a list of pairs of boolean tests and bodies.  The value of the conditional comes from the body of the first test in the list to evaluate to [true].  To simplify the %\index{interpreters}%interpreter we will write, we force each conditional to include a final, default case. *)
 
 Inductive type' : Type := Nat | Bool.
 
@@ -827,7 +835,7 @@
     end; crush.
 Qed.
 
-(** Now the final theorem is easy to prove.  We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct. *)
+(** Now the final theorem is easy to prove. *)
 (* end thide *)
 
 Theorem cfold_correct : forall t (e : exp' t),
@@ -843,6 +851,7 @@
 Qed.
 (* end thide *)
 
+(** We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct. *)
 
 (** * Choosing Between Representations *)
 
@@ -850,10 +859,10 @@
 
    Inductive types are often the most pleasant to work with, after someone has spent the time implementing some basic library functions for them, using fancy [match] annotations.  Many aspects of Coq's logic and tactic support are specialized to deal with inductive types, and you may miss out if you use alternate encodings.
 
-   Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation.  For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types.  Consider a call [get l f], where variable [l] has type [filist A (S n)].  The type of [l] would be simplified to an explicit pair type.  In a proof involving many recursive types, this kind of unhelpful %``%#"#simplification#"#%''% can lead to rapid bloat in the sizes of subgoals.  Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the %``%#"#simplified#"#%''% version.  The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may %``%#"#simplify#"#%''% when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value.
+   Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation.  For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types.  Consider a call [get l f], where variable [l] has type [filist A (S n)].  The type of [l] would be simplified to an explicit pair type.  In a proof involving many recursive types, this kind of unhelpful "simplification" can lead to rapid bloat in the sizes of subgoals.  Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the "simplified" version.  The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may "simplify" when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value.
 
-   Another disadvantage of recursive types is that they only apply to type families whose indices determine their %``%#"#skeletons.#"#%''%  This is not true for all data structures; a good counterexample comes from the richly typed programming language syntax types we have used several times so far.  The fact that a piece of syntax has type [Nat] tells us nothing about the tree structure of that syntax.
+   Another disadvantage of recursive types is that they only apply to type families whose indices determine their "skeletons."  This is not true for all data structures; a good counterexample comes from the richly typed programming language syntax types we have used several times so far.  The fact that a piece of syntax has type [Nat] tells us nothing about the tree structure of that syntax.
 
-   Finally, Coq type inference can be more helpful in constructing values in inductive types.  Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type.  This downside can be mitigated to an extent by writing %``%#"#constructor#"#%''% functions for a recursive type, mirroring the definition of the corresponding inductive type.
+   Finally, Coq type inference can be more helpful in constructing values in inductive types.  Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type.  This downside can be mitigated to an extent by writing "constructor" functions for a recursive type, mirroring the definition of the corresponding inductive type.
 
    Reflexive encodings of data types are seen relatively rarely.  As our examples demonstrated, manipulating index values manually can lead to hard-to-read code.  A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3.  For small developments, avoiding that kind of coding can justify the use of reflexive data structures.  There are also some useful instances of %\index{co-inductive types}%co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *)
--- a/src/Equality.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Equality.v	Wed Jul 25 18:10:26 2012 -0400
@@ -200,7 +200,7 @@
       | _ :: ls' => fun mls idx =>
         match idx with
           | inl pf => match pf with
-                        | refl_equal => fst mls
+                        | eq_refl => fst mls
                       end
           | inr idx' => fhget ls' (snd mls) idx'
         end
@@ -244,13 +244,13 @@
   a0 : a = elm
   ============================
    match a0 in (_ = a2) return (C a2) with
-   | refl_equal => f a1
+   | eq_refl => f a1
    end = f match a0 in (_ = a2) return (B a2) with
-           | refl_equal => a1
+           | eq_refl => a1
            end
        ]]
 
-   This seems like a trivial enough obligation.  The equality proof [a0] must be [refl_equal], since that is the only constructor of [eq].  Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
+   This seems like a trivial enough obligation.  The equality proof [a0] must be [eq_refl], since that is the only constructor of [eq].  Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
     [[
     destruct a0.
 ]]
@@ -261,11 +261,11 @@
 
     This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed.  We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
     [[
-    assert (a0 = refl_equal _).
+    assert (a0 = eq_refl _).
 ]]
 
 <<
-The term "refl_equal ?98" has type "?98 = ?98"
+The term "eq_refl ?98" has type "?98 = ?98"
  while it is expected to have type "a = elm"
 >>
 
@@ -291,7 +291,7 @@
 
   (** It will be helpful to examine the proof terms generated by this sort of strategy.  A simpler example illustrates what is going on. *)
 
-  Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
+  Lemma lemma1 : forall x (pf : x = elm), O = match pf with eq_refl => O end.
 (* begin thide *)
     simple destruct pf; reflexivity.
   Qed.
@@ -304,12 +304,12 @@
 lemma1 = 
 fun (x : A) (pf : x = elm) =>
 match pf as e in (_ = y) return (0 = match e with
-                                     | refl_equal => 0
+                                     | eq_refl => 0
                                      end) with
-| refl_equal => refl_equal 0
+| eq_refl => eq_refl 0
 end
      : forall (x : A) (pf : x = elm), 0 = match pf with
-                                          | refl_equal => 0
+                                          | eq_refl => 0
                                           end
  
     ]]
@@ -320,15 +320,15 @@
   Definition lemma1' :=
     fun (x : A) (pf : x = elm) =>
       match pf return (0 = match pf with
-                             | refl_equal => 0
+                             | eq_refl => 0
                            end) with
-        | refl_equal => refl_equal 0
+        | eq_refl => eq_refl 0
       end.
 (* end thide *)
 
   (** Surprisingly, what seems at first like a _simpler_ lemma is harder to prove. *)
 
-  Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
+  Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with eq_refl => O end.
 (* begin thide *)
     (** %\vspace{-.25in}%[[
     simple destruct pf.
@@ -346,15 +346,15 @@
   Definition lemma2 :=
     fun (x : A) (pf : x = x) =>
       match pf return (0 = match pf with
-                             | refl_equal => 0
+                             | eq_refl => 0
                            end) with
-        | refl_equal => refl_equal 0
+        | eq_refl => eq_refl 0
       end.
 (* end thide *)
 
   (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
 
-  Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
+  Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
 (* begin thide *)
     (** %\vspace{-.25in}%[[
     simple destruct pf.
@@ -371,13 +371,13 @@
      [[
   Definition lemma3' :=
     fun (x : A) (pf : x = x) =>
-      match pf as pf' in (_ = x') return (pf' = refl_equal x') with
-        | refl_equal => refl_equal _
+      match pf as pf' in (_ = x') return (pf' = eq_refl x') with
+        | eq_refl => eq_refl _
       end.
 ]]
 
 <<
-The term "refl_equal x'" has type "x' = x'" while it is expected to have type
+The term "eq_refl x'" has type "x' = x'" while it is expected to have type
  "x = x'"
 >>
 
@@ -385,14 +385,14 @@
 
      Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
 
-  Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
+  Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
     intros; apply UIP_refl.
   Qed.
 
   Check UIP_refl.
   (** %\vspace{-.15in}% [[
 UIP_refl
-     : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
+     : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
      ]]
 
      The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library.  Do the Coq authors know of some clever trick for building such proofs that we have not seen yet?  If they do, they did not use it for this proof.  Rather, the proof is based on an _axiom_. *)
@@ -426,7 +426,7 @@
 Streicher_K = 
 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
      : forall (U : Type) (x : U) (P : x = x -> Prop),
-       P (refl_equal x) -> forall p : x = x, P p
+       P (eq_refl x) -> forall p : x = x, P p
   ]]
 
   This is the unfortunately named %\index{axiom K}``%#"#Streicher's axiom K,#"#%''% which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
@@ -477,7 +477,7 @@
     (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
     fhapp hls1 (fhapp hls2 hls3)
     = match pf in (_ = ls) return fhlist _ ls with
-        | refl_equal => fhapp (fhapp hls1 hls2) hls3
+        | eq_refl => fhapp (fhapp hls1 hls2) hls3
       end.
     induction ls1; crush.
 
@@ -486,7 +486,7 @@
   ============================
    fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
+   | eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
    end
        ]]
 
@@ -519,7 +519,7 @@
    fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
      (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        (a0,
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
@@ -544,7 +544,7 @@
    fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
      (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        (a0,
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
@@ -558,12 +558,12 @@
   ============================
    (a0,
    match pf' in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
    end) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        (a0,
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
@@ -577,10 +577,10 @@
    forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
    (a0,
    match pf' in (_ = ls) return (fhlist B ls) with
-   | refl_equal => f
+   | eq_refl => f
    end) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal => (a0, f)
+   | eq_refl => (a0, f)
    end
         ]]
 
@@ -595,10 +595,10 @@
      (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
    (a0,
    match pf'0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => f
+   | eq_refl => f
    end) =
    match pf0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => (a0, f)
+   | eq_refl => (a0, f)
    end
         ]]
 
@@ -614,10 +614,10 @@
      (f : fhlist B (ls1 ++ ls2 ++ ls3)),
    (a0,
    match pf'0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => f
+   | eq_refl => f
    end) =
    match pf0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => (a0, f)
+   | eq_refl => (a0, f)
    end
         ]]
 
@@ -650,11 +650,11 @@
 
 Infix "==" := JMeq (at level 70, no associativity).
 
-(* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
+(* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
 (* begin thide *)
-Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
-  match pf return (pf == refl_equal _) with
-    | refl_equal => JMeq_refl _
+Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == eq_refl x :=
+  match pf return (pf == eq_refl _) with
+    | eq_refl => JMeq_refl _
   end.
 (* end thide *)
 
@@ -663,7 +663,7 @@
    Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)
 
 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
-  O = match pf with refl_equal => O end.
+  O = match pf with eq_refl => O end.
 (* begin thide *)
   intros; rewrite (UIP_refl' pf); reflexivity.
 Qed.
@@ -862,14 +862,14 @@
 
    To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section.  The rest of the proof is trivial. *)
 
-Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
+Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x.
   intros; rewrite (UIP_refl' pf); reflexivity.
 Qed.
 
 (** The other direction is perhaps more interesting.  Assume that we only have the axiom of the [Eqdep] module available.  We can define [JMeq] in a way that satisfies the same interface as the combination of the [JMeq] module's inductive definition and axiom. *)
 
 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
-  exists pf : B = A, x = match pf with refl_equal => y end.
+  exists pf : B = A, x = match pf with eq_refl => y end.
 
 Infix "===" := JMeq' (at level 70, no associativity).
 
@@ -879,7 +879,7 @@
 
 (** remove printing exists *)
 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
-  intros; unfold JMeq'; exists (refl_equal A); reflexivity.
+  intros; unfold JMeq'; exists (eq_refl A); reflexivity.
 Qed.
 
 (** printing exists $\exists$ *)
@@ -892,7 +892,7 @@
   (** [[
   H : exists pf : A = A,
         x = match pf in (_ = T) return T with
-            | refl_equal => y
+            | eq_refl => y
             end
   ============================
    x = y
@@ -903,7 +903,7 @@
   (** [[
   x0 : A = A
   H : x = match x0 in (_ = T) return T with
-          | refl_equal => y
+          | eq_refl => y
           end
   ============================
    x = y
@@ -915,7 +915,7 @@
   x0 : A = A
   ============================
    match x0 in (_ = T) return T with
-   | refl_equal => y
+   | eq_refl => y
    end = y
       ]]
       *)
--- a/src/Exercises.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Exercises.v	Wed Jul 25 18:10:26 2012 -0400
@@ -201,7 +201,7 @@
   %\item%#<li># Define a recursive function [subst' : forall ts t (e : exp ts t) ts1 t' ts2, ts = ts1 ++ t' :: ts2 -> exp (ts1 ++ ts2) t' -> exp (ts1 ++ ts2) t].  This is the workhorse of substitution in expressions, employing the same proof-passing trick as for [lift'].  You will probably want to use [lift] somewhere in the definition of [subst'].#</li>#
   %\item%#<li># Now [subst] should be a one-liner, defined in terms of [subst'].#</li>#
   %\item%#<li># Prove a correctness theorem for each auxiliary function, leading up to the proof of [subst] correctness.#</li>#
-  %\item%#<li># All of the reasoning about equality proofs in these theorems follows a regular pattern.  If you have an equality proof that you want to replace with [refl_equal] somehow, run [generalize] on that proof variable.  Your goal is to get to the point where you can [rewrite] with the original proof to change the type of the generalized version.  To avoid type errors (the infamous %``%#"#second-order unification#"#%''% failure messages), it will be helpful to run [generalize] on other pieces of the proof context that mention the equality's lefthand side.  You might also want to use [generalize dependent], which generalizes not just one variable but also all variables whose types depend on it.  [generalize dependent] has the sometimes-helpful property of removing from the context all variables that it generalizes.  Once you do manage the mind-bending trick of using the equality proof to rewrite its own type, you will be able to rewrite with [UIP_refl].#</li>#
+  %\item%#<li># All of the reasoning about equality proofs in these theorems follows a regular pattern.  If you have an equality proof that you want to replace with [eq_refl] somehow, run [generalize] on that proof variable.  Your goal is to get to the point where you can [rewrite] with the original proof to change the type of the generalized version.  To avoid type errors (the infamous %``%#"#second-order unification#"#%''% failure messages), it will be helpful to run [generalize] on other pieces of the proof context that mention the equality's lefthand side.  You might also want to use [generalize dependent], which generalizes not just one variable but also all variables whose types depend on it.  [generalize dependent] has the sometimes-helpful property of removing from the context all variables that it generalizes.  Once you do manage the mind-bending trick of using the equality proof to rewrite its own type, you will be able to rewrite with [UIP_refl].#</li>#
   %\item%#<li># The [ext_eq] axiom from the end of this chapter is available in the Coq standard library as [functional_extensionality] in module [FunctionalExtensionality], and you will probably want to use it in the [lift'] and [subst'] correctness proofs.#</li>#
   %\item%#<li># The [change] tactic should come in handy in the proofs about [lift] and [subst], where you want to introduce %``%#"#extraneous#"#%''% list concatenations with [nil] to match the forms of earlier theorems.#</li>#
   %\item%#<li># Be careful about [destruct]ing a term %``%#"#too early.#"#%''%  You can use [generalize] on proof terms to bring into the proof context any important propositions about the term.  Then, when you [destruct] the term, it is updated in the extra propositions, too.  The [case_eq] tactic is another alternative to this approach, based on saving an equality between the original term and its new form.#</li>#
--- a/src/GeneralRec.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/GeneralRec.v	Wed Jul 25 18:10:26 2012 -0400
@@ -332,14 +332,14 @@
               case_eq M; intros ? ? Heq; try rewrite Heq in *; subst
             | [ H : forall n v, ?E n = Some v -> _,
                 _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] =>
-              specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
+              specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
             | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto
           end; simpl in *); eauto 7.
 
 Ltac run := run'; repeat (match goal with
                             | [ H : forall n v, ?E n = Some v -> _
                                 |- context[match ?E ?N with Some _ => _ | None => _ end] ] =>
-                              specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate
+                              specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate
                           end; run').
 
 Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P.
@@ -536,12 +536,12 @@
 (* begin hide *)
 Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y)
   -> x = y.
-  intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
+  intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
 Qed.
 
 Lemma leq_None : forall A (x y : A), leq (Some x) None
   -> False.
-  intros ? ? ? H; generalize (H _ (refl_equal _)); crush.
+  intros ? ? ? H; generalize (H _ (eq_refl _)); crush.
 Qed.
 
 Ltac mergeSort' := run;
--- a/src/Large.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Large.v	Wed Jul 25 18:10:26 2012 -0400
@@ -565,13 +565,13 @@
     (** %\vspace{-.15in}%[[
  == intro x; intro y; intro H; intro H0; intro H4;
        simple eapply trans_eq.
-    simple apply refl_equal.
+    simple apply eq_refl.
     
     simple eapply trans_eq.
-    simple apply refl_equal.
+    simple apply eq_refl.
     
     simple eapply trans_eq.
-    simple apply refl_equal.
+    simple apply eq_refl.
     
     simple apply H1.
     eexact H.
@@ -596,20 +596,20 @@
 1.1.1.1.1.1 depth=6 intro
 1.1.1.1.1.1.1 depth=5 apply H3
 1.1.1.1.1.1.1.1 depth=4 eapply trans_eq
-1.1.1.1.1.1.1.1.1 depth=4 apply refl_equal
+1.1.1.1.1.1.1.1.1 depth=4 apply eq_refl
 1.1.1.1.1.1.1.1.1.1 depth=3 eapply trans_eq
-1.1.1.1.1.1.1.1.1.1.1 depth=3 apply refl_equal
+1.1.1.1.1.1.1.1.1.1.1 depth=3 apply eq_refl
 1.1.1.1.1.1.1.1.1.1.1.1 depth=2 eapply trans_eq
-1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply refl_equal
+1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply eq_refl
 1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 eapply trans_eq
-1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply refl_equal
+1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply eq_refl
 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=0 eapply trans_eq
 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=1 apply sym_eq ; trivial
 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=0 eapply trans_eq
 1.1.1.1.1.1.1.1.1.1.1.1.1.1.3 depth=0 eapply trans_eq
 1.1.1.1.1.1.1.1.1.1.1.1.2 depth=2 apply sym_eq ; trivial
 1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=1 eapply trans_eq
-1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply refl_equal
+1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply eq_refl
 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 depth=0 eapply trans_eq
 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2 depth=1 apply sym_eq ; trivial
 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2.1 depth=0 eapply trans_eq
--- a/src/MoreDep.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/MoreDep.v	Wed Jul 25 18:10:26 2012 -0400
@@ -1211,7 +1211,7 @@
       | Star _ r => dec_star _ _ _
     end); crush;
   match goal with
-    | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
+    | [ H : _ |- _ ] => generalize (H _ _ (eq_refl _))
   end; tauto.
 Defined.
 
--- a/src/Predicates.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Predicates.v	Wed Jul 25 18:10:26 2012 -0400
@@ -25,7 +25,7 @@
 Inductive and := conj.
 Inductive or := or_introl | or_intror.
 Inductive ex := ex_intro.
-Inductive eq := refl_equal.
+Inductive eq := eq_refl.
 Reset unit.
 (* end thide *)
 (* end hide *)
@@ -466,11 +466,11 @@
 
 Print eq.
 (** [[
-  Inductive eq (A : Type) (x : A) : A -> Prop :=  refl_equal : x = x
+  Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
  
   ]]
 
-  Behind the scenes, uses of infix [=] are expanded to instances of [eq].  We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type.  The type of [eq] allows us to state any equalities, even those that are provably false.  However, examining the type of equality's sole constructor [refl_equal], we see that we can only _prove_ equality when its two arguments are syntactically equal.  This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition.  Another way of stating that definition is: equality is defined as the least reflexive relation.
+  Behind the scenes, uses of infix [=] are expanded to instances of [eq].  We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type.  The type of [eq] allows us to state any equalities, even those that are provably false.  However, examining the type of equality's sole constructor [eq_refl], we see that we can only _prove_ equality when its two arguments are syntactically equal.  This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition.  Another way of stating that definition is: equality is defined as the least reflexive relation.
 
 Returning to the example of [isZero], we can see how to work with hypotheses that use this predicate. *)
 
--- a/src/Reflection.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Reflection.v	Wed Jul 25 18:10:26 2012 -0400
@@ -362,7 +362,7 @@
 fun a b c d : A =>
 monoid_reflect (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d))
   (Op (Op (Var a) (Op (Var b) (Var c))) (Var d))
-  (refl_equal (a + (b + (c + (d + e)))))
+  (eq_refl (a + (b + (c + (d + e)))))
      : forall a b c d : A, a + b + c + d = a + (b + c) + d
       ]]
 
--- a/src/Subset.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Subset.v	Wed Jul 25 18:10:26 2012 -0400
@@ -208,12 +208,12 @@
 Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} :=
   match s return {m : nat | proj1_sig s = S m} with
     | exist 0 pf => match zgtz pf with end
-    | exist (S n') pf => exist _ n' (refl_equal _)
+    | exist (S n') pf => exist _ n' (eq_refl _)
   end.
 
 Eval compute in pred_strong3 (exist _ 2 two_gt0).
 (** %\vspace{-.15in}% [[
-     = exist (fun m : nat => 2 = S m) 1 (refl_equal 2)
+     = exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
      : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m}
       ]]
      *)
@@ -298,7 +298,7 @@
                (Bool.absurd_eq_true false (pred_strong4_subproof n _)))))
 | S n' =>
     fun _ : S n' > 0 =>
-    exist (fun m : nat => S n' = S m) n' (refl_equal (S n'))
+    exist (fun m : nat => S n' = S m) n' (eq_refl (S n'))
 end
      : forall n : nat, n > 0 -> {m : nat | n = S m}
  
@@ -308,7 +308,7 @@
 
 Eval compute in pred_strong4 two_gt0.
 (** %\vspace{-.15in}% [[
-     = exist (fun m : nat => 2 = S m) 1 (refl_equal 2)
+     = exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
      : {m : nat | 2 = S m}
      ]]
 
--- a/src/Universes.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Universes.v	Wed Jul 25 18:10:26 2012 -0400
@@ -755,13 +755,13 @@
 
   This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e].  The axiom is logically equivalent to some simpler corollaries.  In the theorem names, %``%#"#UIP#"#%''% stands for %\index{unicity of identity proofs}``%#"#unicity of identity proofs#"#%''%, where %``%#"#identity#"#%''% is a synonym for %``%#"#equality.#"#%''% *)
 
-Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x.
-  intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [
+Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = eq_refl x.
+  intros; replace pf with (eq_rect x (eq x) (eq_refl x) x pf); [
     symmetry; apply eq_rect_eq
     | exact (match pf as pf' return match pf' in _ = y return x = y with
-                                      | refl_equal => refl_equal x
+                                      | eq_refl => eq_refl x
                                     end = pf' with
-               | refl_equal => refl_equal _
+               | eq_refl => eq_refl _
              end) ].
 Qed.
 
@@ -875,12 +875,12 @@
 
 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
   match pf with
-    | refl_equal => v
+    | eq_refl => v
   end.
 
 (** Computation over programs that use [cast] can proceed smoothly. *)
 
-Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12.
+Eval compute in (cast (eq_refl (nat -> nat)) (fun n => S n)) 12.
 (** %\vspace{-.15in}%[[
      = 13
      : nat
@@ -897,7 +897,7 @@
 Eval compute in (cast t3 (fun _ => First)) 12.
 (** [[
      = match t3 in (_ = P) return P with
-       | refl_equal => fun n : nat => First
+       | eq_refl => fun n : nat => First
        end 12
      : fin (12 + 1)
      ]]
@@ -938,7 +938,7 @@
      : fin (13 + 1)
      ]]
 
-   This simple computational reduction hides the use of a recursive function to produce a suitable [refl_equal] proof term.  The recursion originates in our use of [induction] in [t4]'s proof. *)
+   This simple computational reduction hides the use of a recursive function to produce a suitable [eq_refl] proof term.  The recursion originates in our use of [induction] in [t4]'s proof. *)
 
 
 (** ** Methods for Avoiding Axioms *)
@@ -995,8 +995,8 @@
                                     | _ => fun f => {f' : _ | f = Next f'} + {f = First}
                                   end f :=
   match f with
-    | First _ => inright _ (refl_equal _)
-    | Next _ f' => inleft _ (exist _ f' (refl_equal _))
+    | First _ => inright _ (eq_refl _)
+    | Next _ f' => inleft _ (exist _ f' (eq_refl _))
   end.
 (* end thide *)
 
@@ -1161,7 +1161,7 @@
         match natIndex return nth_error (t :: ts) natIndex = Some nat -> nat with
           | O => fun pf =>
             match Some_inj pf in _ = T return T with
-              | refl_equal => x
+              | eq_refl => x
             end
           | S natIndex' => getNat values'' natIndex'
         end