Commit a9173997 authored by Robbert Krebbers's avatar Robbert Krebbers

Improve leibniz_equiv and f_equiv.

It now turns setoid equalities into Leibniz equalities when possible,
and substitutes those.
parent 0a877c71
......@@ -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]
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment