From 11d0b7ad0da0b7aeb37411059150a2baf0bf68fc Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Fri, 29 Jul 2016 10:57:47 -0700
Subject: Add some lemmas to Util.Sigma

---
 src/Util/Sigma.v | 38 ++++++++++++++++++++++++++++++++++++--
 1 file changed, 36 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v
index 9b1ff2c96..901b2f915 100644
--- a/src/Util/Sigma.v
+++ b/src/Util/Sigma.v
@@ -1,6 +1,12 @@
 Require Import Crypto.Util.Equality.
 Require Import Crypto.Util.GlobalSettings.
 
+Local Arguments projT1 {_ _} _.
+Local Arguments projT2 {_ _} _.
+Local Arguments proj1_sig {_ _} _.
+Local Arguments proj1_sig {_ _} _.
+Local Arguments f_equal {_ _} _ {_ _} _.
+
 Section sigT.
   Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
   : projT1 u = projT1 v
@@ -27,6 +33,17 @@ Section sigT.
   : u = v
     := path_sigT_uncurried u v (existT _ p q).
 
+  Definition path_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
+    := path_sigT u v p (P_hprop _ _ _).
+
+  Definition path_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 (f_equal projT1) (path_sigT_hprop P_hprop u v).
+
   Definition path_sigT_nondep {A B : Type} (u v : @sigT A (fun _ => B))
              (p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
   : u = v
@@ -66,11 +83,22 @@ Section sig.
     destruct p; reflexivity.
   Defined.
 
-  Definition path_sig {A : Type} (P : A -> Prop) (u v : sig P)
+  Definition path_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
     := path_sig_uncurried u v (exist _ p q).
 
+  Definition path_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
+    := path_sig u v p (P_hprop _ _ _).
+
+  Definition path_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 (f_equal proj1_sig) (path_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
@@ -94,11 +122,17 @@ Section ex.
     destruct p; reflexivity.
   Defined.
 
-  Definition path_ex' {A : Type} (P : A -> Prop) (u1 v1 : A) (u2 : P u1) (v2 : P v1)
+  Definition path_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
     := path_ex_uncurried' P (ex_intro _ p q).
 
+  Definition path_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
+    := path_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
-- 
cgit v1.2.3