FromPure instances for big_sepM

iris/bi/big_op.v

@@ -1181,6 +1181,37 @@ Section map.
     ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x).
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
+  Lemma big_sepM_pure_1 (φ : K → A → Prop) m :
+    ([∗ map] k↦x ∈ m, ⌜φ k x⌝) ⊢@{PROP} ⌜map_Forall φ m⌝.
+  Proof.
+    induction m using map_ind; simpl.
+    - rewrite pure_True; first by apply True_intro.
+      apply map_Forall_empty.
+    - rewrite -> big_sepM_insert by auto.
+      rewrite -> map_Forall_insert by auto.
+      rewrite IHm sep_and -pure_and.
+      apply pure_mono. done.
+  Qed.
+  Lemma big_sepM_affinely_pure_2 (φ : K → A → Prop) m :
+    <affine> ⌜map_Forall φ m⌝ ⊢@{PROP} ([∗ map] k↦x ∈ m, <affine> ⌜φ k x⌝).
+  Proof.
+    induction m using map_ind; simpl.
+    - rewrite big_sepM_empty. apply affinely_elim_emp.
+    - rewrite -> big_sepM_insert by auto.
+      rewrite -> map_Forall_insert by auto.
+      rewrite pure_and affinely_and IHm persistent_and_sep_1. done.
+  Qed.
+  (** The general backwards direction requires [BiAffine] to cover the empty case. *)
+  Lemma big_sepM_pure `{!BiAffine PROP} (φ : K → A → Prop) m :
+    ([∗ map] k↦x ∈ m, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜map_Forall φ m⌝.
+  Proof.
+    apply (anti_symm (⊢)); first by apply big_sepM_pure_1.
+    rewrite -(affine_affinely (⌜map_Forall φ m⌝)%I).
+    rewrite big_sepM_affinely_pure_2.
+    apply big_sepM_mono=>???.
+    rewrite affine_affinely. done.
+  Qed.
+
   Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
     (<pers> ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, <pers> (Φ k x)).
   Proof. apply (big_opM_commute _). Qed.
@@ -1292,6 +1323,7 @@ Section map.
   Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
   Proof. rewrite big_opM_eq. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
+
 End map.
 
 (* Some lemmas depend on the generalized versions of the above ones. *)

iris/proofmode/class_instances.v

@@ -198,6 +198,14 @@ Global Instance into_pure_persistently P φ :
   IntoPure P φ → IntoPure (<pers> P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
 
+Global Instance into_pure_big_sepM {K A} `{Countable K}
+    (Φ : K → A → PROP) (φ : K → A → Prop) (m: gmap K A) :
+  (∀ k v, IntoPure (Φ k v) (φ k v)) → IntoPure ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
+Proof.
+  rewrite /IntoPure. intros HΦ.
+  setoid_rewrite HΦ. rewrite big_sepM_pure_1. done.
+Qed.
+
 (** FromPure *)
 Global Instance from_pure_emp : @FromPure PROP true emp True.
 Proof. rewrite /FromPure /=. apply (affine _). Qed.
@@ -289,6 +297,20 @@ Proof.
   by rewrite -persistent_absorbingly_affinely_2.
 Qed.
 
+Global Instance from_pure_big_sepM {K A} `{Countable K}
+    a (Φ : K → A → PROP) (φ : K → A → Prop) (m: gmap K A) :
+  (∀ k v, FromPure a (Φ k v) (φ k v)) →
+  TCOr (TCEq a true) (BiAffine PROP) →
+  FromPure a ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
+Proof.
+  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
+  - rewrite big_sepM_affinely_pure_2.
+    setoid_rewrite HΦ. done.
+  - destruct Haffine as [?%TCEq_eq|?]; first done.
+    rewrite -big_sepM_pure.
+    setoid_rewrite HΦ. done.
+Qed.
+
 (** IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
   IntoPersistent true P Q → IntoPersistent p (<pers> P) Q | 0.