From 1ec29dbccc9b2f9cbedf36d032fea1da147231d5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 4 Dec 2016 13:52:52 -0500 Subject: Add lemmas about equality of sigma types --- theories/Init/Logic.v | 39 +++++++++++++ theories/Init/Specif.v | 153 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 192 insertions(+) (limited to 'theories/Init') 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 *) -- cgit v1.2.3