aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--test-suite/success/InversionSigma.v30
-rw-r--r--theories/Init/Tactics.v39
2 files changed, 69 insertions, 0 deletions
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.