big_sepM_impl_strong returns leftover resources

iris/bi/big_op.v

@@ -1450,15 +1450,30 @@ 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) :
+Lemma map_filter_true_id `{Countable K} {A} (P : (K * A → Prop))
+      `{∀ (x : (K * A)), Decision (P x)} (m : gmap K A)
+  : (∀ k x, m !! k = Some x → P (k, x)) → filter P m = m.
+Proof.
+  intros Hi. induction m as [|i y m ? IH] using map_ind; [done|].
+  rewrite map_filter_insert.
+  - rewrite IH; [done|].
+    intros j ??. apply Hi. destruct (decide (i = j)); [naive_solver|].
+    apply lookup_insert_Some. naive_solver.
+  - apply Hi. by rewrite lookup_insert.
+Qed.
+
+Lemma big_sepM_impl_strong `{Countable K} {A B} Φ (Ψ : 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.
+  ([∗ map] k↦y ∈ m2, Ψ k y) ∗
+  ([∗ map] k↦x ∈ (filter (λ '(k, _), m2 !! k = None) m1), Φ k x).
 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_empty left_id.
+    rewrite intuitionistically_elim_emp right_id.
+    rewrite map_filter_true_id; done.
   - apply wand_intro_r.
     rewrite big_sepM_insert; last done.
     rewrite intuitionistically_sep_dup.
@@ -1469,40 +1484,52 @@ Proof.
     + 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.
+      rewrite assoc assoc wand_elim_l -assoc -assoc.
       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 //.
+      specialize (IH (delete i m1)). apply wand_elim_l' in IH.
+      erewrite map_filter_strong_ext.
+      * erewrite <- 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 //.
+      * simpl.
+        intros j x'. destruct (decide (i = j)).
+        { simplify_eq. rewrite lookup_delete lookup_insert. naive_solver. }
+        rewrite lookup_delete_ne // lookup_insert_ne //.
     + rewrite -or_intro_r.
       rewrite impl_wand_2.
-      rewrite pure_True // left_id.
+      rewrite pure_True // left_id -assoc.
       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 //.
+      specialize (IH m1). apply wand_elim_l' in IH.
+      erewrite map_filter_strong_ext.
+      * erewrite <- 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 //.
+      * intros i' x'. simpl.
+        destruct (decide (i = i')) as [?|neq]; first naive_solver.
+        by rewrite lookup_insert_ne.
 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) :
+      Φ (Ψ : 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.
+  ([∗ map] k↦y ∈ m2, Ψ k y) ∗
+  ([∗ map] k↦x ∈ (filter (λ '(k, _), m2 !! k = None) m1), Φ k x).
 Proof.
-  intros Hsub. rewrite big_sepM_impl_foo.
+  intros Hsub. rewrite big_sepM_impl_strong.
   apply wand_mono; last done.
   apply intuitionistically_intro'. rewrite intuitionistically_elim.
   apply forall_intro=> k. apply forall_intro=> y.