From 100690d58b016d715ef1ad974be4c29f7490c4f8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Dec 2020 19:48:09 +0100
Subject: [PATCH] add gmap_view_alloc_big

---
 iris/algebra/lib/gmap_view.v | 26 +++++++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index c56a8030e..30e814b62 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export view gmap dfrac.
-From iris.algebra Require Import local_updates proofmode_classes.
+From iris.algebra Require Import local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
 (** * CMRA for a "view of a gmap".
@@ -323,6 +323,30 @@ Section lemmas.
       rewrite lookup_insert_ne //.
   Qed.
 
+  Lemma gmap_view_alloc_big m m' dq :
+    m' ##ₘ m →
+    ✓ dq →
+    gmap_view_auth 1 m ~~>
+      gmap_view_auth 1 (m' ∪ m) ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
+  Proof.
+    revert m. induction m' as [|k v m'] using map_ind.
+    { intros m _. rewrite big_opM_empty left_id right_id. done. }
+    intros m Hdisj. etrans.
+    { apply IHm'; last done. eapply map_disjoint_weaken_l; first done.
+      apply insert_subseteq. done. }
+    etrans.
+    - eapply cmra_update_op; last reflexivity.
+      eapply (gmap_view_alloc _ k dq); last done.
+      apply lookup_union_None. split; first done.
+      eapply map_disjoint_Some_l; first done.
+      rewrite lookup_insert. done.
+    - (* Turn goal into "L ≡ R". *)
+      eapply cmra_update_proper; [reflexivity| |reflexivity].
+      rewrite -assoc. f_equiv.
+      + rewrite insert_union_l. done.
+      + rewrite big_opM_insert; last done. done.
+  Qed.
+
   Lemma gmap_view_delete m k v :
     gmap_view_auth 1 m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
     gmap_view_auth 1 (delete k m).
-- 
GitLab