From 7043cedcd0b5d02f3dff51f403b9c0fa1a28892c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 4 Dec 2016 13:13:08 -0500 Subject: Add more groupoid-like theorems about [eq] --- theories/Init/Logic.v | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 3eefe9a84..437d802d8 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -313,8 +313,8 @@ Arguments eq_ind [A] x P _ y _. Arguments eq_rec [A] x P _ y _. Arguments eq_rect [A] x P _ y _. -Hint Resolve I conj or_introl or_intror : core. -Hint Resolve eq_refl: core. +Hint Resolve I conj or_introl or_intror : core. +Hint Resolve eq_refl: core. Hint Resolve ex_intro ex_intro2: core. Section Logic_lemmas. @@ -504,6 +504,11 @@ Proof. reflexivity. Defined. +Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x). +Proof. + reflexivity. +Defined. + Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e'). Proof. destruct e'. @@ -522,6 +527,19 @@ destruct e, e'. reflexivity. Defined. +Lemma eq_trans_eq_rect_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x), + eq_rect _ P k _ (eq_trans e e') = eq_rect _ P (eq_rect _ P k _ e) _ e'. +Proof. + destruct e, e'; reflexivity. +Defined. + +Lemma eq_rect_const : forall A P (x y:A) (e:x=y) (k:P), + eq_rect _ (fun _ : A => P) k _ e = k. +Proof. + destruct e; reflexivity. +Defined. + + (* Aliases *) Notation sym_eq := eq_sym (compat "8.3"). @@ -575,7 +593,7 @@ Proof. assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto). destruct H. assumption. -Qed. +Qed. Lemma forall_exists_coincide_unique_domain : forall A (P:A->Prop), @@ -587,7 +605,7 @@ Proof. exists x. split; [trivial|]. destruct H with (Q:=fun x'=>x=x') as (_,Huniq). apply Huniq. exists x; auto. -Qed. +Qed. (** * Being inhabited *) -- cgit v1.2.3 From 954a125f4470cf7d723cd78b003a4cf8c17ca3f6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Dec 2016 11:05:02 -0500 Subject: Use [rew] notations rather than [eq_rect] As per Hugo's request in https://github.com/coq/coq/pull/384#issuecomment-264891011 --- theories/Init/Logic.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 437d802d8..12ec9dd77 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -528,13 +528,13 @@ reflexivity. Defined. Lemma eq_trans_eq_rect_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x), - eq_rect _ P k _ (eq_trans e e') = eq_rect _ P (eq_rect _ P k _ e) _ e'. + rew (eq_trans e e') in k = rew e' in rew e in k. Proof. destruct e, e'; reflexivity. Defined. Lemma eq_rect_const : forall A P (x y:A) (e:x=y) (k:P), - eq_rect _ (fun _ : A => P) k _ e = k. + rew [fun _ => P] e in k = k. Proof. destruct e; reflexivity. Defined. -- cgit v1.2.3 From 1f705c9010a7a84d04ff393ac43d5af8e308dd81 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Feb 2017 20:42:52 -0500 Subject: Use [rew_] instead of [eq_rect_] prefix As per Hugo's request. --- theories/Init/Logic.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 12ec9dd77..d6076f86d 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -527,13 +527,13 @@ destruct e, e'. reflexivity. Defined. -Lemma eq_trans_eq_rect_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x), +Lemma eq_trans_rew_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x), rew (eq_trans e e') in k = rew e' in rew e in k. Proof. destruct e, e'; reflexivity. Defined. -Lemma eq_rect_const : forall A P (x y:A) (e:x=y) (k:P), +Lemma rew_const : forall A P (x y:A) (e:x=y) (k:P), rew [fun _ => P] e in k = k. Proof. destruct e; reflexivity. -- cgit v1.2.3 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 From 7cecf9a675145a4171bf8c8b6bb153caee93d503 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 4 Dec 2016 14:03:52 -0500 Subject: Add an [inversion_sigma] tactic This tactic does better than [inversion] at sigma types. --- test-suite/success/InversionSigma.v | 30 ++++++++++++++++++++++++++++ theories/Init/Tactics.v | 39 +++++++++++++++++++++++++++++++++++++ 2 files changed, 69 insertions(+) create mode 100644 test-suite/success/InversionSigma.v (limited to 'theories/Init') diff --git a/test-suite/success/InversionSigma.v b/test-suite/success/InversionSigma.v new file mode 100644 index 000000000..c19939eab --- /dev/null +++ b/test-suite/success/InversionSigma.v @@ -0,0 +1,30 @@ +Section inversion_sigma. + Local Unset Implicit Arguments. + Context A (B : A -> Prop) (C : forall a, B a -> Prop) + (D : forall a b, C a b -> Prop) (E : forall a b c, D a b c -> Prop). + + (* Require that, after destructing sigma types and inverting + equalities, we can subst equalities of variables only, and reduce + down to [eq_refl = eq_refl]. *) + Local Ltac test_inversion_sigma := + intros; + repeat match goal with + | [ H : sig _ |- _ ] => destruct H + | [ H : sigT _ |- _ ] => destruct H + end; simpl in *; + inversion_sigma; + repeat match goal with + | [ H : ?x = ?y |- _ ] => is_var x; is_var y; subst x; simpl in * + end; + match goal with + | [ |- eq_refl = eq_refl ] => reflexivity + end. + + Goal forall (x y : { a : A & { b : { b : B a & C a b } & { d : D a (projT1 b) (projT2 b) & E _ _ _ d } } }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. +End inversion_sigma. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 7a846cd1b..e01c07a99 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -243,3 +243,42 @@ with the actual [dependent induction] tactic. *) Tactic Notation "dependent" "induction" ident(H) := fail "To use dependent induction, first [Require Import Coq.Program.Equality.]". + +(** *** [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[proj1_sig (exist _ ?x ?p)] + => let G' := context G[x] in change G' in H + | context G[proj2_sig (exist _ ?x ?p)] + => let G' := context G[p] in change G' in H + | 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_using H rect := + let H0 := fresh H in + let H1 := fresh H in + induction H as [H0 H1] using (rect _ _ _ _); + simpl_proj_exist_in H0; + simpl_proj_exist_in H1. +Ltac inversion_sigma_step := + match goal with + | [ H : _ = exist _ _ _ |- _ ] + => induction_sigma_in_using H @eq_sig_rect + | [ H : _ = existT _ _ _ |- _ ] + => induction_sigma_in_using H @eq_sigT_rect + | [ H : exist _ _ _ = _ |- _ ] + => induction_sigma_in_using H @eq_sig_rect + | [ H : existT _ _ _ = _ |- _ ] + => induction_sigma_in_using H @eq_sigT_rect + end. +Ltac inversion_sigma := repeat inversion_sigma_step. -- cgit v1.2.3 From 94958a408aac22f35165fb3eb571f1c3310f060b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Dec 2016 11:13:15 -0500 Subject: Use [rew] notations rather than [eq_rect] As per Hugo's suggestion in https://github.com/coq/coq/pull/384#issuecomment-264891011 --- theories/Init/Logic.v | 10 +++++----- theories/Init/Specif.v | 29 +++++++++++++++-------------- 2 files changed, 20 insertions(+), 19 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 968922737..b855154ac 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -654,7 +654,7 @@ Declare Right Step iff_trans. 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) + (pq : exists p : u1 = v1, rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2. Proof. destruct pq as [p q]. @@ -663,7 +663,7 @@ Section ex. 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) + (p : u1 = v1) (q : rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2 := eq_ex_uncurried' P (ex_intro _ p q). @@ -674,13 +674,13 @@ Section ex. := 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 + : rew [fun a => ex (Q a)] H in u = 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 + (rew H in u1) + match H in (_ = y) return Q y (rew H in u1) with | eq_refl => u2 end end. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index b6f92358b..cdc918275 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -219,6 +219,7 @@ Proof. Qed. (** Equality of sigma types *) +Import EqNotations. (** Equality for [sigT] *) Section sigT. @@ -230,14 +231,14 @@ Section sigT. (** 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. + : rew projT1_eq p in projT2 u = 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)) + (pq : sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. @@ -248,7 +249,7 @@ Section sigT. (** 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) + (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v) : u = v := eq_sigT_uncurried u v (existT _ p q). @@ -265,7 +266,7 @@ Section sigT. 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)). + : u = v <-> (sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)). Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ]. Defined. @@ -292,11 +293,11 @@ Section sigT. (** 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 + : rew [fun a => sigT (Q a)] H in u = 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 + (rew H in projT1 u) + match H in (_ = y) return Q y (rew H in projT1 u) with | eq_refl => projT2 u end. Proof. @@ -312,13 +313,13 @@ Section sig. := 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. + : rew proj1_sig_eq p in proj2_sig u = 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}) + (pq : {p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v}) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. @@ -328,7 +329,7 @@ Section sig. 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) + (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) : u = v := eq_sig_uncurried u v (exist _ p q). @@ -347,7 +348,7 @@ Section sig. 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)). + : u = v <-> (sig (fun p : proj1_sig u = proj1_sig v => rew p in proj2_sig u = proj2_sig v)). Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig_uncurried ]. Defined. @@ -358,11 +359,11 @@ Section sig. := 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 + : rew [fun a => sig (Q a)] H in u = 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 + (rew H in proj1_sig u) + match H in (_ = y) return Q y (rew H in proj1_sig u) with | eq_refl => proj2_sig u end. Proof. -- cgit v1.2.3 From 592f607ad27c0c42d0a5185163dd06f7f5d5cc1e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Dec 2016 16:15:52 -0500 Subject: Add lemmas for ex2 --- theories/Init/Logic.v | 54 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index b855154ac..1f94f7586 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -688,3 +688,57 @@ Section ex. destruct H, u; reflexivity. Defined. End ex. + +(** Equality for [ex2] *) +Section ex2. + Local Unset Implicit Arguments. + + Definition eq_ex2_uncurried' {A : Type} (P Q : A -> Prop) {u1 v1 : A} + {u2 : P u1} {v2 : P v1} + {u3 : Q u1} {v3 : Q v1} + (pq : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3) + : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3. + Proof. + destruct pq as [p q r]. + destruct r, q, p; simpl in *. + reflexivity. + Defined. + + Definition eq_ex2' {A : Type} {P Q : A -> Prop} + (u1 v1 : A) + (u2 : P u1) (v2 : P v1) + (u3 : Q u1) (v3 : Q v1) + (p : u1 = v1) (q : rew p in u2 = v2) (r : rew p in u3 = v3) + : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3 + := eq_ex2_uncurried' P Q (ex_intro2 _ _ p q r). + + Definition eq_ex2'_hprop {A} {P Q : A -> Prop} + (P_hprop : forall (x : A) (p q : P x), p = q) + (Q_hprop : forall (x : A) (p q : Q x), p = q) + (u1 v1 : A) (u2 : P u1) (v2 : P v1) (u3 : Q u1) (v3 : Q v1) + (p : u1 = v1) + : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3 + := eq_ex2' u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _). + + Lemma eq_rect_ex2 {A x} {P : A -> Type} + (Q : forall a, P a -> Prop) + (R : forall a, P a -> Prop) + (u : ex2 (Q x) (R x)) {y} (H : x = y) + : rew [fun a => ex2 (Q a) (R a)] H in u + = match u with + | ex_intro2 _ _ u1 u2 u3 + => ex_intro2 + (Q y) + (R y) + (rew H in u1) + match H in (_ = y) return Q y (rew H in u1) with + | eq_refl => u2 + end + match H in (_ = y) return R y (rew H in u1) with + | eq_refl => u3 + end + end. + Proof. + destruct H, u; reflexivity. + Defined. +End ex2. -- cgit v1.2.3 From fbec6e43c5dc3b93e61a3313ebf91196407892ca Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Dec 2016 16:43:40 -0500 Subject: Add equality lemmas for sig2 and sigT2 --- test-suite/success/InversionSigma.v | 12 +- theories/Init/Specif.v | 222 ++++++++++++++++++++++++++++++++++++ theories/Init/Tactics.v | 24 ++++ 3 files changed, 257 insertions(+), 1 deletion(-) (limited to 'theories/Init') diff --git a/test-suite/success/InversionSigma.v b/test-suite/success/InversionSigma.v index c19939eab..51f33c7ce 100644 --- a/test-suite/success/InversionSigma.v +++ b/test-suite/success/InversionSigma.v @@ -1,6 +1,6 @@ Section inversion_sigma. Local Unset Implicit Arguments. - Context A (B : A -> Prop) (C : forall a, B a -> Prop) + Context A (B : A -> Prop) (C C' : forall a, B a -> Prop) (D : forall a b, C a b -> Prop) (E : forall a b c, D a b c -> Prop). (* Require that, after destructing sigma types and inverting @@ -11,6 +11,8 @@ Section inversion_sigma. repeat match goal with | [ H : sig _ |- _ ] => destruct H | [ H : sigT _ |- _ ] => destruct H + | [ H : sig2 _ _ |- _ ] => destruct H + | [ H : sigT2 _ _ |- _ ] => destruct H end; simpl in *; inversion_sigma; repeat match goal with @@ -27,4 +29,12 @@ Section inversion_sigma. Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } }) (p : x = y), p = p. Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : { a : A & B a } & C _ (projT2 a) & C' _ (projT2 a) }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : { a : A & B a } | C _ (projT2 a) & C' _ (projT2 a) }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. End inversion_sigma. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index cdc918275..1d8a40ebb 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -371,6 +371,228 @@ Section sig. Defined. End sig. +(** Equality for [sigT] *) +Section sigT2. + (* We make [sigT_of_sigT2] a coercion so we can use [projT1], [projT2] on [sigT2] *) + Local Coercion sigT_of_sigT2 : sigT2 >-> sigT. + Local Unset Implicit Arguments. + (** Projecting an equality of a pair to equality of the first components *) + Definition sigT_of_sigT2_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) + : u = v :> sigT _ + := f_equal _ p. + Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) + : projT1 u = projT1 v + := projT1_eq (sigT_of_sigT2_eq p). + + (** Projecting an equality of a pair to equality of the second components *) + Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) + : rew projT1_of_sigT2_eq p in projT2 u = projT2 v. + Proof. + destruct p; reflexivity. + Defined. + + (** Projecting an equality of a pair to equality of the third components *) + Definition projT3_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) + : rew projT1_of_sigT2_eq p in projT3 u = projT3 v. + Proof. + destruct p; reflexivity. + Defined. + + (** Equality of [sigT2] is itself a [sigT2] *) + Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : sigT2 P Q) + (pqr : { p : projT1 u = projT1 v + & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }) + : u = v. + Proof. + destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. + destruct pqr as [p q r]. + destruct r, q, p; simpl. + reflexivity. + Defined. + + (** Curried version of proving equality of sigma types *) + Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : sigT2 P Q) + (p : projT1 u = projT1 v) + (q : rew p in projT2 u = projT2 v) + (r : rew p in projT3 u = projT3 v) + : u = v + := eq_sigT2_uncurried u v (existT2 _ _ p q r). + + (** Equality of [sigT2] when the second property is an hProp *) + Definition eq_sigT2_hprop {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q) + (u v : @sigT2 A P Q) + (p : u = v :> sigT _) + : u = v + := eq_sigT2 u v (projT1_eq p) (projT2_eq p) (Q_hprop _ _ _). + + (** Equivalence of equality of [sigT2] with a [sigT2] 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_sigT2_uncurried_iff {A P Q} + (u v : @sigT2 A P Q) + : u = v + <-> { p : projT1 u = projT1 v + & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }. + Proof. + split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT2_uncurried ]. + Defined. + + (** Induction principle for [@eq (sigT2 _ _)] *) + Definition eq_sigT2_rect {A P Q} {u v : @sigT2 A P Q} (R : u = v -> Type) + (f : forall p q r, R (eq_sigT2 u v p q r)) + : forall p, R p. + Proof. + intro p. + specialize (f (projT1_of_sigT2_eq p) (projT2_of_sigT2_eq p) (projT3_eq p)). + destruct u, p; exact f. + Defined. + Definition eq_sigT2_rec {A P Q u v} (R : u = v :> @sigT2 A P Q -> Set) := eq_sigT2_rect R. + Definition eq_sigT2_ind {A P Q u v} (R : u = v :> @sigT2 A P Q -> Prop) := eq_sigT2_rec R. + + (** Equivalence of equality of [sigT2] involving hProps with equality of the first components *) + Definition eq_sigT2_hprop_iff {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q) + (u v : @sigT2 A P Q) + : u = v <-> (u = v :> sigT _) + := conj (fun p => f_equal (@sigT_of_sigT2 _ _ _) p) (eq_sigT2_hprop Q_hprop u v). + + (** Non-dependent classification of equality of [sigT] *) + Definition eq_sigT2_nondep {A B C : Type} (u v : @sigT2 A (fun _ => B) (fun _ => C)) + (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v) + : u = v + := @eq_sigT2 _ _ _ u v p (eq_trans (eq_rect_const _ _) q) (eq_trans (eq_rect_const _ _) r). + + (** Classification of transporting across an equality of [sigT2]s *) + Lemma eq_rect_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) + (u : sigT2 (Q x) (R x)) + {y} (H : x = y) + : rew [fun a => sigT2 (Q a) (R a)] H in u + = existT2 + (Q y) + (R y) + (rew H in projT1 u) + match H in (_ = y) return Q y (rew H in projT1 u) with + | eq_refl => projT2 u + end + match H in (_ = y) return R y (rew H in projT1 u) with + | eq_refl => projT3 u + end. + Proof. + destruct H, u; reflexivity. + Defined. +End sigT2. + +(** Equality for [sig2] *) +Section sig2. + (* We make [sig_of_sig2] a coercion so we can use [proj1], [proj2] on [sig2] *) + Local Coercion sig_of_sig2 : sig2 >-> sig. + Local Unset Implicit Arguments. + (** Projecting an equality of a pair to equality of the first components *) + Definition sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) + : u = v :> sig _ + := f_equal _ p. + Definition proj1_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) + : proj1_sig u = proj1_sig v + := proj1_sig_eq (sig_of_sig2_eq p). + + (** Projecting an equality of a pair to equality of the second components *) + Definition proj2_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) + : rew proj1_sig_of_sig2_eq p in proj2_sig u = proj2_sig v. + Proof. + destruct p; reflexivity. + Defined. + + (** Projecting an equality of a pair to equality of the third components *) + Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) + : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v. + Proof. + destruct p; reflexivity. + Defined. + + (** Equality of [sig2] is itself a [sig2] *) + Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : sig2 P Q) + (pqr : { p : proj1_sig u = proj1_sig v + | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }) + : u = v. + Proof. + destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. + destruct pqr as [p q r]. + destruct r, q, p; simpl. + reflexivity. + Defined. + + (** Curried version of proving equality of sigma types *) + Definition eq_sig2 {A} {P Q : A -> Prop} (u v : sig2 P Q) + (p : proj1_sig u = proj1_sig v) + (q : rew p in proj2_sig u = proj2_sig v) + (r : rew p in proj3_sig u = proj3_sig v) + : u = v + := eq_sig2_uncurried u v (exist2 _ _ p q r). + + (** Equality of [sig2] when the second property is an hProp *) + Definition eq_sig2_hprop {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) + (u v : @sig2 A P Q) + (p : u = v :> sig _) + : u = v + := eq_sig2 u v (proj1_sig_eq p) (proj2_sig_eq p) (Q_hprop _ _ _). + + (** Equivalence of equality of [sig2] with a [sig2] 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_sig2_uncurried_iff {A P Q} + (u v : @sig2 A P Q) + : u = v + <-> { p : proj1_sig u = proj1_sig v + | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }. + Proof. + split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig2_uncurried ]. + Defined. + + (** Induction principle for [@eq (sig2 _ _)] *) + Definition eq_sig2_rect {A P Q} {u v : @sig2 A P Q} (R : u = v -> Type) + (f : forall p q r, R (eq_sig2 u v p q r)) + : forall p, R p. + Proof. + intro p. + specialize (f (proj1_sig_of_sig2_eq p) (proj2_sig_of_sig2_eq p) (proj3_sig_eq p)). + destruct u, p; exact f. + Defined. + Definition eq_sig2_rec {A P Q u v} (R : u = v :> @sig2 A P Q -> Set) := eq_sig2_rect R. + Definition eq_sig2_ind {A P Q u v} (R : u = v :> @sig2 A P Q -> Prop) := eq_sig2_rec R. + + (** Equivalence of equality of [sig2] involving hProps with equality of the first components *) + Definition eq_sig2_hprop_iff {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) + (u v : @sig2 A P Q) + : u = v <-> (u = v :> sig _) + := conj (fun p => f_equal (@sig_of_sig2 _ _ _) p) (eq_sig2_hprop Q_hprop u v). + + (** Non-dependent classification of equality of [sig] *) + Definition eq_sig2_nondep {A} {B C : Prop} (u v : @sig2 A (fun _ => B) (fun _ => C)) + (p : proj1_sig u = proj1_sig v) (q : proj2_sig u = proj2_sig v) (r : proj3_sig u = proj3_sig v) + : u = v + := @eq_sig2 _ _ _ u v p (eq_trans (eq_rect_const _ _) q) (eq_trans (eq_rect_const _ _) r). + + (** Classification of transporting across an equality of [sig2]s *) + Lemma eq_rect_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) + (u : sig2 (Q x) (R x)) + {y} (H : x = y) + : rew [fun a => sig2 (Q a) (R a)] H in u + = exist2 + (Q y) + (R y) + (rew H in proj1_sig u) + match H in (_ = y) return Q y (rew H in proj1_sig u) with + | eq_refl => proj2_sig u + end + match H in (_ = y) return R y (rew H in proj1_sig u) with + | eq_refl => proj3_sig u + end. + Proof. + destruct H, u; reflexivity. + Defined. +End sig2. + (** [sumbool] is a boolean type equipped with the justification of their value *) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index e01c07a99..aab385ef7 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -263,6 +263,14 @@ Ltac simpl_proj_exist_in H := => 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 + | context G[proj3_sig (exist2 _ _ ?x ?p ?q)] + => let G' := context G[q] in change G' in H + | context G[projT3 (existT2 _ _ ?x ?p ?q)] + => let G' := context G[q] in change G' in H + | context G[sig_of_sig2 (@exist2 ?A ?P ?Q ?x ?p ?q)] + => let G' := context G[@exist A P x p] in change G' in H + | context G[sigT_of_sigT2 (@existT2 ?A ?P ?Q ?x ?p ?q)] + => let G' := context G[@existT A P x p] in change G' in H end. Ltac induction_sigma_in_using H rect := let H0 := fresh H in @@ -270,6 +278,14 @@ Ltac induction_sigma_in_using H rect := induction H as [H0 H1] using (rect _ _ _ _); simpl_proj_exist_in H0; simpl_proj_exist_in H1. +Ltac induction_sigma2_in_using H rect := + let H0 := fresh H in + let H1 := fresh H in + let H2 := fresh H in + induction H as [H0 H1 H2] using (rect _ _ _ _ _); + simpl_proj_exist_in H0; + simpl_proj_exist_in H1; + simpl_proj_exist_in H2. Ltac inversion_sigma_step := match goal with | [ H : _ = exist _ _ _ |- _ ] @@ -280,5 +296,13 @@ Ltac inversion_sigma_step := => induction_sigma_in_using H @eq_sig_rect | [ H : existT _ _ _ = _ |- _ ] => induction_sigma_in_using H @eq_sigT_rect + | [ H : _ = exist2 _ _ _ _ _ |- _ ] + => induction_sigma2_in_using H @eq_sig2_rect + | [ H : _ = existT2 _ _ _ _ _ |- _ ] + => induction_sigma2_in_using H @eq_sigT2_rect + | [ H : exist2 _ _ _ _ _ = _ |- _ ] + => induction_sigma_in_using H @eq_sig2_rect + | [ H : existT2 _ _ _ _ _ = _ |- _ ] + => induction_sigma_in_using H @eq_sigT2_rect end. Ltac inversion_sigma := repeat inversion_sigma_step. -- cgit v1.2.3 From 6d3c5956ee7c56c816750f3879a5ddafcdf81f0f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Feb 2017 20:42:52 -0500 Subject: Use [rew_] instead of [eq_rect_] prefix As per Hugo's request. --- theories/Init/Logic.v | 4 ++-- theories/Init/Specif.v | 14 +++++++------- 2 files changed, 9 insertions(+), 9 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 1f94f7586..b5d99aac6 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -673,7 +673,7 @@ Section ex. : 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) + Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y) : rew [fun a => ex (Q a)] H in u = match u with | ex_intro _ u1 u2 @@ -720,7 +720,7 @@ Section ex2. : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3 := eq_ex2' u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _). - Lemma eq_rect_ex2 {A x} {P : A -> Type} + Lemma rew_ex2 {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (R : forall a, P a -> Prop) (u : ex2 (Q x) (R x)) {y} (H : x = y) diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 1d8a40ebb..f3570b0d6 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -289,10 +289,10 @@ Section 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). + := @eq_sigT _ _ u v p (eq_trans (rew_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) + Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sigT (Q x)) {y} (H : x = y) : rew [fun a => sigT (Q a)] H in u = existT (Q y) @@ -358,7 +358,7 @@ Section sig. : 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) + Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sig (Q x)) {y} (H : x = y) : rew [fun a => sig (Q a)] H in u = exist (Q y) @@ -460,10 +460,10 @@ Section sigT2. Definition eq_sigT2_nondep {A B C : Type} (u v : @sigT2 A (fun _ => B) (fun _ => C)) (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v) : u = v - := @eq_sigT2 _ _ _ u v p (eq_trans (eq_rect_const _ _) q) (eq_trans (eq_rect_const _ _) r). + := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). (** Classification of transporting across an equality of [sigT2]s *) - Lemma eq_rect_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) + Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) (u : sigT2 (Q x) (R x)) {y} (H : x = y) : rew [fun a => sigT2 (Q a) (R a)] H in u @@ -571,10 +571,10 @@ Section sig2. Definition eq_sig2_nondep {A} {B C : Prop} (u v : @sig2 A (fun _ => B) (fun _ => C)) (p : proj1_sig u = proj1_sig v) (q : proj2_sig u = proj2_sig v) (r : proj3_sig u = proj3_sig v) : u = v - := @eq_sig2 _ _ _ u v p (eq_trans (eq_rect_const _ _) q) (eq_trans (eq_rect_const _ _) r). + := @eq_sig2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). (** Classification of transporting across an equality of [sig2]s *) - Lemma eq_rect_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) + Lemma rew_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) (u : sig2 (Q x) (R x)) {y} (H : x = y) : rew [fun a => sig2 (Q a) (R a)] H in u -- cgit v1.2.3 From 4e12d9eb8945120c5cfdb36964fba54dde767b51 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Feb 2017 20:43:46 -0500 Subject: Replace [ex'] with [ex] The ' was originally denoting that we were taking in the projections and applying the constructor in the conclusion, rather than taking in the bundled versions and projecting them out (because the projections don't exist for [ex] and [ex2]). But we don't have versions like this for [sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the ' to the [ex] and [ex2] versions. --- theories/Init/Logic.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index b5d99aac6..35591cbe3 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -653,7 +653,7 @@ 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} + Definition eq_ex_uncurried {A : Type} (P : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : exists p : u1 = v1, rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2. Proof. @@ -662,16 +662,16 @@ Section ex. destruct p; reflexivity. Defined. - Definition eq_ex' {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1) + Definition eq_ex {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1) (p : u1 = v1) (q : rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2 - := eq_ex_uncurried' P (ex_intro _ p q). + := 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) + 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 _ _ _). + := eq_ex u1 v1 u2 v2 p (P_hprop _ _ _). Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y) : rew [fun a => ex (Q a)] H in u @@ -693,7 +693,7 @@ End ex. Section ex2. Local Unset Implicit Arguments. - Definition eq_ex2_uncurried' {A : Type} (P Q : A -> Prop) {u1 v1 : A} + Definition eq_ex2_uncurried {A : Type} (P Q : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} (pq : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3) @@ -704,21 +704,21 @@ Section ex2. reflexivity. Defined. - Definition eq_ex2' {A : Type} {P Q : A -> Prop} + Definition eq_ex2 {A : Type} {P Q : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1) (u3 : Q u1) (v3 : Q v1) (p : u1 = v1) (q : rew p in u2 = v2) (r : rew p in u3 = v3) : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3 - := eq_ex2_uncurried' P Q (ex_intro2 _ _ p q r). + := eq_ex2_uncurried P Q (ex_intro2 _ _ p q r). - Definition eq_ex2'_hprop {A} {P Q : A -> Prop} + Definition eq_ex2_hprop {A} {P Q : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (Q_hprop : forall (x : A) (p q : Q x), p = q) (u1 v1 : A) (u2 : P u1) (v2 : P v1) (u3 : Q u1) (v3 : Q v1) (p : u1 = v1) : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3 - := eq_ex2' u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _). + := eq_ex2 u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _). Lemma rew_ex2 {A x} {P : A -> Type} (Q : forall a, P a -> Prop) -- cgit v1.2.3 From dcc77d0dd478b2758d41e35975d31b12e86f61ca Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Feb 2017 01:59:36 -0500 Subject: Use extended notation for ex, ex2 types --- theories/Init/Logic.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 35591cbe3..845b8ee9f 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -673,8 +673,8 @@ Section ex. : ex_intro P u1 u2 = ex_intro P v1 v2 := eq_ex u1 v1 u2 v2 p (P_hprop _ _ _). - Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y) - : rew [fun a => ex (Q a)] H in u + Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : exists p, Q x p) {y} (H : x = y) + : rew [fun a => exists p, Q a p] H in u = match u with | ex_intro _ u1 u2 => ex_intro @@ -723,8 +723,8 @@ Section ex2. Lemma rew_ex2 {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (R : forall a, P a -> Prop) - (u : ex2 (Q x) (R x)) {y} (H : x = y) - : rew [fun a => ex2 (Q a) (R a)] H in u + (u : exists2 p, Q x p & R x p) {y} (H : x = y) + : rew [fun a => exists2 p, Q a p & R a p] H in u = match u with | ex_intro2 _ _ u1 u2 u3 => ex_intro2 -- cgit v1.2.3 From 90ddbd7f0b10c0635dc3c5b948b4c0f049d45350 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Feb 2017 11:15:24 -0500 Subject: Use notations for [sig], [sigT], [sig2], [sigT2] --- theories/Init/Specif.v | 126 ++++++++++++++++++++++++------------------------- 1 file changed, 63 insertions(+), 63 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index f3570b0d6..5da6feee2 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -225,20 +225,20 @@ Import EqNotations. 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) + Definition projT1_eq {A} {P : A -> Type} {u v : { a : A & P a }} (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) + Definition projT2_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v) : rew projT1_eq p in projT2 u = 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 => rew p in projT2 u = projT2 v)) + Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a }) + (pq : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. @@ -248,14 +248,14 @@ Section sigT. Defined. (** Curried version of proving equality of sigma types *) - Definition eq_sigT {A : Type} {P : A -> Type} (u v : sigT P) + Definition eq_sigT {A : Type} {P : A -> Type} (u v : { a : A & P a }) (p : projT1 u = projT1 v) (q : rew p in projT2 u = 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) + (u v : { a : A & P a }) (p : projT1 u = projT1 v) : u = v := eq_sigT u v p (P_hprop _ _ _). @@ -265,35 +265,35 @@ Section sigT. 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 : { a : A & P a }) : u = v <-> (sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = 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) + Definition eq_sigT_rect {A P} {u v : { a : A & P a }} (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. + Definition eq_sigT_rec {A P u v} (Q : u = v :> { a : A & P a } -> Set) := eq_sigT_rect Q. + Definition eq_sigT_ind {A P u v} (Q : u = v :> { a : A & P a } -> 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 : { a : A & P a }) : 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)) + Definition eq_sigT_nondep {A B : Type} (u v : { a : A & B }) (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) : u = v := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q). (** Classification of transporting across an equality of [sigT]s *) - Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sigT (Q x)) {y} (H : x = y) - : rew [fun a => sigT (Q a)] H in u + Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x & Q x p }) {y} (H : x = y) + : rew [fun a => { p : P a & Q a p }] H in u = existT (Q y) (rew H in projT1 u) @@ -308,18 +308,18 @@ 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) + Definition proj1_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (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) + Definition proj2_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) : rew proj1_sig_eq p in proj2_sig u = 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 | rew p in proj2_sig u = proj2_sig v}) + Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : { a : A | P a }) + (pq : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. @@ -328,38 +328,38 @@ Section sig. destruct p; reflexivity. Defined. - Definition eq_sig {A : Type} {P : A -> Prop} (u v : sig P) + Definition eq_sig {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = 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) + Definition eq_sig_rect {A P} {u v : { a : A | P a }} (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_rec {A P u v} (Q : u = v :> { a : A | P a } -> Set) := eq_sig_rect Q. + Definition eq_sig_ind {A P u v} (Q : u = v :> { a : A | P a } -> 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) + (u v : { a : A | P a }) (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 => rew p in proj2_sig u = proj2_sig v)). + (u v : { a : A | P a }) + : u = v <-> { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = 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 : { a : A | P a }) : u = v <-> (proj1_sig u = proj1_sig v) := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v). - Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sig (Q x)) {y} (H : x = y) - : rew [fun a => sig (Q a)] H in u + Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x | Q x p }) {y} (H : x = y) + : rew [fun a => { p : P a | Q a p }] H in u = exist (Q y) (rew H in proj1_sig u) @@ -377,29 +377,29 @@ Section sigT2. Local Coercion sigT_of_sigT2 : sigT2 >-> sigT. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) - Definition sigT_of_sigT2_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) - : u = v :> sigT _ + Definition sigT_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) + : u = v :> { a : A & P a } := f_equal _ p. - Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) + Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) : projT1 u = projT1 v := projT1_eq (sigT_of_sigT2_eq p). (** Projecting an equality of a pair to equality of the second components *) - Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) + Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) : rew projT1_of_sigT2_eq p in projT2 u = projT2 v. Proof. destruct p; reflexivity. Defined. (** Projecting an equality of a pair to equality of the third components *) - Definition projT3_eq {A} {P Q : A -> Type} {u v : sigT2 P Q} (p : u = v) + Definition projT3_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) : rew projT1_of_sigT2_eq p in projT3 u = projT3 v. Proof. destruct p; reflexivity. Defined. (** Equality of [sigT2] is itself a [sigT2] *) - Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : sigT2 P Q) + Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) (pqr : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }) : u = v. @@ -411,7 +411,7 @@ Section sigT2. Defined. (** Curried version of proving equality of sigma types *) - Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : sigT2 P Q) + Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v) (r : rew p in projT3 u = projT3 v) @@ -420,8 +420,8 @@ Section sigT2. (** Equality of [sigT2] when the second property is an hProp *) Definition eq_sigT2_hprop {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q) - (u v : @sigT2 A P Q) - (p : u = v :> sigT _) + (u v : { a : A & P a & Q a }) + (p : u = v :> { a : A & P a }) : u = v := eq_sigT2 u v (projT1_eq p) (projT2_eq p) (Q_hprop _ _ _). @@ -430,7 +430,7 @@ Section sigT2. don't. If we wanted to deal with proofs of equality of Σ types in dependent positions, we'd need it. *) Definition eq_sigT2_uncurried_iff {A P Q} - (u v : @sigT2 A P Q) + (u v : { a : A & P a & Q a }) : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }. @@ -439,7 +439,7 @@ Section sigT2. Defined. (** Induction principle for [@eq (sigT2 _ _)] *) - Definition eq_sigT2_rect {A P Q} {u v : @sigT2 A P Q} (R : u = v -> Type) + Definition eq_sigT2_rect {A P Q} {u v : { a : A & P a & Q a }} (R : u = v -> Type) (f : forall p q r, R (eq_sigT2 u v p q r)) : forall p, R p. Proof. @@ -447,26 +447,26 @@ Section sigT2. specialize (f (projT1_of_sigT2_eq p) (projT2_of_sigT2_eq p) (projT3_eq p)). destruct u, p; exact f. Defined. - Definition eq_sigT2_rec {A P Q u v} (R : u = v :> @sigT2 A P Q -> Set) := eq_sigT2_rect R. - Definition eq_sigT2_ind {A P Q u v} (R : u = v :> @sigT2 A P Q -> Prop) := eq_sigT2_rec R. + Definition eq_sigT2_rec {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Set) := eq_sigT2_rect R. + Definition eq_sigT2_ind {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Prop) := eq_sigT2_rec R. (** Equivalence of equality of [sigT2] involving hProps with equality of the first components *) Definition eq_sigT2_hprop_iff {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q) - (u v : @sigT2 A P Q) - : u = v <-> (u = v :> sigT _) + (u v : { a : A & P a & Q a }) + : u = v <-> (u = v :> { a : A & P a }) := conj (fun p => f_equal (@sigT_of_sigT2 _ _ _) p) (eq_sigT2_hprop Q_hprop u v). (** Non-dependent classification of equality of [sigT] *) - Definition eq_sigT2_nondep {A B C : Type} (u v : @sigT2 A (fun _ => B) (fun _ => C)) + Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C }) (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v) : u = v := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). (** Classification of transporting across an equality of [sigT2]s *) Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) - (u : sigT2 (Q x) (R x)) + (u : { p : P x & Q x p & R x p }) {y} (H : x = y) - : rew [fun a => sigT2 (Q a) (R a)] H in u + : rew [fun a => { p : P a & Q a p & R a p }] H in u = existT2 (Q y) (R y) @@ -488,29 +488,29 @@ Section sig2. Local Coercion sig_of_sig2 : sig2 >-> sig. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) - Definition sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) - : u = v :> sig _ + Definition sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) + : u = v :> { a : A | P a } := f_equal _ p. - Definition proj1_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) + Definition proj1_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : proj1_sig u = proj1_sig v := proj1_sig_eq (sig_of_sig2_eq p). (** Projecting an equality of a pair to equality of the second components *) - Definition proj2_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) + Definition proj2_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : rew proj1_sig_of_sig2_eq p in proj2_sig u = proj2_sig v. Proof. destruct p; reflexivity. Defined. (** Projecting an equality of a pair to equality of the third components *) - Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : sig2 P Q} (p : u = v) + Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v. Proof. destruct p; reflexivity. Defined. (** Equality of [sig2] is itself a [sig2] *) - Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : sig2 P Q) + Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a }) (pqr : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }) : u = v. @@ -522,7 +522,7 @@ Section sig2. Defined. (** Curried version of proving equality of sigma types *) - Definition eq_sig2 {A} {P Q : A -> Prop} (u v : sig2 P Q) + Definition eq_sig2 {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a }) (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) (r : rew p in proj3_sig u = proj3_sig v) @@ -531,8 +531,8 @@ Section sig2. (** Equality of [sig2] when the second property is an hProp *) Definition eq_sig2_hprop {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) - (u v : @sig2 A P Q) - (p : u = v :> sig _) + (u v : { a : A | P a & Q a }) + (p : u = v :> { a : A | P a }) : u = v := eq_sig2 u v (proj1_sig_eq p) (proj2_sig_eq p) (Q_hprop _ _ _). @@ -541,7 +541,7 @@ Section sig2. don't. If we wanted to deal with proofs of equality of Σ types in dependent positions, we'd need it. *) Definition eq_sig2_uncurried_iff {A P Q} - (u v : @sig2 A P Q) + (u v : { a : A | P a & Q a }) : u = v <-> { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }. @@ -550,7 +550,7 @@ Section sig2. Defined. (** Induction principle for [@eq (sig2 _ _)] *) - Definition eq_sig2_rect {A P Q} {u v : @sig2 A P Q} (R : u = v -> Type) + Definition eq_sig2_rect {A P Q} {u v : { a : A | P a & Q a }} (R : u = v -> Type) (f : forall p q r, R (eq_sig2 u v p q r)) : forall p, R p. Proof. @@ -558,13 +558,13 @@ Section sig2. specialize (f (proj1_sig_of_sig2_eq p) (proj2_sig_of_sig2_eq p) (proj3_sig_eq p)). destruct u, p; exact f. Defined. - Definition eq_sig2_rec {A P Q u v} (R : u = v :> @sig2 A P Q -> Set) := eq_sig2_rect R. - Definition eq_sig2_ind {A P Q u v} (R : u = v :> @sig2 A P Q -> Prop) := eq_sig2_rec R. + Definition eq_sig2_rec {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Set) := eq_sig2_rect R. + Definition eq_sig2_ind {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Prop) := eq_sig2_rec R. (** Equivalence of equality of [sig2] involving hProps with equality of the first components *) Definition eq_sig2_hprop_iff {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) - (u v : @sig2 A P Q) - : u = v <-> (u = v :> sig _) + (u v : { a : A | P a & Q a }) + : u = v <-> (u = v :> { a : A | P a }) := conj (fun p => f_equal (@sig_of_sig2 _ _ _) p) (eq_sig2_hprop Q_hprop u v). (** Non-dependent classification of equality of [sig] *) @@ -575,9 +575,9 @@ Section sig2. (** Classification of transporting across an equality of [sig2]s *) Lemma rew_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) - (u : sig2 (Q x) (R x)) + (u : { p : P x | Q x p & R x p }) {y} (H : x = y) - : rew [fun a => sig2 (Q a) (R a)] H in u + : rew [fun a => { p : P a | Q a p & R a p }] H in u = exist2 (Q y) (R y) -- cgit v1.2.3 From 745a26bbf47281cbf30ed97cf61c92d4c2ac006c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 14:08:33 -0400 Subject: Remove reference to [IsIso] --- theories/Init/Specif.v | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 5da6feee2..e4c57c6c1 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -261,9 +261,8 @@ Section sigT. := 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. *) + (** We could actually prove an isomorphism here, and not just [<->], + but for simplicity, we don't. *) Definition eq_sigT_uncurried_iff {A P} (u v : { a : A & P a }) : u = v <-> (sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)). @@ -426,9 +425,8 @@ Section sigT2. := eq_sigT2 u v (projT1_eq p) (projT2_eq p) (Q_hprop _ _ _). (** Equivalence of equality of [sigT2] with a [sigT2] 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. *) + (** We could actually prove an isomorphism here, and not just [<->], + but for simplicity, we don't. *) Definition eq_sigT2_uncurried_iff {A P Q} (u v : { a : A & P a & Q a }) : u = v @@ -537,9 +535,8 @@ Section sig2. := eq_sig2 u v (proj1_sig_eq p) (proj2_sig_eq p) (Q_hprop _ _ _). (** Equivalence of equality of [sig2] with a [sig2] 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. *) + (** We could actually prove an isomorphism here, and not just [<->], + but for simplicity, we don't. *) Definition eq_sig2_uncurried_iff {A P Q} (u v : { a : A | P a & Q a }) : u = v -- cgit v1.2.3 From 179e1d5451411f96a5032e244f2f6cd57463e3bd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 14:09:23 -0400 Subject: Use notation for sigT --- theories/Init/Specif.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index e4c57c6c1..771a10531 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -265,7 +265,7 @@ Section sigT. but for simplicity, we don't. *) Definition eq_sigT_uncurried_iff {A P} (u v : { a : A & P a }) - : u = v <-> (sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)). + : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ]. Defined. -- cgit v1.2.3 From abe171759d3548cda6355fa4ca623c954145322c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 14:23:38 -0400 Subject: Add forward-chaining versions: [eq_sig*_uncurried] --- theories/Init/Specif.v | 56 +++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 44 insertions(+), 12 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 771a10531..e1d8991d1 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -237,14 +237,21 @@ Section sigT. Defined. (** Equality of [sigT] is itself a [sigT] *) + Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} + (pq : { p : u1 = v1 & rew p in u2 = v2 }) + : existT _ u1 u2 = existT _ v1 v2. + Proof. + destruct pq as [p q]. + destruct q; simpl in *. + destruct p; reflexivity. + Defined. + Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a }) (pq : { p : projT1 u = projT1 v & rew p in projT2 u = 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. + apply eq_existT_uncurried; exact pq. Defined. (** Curried version of proving equality of sigma types *) @@ -317,14 +324,21 @@ Section sig. destruct p; reflexivity. Defined. + Definition eq_exist_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} + (pq : { p : u1 = v1 | rew p in u2 = v2 }) + : exist _ u1 u2 = exist _ v1 v2. + Proof. + destruct pq as [p q]. + destruct q; simpl in *. + destruct p; reflexivity. + Defined. + Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (pq : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = 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. + apply eq_exist_uncurried; exact pq. Defined. Definition eq_sig {A : Type} {P : A -> Prop} (u v : { a : A | P a }) @@ -398,15 +412,24 @@ Section sigT2. Defined. (** Equality of [sigT2] is itself a [sigT2] *) + Definition eq_existT2_uncurried {A : Type} {P Q : A -> Type} + {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} + (pqr : { p : u1 = v1 + & rew p in u2 = v2 & rew p in u3 = v3 }) + : existT2 _ _ u1 u2 u3 = existT2 _ _ v1 v2 v3. + Proof. + destruct pqr as [p q r]. + destruct r, q, p; simpl. + reflexivity. + Defined. + Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) (pqr : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }) : u = v. Proof. destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. - destruct pqr as [p q r]. - destruct r, q, p; simpl. - reflexivity. + apply eq_existT2_uncurried; exact pqr. Defined. (** Curried version of proving equality of sigma types *) @@ -508,15 +531,24 @@ Section sig2. Defined. (** Equality of [sig2] is itself a [sig2] *) + Definition eq_exist2_uncurried {A} {P Q : A -> Prop} + {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} + (pqr : { p : u1 = v1 + | rew p in u2 = v2 & rew p in u3 = v3 }) + : exist2 _ _ u1 u2 u3 = exist2 _ _ v1 v2 v3. + Proof. + destruct pqr as [p q r]. + destruct r, q, p; simpl. + reflexivity. + Defined. + Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a }) (pqr : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }) : u = v. Proof. destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. - destruct pqr as [p q r]. - destruct r, q, p; simpl. - reflexivity. + apply eq_exist2_uncurried; exact pqr. Defined. (** Curried version of proving equality of sigma types *) -- cgit v1.2.3 From 97480f826658043204d41a9454f96a355a608853 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 14:40:04 -0400 Subject: Use a local [rew dependent] notation --- theories/Init/Specif.v | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index e1d8991d1..2b4cc745f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -220,6 +220,12 @@ Qed. (** Equality of sigma types *) Import EqNotations. +Local Notation "'rew' 'dependent' [ Q ] H 'in' H'" + := (match H as p in (_ = y) return Q y (rew p in _) with + | eq_refl => H' + end) + (at level 10, H' at level 10, + format "'[' 'rew' 'dependent' [ Q ] '/ ' H in '/' H' ']'"). (** Equality for [sigT] *) Section sigT. @@ -303,9 +309,7 @@ Section sigT. = existT (Q y) (rew H in projT1 u) - match H in (_ = y) return Q y (rew H in projT1 u) with - | eq_refl => projT2 u - end. + (rew dependent [Q] H in (projT2 u)). Proof. destruct H, u; reflexivity. Defined. @@ -376,9 +380,7 @@ Section sig. = exist (Q y) (rew H in proj1_sig u) - match H in (_ = y) return Q y (rew H in proj1_sig u) with - | eq_refl => proj2_sig u - end. + (rew dependent [Q] H in proj2_sig u). Proof. destruct H, u; reflexivity. Defined. @@ -492,12 +494,8 @@ Section sigT2. (Q y) (R y) (rew H in projT1 u) - match H in (_ = y) return Q y (rew H in projT1 u) with - | eq_refl => projT2 u - end - match H in (_ = y) return R y (rew H in projT1 u) with - | eq_refl => projT3 u - end. + (rew dependent [Q] H in projT2 u) + (rew dependent [R] H in projT3 u). Proof. destruct H, u; reflexivity. Defined. @@ -611,12 +609,8 @@ Section sig2. (Q y) (R y) (rew H in proj1_sig u) - match H in (_ = y) return Q y (rew H in proj1_sig u) with - | eq_refl => proj2_sig u - end - match H in (_ = y) return R y (rew H in proj1_sig u) with - | eq_refl => proj3_sig u - end. + (rew dependent [Q] H in proj2_sig u) + (rew dependent [R] H in proj3_sig u). Proof. destruct H, u; reflexivity. Defined. -- cgit v1.2.3 From 0a2362cd8547bc073d60470c2a49174dd15634d0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 14:41:36 -0400 Subject: Remove motive argument from [rew dependent] --- theories/Init/Specif.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2b4cc745f..fc7250e2f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -220,12 +220,12 @@ Qed. (** Equality of sigma types *) Import EqNotations. -Local Notation "'rew' 'dependent' [ Q ] H 'in' H'" - := (match H as p in (_ = y) return Q y (rew p in _) with +Local Notation "'rew' 'dependent' H 'in' H'" + := (match H with | eq_refl => H' end) (at level 10, H' at level 10, - format "'[' 'rew' 'dependent' [ Q ] '/ ' H in '/' H' ']'"). + format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'"). (** Equality for [sigT] *) Section sigT. @@ -309,7 +309,7 @@ Section sigT. = existT (Q y) (rew H in projT1 u) - (rew dependent [Q] H in (projT2 u)). + (rew dependent H in (projT2 u)). Proof. destruct H, u; reflexivity. Defined. @@ -380,7 +380,7 @@ Section sig. = exist (Q y) (rew H in proj1_sig u) - (rew dependent [Q] H in proj2_sig u). + (rew dependent H in proj2_sig u). Proof. destruct H, u; reflexivity. Defined. @@ -494,8 +494,8 @@ Section sigT2. (Q y) (R y) (rew H in projT1 u) - (rew dependent [Q] H in projT2 u) - (rew dependent [R] H in projT3 u). + (rew dependent H in projT2 u) + (rew dependent H in projT3 u). Proof. destruct H, u; reflexivity. Defined. @@ -609,8 +609,8 @@ Section sig2. (Q y) (R y) (rew H in proj1_sig u) - (rew dependent [Q] H in proj2_sig u) - (rew dependent [R] H in proj3_sig u). + (rew dependent H in proj2_sig u) + (rew dependent H in proj3_sig u). Proof. destruct H, u; reflexivity. Defined. -- cgit v1.2.3 From 9922c243e6d6a01d7308a6b1ce2aefd44d1b100e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 25 Apr 2017 14:49:18 -0400 Subject: Add some more comments about sigma equalities Forwards/backwards reasoning thoughts come from https://github.com/coq/coq/pull/385#discussion_r111008347 --- theories/Init/Specif.v | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index fc7250e2f..2555276e4 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -242,7 +242,7 @@ Section sigT. destruct p; reflexivity. Defined. - (** Equality of [sigT] is itself a [sigT] *) + (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *) Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : { p : u1 = v1 & rew p in u2 = v2 }) : existT _ u1 u2 = existT _ v1 v2. @@ -252,6 +252,7 @@ Section sigT. destruct p; reflexivity. Defined. + (** Equality of [sigT] is itself a [sigT] (backwards-reasoning version) *) Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a }) (pq : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }) : u = v. @@ -318,16 +319,19 @@ End sigT. (** Equality for [sig] *) Section sig. Local Unset Implicit Arguments. + (** Projecting an equality of a pair to equality of the first components *) Definition proj1_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) : proj1_sig u = proj1_sig v := f_equal (@proj1_sig _ _) p. + (** Projecting an equality of a pair to equality of the second components *) Definition proj2_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) : rew proj1_sig_eq p in proj2_sig u = proj2_sig v. Proof. destruct p; reflexivity. Defined. + (** Equality of [sig] is itself a [sig] (forwards-reasoning version) *) Definition eq_exist_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : { p : u1 = v1 | rew p in u2 = v2 }) : exist _ u1 u2 = exist _ v1 v2. @@ -337,6 +341,7 @@ Section sig. destruct p; reflexivity. Defined. + (** Equality of [sig] is itself a [sig] (backwards-reasoning version) *) Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (pq : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }) : u = v. @@ -345,11 +350,13 @@ Section sig. apply eq_exist_uncurried; exact pq. Defined. + (** Curried version of proving equality of sigma types *) Definition eq_sig {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) : u = v := eq_sig_uncurried u v (exist _ p q). + (** Induction principle for [@eq (sig _)] *) Definition eq_sig_rect {A P} {u v : { a : A | P a }} (Q : u = v -> Type) (f : forall p q, Q (eq_sig u v p q)) : forall p, Q p. @@ -357,12 +364,16 @@ Section sig. Definition eq_sig_rec {A P u v} (Q : u = v :> { a : A | P a } -> Set) := eq_sig_rect Q. Definition eq_sig_ind {A P u v} (Q : u = v :> { a : A | P a } -> Prop) := eq_sig_rec Q. + (** Equality of [sig] when the property is an hProp *) Definition eq_sig_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A | P a }) (p : proj1_sig u = proj1_sig v) : u = v := eq_sig u v p (P_hprop _ _ _). + (** Equivalence of equality of [sig] with a [sig] of equality *) + (** We could actually prove an isomorphism here, and not just [<->], + but for simplicity, we don't. *) Definition eq_sig_uncurried_iff {A} {P : A -> Prop} (u v : { a : A | P a }) : u = v <-> { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }. @@ -370,6 +381,7 @@ Section sig. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig_uncurried ]. Defined. + (** Equivalence of equality of [sig] involving hProps with equality of the first components *) Definition eq_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A | P a }) : u = v <-> (proj1_sig u = proj1_sig v) @@ -413,7 +425,7 @@ Section sigT2. destruct p; reflexivity. Defined. - (** Equality of [sigT2] is itself a [sigT2] *) + (** Equality of [sigT2] is itself a [sigT2] (forwards-reasoning version) *) Definition eq_existT2_uncurried {A : Type} {P Q : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} (pqr : { p : u1 = v1 @@ -425,6 +437,7 @@ Section sigT2. reflexivity. Defined. + (** Equality of [sigT2] is itself a [sigT2] (backwards-reasoning version) *) Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) (pqr : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }) @@ -528,7 +541,7 @@ Section sig2. destruct p; reflexivity. Defined. - (** Equality of [sig2] is itself a [sig2] *) + (** Equality of [sig2] is itself a [sig2] (fowards-reasoning version) *) Definition eq_exist2_uncurried {A} {P Q : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} (pqr : { p : u1 = v1 @@ -540,6 +553,7 @@ Section sig2. reflexivity. Defined. + (** Equality of [sig2] is itself a [sig2] (backwards-reasoning version) *) Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a }) (pqr : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }) -- cgit v1.2.3 From 37ff7235fe4d489a35458bb12abdf497480cf5c5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 May 2017 16:38:52 -0400 Subject: Make new proofs of equality Qed As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461 --- theories/Init/Logic.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 845b8ee9f..4c0c18772 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -507,7 +507,7 @@ Defined. Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x). Proof. reflexivity. -Defined. +Qed. Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e'). Proof. @@ -531,13 +531,13 @@ Lemma eq_trans_rew_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k: rew (eq_trans e e') in k = rew e' in rew e in k. Proof. destruct e, e'; reflexivity. -Defined. +Qed. Lemma rew_const : forall A P (x y:A) (e:x=y) (k:P), rew [fun _ => P] e in k = k. Proof. destruct e; reflexivity. -Defined. +Qed. (* Aliases *) -- cgit v1.2.3 From c6a05d73fc195cc7d5ffb62f2109617701d4791c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 May 2017 16:40:31 -0400 Subject: Make theorems about ex equality Qed As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461 --- theories/Init/Logic.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4c0c18772..1cd2f4cde 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -660,7 +660,7 @@ Section ex. destruct pq as [p q]. destruct q; simpl in *. destruct p; reflexivity. - Defined. + Qed. Definition eq_ex {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1) (p : u1 = v1) (q : rew p in u2 = v2) @@ -686,7 +686,7 @@ Section ex. end. Proof. destruct H, u; reflexivity. - Defined. + Qed. End ex. (** Equality for [ex2] *) @@ -702,7 +702,7 @@ Section ex2. destruct pq as [p q r]. destruct r, q, p; simpl in *. reflexivity. - Defined. + Qed. Definition eq_ex2 {A : Type} {P Q : A -> Prop} (u1 v1 : A) @@ -740,5 +740,5 @@ Section ex2. end. Proof. destruct H, u; reflexivity. - Defined. + Qed. End ex2. -- cgit v1.2.3 From 08751d1328c11a6e1a8427a12970587b12b9878a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 May 2017 16:51:37 -0400 Subject: Use the rew dependent notation in ex, ex2 proofs --- theories/Init/Logic.v | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 1cd2f4cde..4db11ae77 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -650,6 +650,13 @@ Qed. Declare Left Step iff_stepl. Declare Right Step iff_trans. +Local Notation "'rew' 'dependent' H 'in' H'" + := (match H with + | eq_refl => H' + end) + (at level 10, H' at level 10, + format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'"). + (** Equality for [ex] *) Section ex. Local Unset Implicit Arguments. @@ -680,9 +687,7 @@ Section ex. => ex_intro (Q y) (rew H in u1) - match H in (_ = y) return Q y (rew H in u1) with - | eq_refl => u2 - end + (rew dependent H in u2) end. Proof. destruct H, u; reflexivity. @@ -731,12 +736,8 @@ Section ex2. (Q y) (R y) (rew H in u1) - match H in (_ = y) return Q y (rew H in u1) with - | eq_refl => u2 - end - match H in (_ = y) return R y (rew H in u1) with - | eq_refl => u3 - end + (rew dependent H in u2) + (rew dependent H in u3) end. Proof. destruct H, u; reflexivity. -- cgit v1.2.3 From 3451053f94daa436150f9630dd1746c768ea37f9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 25 May 2017 14:59:16 -0400 Subject: Give explicit proof terms to proj2_sig_eq etc. --- theories/Init/Specif.v | 36 ++++++++++++------------------------ 1 file changed, 12 insertions(+), 24 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2555276e4..a1406bb53 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -237,10 +237,8 @@ Section sigT. (** Projecting an equality of a pair to equality of the second components *) Definition projT2_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v) - : rew projT1_eq p in projT2 u = projT2 v. - Proof. - destruct p; reflexivity. - Defined. + : rew projT1_eq p in projT2 u = projT2 v + := rew dependent p in eq_refl. (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *) Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} @@ -326,10 +324,8 @@ Section sig. (** Projecting an equality of a pair to equality of the second components *) Definition proj2_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) - : rew proj1_sig_eq p in proj2_sig u = proj2_sig v. - Proof. - destruct p; reflexivity. - Defined. + : rew proj1_sig_eq p in proj2_sig u = proj2_sig v + := rew dependent p in eq_refl. (** Equality of [sig] is itself a [sig] (forwards-reasoning version) *) Definition eq_exist_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} @@ -413,17 +409,13 @@ Section sigT2. (** Projecting an equality of a pair to equality of the second components *) Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) - : rew projT1_of_sigT2_eq p in projT2 u = projT2 v. - Proof. - destruct p; reflexivity. - Defined. + : rew projT1_of_sigT2_eq p in projT2 u = projT2 v + := rew dependent p in eq_refl. (** Projecting an equality of a pair to equality of the third components *) Definition projT3_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) - : rew projT1_of_sigT2_eq p in projT3 u = projT3 v. - Proof. - destruct p; reflexivity. - Defined. + : rew projT1_of_sigT2_eq p in projT3 u = projT3 v + := rew dependent p in eq_refl. (** Equality of [sigT2] is itself a [sigT2] (forwards-reasoning version) *) Definition eq_existT2_uncurried {A : Type} {P Q : A -> Type} @@ -529,17 +521,13 @@ Section sig2. (** Projecting an equality of a pair to equality of the second components *) Definition proj2_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) - : rew proj1_sig_of_sig2_eq p in proj2_sig u = proj2_sig v. - Proof. - destruct p; reflexivity. - Defined. + : rew proj1_sig_of_sig2_eq p in proj2_sig u = proj2_sig v + := rew dependent p in eq_refl. (** Projecting an equality of a pair to equality of the third components *) Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) - : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v. - Proof. - destruct p; reflexivity. - Defined. + : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v + := rew dependent p in eq_refl. (** Equality of [sig2] is itself a [sig2] (fowards-reasoning version) *) Definition eq_exist2_uncurried {A} {P Q : A -> Prop} -- cgit v1.2.3 From 6547fc39a3d2a0e1b82921b0747c6eb2e76e6f3b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 25 May 2017 15:03:44 -0400 Subject: More uniform indentation of sigma lemmas --- theories/Init/Specif.v | 88 +++++++++++++++++++++++++------------------------- 1 file changed, 44 insertions(+), 44 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index a1406bb53..95734991d 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -232,18 +232,18 @@ 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 : { a : A & P a }} (p : u = v) - : projT1 u = projT1 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 : { a : A & P a }} (p : u = v) - : rew projT1_eq p in projT2 u = projT2 v + : rew projT1_eq p in projT2 u = projT2 v := rew dependent p in eq_refl. (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *) Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : { p : u1 = v1 & rew p in u2 = v2 }) - : existT _ u1 u2 = existT _ v1 v2. + : existT _ u1 u2 = existT _ v1 v2. Proof. destruct pq as [p q]. destruct q; simpl in *. @@ -253,7 +253,7 @@ Section sigT. (** Equality of [sigT] is itself a [sigT] (backwards-reasoning version) *) Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a }) (pq : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }) - : u = v. + : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. apply eq_existT_uncurried; exact pq. @@ -262,7 +262,7 @@ Section sigT. (** Curried version of proving equality of sigma types *) Definition eq_sigT {A : Type} {P : A -> Type} (u v : { a : A & P a }) (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v) - : u = v + : u = v := eq_sigT_uncurried u v (existT _ p q). (** Equality of [sigT] when the property is an hProp *) @@ -299,16 +299,16 @@ Section sigT. (** Non-dependent classification of equality of [sigT] *) Definition eq_sigT_nondep {A B : Type} (u v : { a : A & B }) (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) - : u = v + : u = v := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q). (** Classification of transporting across an equality of [sigT]s *) Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x & Q x p }) {y} (H : x = y) - : rew [fun a => { p : P a & Q a p }] H in u - = existT - (Q y) - (rew H in projT1 u) - (rew dependent H in (projT2 u)). + : rew [fun a => { p : P a & Q a p }] H in u + = existT + (Q y) + (rew H in projT1 u) + (rew dependent H in (projT2 u)). Proof. destruct H, u; reflexivity. Defined. @@ -319,18 +319,18 @@ Section sig. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) Definition proj1_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) - : proj1_sig u = proj1_sig v + : proj1_sig u = proj1_sig v := f_equal (@proj1_sig _ _) p. (** Projecting an equality of a pair to equality of the second components *) Definition proj2_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) - : rew proj1_sig_eq p in proj2_sig u = proj2_sig v + : rew proj1_sig_eq p in proj2_sig u = proj2_sig v := rew dependent p in eq_refl. (** Equality of [sig] is itself a [sig] (forwards-reasoning version) *) Definition eq_exist_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : { p : u1 = v1 | rew p in u2 = v2 }) - : exist _ u1 u2 = exist _ v1 v2. + : exist _ u1 u2 = exist _ v1 v2. Proof. destruct pq as [p q]. destruct q; simpl in *. @@ -340,7 +340,7 @@ Section sig. (** Equality of [sig] is itself a [sig] (backwards-reasoning version) *) Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (pq : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }) - : u = v. + : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. apply eq_exist_uncurried; exact pq. @@ -349,7 +349,7 @@ Section sig. (** Curried version of proving equality of sigma types *) Definition eq_sig {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) - : u = v + : u = v := eq_sig_uncurried u v (exist _ p q). (** Induction principle for [@eq (sig _)] *) @@ -384,11 +384,11 @@ Section sig. := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v). Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x | Q x p }) {y} (H : x = y) - : rew [fun a => { p : P a | Q a p }] H in u - = exist - (Q y) - (rew H in proj1_sig u) - (rew dependent H in proj2_sig u). + : rew [fun a => { p : P a | Q a p }] H in u + = exist + (Q y) + (rew H in proj1_sig u) + (rew dependent H in proj2_sig u). Proof. destruct H, u; reflexivity. Defined. @@ -409,12 +409,12 @@ Section sigT2. (** Projecting an equality of a pair to equality of the second components *) Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) - : rew projT1_of_sigT2_eq p in projT2 u = projT2 v + : rew projT1_of_sigT2_eq p in projT2 u = projT2 v := rew dependent p in eq_refl. (** Projecting an equality of a pair to equality of the third components *) Definition projT3_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) - : rew projT1_of_sigT2_eq p in projT3 u = projT3 v + : rew projT1_of_sigT2_eq p in projT3 u = projT3 v := rew dependent p in eq_refl. (** Equality of [sigT2] is itself a [sigT2] (forwards-reasoning version) *) @@ -422,7 +422,7 @@ Section sigT2. {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} (pqr : { p : u1 = v1 & rew p in u2 = v2 & rew p in u3 = v3 }) - : existT2 _ _ u1 u2 u3 = existT2 _ _ v1 v2 v3. + : existT2 _ _ u1 u2 u3 = existT2 _ _ v1 v2 v3. Proof. destruct pqr as [p q r]. destruct r, q, p; simpl. @@ -433,7 +433,7 @@ Section sigT2. Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) (pqr : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }) - : u = v. + : u = v. Proof. destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. apply eq_existT2_uncurried; exact pqr. @@ -444,7 +444,7 @@ Section sigT2. (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v) (r : rew p in projT3 u = projT3 v) - : u = v + : u = v := eq_sigT2_uncurried u v (existT2 _ _ p q r). (** Equality of [sigT2] when the second property is an hProp *) @@ -461,7 +461,7 @@ Section sigT2. (u v : { a : A & P a & Q a }) : u = v <-> { p : projT1 u = projT1 v - & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }. + & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT2_uncurried ]. Defined. @@ -487,20 +487,20 @@ Section sigT2. (** Non-dependent classification of equality of [sigT] *) Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C }) (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v) - : u = v + : u = v := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). (** Classification of transporting across an equality of [sigT2]s *) Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) (u : { p : P x & Q x p & R x p }) {y} (H : x = y) - : rew [fun a => { p : P a & Q a p & R a p }] H in u - = existT2 - (Q y) - (R y) - (rew H in projT1 u) - (rew dependent H in projT2 u) - (rew dependent H in projT3 u). + : rew [fun a => { p : P a & Q a p & R a p }] H in u + = existT2 + (Q y) + (R y) + (rew H in projT1 u) + (rew dependent H in projT2 u) + (rew dependent H in projT3 u). Proof. destruct H, u; reflexivity. Defined. @@ -556,7 +556,7 @@ Section sig2. (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) (r : rew p in proj3_sig u = proj3_sig v) - : u = v + : u = v := eq_sig2_uncurried u v (exist2 _ _ p q r). (** Equality of [sig2] when the second property is an hProp *) @@ -599,20 +599,20 @@ Section sig2. (** Non-dependent classification of equality of [sig] *) Definition eq_sig2_nondep {A} {B C : Prop} (u v : @sig2 A (fun _ => B) (fun _ => C)) (p : proj1_sig u = proj1_sig v) (q : proj2_sig u = proj2_sig v) (r : proj3_sig u = proj3_sig v) - : u = v + : u = v := @eq_sig2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). (** Classification of transporting across an equality of [sig2]s *) Lemma rew_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) (u : { p : P x | Q x p & R x p }) {y} (H : x = y) - : rew [fun a => { p : P a | Q a p & R a p }] H in u - = exist2 - (Q y) - (R y) - (rew H in proj1_sig u) - (rew dependent H in proj2_sig u) - (rew dependent H in proj3_sig u). + : rew [fun a => { p : P a | Q a p & R a p }] H in u + = exist2 + (Q y) + (R y) + (rew H in proj1_sig u) + (rew dependent H in proj2_sig u) + (rew dependent H in proj3_sig u). Proof. destruct H, u; reflexivity. Defined. -- cgit v1.2.3