Make [inversion_{prod,sigma}] stronger

It can now handle paths used in dependent places.

1 files changed, 19 insertions, 2 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.