From db2eced3613819474ceb9f0bb56114dfdfa9daea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 15:37:17 +0200
Subject: [PATCH] Lemma for inclusion of singleton gmaps.

We only had the step-indexed version before. Unfortunately, the non
step-indexed version does not follow from the step-indexed version.
---
 algebra/gmap.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/algebra/gmap.v b/algebra/gmap.v
index c33b1905e..d43d6611e 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -264,6 +264,23 @@ Proof.
       * by rewrite Hi lookup_op lookup_singleton lookup_delete.
       * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
 Qed.
+(* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *)
+Lemma singleton_included m i x :
+  {[ i := x ]} ≼ m ↔ ∃ y, m !! i ≡ Some y ∧ (x ≼ y ∨ x ≡ y).
+Proof.
+  split.
+  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
+    case (m' !! i)=> [y|]=> Hm.
+    + exists (x â‹… y); eauto using cmra_included_l.
+    + exists x; eauto.
+  - intros (y&Hi&[[z ?]| ->]).
+    + exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
+      * rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
+      * by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
+    + exists (delete i m)=> j; destruct (decide (i = j)) as [->|].
+      * by rewrite Hi lookup_op lookup_singleton lookup_delete.
+      * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
+Qed.
 
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
   x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
-- 
GitLab