From a917399700a52f98d95fe6753506cbc1d0d2442c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Feb 2016 13:34:32 +0100
Subject: [PATCH] Improve leibniz_equiv and f_equiv.
It now turns setoid equalities into Leibniz equalities when possible,
and substitutes those.
---
theories/tactics.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index ef7d365b..a9a76e87 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -188,6 +188,7 @@ Tactic Notation "simplify_eq" := repeat
| H : ?x = _ |- _ => subst x
| H : _ = ?x |- _ => subst x
| H : _ = _ |- _ => discriminate H
+ | H : _ ≡ _ |- _ => apply leibniz_equiv in H
| H : ?f _ = ?f _ |- _ => apply (inj f) in H
| H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H
(* before [injection] to circumvent bug #2939 in some situations *)
@@ -237,7 +238,7 @@ Ltac f_equiv :=
| |- pointwise_relation _ _ _ _ => intros ?
end;
(* Normalize away equalities. *)
- subst;
+ simplify_eq;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try match goal with
| _ => first [ reflexivity | assumption | symmetry; assumption]
--
GitLab