Notion of (in)finite predicates

As discussed in iris!217 (merged)

I have directly taken the opportunity to state set_finite using the new pred_finite.

theories/fin_sets.v

@@ -35,6 +35,10 @@ Proof.
 Defined.
 
 (** * The [elements] operation *)
+Global Instance set_unfold_elements X x P :
+  SetUnfold (x ∈ X) P → SetUnfold (x ∈ elements X) P.
+Proof. constructor. by rewrite elem_of_elements, (set_unfold (x ∈ X) P). Qed.
+
 Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
 Proof.
   intros ?? E. apply NoDup_Permutation.
@@ -321,4 +325,21 @@ Proof.
  refine (cast_if (decide (Exists P (elements X))));
    by rewrite set_Exists_elements.
 Defined.
+
+(** Alternative versions of finite and infinite predicates *)
+Lemma pred_finite_set (P : A → Prop) :
+  pred_finite P ↔ (∃ X : C, ∀ x, P x → x ∈ X).
+Proof.
+  split.
+  - intros [xs Hfin]. exists (list_to_set xs). set_solver.
+  - intros [X Hfin]. exists (elements X). set_solver.
+Qed.
+
+Lemma pred_infinite_set (P : A → Prop) :
+  pred_infinite P ↔ (∀ X : C, ∃ x, P x ∧ x ∉ X).
+Proof.
+  split.
+  - intros Hinf X. destruct (Hinf (elements X)). set_solver.
+  - intros Hinf xs. destruct (Hinf (list_to_set xs)). set_solver.
+Qed.
 End fin_set.