From 0b0728b5a447d6f7ff5fdf80c87d66ac714c3151 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Fri, 29 Jul 2016 10:46:55 -0700
Subject: Set Asymmetric Patterns, add util lemmas about sig

---
 src/Util/Sigma.v | 116 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 116 insertions(+)
 create mode 100644 src/Util/Sigma.v

(limited to 'src/Util/Sigma.v')

diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v
new file mode 100644
index 000000000..9b1ff2c96
--- /dev/null
+++ b/src/Util/Sigma.v
@@ -0,0 +1,116 @@
+Require Import Crypto.Util.Equality.
+Require Import Crypto.Util.GlobalSettings.
+
+Section sigT.
+  Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
+  : projT1 u = projT1 v
+    := f_equal (@projT1 _ _) p.
+
+  Definition pr2_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
+  : eq_rect _ _ (projT2 u) _ (pr1_path p) = projT2 v.
+  Proof.
+    destruct p; reflexivity.
+  Defined.
+
+  Definition path_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.
+
+  Definition path_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
+    := path_sigT_uncurried u v (existT _ p q).
+
+  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
+    := @path_sigT _ _ u v p (eq_trans (transport_const _ _) q).
+
+  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.
+
+Section sig.
+  Definition proj1_sig_path {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_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+  : eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v.
+  Proof.
+    destruct p; reflexivity.
+  Defined.
+
+  Definition path_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 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).
+
+  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.
+
+Section ex.
+  Definition path_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 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).
+
+  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.
-- 
cgit v1.2.3