From e18fe0f6dae676f8aeb5b921f74fc4b65c4c9adf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Feb 2019 19:21:11 +0100
Subject: [PATCH] Alternative versions of finite/infinite predicates in terms
 of sets.

---
 theories/fin_sets.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 932ff62f..588b58af 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -325,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.
-- 
GitLab