Merge branch 'ci/ralf/ghost-map-big' into 'master'

Add big-op lemmas to ghost map

See merge request iris/iris!649

iris/base_logic/lib/ghost_map.v

@@ -175,7 +175,7 @@ Section lemmas.
   Qed.
 
   (** * Lemmas about the interaction of [ghost_map_auth] with the elements *)
-  Lemma ghost_map_lookup k γ q m dq v :
+  Lemma ghost_map_lookup {γ q m k dq v} :
     ghost_map_auth γ q m -∗ k ↪[γ]{dq} v -∗ ⌜m !! k = Some v⌝.
   Proof.
     unseal. iIntros "Hauth Hel".
@@ -215,4 +215,81 @@ Section lemmas.
     rewrite insert_delete. eauto.
   Qed.
 
+  (** Derived big-op versions of above lemmas *)
+  Lemma ghost_map_lookup_big {γ q m} m0 :
+    ghost_map_auth γ q m -∗
+    ([∗ map] k↦v ∈ m0, k ↪[γ] v) -∗
+    ⌜m0 ⊆ m⌝.
+  Proof.
+    iInduction m0 as [|k v m0 Hk IH] "IH" using map_ind.
+    { iIntros "_ _". iPureIntro. apply map_empty_subseteq. }
+    rewrite big_sepM_insert //. iIntros "Hauth [Helem Hm0]".
+    iDestruct (ghost_map_lookup with "Hauth Helem") as %Helem.
+    iDestruct ("IH" with "Hauth Hm0") as %Hm0.
+    iPureIntro. apply insert_subseteq_l; done.
+  Qed.
+
+  Lemma ghost_map_insert_big {γ m} m' :
+    m' ##ₘ m →
+    ghost_map_auth γ 1 m ==∗
+    ghost_map_auth γ 1 (m' ∪ m) ∗ ([∗ map] k ↦ v ∈ m', k ↪[γ] v).
+  Proof.
+    iInduction m' as [|k v m' Hk] "IH" using map_ind forall (m); iIntros (Hdisj) "Hm".
+    { rewrite left_id_L. auto. }
+    iMod ("IH" with "[] Hm") as "[Hm'm Hm']".
+    { iPureIntro. by eapply map_disjoint_insert_l. }
+    decompose_map_disjoint.
+    rewrite !big_opM_insert // -insert_union_l //.
+    by iMod (ghost_map_insert with "Hm'm") as "($ & $)";
+      first by apply lookup_union_None.
+  Qed.
+  Lemma ghost_map_insert_persist_big {γ m} m' :
+    m' ##ₘ m →
+    ghost_map_auth γ 1 m ==∗
+    ghost_map_auth γ 1 (m' ∪ m) ∗ ([∗ map] k ↦ v ∈ m', k ↪[γ]□ v).
+  Proof.
+    iIntros (Hdisj) "Hauth".
+    iMod (ghost_map_insert_big m' with "Hauth") as "[$ Helem]"; first done.
+    iApply big_sepM_bupd. iApply (big_sepM_impl with "Helem").
+    iIntros "!#" (k v) "_". iApply ghost_map_elem_persist.
+  Qed.
+
+  Lemma ghost_map_delete_big {γ m} m0 :
+    ghost_map_auth γ 1 m -∗
+    ([∗ map] k↦v ∈ m0, k ↪[γ] v) ==∗
+    ghost_map_auth γ 1 (m ∖ m0).
+  Proof.
+    iInduction m0 as [|k v m0 Hk IH] "IH" using map_ind.
+    { iIntros "Hauth _". rewrite right_id_L //. }
+    rewrite big_sepM_insert //. iIntros "Hauth [Helem Hm0]".
+    iMod ("IH" with "Hauth Hm0") as "Hauth".
+    iMod (ghost_map_delete with "Hauth Helem") as "Hauth".
+    rewrite -delete_difference. done.
+  Qed.
+
+  Theorem ghost_map_update_big {γ m} m0 m1 :
+    dom (gset K) m0 = dom (gset K) m1 →
+    ghost_map_auth γ 1 m -∗
+    ([∗ map] k↦v ∈ m0, k ↪[γ] v) ==∗
+    ghost_map_auth γ 1 (m1 ∪ m) ∗
+        [∗ map] k↦v ∈ m1, k ↪[γ] v.
+  Proof.
+    iIntros (Hdom%eq_sym) "Hauth Hm0".
+    iInduction m0 as [|k v m0 Hk] "IH" using map_ind forall (m m1 Hdom).
+    - rewrite dom_empty_L in Hdom.
+      apply dom_empty_inv_L in Hdom as ->.
+      rewrite left_id_L big_sepM_empty.
+      by iFrame.
+    - rewrite big_sepM_insert //.
+      iDestruct "Hm0" as "[Hl Hm0]".
+      rewrite dom_insert_L in Hdom.
+      assert (k ∈ dom (gset K) m1) as Hindom by set_solver.
+      apply elem_of_dom in Hindom as [v' Hlookup].
+      iMod (ghost_map_update v' with "Hauth Hl") as "[Hauth Hl]".
+      iMod ("IH" $! (<[k:=v']> m) (delete k m1) with "[%] Hauth Hm0") as "[Hauth Hm0]".
+      { apply (not_elem_of_dom (D:=gset K)) in Hk. set_solver. }
+      rewrite union_delete_insert //. iFrame. iClear "#".
+      iApply big_sepM_delete; first done. by iFrame.
+  Qed.
+
 End lemmas.