More properties and set_solver for filter.

base_logic/big_op.v

@@ -472,6 +472,19 @@ Section gset.
   Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
   Proof. apply: big_opS_singleton. Qed.
 
+  Lemma big_sepS_filter (P : A → Prop) `{∀ x, Decision (P x)} Φ X :
+    ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ■ P y → Φ y).
+  Proof.
+    induction X as [|x X ? IH] using collection_ind_L.
+    { by rewrite filter_empty_L !big_sepS_empty. }
+    destruct (decide (P x)).
+    - rewrite filter_union_L filter_singleton_L //.
+      rewrite !big_sepS_insert //; last set_solver.
+      by rewrite IH pure_True // left_id.
+    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
+      by rewrite !big_sepS_insert // IH pure_False // False_impl left_id.
+  Qed.
+
   Lemma big_sepS_sepS Φ Ψ X :
     ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y).
   Proof. apply: big_opS_opS. Qed.

prelude/fin_collections.v

@@ -14,6 +14,7 @@ Definition collection_fold `{Elements A C} {B}
 Instance collection_filter
     `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
   of_list (filter P (elements X)).
+Typeclasses Opaque collection_filter.
 
 Section fin_collection.
 Context `{FinCollection A C}.
@@ -211,12 +212,41 @@ Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
 Proof. unfold_leibniz. apply (minimal_exists R). Qed.
 
 (** * Filter *)
-Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
-  x ∈ filter P X ↔ P x ∧ x ∈ X.
-Proof.
-  unfold filter, collection_filter.
-  by rewrite elem_of_of_list, elem_of_list_filter, elem_of_elements.
-Qed.
+Section filter.
+  Context (P : A → Prop) `{!∀ x, Decision (P x)}.
+
+  Lemma elem_of_filter X x : x ∈ filter P X ↔ P x ∧ x ∈ X.
+  Proof.
+    unfold filter, collection_filter.
+    by rewrite elem_of_of_list, elem_of_list_filter, elem_of_elements.
+  Qed.
+  Global Instance set_unfold_filter X Q :
+    SetUnfold (x ∈ X) Q → SetUnfold (x ∈ filter P X) (P x ∧ Q).
+  Proof.
+    intros ??; constructor. by rewrite elem_of_filter, (set_unfold (x ∈ X) Q).
+  Qed.
+
+  Lemma filter_empty : filter P (∅:C) ≡ ∅.
+  Proof. set_solver. Qed.
+  Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
+  Proof. set_solver. Qed.
+  Lemma filter_singleton x : P x → filter P ({[ x ]} : C) ≡ {[ x ]}.
+  Proof. set_solver. Qed.
+  Lemma filter_singleton_not x : ¬P x → filter P ({[ x ]} : C) ≡ ∅.
+  Proof. set_solver. Qed.
+
+  Section leibniz_equiv.
+    Context `{!LeibnizEquiv C}.
+    Lemma filter_empty_L : filter P (∅:C) = ∅.
+    Proof. set_solver. Qed.
+    Lemma filter_union_L X Y : filter P (X ∪ Y) = filter P X ∪ filter P Y.
+    Proof. set_solver. Qed.
+    Lemma filter_singleton_L x : P x → filter P ({[ x ]} : C) = {[ x ]}.
+    Proof. set_solver. Qed.
+    Lemma filter_singleton_not_L x : ¬P x → filter P ({[ x ]} : C) = ∅.
+    Proof. set_solver. Qed.
+  End leibniz_equiv.
+End filter.
 
 (** * Decision procedures *)
 Global Instance set_Forall_dec `(P : A → Prop)