Replaced misc.inj_right_pair2 with stdlib's Eqdep_dec.inj_pair2_eq_dec

doc/chapter-primrec.tex

@@ -58,9 +58,9 @@ \subsubsection{The constant function of value 0}
 % builds the constant function of type $\mathbb{N}^n \arrow \mathbb{N}$ which returns $0$.
 
 
-\subsection{Constant functions}
+\subsubsection{Constant functions}
 
-Let $k$ be some natural number; the constant function hich always returns $k$ is built through $k$ nested compositions of the 
+Let $k$ be some natural number; the unary constant function which always returns $k$ is built through $k$ nested compositions of the 
 successor function to the  unary constant function which returns $0$.
 
 
@@ -101,7 +101,7 @@ \subsubsection{Multiplication on natural natural numbers}
 \end{align*}  
 
 This function is an instance of the primitive recursion scheme,
-with $n=1$, $g$ the constant unary function which returns $0$ (see subsection~\vref{sect:k0}),
+with $n=1$, $g$ is the constant unary function which returns $0$ (see subsection~\vref{sect:k0}),
  and $h$ the function defined by $h(p,x,n_1)=x+n_1$, which can be written as the composition of $+$ and the projections 
 $\pi_{2,3}$ and $\pi_{3,3}$ (the three of them  being  primitive recursive).
 

theories/ordinals/Ackermann/LNN2LNT.v

@@ -174,7 +174,7 @@ Proof.
   simpl; destruct (consTerms LNN 0 b) as [(a2, b1) p0].
   simpl in p; inversion p.
   assert (b = Tcons a0 b0)
-    by refine (inj_right_pair2 _ eq_nat_dec _ _ _ _ H1).
+    by refine (inj_pair2_eq_dec  _ eq_nat_dec _ _ _ _ H1).
   rewrite H in p0; simpl in p0; inversion p0; reflexivity.
 Qed.
 

theories/ordinals/Ackermann/fol.v

@@ -187,7 +187,7 @@ Proof.
       + intros H; rewrite <- H; auto.
       + intros H; inversion H as [H1].
         eapply
-          inj_right_pair2 with
+          inj_pair2_eq_dec with
           (P := 
              fun f : Functions L =>
                Terms (arityF L f)); assumption.
@@ -232,7 +232,7 @@ Proof.
          rewrite <- p in H2; inversion H2; reflexivity. 
     * right; intro H2; elim b1.
       rewrite <- p in H2; inversion H2.
-      eapply inj_right_pair2 with (P := fun n : nat => Terms n).
+      eapply inj_pair2_eq_dec with (P := fun n : nat => Terms n).
       apply eq_nat_dec.
       assumption.
 Qed.
@@ -255,7 +255,7 @@ Proof.
     + right. intro H; elim b0.
       rewrite <- p in H.
       inversion H.
-      eapply inj_right_pair2 with (P := fun n : nat => Terms n).
+      eapply inj_pair2_eq_dec with (P := fun n : nat => Terms n).
       * apply eq_nat_dec.
       * assumption.
 Qed.
@@ -298,7 +298,7 @@ Proof.
         + simpl in |- *; split.
           * intros H; rewrite H; reflexivity.
           * intros H; inversion H.
-            eapply inj_right_pair2 with
+            eapply inj_pair2_eq_dec with
               (P := 
                  fun f : Relations L =>
                    Terms (arityR L f)).

theories/ordinals/Ackermann/folLogic3.v

@@ -475,8 +475,8 @@ Proof.
       inversion e0.
       inversion e. 
       auto.
-      rewrite (inj_right_pair2 _ eq_nat_dec _ _ _ _ H4).
-      rewrite (inj_right_pair2 _ eq_nat_dec _ _ _ _ H6).
+      rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H4).
+      rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H6).
       auto.
 Qed.
 
@@ -498,8 +498,8 @@ Proof.
     inversion e.
     split.
     + apply subWithEqualsTerm; auto.
-    + rewrite (inj_right_pair2 _ eq_nat_dec _ _ _ _ H2).
-      now rewrite (inj_right_pair2 _ eq_nat_dec _ _ _ _ H4).
+    + rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H2).
+      now rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H4).
 Qed.
 
 Lemma subWithEquals :

theories/ordinals/Ackermann/misc.v

@@ -1,35 +1,4 @@
-Require Import Eqdep_dec.
+Require Export Eqdep_dec.
 
-#[global] Set Asymmetric Patterns.
+#[global] Set Asymmetric Patterns. 
 
-Lemma inj_right_pair2 (A: Set):
-  (forall x y : A, {x = y} + {x <> y}) ->
-  forall (x : A) (P : A -> Set) (y y' : P x),
-    existT P x y = existT P x y' -> y = y'.
-Proof.
-  intros H x P y y' H0.
-  set (Proj :=
-         fun (e : sigT P) (def : P x) =>
-           match e with
-           | existT x' dep =>
-               match H x' x with
-               | left eqdep => eq_rec x' P dep x eqdep
-               | _ => def
-               end
-           end) in *.
-  cut (Proj (existT P x y) y = Proj (existT P x y') y).
-  - simpl; destruct  (H x x) as [e | n]. 
-    + intro e0;
-        set
-          (B :=
-             K_dec_set H
-               (fun z : x = x =>
-                  eq_rec x P y x z = eq_rec x P y' x z ->
-                  eq_rec x P y x (refl_equal x) = 
-                    eq_rec x P y' x (refl_equal x))
-               (fun z : eq_rec x P y x (refl_equal x) = 
-                          eq_rec x P y' x (refl_equal x) =>
-                  z) e e0) in *; apply B.
-    + now destruct n.
-  - now rewrite H0.
-Qed.

theories/ordinals/Ackermann/model.v

@@ -658,7 +658,7 @@ Proof.
            simpl in H0.
            rewrite H2 in H0.
            apply (Hreca (n0 (interpTerm value a0)) b0).
-           ++ apply (inj_right_pair2 _ eq_nat_dec _ _ _ _ H3).
+           ++ apply (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H3).
            ++ auto.
     + simpl in |- *.
       intros H0; apply H0.
@@ -713,7 +713,7 @@ Proof.
            inversion H.
            simpl; rewrite H1.
            apply Hreca.
-           apply (inj_right_pair2 _ eq_nat_dec _ _ _ _ H2).
+           apply (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H2).
   - auto.
 Qed.