From 714cc8cabaa7d534a148637716444c9386ee12a8 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.
---
heap_lang/heap.v | 4 ++--
prelude/tactics.v | 3 ++-
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index d31ec3f44..b01ed8e61 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -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.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index fa51a9962..1b96ec4f0 100644
--- a/prelude/tactics.v
+++ b/prelude/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