Pass through DataStruct, to incorporate new coqdoc features; globally replace...

Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]

src/Exercises.v

@@ -201,7 +201,7 @@ forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts)
   %\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>#

src/GeneralRec.v

@@ -332,14 +332,14 @@ Ltac run' := unfold run, runTo in *; try red; crush;
               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 @@ End Fix.
 (* 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;

src/Large.v

@@ -565,13 +565,13 @@ Finished transaction in 2. secs (1.264079u,0.s)
     (** %\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 @@ Finished transaction in 2. secs (1.264079u,0.s)
 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

src/MoreDep.v

@@ -1211,7 +1211,7 @@ Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
       | Star _ r => dec_star _ _ _
     end); crush;
   match goal with
-    | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
+    | [ H : _ |- _ ] => generalize (H _ _ (eq_refl _))
   end; tauto.
 Defined.
 

src/Predicates.v

@@ -25,7 +25,7 @@ Inductive prod := .
 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 @@ For instance, our definition [isZero] makes the predicate provable only when the
 
 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. *)
 

src/Reflection.v

@@ -362,7 +362,7 @@ t1 =
 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
       ]]
 

src/Subset.v

@@ -208,12 +208,12 @@ We can continue on in the process of refining [pred]'s type.  Let us change its
 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 @@ match n as n0 return (n0 > 0 -> {m : nat | n0 = S m}) with
                (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 @@ We see the code we entered, with some proofs filled in.  The first proof obligat
 
 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}
      ]]
 

src/Universes.v

@@ -755,13 +755,13 @@ Print eq_rect_eq.
 
   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 choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y :
 
 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 @@ Qed.
 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 @@ Eval compute in cast (t4 13) First.
      : 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 @@ Definition finOut n (f : fin n) : match n return fin n -> Type with
                                     | _ => 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 @@ Section withTypes.
         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