From 585e14a6fe331539626a0ae2188aa51985c4f570 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 11:23:23 -0700 Subject: Make [inversion_{prod,sigma}] stronger It can now handle paths used in dependent places. --- src/Util/Prod.v | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'src/Util/Prod.v') 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. -- cgit v1.2.3