Add generalized implication lemma for big_sepM

iris/bi/big_op.v

@@ -1450,6 +1450,73 @@ Lemma big_sepM_sep_zip `{Countable K} {A B}
   ([∗ map] k↦x ∈ m1, Φ1 k x) ∗ ([∗ map] k↦y ∈ m2, Φ2 k y).
 Proof. apply big_opM_sep_zip. Qed.
 
+Lemma big_sepM_impl_foo `{Countable K} {A B} Φ `{∀ k x, Affine (Φ k x)}
+      (Ψ : K → B → PROP) m1 (m2 : gmap K B) :
+  ([∗ map] k↦x ∈ m1, Φ k x) -∗
+  □ (∀ (k : K) (y : B), ⌜m2 !! k = Some y⌝ →
+      ((∃ (x : A), ⌜m1 !! k = Some x⌝ ∧ Φ k x) ∨ ⌜m1 !! k = None⌝) -∗ Ψ k y) -∗
+  [∗ map] k↦y ∈ m2, Ψ k y.
+Proof.
+  revert m1. induction m2 as [|i y m ? IH] using map_ind=> m1.
+  - apply wand_intro_r. rewrite big_sepM_empty. apply: affine.
+  - apply wand_intro_r.
+    rewrite big_sepM_insert; last done.
+    rewrite intuitionistically_sep_dup.
+    rewrite assoc. rewrite (comm _ _ (□ _))%I.
+    rewrite {1}intuitionistically_elim {1}(forall_elim i) {1}(forall_elim y).
+    rewrite lookup_insert pure_True // left_id.
+    destruct (m1 !! i) as [x|] eqn:Hl.
+    + rewrite -or_intro_l -(exist_intro x).
+      rewrite pure_True // left_id.
+      rewrite big_sepM_delete; last apply Hl.
+      rewrite assoc assoc wand_elim_l -assoc.
+      apply sep_mono_r.
+      specialize (IH (delete i m1)). apply wand_elim_l' in IH. rewrite -IH.
+      apply sep_mono_r.
+      apply intuitionistically_intro'. rewrite intuitionistically_elim.
+      apply forall_intro=> k. apply forall_intro=> b.
+      rewrite (forall_elim k) (forall_elim b).
+      apply impl_intro_l, pure_elim_l=> ?.
+      assert (i ≠ k) by congruence.
+      rewrite lookup_insert_ne // pure_True // left_id.
+      rewrite lookup_delete_ne //.
+    + rewrite -or_intro_r.
+      rewrite impl_wand_2.
+      rewrite pure_True // left_id.
+      apply sep_mono_r.
+      specialize (IH m1). apply wand_elim_l' in IH. rewrite -IH.
+      apply sep_mono_r.
+      apply intuitionistically_intro'. rewrite intuitionistically_elim.
+      apply forall_intro=> k. apply forall_intro=> b.
+      rewrite (forall_elim k) (forall_elim b).
+      apply impl_intro_l, pure_elim_l=> ?.
+      rewrite lookup_insert_ne; last congruence.
+      rewrite pure_True // left_id //.
+Qed.
+
+Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
+      Φ `{∀ k x, Affine (Φ k x)} (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
+  dom (gset _) m2 ⊆ dom _ m1 →
+  ([∗ map] k↦x ∈ m1, Φ k x) -∗
+  □ (∀ (k : K) (x : A) (y : B),
+      ⌜m1 !! k = Some x⌝ → ⌜m2 !! k = Some y⌝ → Φ k x -∗ Ψ k y) -∗
+  [∗ map] k↦y ∈ m2, Ψ k y.
+Proof.
+  intros Hsub. rewrite big_sepM_impl_foo.
+  apply wand_mono; last done.
+  apply intuitionistically_intro'. rewrite intuitionistically_elim.
+  apply forall_intro=> k. apply forall_intro=> y.
+  apply impl_intro_l, pure_elim_l=> look.
+  apply wand_intro_r. apply wand_elim_r'.
+  apply or_elim.
+  - apply exist_elim=> x. apply pure_elim_l=> ?.
+    rewrite (forall_elim k) (forall_elim x) (forall_elim y).
+    do 2 rewrite pure_True // left_id.
+    apply wand_intro_l. apply wand_elim_l.
+  - rewrite -not_elem_of_dom. apply pure_elim'=> ?.
+    apply elem_of_dom_2 in look. set_solver.
+Qed.
+
 (** ** Big ops over two maps *)
 Lemma big_sepM2_alt `{Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
   ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊣⊢