Merge branch 'robbert/pred_infinite' into 'master'

Notion of (in)finite predicates

See merge request !56

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.

theories/sets.v

@@ -990,17 +990,39 @@ Section set_monad.
 End set_monad.
 
 (** Finite sets *)
-Definition set_finite `{ElemOf A B} (X : B) := ∃ l : list A, ∀ x, x ∈ X → x ∈ l.
+Definition pred_finite {A} (P : A → Prop) := ∃ xs : list A, ∀ x, P x → x ∈ xs.
+Definition set_finite `{ElemOf A B} (X : B) := pred_finite (∈ X).
 
-Section finite.
+Definition pred_infinite {A} (P : A → Prop) := ∀ xs : list A, ∃ x, P x ∧ x ∉ xs.
+Definition set_infinite `{ElemOf A C} (X : C) := pred_infinite (∈ X).
+
+Section pred_finite_infinite.
+  Lemma pred_finite_impl {A} (P Q : A → Prop) :
+    pred_finite P → (∀ x, Q x → P x) → pred_finite Q.
+  Proof. unfold pred_finite. set_solver. Qed.
+
+  Lemma pred_infinite_impl {A} (P Q : A → Prop) :
+    pred_infinite P → (∀ x, P x → Q x) → pred_infinite Q.
+  Proof. unfold pred_infinite. set_solver. Qed.
+
+  Lemma pred_not_infinite_finite {A} (P : A → Prop) :
+    pred_infinite P → pred_finite P → False.
+  Proof. intros Hinf [xs ?]. destruct (Hinf xs). set_solver. Qed.
+End pred_finite_infinite.
+
+Section set_finite_infinite.
   Context `{SemiSet A C}.
   Implicit Types X Y : C.
 
+  Lemma set_not_infinite_finite X : set_infinite X → set_finite X → False.
+  Proof. apply pred_not_infinite_finite. Qed.
+
   Global Instance set_finite_subseteq :
     Proper (flip (⊆) ==> impl) (@set_finite A C _).
-  Proof. intros X Y HX [l Hl]; exists l; set_solver. Qed.
+  Proof. intros X Y HX ?. eapply pred_finite_impl; set_solver. Qed.
   Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A C _).
   Proof. intros X Y HX; apply exist_proper. by setoid_rewrite HX. Qed.
+
   Lemma empty_finite : set_finite (∅ : C).
   Proof. by exists []; intros ?; rewrite elem_of_empty. Qed.
   Lemma singleton_finite (x : A) : set_finite ({[ x ]} : C).
@@ -1014,7 +1036,18 @@ Section finite.
   Proof. intros [l ?]; exists l; set_solver. Qed.
   Lemma union_finite_inv_r X Y : set_finite (X ∪ Y) → set_finite Y.
   Proof. intros [l ?]; exists l; set_solver. Qed.
-End finite.
+
+  Global Instance set_infinite_subseteq :
+    Proper ((⊆) ==> impl) (@set_infinite A C _).
+  Proof. intros X Y HX ?. eapply pred_infinite_impl; set_solver. Qed.
+  Global Instance set_infinite_proper : Proper ((≡) ==> iff) (@set_infinite A C _).
+  Proof. intros X Y HX; apply forall_proper. by setoid_rewrite HX. Qed.
+
+  Lemma union_infinite_l X Y : set_infinite X → set_infinite (X ∪ Y).
+  Proof. intros Hinf xs. destruct (Hinf xs). set_solver. Qed.
+  Lemma union_infinite_r X Y : set_infinite Y → set_infinite (X ∪ Y).
+  Proof. intros Hinf xs. destruct (Hinf xs). set_solver. Qed.
+End set_finite_infinite.
 
 Section more_finite.
   Context `{Set_ A C}.
@@ -1032,6 +1065,10 @@ Section more_finite.
     intros [l ?] [k ?]; exists (l ++ k).
     intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; set_solver.
   Qed.
+
+  Lemma difference_infinite X Y :
+    set_infinite X → set_finite Y → set_infinite (X ∖ Y).
+  Proof. intros Hinf [xs ?] xs'. destruct (Hinf (xs ++ xs')). set_solver. Qed.
 End more_finite.
 
 (** Sets of sequences of natural numbers *)