Big ops and None.

algebra/cmra_big_op.v

@@ -375,6 +375,33 @@ Section gset.
 End gset.
 End big_op.
 
+(** Option *)
+Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
+  ([⋅ list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
+Proof.
+  revert f. induction l as [|x l IH]=> f //=.
+  rewrite big_opL_cons op_None IH. split.
+  - intros [??] [|k] y ?; naive_solver.
+  - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)).
+Qed.
+Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m :
+  ([⋅ map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
+Proof.
+  induction m as [|i x m ? IH] using map_ind=> //=.
+  rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
+  { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
+  intros Hm; split.
+  - apply (Hm i). by simplify_map_eq.
+  - intros k y ?. apply (Hm k). by simplify_map_eq.
+Qed.
+Lemma big_opS_None {M : cmraT} `{Countable A} (f : A → option M) X :
+  ([⋅ set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
+Proof.
+  induction X as [|x X ? IH] using collection_ind_L; [done|].
+  rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
+Qed.
+
+(** Commuting with respect to homomorphisms *)
 Lemma big_opL_commute {M1 M2 : ucmraT} {A} (h : M1 → M2)
     `{!UCMRAHomomorphism h} (f : nat → A → M1) l :
   h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)).