Merge PR#385: Equality of sigma types

3 files changed, 580 insertions, 4 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 3eefe9a84..4db11ae77 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -313,8 +313,8 @@ Arguments eq_ind [A] x P _ y _.
 Arguments eq_rec [A] x P _ y _.
 Arguments eq_rect [A] x P _ y _.
 
-Hint Resolve I conj or_introl or_intror : core. 
-Hint Resolve eq_refl: core. 
+Hint Resolve I conj or_introl or_intror : core.
+Hint Resolve eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
 
 Section Logic_lemmas.
@@ -504,6 +504,11 @@ Proof.
   reflexivity.
 Defined.
 
+Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x).
+Proof.
+  reflexivity.
+Qed.
+
 Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e').
 Proof.
 destruct e'.
@@ -522,6 +527,19 @@ destruct e, e'.
 reflexivity.
 Defined.
 
+Lemma eq_trans_rew_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x),
+    rew (eq_trans e e') in k = rew e' in rew e in k.
+Proof.
+  destruct e, e'; reflexivity.
+Qed.
+
+Lemma rew_const : forall A P (x y:A) (e:x=y) (k:P),
+    rew [fun _ => P] e in k = k.
+Proof.
+  destruct e; reflexivity.
+Qed.
+
+
 (* Aliases *)
 
 Notation sym_eq := eq_sym (compat "8.3").
@@ -575,7 +593,7 @@ Proof.
     assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto).
     destruct H.
     assumption.
-Qed.   
+Qed.
 
 Lemma forall_exists_coincide_unique_domain :
   forall A (P:A->Prop),
@@ -587,7 +605,7 @@ Proof.
   exists x. split; [trivial|].
   destruct H with (Q:=fun x'=>x=x') as (_,Huniq).
   apply Huniq. exists x; auto.
-Qed.       
+Qed.
 
 (** * Being inhabited *)
 
@@ -631,3 +649,97 @@ Qed.
 
 Declare Left Step iff_stepl.
 Declare Right Step iff_trans.
+
+Local Notation "'rew' 'dependent' H 'in' H'"
+  := (match H with
+      | eq_refl => H'
+      end)
+       (at level 10, H' at level 10,
+        format "'[' 'rew'  'dependent'  '/    ' H  in  '/' H' ']'").
+
+(** Equality for [ex] *)
+Section ex.
+  Local Unset Implicit Arguments.
+  Definition eq_ex_uncurried {A : Type} (P : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+             (pq : exists p : u1 = v1, rew p in u2 = v2)
+  : ex_intro P u1 u2 = ex_intro P v1 v2.
+  Proof.
+    destruct pq as [p q].
+    destruct q; simpl in *.
+    destruct p; reflexivity.
+  Qed.
+
+  Definition eq_ex {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1)
+             (p : u1 = v1) (q : rew p in u2 = v2)
+  : ex_intro P u1 u2 = ex_intro P v1 v2
+    := eq_ex_uncurried P (ex_intro _ p q).
+
+  Definition eq_ex_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+             (u1 v1 : A) (u2 : P u1) (v2 : P v1)
+             (p : u1 = v1)
+    : ex_intro P u1 u2 = ex_intro P v1 v2
+    := eq_ex u1 v1 u2 v2 p (P_hprop _ _ _).
+
+  Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : exists p, Q x p) {y} (H : x = y)
+  : rew [fun a => exists p, Q a p] H in u
+    = match u with
+        | ex_intro _ u1 u2
+          => ex_intro
+               (Q y)
+               (rew H in u1)
+               (rew dependent H in u2)
+      end.
+  Proof.
+    destruct H, u; reflexivity.
+  Qed.
+End ex.
+
+(** Equality for [ex2] *)
+Section ex2.
+  Local Unset Implicit Arguments.
+
+  Definition eq_ex2_uncurried {A : Type} (P Q : A -> Prop) {u1 v1 : A}
+             {u2 : P u1} {v2 : P v1}
+             {u3 : Q u1} {v3 : Q v1}
+             (pq : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3)
+  : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3.
+  Proof.
+    destruct pq as [p q r].
+    destruct r, q, p; simpl in *.
+    reflexivity.
+  Qed.
+
+  Definition eq_ex2 {A : Type} {P Q : A -> Prop}
+             (u1 v1 : A)
+             (u2 : P u1) (v2 : P v1)
+             (u3 : Q u1) (v3 : Q v1)
+             (p : u1 = v1) (q : rew p in u2 = v2) (r : rew p in u3 = v3)
+  : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
+    := eq_ex2_uncurried P Q (ex_intro2 _ _ p q r).
+
+  Definition eq_ex2_hprop {A} {P Q : A -> Prop}
+             (P_hprop : forall (x : A) (p q : P x), p = q)
+             (Q_hprop : forall (x : A) (p q : Q x), p = q)
+             (u1 v1 : A) (u2 : P u1) (v2 : P v1) (u3 : Q u1) (v3 : Q v1)
+             (p : u1 = v1)
+    : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
+    := eq_ex2 u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _).
+
+  Lemma rew_ex2 {A x} {P : A -> Type}
+        (Q : forall a, P a -> Prop)
+        (R : forall a, P a -> Prop)
+        (u : exists2 p, Q x p & R x p) {y} (H : x = y)
+  : rew [fun a => exists2 p, Q a p & R a p] H in u
+    = match u with
+        | ex_intro2 _ _ u1 u2 u3
+          => ex_intro2
+               (Q y)
+               (R y)
+               (rew H in u1)
+               (rew dependent H in u2)
+               (rew dependent H in u3)
+      end.
+  Proof.
+    destruct H, u; reflexivity.
+  Qed.
+End ex2.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 43a441fc5..95734991d 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -218,6 +218,407 @@ Proof.
   intros [[x y]];exists x;exact y.
 Qed.
 
