aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-09-14 21:16:12 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-09-14 21:16:12 -0400
commitb98ec63895887435aa6f08436715200d33a62d98 (patch)
treec605dc8fe8656a628e5fa4edf097d972f7fbfd62 /src/Util
parenta3a077040a311f32199c86700a463a5cf661b76a (diff)
Add PrimitiveSigma
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/Equality.v7
-rw-r--r--src/Util/PrimitiveSigma.v226
2 files changed, 233 insertions, 0 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 04335dbd4..d1a711821 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -8,6 +8,13 @@ Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.Isomorphism.
Require Import Crypto.Util.HProp.
+Import EqNotations.
+
+Definition f_equal_dep {A B} (f : forall a : A, B a) (x y : A) (H : x = y) : rew [B] H in f x = f y
+ := match H with
+ | eq_refl => eq_refl
+ end.
+
(** Most of the structure of proofs of equalities fits into what
mathematicians call a weak ∞-groupoid. (In fact, one way of
*defining* a weak ∞-groupoid is via what's called the J-rule,
diff --git a/src/Util/PrimitiveSigma.v b/src/Util/PrimitiveSigma.v
new file mode 100644
index 000000000..3551b479a
--- /dev/null
+++ b/src/Util/PrimitiveSigma.v
@@ -0,0 +1,226 @@
+(** * Definition and classification of the [Σ] Type, with primitive projections *)
+(** In this file, we classify the basic structure of Σ types ([sigT]
+ in Coq). In particular, we classify equalities of dependent pairs
+ (inhabitants of Σ types), so that when we have an equality between
+ two such pairs, or when we want such an equality, we have a
+ systematic way of reducing such equalities to equalities at
+ simpler types. *)
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.IffT.
+Require Import Crypto.Util.Equality.
+Require Import Crypto.Util.GlobalSettings.
+
+Local Set Primitive Projections.
+
+Delimit Scope primproj_type_scope with primproj_type.
+Delimit Scope primproj_scope with primproj.
+
+Import EqNotations.
+Module Import Primitive.
+ Record sigT {A} P := existT { projT1 : A ; projT2 : P projT1 }.
+ Global Arguments existT {_} _ _ _.
+ Global Arguments projT1 {_ _} _.
+ Global Arguments projT2 {_ _} _.
+
+ Module Import Notations.
+ Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.
+ Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
+ Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope.
+ Add Printing Let sigT.
+ End Notations.
+
+ Add Printing Let sigT.
+
+ Local Set Implicit Arguments.
+
+ Definition sigT_beq A P (eq_A : A -> A -> bool) (eq_P : forall a a', P a -> P a' -> bool) (X Y : @sigT A P) : bool
+ := let (a, b) := X in let (a', b') := Y in (eq_A a a' && eq_P _ _ b b')%bool.
+ Global Arguments sigT_beq / .
+ Lemma sigT_dec_bl A P eq_A eq_P
+ (A_bl : forall x y : A, eq_A x y = true -> x = y)
+ (P_bl : forall a a' x y (pf : eq_A a a' = true), eq_P a a' x y = true -> rew [P] (A_bl _ _ pf) in x = y)
+ (x y : @sigT A P)
+ : sigT_beq eq_A eq_P x y = true -> x = y.
+ Proof.
+ destruct x as [a b], y as [a' b'].
+ specialize (P_bl a a' b b'); cbn.
+ generalize dependent (A_bl a a'); clear A_bl; intros A_bl P_bl H.
+ edestruct eq_A; cbn in *;
+ destruct (eq_A a a');
+ first [ specialize (P_bl eq_refl); generalize dependent (A_bl eq_refl)
+ | specialize (P_bl H); generalize dependent (A_bl H) ];
+ clear A_bl; intros A_bl P_bl; try specialize (P_bl H); subst;
+ cbn [eq_rect] in *;
+ try reflexivity.
+ all: edestruct eq_P; first [ specialize (P_bl eq_refl) | specialize (P_bl H) ]; subst;
+ reflexivity.
+ Defined.
+ Lemma sigT_dec_bl_nd A P eq_A eq_P
+ (A_bl : forall x y : A, eq_A x y = true -> x = y)
+ (P_bl : forall a a' x y (pf : a = a'), rew [P] pf in x = y)
+ (x y : @sigT A P)
+ : sigT_beq eq_A eq_P x y = true -> x = y.
+ Proof.
+ apply (@sigT_dec_bl A P eq_A eq_P A_bl); intros; apply P_bl.
+ Defined.
+
+ Lemma sigT_dec_lb A P eq_A (eq_P : forall a a', P a -> P a' -> bool)
+ (A_lb : forall x y : A, x = y -> eq_A x y = true)
+ (P_lb : forall a (x y : P a), x = y -> eq_P a a x y = true)
+ (x y : @sigT A P)
+ : x = y -> sigT_beq eq_A eq_P x y = true.
+ Proof.
+ intro; subst y; specialize (A_lb _ _ (eq_refl (projT1 x))); specialize (P_lb _ _ _ (eq_refl (projT2 x))); cbn in *.
+ edestruct eq_A, eq_P; (reflexivity + assumption).
+ Defined.
+ Definition sigT_eq_dec A P eq_A eq_P
+ (A_bl : forall x y : A, eq_A x y = true -> x = y)
+ (P_bl : forall a a' x y (pf : eq_A a a' = true), eq_P a a' x y = true -> rew [P] (A_bl _ _ pf) in x = y)
+ (A_lb : forall x y : A, x = y -> eq_A x y = true)
+ (P_lb : forall a (x y : P a), x = y -> eq_P a a x y = true)
+ (x y : @sigT A P)
+ : {x = y} + {x <> y}.
+ Proof.
+ refine (let H := let b := @sigT_beq A P eq_A eq_P x y in if b as b0 return ({b0 = true} + {b0 = false}) then left eq_refl else right eq_refl in
+ match H with
+ | left e => left (@sigT_dec_bl A P eq_A eq_P A_bl P_bl x y e)
+ | right H' => right (fun e => _ (@sigT_dec_lb A P eq_A eq_P A_lb P_lb x y e))
+ end).
+ congruence.
+ Defined.
+End Primitive.
+Notation "{ x & P }" := (sigT (fun x => P%primproj_type)) : primproj_type_scope.
+Notation "{ x : A & P }" := (sigT (A:=A%primproj_type) (fun x => P%primproj_type)) : primproj_type_scope.
+Notation "{ ' pat : A & P }" := (sigT (A:=A%primproj_type) (fun pat => P%primproj_type)) : primproj_type_scope.
+Add Printing Let sigT.
+
+Import Primitive.Notations.
+
+Local Arguments f_equal {_ _} _ {_ _} _.
+
+Definition projT1_existT {A B} (a:A) (b:B a) : projT1 (existT B a b) = a := eq_refl.
+Definition projT2_existT {A B} (a:A) (b:B a) : projT2 (existT B a b) = b := eq_refl.
+Create HintDb cancel_primsig discriminated. Hint Rewrite @projT1_existT @projT2_existT : cancel_primsig.
+
+(** ** Equality for [sigT] *)
+Section sigT.
+
+ (** *** Projecting an equality of a pair to equality of the first components *)
+ Definition pr1_path {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 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.
+
+ (** *** Equality of [sigT] is itself a [sigT] *)
+ 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.
+
+ (** *** Curried version of proving equality of sigma types *)
+ 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).
+
+ (** *** Equality of [sigT] when the property is an hProp *)
+ 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 _ _ _).
+
+ (** *** 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 path_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 path_sigT_uncurried ].
+ Defined.
+
+ (** *** Induction principle for [@eq (sigT _)] *)
+ Definition path_sigT_rect {A P} {u v : @sigT A P} (Q : u = v -> Type)
+ (f : forall p q, Q (path_sigT u v p q))
+ : forall p, Q p.
+ Proof. intro p; specialize (f (pr1_path p) (pr2_path p)); destruct p; exact f. Defined.
+ Definition path_sigT_rec {A P u v} (Q : u = v :> @sigT A P -> Set) := path_sigT_rect Q.
+ Definition path_sigT_ind {A P u v} (Q : u = v :> @sigT A P -> Prop) := path_sigT_rec Q.
+
+ (** *** Equivalence of equality of [sigT] involving hProps with equality of the first components *)
+ 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).
+
+ (** *** Non-dependent classification of equality of [sigT] *)
+ 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).
+
+ (** *** 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; reflexivity.
+ Defined.
+
+ (** *** η Principle for [sigT] *)
+ Definition sigT_eta {A P} (p : { a : A & P a })
+ : p = existT _ (projT1 p) (projT2 p)
+ := eq_refl.
+End sigT.
+
+(** ** Useful Tactics *)
+(** *** [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[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
+ end.
+Ltac induction_sigma_in_as_using H H0 H1 rect :=
+ induction H as [H0 H1] using (rect _ _ _ _);
+ simpl_proj_exist_in H0;
+ simpl_proj_exist_in H1.
+Ltac induction_sigma_in_using H rect :=
+ let H0 := fresh H in
+ let H1 := fresh H in
+ induction_sigma_in_as_using H H0 H1 rect.
+Ltac inversion_sigma_step :=
+ match goal with
+ | [ H : _ = existT _ _ _ |- _ ]
+ => induction_sigma_in_using H @path_sigT_rect
+ | [ H : existT _ _ _ = _ |- _ ]
+ => induction_sigma_in_using H @path_sigT_rect
+ end.
+Ltac inversion_sigma := repeat inversion_sigma_step.