Add lemmas about equality of sigma types

2 files changed, 192 insertions, 0 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index d6076f86d..968922737 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -649,3 +649,42 @@ Qed.
 
 Declare Left Step iff_stepl.
 Declare Right Step iff_trans.
+
+(** 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, eq_rect _ _ u2 _ p = v2)
+  : ex_intro P u1 u2 = ex_intro P v1 v2.
+  Proof.
+    destruct pq as [p q].
+    destruct q; simpl in *.
+    destruct p; reflexivity.
+  Defined.
+
+  Definition eq_ex' {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1)
+             (p : u1 = v1) (q : eq_rect _ _ u2 _ p = 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 eq_rect_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y)
+  : eq_rect x (fun a => ex (Q a)) u y H
+    = match u with
+        | ex_intro _ u1 u2
+          => ex_intro
+               (Q y)
+               (eq_rect x P u1 y H)
+               match H in (_ = y) return Q y (eq_rect x P u1 y H) with
+                 | eq_refl => u2
+               end
+      end.
+  Proof.
+    destruct H, u; reflexivity.
+  Defined.
+End ex.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 43a441fc5..b6f92358b 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -218,6 +218,159 @@ Proof.
   intros [[x y]];exists x;exact y.
 Qed.
 
+(** Equality of sigma types *)
+
+(** 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 : sigT P} (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 : sigT P} (p : u = v)
+  : eq_rect _ _ (projT2 u) _ (projT1_eq p) = projT2 v.
+  Proof.
+    destruct p; reflexivity.
+  Defined.
+
+  (** Equality of [sigT] is itself a [sigT] *)
+  Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : sigT P)
+             (pq : sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = projT2 v))
+  : u = v.
+  Proof.
+    destruct u as [u1 u2], v as [v1 v2]; simpl in *.
+    destruct pq as [p q].
+    destruct q; simpl in *.
+    destruct p; reflexivity.
+  Defined.
+
+  (** Curried version of proving equality of sigma types *)
+  Definition eq_sigT {A : Type} {P : A -> Type} (u v : sigT P)
+             (p : projT1 u = projT1 v) (q : eq_rect _ _ (projT2 u) _ p = 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 : @sigT A P)
+             (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 use [IsIso] here, but for simplicity, we
+      don't.  If we wanted to deal with proofs of equality of Σ types
+      in dependent positions, we'd need it. *)
+  Definition eq_sigT_uncurried_iff {A P}
+             (u v : @sigT A P)
+    : u = v <-> (sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = 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 : @sigT A P} (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 :> @sigT A P -> Set) := eq_sigT_rect Q.
+  Definition eq_sigT_ind {A P u v} (Q : u = v :> @sigT A P -> 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 : @sigT A P)
+    : 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 : @sigT A (fun _ => B))
+             (p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
+  : u = v
+    := @eq_sigT _ _ u v p (eq_trans (eq_rect_const _ _) q).
+
+  (** Classification of transporting across an equality of [sigT]s *)
+  Lemma eq_rect_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sigT (Q x)) {y} (H : x = y)
+  : eq_rect x (fun a => sigT (Q a)) u y H
+    = existT
+        (Q y)
+        (eq_rect x P (projT1 u) y H)
+        match H in (_ = y) return Q y (eq_rect x P (projT1 u) y H) with
+          | eq_refl => projT2 u
+        end.
+  Proof.
+    destruct H, u; reflexivity.
+  Defined.
+End sigT.
+
+(** Equality for [sig] *)
+Section sig.
+  Local Unset Implicit Arguments.
+  Definition proj1_sig_eq {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+  : proj1_sig u = proj1_sig v
+    := f_equal (@proj1_sig _ _) p.
+
+  Definition proj2_sig_eq {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+  : eq_rect _ _ (proj2_sig u) _ (proj1_sig_eq p) = proj2_sig v.
+  Proof.
+    destruct p; reflexivity.
+  Defined.
+
+  Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : sig P)
+             (pq : {p : proj1_sig u = proj1_sig v | eq_rect _ _ (proj2_sig u) _ p = proj2_sig v})
+  : u = v.
+  Proof.
+    destruct u as [u1 u2], v as [v1 v2]; simpl in *.
+    destruct pq as [p q].
+    destruct q; simpl in *.
+    destruct p; reflexivity.
+  Defined.
+
+  Definition eq_sig {A : Type} {P : A -> Prop} (u v : sig P)
+             (p : proj1_sig u = proj1_sig v) (q : eq_rect _ _ (proj2_sig u) _ p = proj2_sig v)
+  : u = v
+    := eq_sig_uncurried u v (exist _ p q).
+
+  Definition eq_sig_rect {A P} {u v : @sig A P} (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 :> @sig A P -> Set) := eq_sig_rect Q.
+  Definition eq_sig_ind {A P u v} (Q : u = v :> @sig A P -> Prop) := eq_sig_rec Q.
+
+  Definition eq_sig_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+             (u v : @sig A P)
+             (p : proj1_sig u = proj1_sig v)
+    : u = v
+    := eq_sig u v p (P_hprop _ _ _).
+
+  Definition eq_sig_uncurried_iff {A} {P : A -> Prop}
+             (u v : @sig A P)
+    : u = v <-> (sig (fun p : proj1_sig u = proj1_sig v => eq_rect _ _ (proj2_sig u) _ p = proj2_sig v)).
+  Proof.
+    split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig_uncurried ].
+  Defined.
+
+  Definition eq_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+             (u v : @sig A P)
+    : u = v <-> (proj1_sig u = proj1_sig v)
+    := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v).
+
+  Lemma eq_rect_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sig (Q x)) {y} (H : x = y)
+  : eq_rect x (fun a => sig (Q a)) u y H
+    = exist
+        (Q y)
+        (eq_rect x P (proj1_sig u) y H)
+        match H in (_ = y) return Q y (eq_rect x P (proj1_sig u) y H) with
+          | eq_refl => proj2_sig u
+        end.
+  Proof.
+    destruct H, u; reflexivity.
+  Defined.
+End sig.
+
+
 (** [sumbool] is a boolean type equipped with the justification of
     their value *)