+(** Equality of sigma types *)
+Import EqNotations.
+Local Notation "'rew' 'dependent' H 'in' H'"
+  := (match H with
+      | eq_refl => H'
+      end)
+       (at level 10, H' at level 10,
+        format "'[' 'rew'  'dependent'  '/    ' H  in  '/' H' ']'").
+
+(** Equality for [sigT] *)
+Section sigT.
+  Local Unset Implicit Arguments.
+  (** Projecting an equality of a pair to equality of the first components *)
+  Definition projT1_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v)
+    : projT1 u = projT1 v
+    := f_equal (@projT1 _ _) p.
+
+  (** Projecting an equality of a pair to equality of the second components *)
+  Definition projT2_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v)
+    : rew projT1_eq p in projT2 u = projT2 v
+    := rew dependent p in eq_refl.
+
+  (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *)
+  Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+             (pq : { p : u1 = v1 & rew p in u2 = v2 })
+    : existT _ u1 u2 = existT _ v1 v2.
+  Proof.
+    destruct pq as [p q].
+    destruct q; simpl in *.
+    destruct p; reflexivity.
+  Defined.
+
+  (** Equality of [sigT] is itself a [sigT] (backwards-reasoning version) *)
+  Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a })
+             (pq : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v })
+    : u = v.
+  Proof.
+    destruct u as [u1 u2], v as [v1 v2]; simpl in *.
+    apply eq_existT_uncurried; exact pq.
+  Defined.
+
+  (** Curried version of proving equality of sigma types *)
+  Definition eq_sigT {A : Type} {P : A -> Type} (u v : { a : A & P a })
+             (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v)
+    : u = v
+    := eq_sigT_uncurried u v (existT _ p q).
+
+  (** Equality of [sigT] when the property is an hProp *)
+  Definition eq_sigT_hprop {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
+             (u v : { a : A & P a })
+             (p : projT1 u = projT1 v)
+    : u = v
+    := eq_sigT u v p (P_hprop _ _ _).
+
+  (** Equivalence of equality of [sigT] with a [sigT] of equality *)
+  (** We could actually prove an isomorphism here, and not just [<->],
+      but for simplicity, we don't. *)
+  Definition eq_sigT_uncurried_iff {A P}
+             (u v : { a : A & P a })
+    : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }.
+  Proof.
+    split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ].
+  Defined.
+
+  (** Induction principle for [@eq (sigT _)] *)
+  Definition eq_sigT_rect {A P} {u v : { a : A & P a }} (Q : u = v -> Type)
+             (f : forall p q, Q (eq_sigT u v p q))
+    : forall p, Q p.
+  Proof. intro p; specialize (f (projT1_eq p) (projT2_eq p)); destruct u, p; exact f. Defined.
+  Definition eq_sigT_rec {A P u v} (Q : u = v :> { a : A & P a } -> Set) := eq_sigT_rect Q.
+  Definition eq_sigT_ind {A P u v} (Q : u = v :> { a : A & P a } -> Prop) := eq_sigT_rec Q.
+
+  (** Equivalence of equality of [sigT] involving hProps with equality of the first components *)
+  Definition eq_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
+             (u v : { a : A & P a })
+    : u = v <-> (projT1 u = projT1 v)
+    := conj (fun p => f_equal (@projT1 _ _) p) (eq_sigT_hprop P_hprop u v).
+
+  (** Non-dependent classification of equality of [sigT] *)
+  Definition eq_sigT_nondep {A B : Type} (u v : { a : A & B })
+             (p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
+    : u = v
+    := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q).
+
+  (** Classification of transporting across an equality of [sigT]s *)
+  Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x & Q x p }) {y} (H : x = y)
+    : rew [fun a => { p : P a & Q a p }] H in u
+      = existT
+          (Q y)
+          (rew H in projT1 u)
+          (rew dependent H in (projT2 u)).
+  Proof.
+    destruct H, u; reflexivity.
+  Defined.
+End sigT.
+
+(** Equality for [sig] *)
+Section sig.
+  Local Unset Implicit Arguments.
+  (** Projecting an equality of a pair to equality of the first components *)
+  Definition proj1_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v)
+    : proj1_sig u = proj1_sig v
+    := f_equal (@proj1_sig _ _) p.
+
+  (** Projecting an equality of a pair to equality of the second components *)
+  Definition proj2_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v)
+    : rew proj1_sig_eq p in proj2_sig u = proj2_sig v
+    := rew dependent p in eq_refl.
+
+  (** Equality of [sig] is itself a [sig] (forwards-reasoning version) *)
+  Definition eq_exist_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+             (pq : { p : u1 = v1 | rew p in u2 = v2 })
+    : exist _ u1 u2 = exist _ v1 v2.
+  Proof.
+    destruct pq as [p q].
+    destruct q; simpl in *.
+    destruct p; reflexivity.
+  Defined.
+
+  (** Equality of [sig] is itself a [sig] (backwards-reasoning version) *)
+  Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : { a : A | P a })
+             (pq : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v })
+    : u = v.
+  Proof.
+    destruct u as [u1 u2], v as [v1 v2]; simpl in *.
+    apply eq_exist_uncurried; exact pq.
+  Defined.
+
+  (** Curried version of proving equality of sigma types *)
+  Definition eq_sig {A : Type} {P : A -> Prop} (u v : { a : A | P a })
+             (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v)
+    : u = v
+    := eq_sig_uncurried u v (exist _ p q).
+
+  (** Induction principle for [@eq (sig _)] *)
+  Definition eq_sig_rect {A P} {u v : { a : A | P a }} (Q : u = v -> Type)
+             (f : forall p q, Q (eq_sig u v p q))
+    : forall p, Q p.
+  Proof. intro p; specialize (f (proj1_sig_eq p) (proj2_sig_eq p)); destruct u, p; exact f. Defined.
+  Definition eq_sig_rec {A P u v} (Q : u = v :> { a : A | P a } -> Set) := eq_sig_rect Q.
+  Definition eq_sig_ind {A P u v} (Q : u = v :> { a : A | P a } -> Prop) := eq_sig_rec Q.
+
+  (** Equality of [sig] when the property is an hProp *)
+  Definition eq_sig_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+             (u v : { a : A | P a })
+             (p : proj1_sig u = proj1_sig v)
+    : u = v
+    := eq_sig u v p (P_hprop _ _ _).
+
+  (** Equivalence of equality of [sig] with a [sig] of equality *)
+  (** We could actually prove an isomorphism here, and not just [<->],
+      but for simplicity, we don't. *)
+  Definition eq_sig_uncurried_iff {A} {P : A -> Prop}
+             (u v : { a : A | P a })
+    : u = v <-> { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }.
+  Proof.
+    split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig_uncurried ].
+  Defined.
+
+  (** Equivalence of equality of [sig] involving hProps with equality of the first components *)
+  Definition eq_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+             (u v : { a : A | P a })
+    : u = v <-> (proj1_sig u = proj1_sig v)
+    := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v).
+
+  Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x | Q x p }) {y} (H : x = y)
+    : rew [fun a => { p : P a | Q a p }] H in u
+      = exist
+          (Q y)
+          (rew H in proj1_sig u)
+          (rew dependent H in proj2_sig u).
+  Proof.
+    destruct H, u; reflexivity.
+  Defined.
+End sig.
+
+(** Equality for [sigT] *)
+Section sigT2.
+  (* We make [sigT_of_sigT2] a coercion so we can use [projT1], [projT2] on [sigT2] *)
+  Local Coercion sigT_of_sigT2 : sigT2 >-> sigT.
+  Local Unset Implicit Arguments.
+  (** Projecting an equality of a pair to equality of the first components *)
+  Definition sigT_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+    : u = v :> { a : A & P a }
+    := f_equal _ p.
+  Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+    : projT1 u = projT1 v
+    := projT1_eq (sigT_of_sigT2_eq p).
+
+  (** Projecting an equality of a pair to equality of the second components *)
+  Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+    : rew projT1_of_sigT2_eq p in projT2 u = projT2 v
+    := rew dependent p in eq_refl.
+
+  (** Projecting an equality of a pair to equality of the third components *)
+  Definition projT3_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+    : rew projT1_of_sigT2_eq p in projT3 u = projT3 v
+    := rew dependent p in eq_refl.
+
+  (** Equality of [sigT2] is itself a [sigT2] (forwards-reasoning version) *)
+  Definition eq_existT2_uncurried {A : Type} {P Q : A -> Type}
+             {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
+             (pqr : { p : u1 = v1
+                    & rew p in u2 = v2 & rew p in u3 = v3 })
+    : existT2 _ _ u1 u2 u3 = existT2 _ _ v1 v2 v3.
+  Proof.
+    destruct pqr as [p q r].
+    destruct r, q, p; simpl.
+    reflexivity.
+  Defined.
+
+  (** Equality of [sigT2] is itself a [sigT2] (backwards-reasoning version) *)
+  Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a })
+             (pqr : { p : projT1 u = projT1 v
+                    & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v })
+    : u = v.
+  Proof.
+    destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *.
+    apply eq_existT2_uncurried; exact pqr.
+  Defined.
+
+  (** Curried version of proving equality of sigma types *)
+  Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a })
+             (p : projT1 u = projT1 v)
+             (q : rew p in projT2 u = projT2 v)
+             (r : rew p in projT3 u = projT3 v)
+    : u = v
+    := eq_sigT2_uncurried u v (existT2 _ _ p q r).
+
+  (** Equality of [sigT2] when the second property is an hProp *)
+  Definition eq_sigT2_hprop {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+             (u v : { a : A & P a & Q a })
+             (p : u = v :> { a : A & P a })
+    : u = v
+    := eq_sigT2 u v (projT1_eq p) (projT2_eq p) (Q_hprop _ _ _).
+
+  (** Equivalence of equality of [sigT2] with a [sigT2] of equality *)
+  (** We could actually prove an isomorphism here, and not just [<->],
+      but for simplicity, we don't. *)
+  Definition eq_sigT2_uncurried_iff {A P Q}
+             (u v : { a : A & P a & Q a })
+    : u = v
+      <-> { p : projT1 u = projT1 v
+          & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }.
+  Proof.
+    split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT2_uncurried ].
+  Defined.
+
+  (** Induction principle for [@eq (sigT2 _ _)] *)
+  Definition eq_sigT2_rect {A P Q} {u v : { a : A & P a & Q a }} (R : u = v -> Type)
+             (f : forall p q r, R (eq_sigT2 u v p q r))
+    : forall p, R p.
+  Proof.
+    intro p.
+    specialize (f (projT1_of_sigT2_eq p) (projT2_of_sigT2_eq p) (projT3_eq p)).
+    destruct u, p; exact f.
+  Defined.
+  Definition eq_sigT2_rec {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Set) := eq_sigT2_rect R.
+  Definition eq_sigT2_ind {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Prop) := eq_sigT2_rec R.
+
+  (** Equivalence of equality of [sigT2] involving hProps with equality of the first components *)
+  Definition eq_sigT2_hprop_iff {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+             (u v : { a : A & P a & Q a })
+    : u = v <-> (u = v :> { a : A & P a })
+    := conj (fun p => f_equal (@sigT_of_sigT2 _ _ _) p) (eq_sigT2_hprop Q_hprop u v).
+
+  (** Non-dependent classification of equality of [sigT] *)
+  Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C })
+             (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v)
+    : u = v
+    := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
+
+  (** Classification of transporting across an equality of [sigT2]s *)
+  Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
+        (u : { p : P x & Q x p & R x p })
+        {y} (H : x = y)
+    : rew [fun a => { p : P a & Q a p & R a p }] H in u
+      = existT2
+          (Q y)
+          (R y)
+          (rew H in projT1 u)
+          (rew dependent H in projT2 u)
+          (rew dependent H in projT3 u).
+  Proof.
+    destruct H, u; reflexivity.
+  Defined.
+End sigT2.
+
+(** Equality for [sig2] *)
+Section sig2.
+  (* We make [sig_of_sig2] a coercion so we can use [proj1], [proj2] on [sig2] *)
+  Local Coercion sig_of_sig2 : sig2 >-> sig.
+  Local Unset Implicit Arguments.
+  (** Projecting an equality of a pair to equality of the first components *)
+  Definition sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+    : u = v :> { a : A | P a }
+    := f_equal _ p.
+  Definition proj1_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+    : proj1_sig u = proj1_sig v
+    := proj1_sig_eq (sig_of_sig2_eq p).
+
+  (** Projecting an equality of a pair to equality of the second components *)
+  Definition proj2_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+    : rew proj1_sig_of_sig2_eq p in proj2_sig u = proj2_sig v
+    := rew dependent p in eq_refl.
+
+  (** Projecting an equality of a pair to equality of the third components *)
+  Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+    : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v
+    := rew dependent p in eq_refl.
+
+  (** Equality of [sig2] is itself a [sig2] (fowards-reasoning version) *)
+  Definition eq_exist2_uncurried {A} {P Q : A -> Prop}
+             {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
+             (pqr : { p : u1 = v1
+                    | rew p in u2 = v2 & rew p in u3 = v3 })
+    : exist2 _ _ u1 u2 u3 = exist2 _ _ v1 v2 v3.
+  Proof.
+    destruct pqr as [p q r].
+    destruct r, q, p; simpl.
+    reflexivity.
+  Defined.
+
+  (** Equality of [sig2] is itself a [sig2] (backwards-reasoning version) *)
+  Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a })
+             (pqr : { p : proj1_sig u = proj1_sig v
+                    | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v })
+    : u = v.
+  Proof.
+    destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *.
+    apply eq_exist2_uncurried; exact pqr.
+  Defined.
+
+  (** Curried version of proving equality of sigma types *)
+  Definition eq_sig2 {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a })
+             (p : proj1_sig u = proj1_sig v)
+             (q : rew p in proj2_sig u = proj2_sig v)
+             (r : rew p in proj3_sig u = proj3_sig v)
+    : u = v
+    := eq_sig2_uncurried u v (exist2 _ _ p q r).
+
+  (** Equality of [sig2] when the second property is an hProp *)
+  Definition eq_sig2_hprop {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+             (u v : { a : A | P a & Q a })
+             (p : u = v :> { a : A | P a })
+    : u = v
+    := eq_sig2 u v (proj1_sig_eq p) (proj2_sig_eq p) (Q_hprop _ _ _).
+
+  (** Equivalence of equality of [sig2] with a [sig2] of equality *)
+  (** We could actually prove an isomorphism here, and not just [<->],
+      but for simplicity, we don't. *)
+  Definition eq_sig2_uncurried_iff {A P Q}
+             (u v : { a : A | P a & Q a })
+    : u = v
+      <-> { p : proj1_sig u = proj1_sig v
+          | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }.
+  Proof.
+    split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig2_uncurried ].
+  Defined.
+
+  (** Induction principle for [@eq (sig2 _ _)] *)
+  Definition eq_sig2_rect {A P Q} {u v : { a : A | P a & Q a }} (R : u = v -> Type)
+             (f : forall p q r, R (eq_sig2 u v p q r))
+    : forall p, R p.
+  Proof.
+    intro p.
+    specialize (f (proj1_sig_of_sig2_eq p) (proj2_sig_of_sig2_eq p) (proj3_sig_eq p)).
+    destruct u, p; exact f.
+  Defined.
+  Definition eq_sig2_rec {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Set) := eq_sig2_rect R.
+  Definition eq_sig2_ind {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Prop) := eq_sig2_rec R.
+
+  (** Equivalence of equality of [sig2] involving hProps with equality of the first components *)
+  Definition eq_sig2_hprop_iff {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+             (u v : { a : A | P a & Q a })
+    : u = v <-> (u = v :> { a : A | P a })
+    := conj (fun p => f_equal (@sig_of_sig2 _ _ _) p) (eq_sig2_hprop Q_hprop u v).
+
+  (** Non-dependent classification of equality of [sig] *)
+  Definition eq_sig2_nondep {A} {B C : Prop} (u v : @sig2 A (fun _ => B) (fun _ => C))
+             (p : proj1_sig u = proj1_sig v) (q : proj2_sig u = proj2_sig v) (r : proj3_sig u = proj3_sig v)
+    : u = v
+    := @eq_sig2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
+
+  (** Classification of transporting across an equality of [sig2]s *)
+  Lemma rew_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
+        (u : { p : P x | Q x p & R x p })
+        {y} (H : x = y)
+    : rew [fun a => { p : P a | Q a p & R a p }] H in u
+      = exist2
+          (Q y)
+          (R y)
+          (rew H in proj1_sig u)
+          (rew dependent H in proj2_sig u)
+          (rew dependent H in proj3_sig u).
+  Proof.
+    destruct H, u; reflexivity.
+  Defined.
+End sig2.
+
+
 (** [sumbool] is a boolean type equipped with the justification of
     their value *)
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 7a846cd1b..aab385ef7 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -243,3 +243,66 @@ with the actual [dependent induction] tactic. *)
 
 Tactic Notation "dependent" "induction" ident(H) :=
   fail "To use dependent induction, first [Require Import Coq.Program.Equality.]".
+
+(** *** [inversion_sigma] *)
+(** The built-in [inversion] will frequently leave equalities of
+    dependent pairs.  When the first type in the pair is an hProp or
+    otherwise simplifies, [inversion_sigma] is useful; it will replace
+    the equality of pairs with a pair of equalities, one involving a
+    term casted along the other.  This might also prove useful for
+    writing a version of [inversion] / [dependent destruction] which
+    does not lose information, i.e., does not turn a goal which is
+    provable into one which requires axiom K / UIP.  *)
+Ltac simpl_proj_exist_in H :=
+  repeat match type of H with
+         | context G[proj1_sig (exist _ ?x ?p)]
+           => let G' := context G[x] in change G' in H
+         | context G[proj2_sig (exist _ ?x ?p)]
+           => let G' := context G[p] in change G' in H
+         | context G[projT1 (existT _ ?x ?p)]
+           => let G' := context G[x] in change G' in H
+         | context G[projT2 (existT _ ?x ?p)]
+           => let G' := context G[p] in change G' in H
+         | context G[proj3_sig (exist2 _ _ ?x ?p ?q)]
+           => let G' := context G[q] in change G' in H
+         | context G[projT3 (existT2 _ _ ?x ?p ?q)]
+           => let G' := context G[q] in change G' in H
+         | context G[sig_of_sig2 (@exist2 ?A ?P ?Q ?x ?p ?q)]
+           => let G' := context G[@exist A P x p] in change G' in H
+         | context G[sigT_of_sigT2 (@existT2 ?A ?P ?Q ?x ?p ?q)]
+           => let G' := context G[@existT A P x p] in change G' in H
+         end.
+Ltac induction_sigma_in_using H rect :=
+  let H0 := fresh H in
+  let H1 := fresh H in
+  induction H as [H0 H1] using (rect _ _ _ _);
+  simpl_proj_exist_in H0;
+  simpl_proj_exist_in H1.
+Ltac induction_sigma2_in_using H rect :=
+  let H0 := fresh H in
+  let H1 := fresh H in
+  let H2 := fresh H in
+  induction H as [H0 H1 H2] using (rect _ _ _ _ _);
+  simpl_proj_exist_in H0;
+  simpl_proj_exist_in H1;
+  simpl_proj_exist_in H2.
+Ltac inversion_sigma_step :=
+  match goal with
+  | [ H : _ = exist _ _ _ |- _ ]
+    => induction_sigma_in_using H @eq_sig_rect
+  | [ H : _ = existT _ _ _ |- _ ]
+    => induction_sigma_in_using H @eq_sigT_rect
+  | [ H : exist _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sig_rect
+  | [ H : existT _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sigT_rect
+  | [ H : _ = exist2 _ _ _ _ _ |- _ ]
+    => induction_sigma2_in_using H @eq_sig2_rect
+  | [ H : _ = existT2 _ _ _ _ _ |- _ ]
+    => induction_sigma2_in_using H @eq_sigT2_rect
+  | [ H : exist2 _ _ _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sig2_rect
+  | [ H : existT2 _ _ _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sigT2_rect
+  end.
+Ltac inversion_sigma := repeat inversion_sigma_step.