diff options
author | Jason Gross <jagro@google.com> | 2016-09-05 11:23:23 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-09-05 11:27:34 -0700 |
commit | 585e14a6fe331539626a0ae2188aa51985c4f570 (patch) | |
tree | ee07c543d0e8102c1af8255ecefe11f531c57e98 | |
parent | 2deb16b97b4558d92e2a431b49f1168a9281732c (diff) |
Make [inversion_{prod,sigma}] stronger
It can now handle paths used in dependent places.
-rw-r--r-- | src/Util/Prod.v | 21 | ||||
-rw-r--r-- | src/Util/Sigma.v | 33 |
2 files changed, 48 insertions, 6 deletions
diff --git a/src/Util/Prod.v b/src/Util/Prod.v index 2d788aa32..39e32865f 100644 --- a/src/Util/Prod.v +++ b/src/Util/Prod.v @@ -54,9 +54,18 @@ Section prod. split; [ intro; subst; split; reflexivity | apply path_prod_uncurried ]. Defined. + (** *** Eta-expansion of [@eq (prod _ _)] *) Definition path_prod_eta {A B} {u v : @prod A B} (p : u = v) : p = path_prod_uncurried u v (fst_path p, snd_path p). Proof. destruct u, p; reflexivity. Defined. + + (** *** Induction principle for [@eq (prod _ _)] *) + Definition path_prod_rect {A B} {u v : @prod A B} (P : u = v -> Type) + (f : forall p q, P (path_prod_uncurried u v (p, q))) + : forall p, P p. + Proof. intro p; specialize (f (fst_path p) (snd_path p)); destruct u, p; exact f. Defined. + Definition path_prod_rec {A B u v} (P : u = v :> @prod A B -> Set) := path_prod_rect P. + Definition path_prod_ind {A B u v} (P : u = v :> @prod A B -> Prop) := path_prod_rec P. End prod. (** ** Useful Tactics *) @@ -68,9 +77,17 @@ Ltac simpl_proj_pair_in H := | context G[snd (pair ?x ?p)] => let G' := context G[p] in change G' in H end. +Ltac induction_path_prod H := + let H0 := fresh H in + let H1 := fresh H in + induction H as [H0 H1] using path_prod_rect; + simpl_proj_pair_in H0; + simpl_proj_pair_in H1. Ltac inversion_prod_step := match goal with - | [ H : pair _ _ = pair _ _ |- _ ] - => apply path_prod_uncurried_iff in H; simpl_proj_pair_in H; destruct H + | [ H : _ = pair _ _ |- _ ] + => induction_path_prod H + | [ H : pair _ _ = _ |- _ ] + => induction_path_prod H end. Ltac inversion_prod := repeat inversion_prod_step. diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 414919493..9259e1a1d 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -63,6 +63,14 @@ Section sigT. split; [ intro; subst; exists eq_refl; reflexivity | apply path_sigT_uncurried ]. Defined. + (** *** Induction principle for [@eq (sigT _)] *) + Definition path_sigT_rect {A P} {u v : @sigT A P} (Q : u = v -> Type) + (f : forall p q, Q (path_sigT u v p q)) + : forall p, Q p. + Proof. intro p; specialize (f (pr1_path p) (pr2_path p)); destruct u, p; exact f. Defined. + Definition path_sigT_rec {A P u v} (Q : u = v :> @sigT A P -> Set) := path_sigT_rect Q. + Definition path_sigT_ind {A P u v} (Q : u = v :> @sigT A P -> Prop) := path_sigT_rec Q. + (** *** Equivalence of equality of [sigT] involving hProps with equality of the first components *) Definition path_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : @sigT A P) @@ -116,6 +124,13 @@ Section sig. : u = v := path_sig_uncurried u v (exist _ p q). + Definition path_sig_rect {A P} {u v : @sig A P} (Q : u = v -> Type) + (f : forall p q, Q (path_sig u v p q)) + : forall p, Q p. + Proof. intro p; specialize (f (proj1_sig_path p) (proj2_sig_path p)); destruct u, p; exact f. Defined. + Definition path_sig_rec {A P u v} (Q : u = v :> @sig A P -> Set) := path_sig_rect Q. + Definition path_sig_ind {A P u v} (Q : u = v :> @sig A P -> Prop) := path_sig_rec Q. + Definition path_sig_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : @sig A P) (p : proj1_sig u = proj1_sig v) @@ -206,11 +221,21 @@ Ltac simpl_proj_exist_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 _ _ _ = exist _ _ _ |- _ ] - => apply path_sig_uncurried_iff in H; simpl_proj_exist_in H; destruct H - | [ H : existT _ _ _ = existT _ _ _ |- _ ] - => apply path_sigT_uncurried_iff in H; simpl_proj_exist_in H; destruct H + | [ H : _ = exist _ _ _ |- _ ] + => induction_sigma_in_using H @path_sig_rect + | [ H : _ = existT _ _ _ |- _ ] + => induction_sigma_in_using H @path_sigT_rect + | [ H : exist _ _ _ = _ |- _ ] + => induction_sigma_in_using H @path_sig_rect + | [ H : existT _ _ _ = _ |- _ ] + => induction_sigma_in_using H @path_sigT_rect end. Ltac inversion_sigma := repeat inversion_sigma_step. |