From e49c4aa0d320854dc4d4f16ddc2679d64adc8b39 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 26 Nov 2018 15:33:32 +0100
Subject: [PATCH] Commonly used variant of `singleton_included` when the
 element is exclusive.

---
 theories/algebra/gmap.v        | 7 +++++++
 theories/heap_lang/proph_map.v | 6 ++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index ef26c1a77..835c77941 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -278,6 +278,13 @@ Proof.
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
     + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
+Lemma singleton_included_exclusive m i x :
+  Exclusive x → ✓ m →
+  {[ i := x ]} ≼ m ↔ m !! i ≡ Some x.
+Proof.
+  intros ? Hm. rewrite singleton_included. split; last by eauto.
+  intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
+Qed.
 
 Global Instance singleton_cancelable i x :
   Cancelable (Some x) → Cancelable {[ i := x ]}.
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 21d9858d3..cb03d7717 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -121,10 +121,8 @@ Section to_proph_map.
   Lemma proph_map_singleton_included R p v :
     {[p := Excl v]} ≼ to_proph_map R → R !! p = Some v.
   Proof.
-    rewrite singleton_included=> -[v' []].
-    rewrite /to_proph_map lookup_fmap fmap_Some_equiv=> -[v'' [Hp ->]].
-    intros [=->]%Some_included_exclusive%leibniz_equiv_iff; first done; last done.
-    apply excl_exclusive.
+    rewrite singleton_included_exclusive; last by apply to_proph_map_valid.
+    by rewrite leibniz_equiv_iff /to_proph_map lookup_fmap fmap_Some=> -[v' [-> [->]]].
   Qed.
 End to_proph_map.
 
-- 
GitLab