Merge branch 'ralf/gmap_view_alloc_big' into 'master'

add gmap_view_alloc_big

See merge request iris/iris!598

iris/algebra/lib/gmap_view.v

 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,21 @@ 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.
+    intros. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
+    { rewrite big_opM_empty left_id_L right_id. done. }
+    etrans; first by apply IH.
+    rewrite big_opM_insert // assoc.
+    apply cmra_update_op; last done.
+    rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); last done.
+    by apply lookup_union_None.
+  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).