Commit 714cc8ca 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 c59e1f85
Pipeline #169 passed with stage
......@@ -47,7 +47,7 @@ Section heap.
(** Conversion to heaps and back *)
Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
Proof. by intros ??; fold_leibniz=>->. Qed.
Proof. solve_proper. Qed.
Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
Proof.
apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
......@@ -96,7 +96,7 @@ Section heap.
(** Propers *)
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
Proof. solve_proper. Qed.
(** General properties of mapsto *)
Lemma heap_mapsto_disjoint l v1 v2 : (l v1 l v2)%I False.
......
......@@ -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