From f31e57b620562722079c20363be4aa9c6f128a71 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 22 Nov 2016 23:35:49 +0100
Subject: [PATCH] More set_Forall and set_Exists stuff for finite sets.

---
 prelude/fin_collections.v | 36 ++++++++++++++++++++++++++++--------
 1 file changed, 28 insertions(+), 8 deletions(-)

diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 4d9cf7711..8db35f474 100644
--- a/prelude/fin_collections.v
+++ b/prelude/fin_collections.v
@@ -249,18 +249,38 @@ Section filter.
 End filter.
 
 (** * Decision procedures *)
-Global Instance set_Forall_dec `(P : A → Prop)
-  `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
+Lemma set_Forall_elements P X : set_Forall P X ↔ Forall P (elements X).
+Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
+Lemma set_Exists_elements P X : set_Exists P X ↔ Exists P (elements X).
+Proof. rewrite Exists_exists. by setoid_rewrite elem_of_elements. Qed.
+
+Lemma set_Forall_Exists_dec {P Q : A → Prop} (dec : ∀ x, {P x} + {Q x}) X :
+  {set_Forall P X} + {set_Exists Q X}.
+Proof.
+ refine (cast_if (Forall_Exists_dec dec (elements X)));
+   [by apply set_Forall_elements|by apply set_Exists_elements].
+Defined.
+
+Lemma not_set_Forall_Exists P `{dec : ∀ x, Decision (P x)} X :
+  ¬set_Forall P X → set_Exists (not ∘ P) X.
+Proof. intro. by destruct (set_Forall_Exists_dec dec X). Qed.
+Lemma not_set_Exists_Forall P `{dec : ∀ x, Decision (P x)} X :
+  ¬set_Exists P X → set_Forall (not ∘ P) X.
+Proof.
+  by destruct (@set_Forall_Exists_dec
+    (not ∘ P) _ (λ x, swap_if (decide (P x))) X).
+Qed.
+
+Global Instance set_Forall_dec (P : A → Prop) `{∀ x, Decision (P x)} X :
+  Decision (set_Forall P X) | 100.
 Proof.
-  refine (cast_if (decide (Forall P (elements X))));
-    abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
-      by rewrite <-Forall_forall).
+ refine (cast_if (decide (Forall P (elements X))));
+   by rewrite set_Forall_elements.
 Defined.
 Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
   Decision (set_Exists P X) | 100.
 Proof.
-  refine (cast_if (decide (Exists P (elements X))));
-    abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
-      by rewrite <-Exists_exists).
+ refine (cast_if (decide (Exists P (elements X))));
+   by rewrite set_Exists_elements.
 Defined.
 End fin_collection.
-- 
GitLab