From 6f19c369c47e25ca164e56dd3a9b4e17b15440da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 6 Sep 2021 08:44:31 +0200
Subject: [PATCH] =?UTF-8?q?Shorter=20proof=20for=20=E2=88=83,=20also=20add?=
 =?UTF-8?q?=20proof=20for=20=E2=88=80.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/list.v | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index c68da7b5..1b16fbfa 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -939,21 +939,6 @@ Proof.
   destruct (nth_lookup_or_length l i d); [done | by lia].
 Qed.
 
-Lemma list_in_dec (P : A → Prop) (l : list A) :
-  (∀ x, Decision (P x)) →
-  Decision (∃ x, P x ∧ x ∈ l).
-Proof.
-  intros HdecP. induction l as [ | it l IH].
-  - right. intros (it & _ & []%elem_of_nil).
-  - destruct IH as [ IH | IH].
-    + left. destruct IH as (it' & Hit' & Hin).
-      exists it'. split; [done|]. right. done.
-    + destruct (HdecP it) as [Hit | Hnit].
-      { left. exists it. split; [done|]. by left. }
-      right. intros (it' & Hit' & [-> | Hin]%elem_of_cons); [done|].
-      apply IH. eauto.
-Qed.
-
 (** ** Properties of the [NoDup] predicate *)
 Lemma NoDup_nil : NoDup (@nil A) ↔ True.
 Proof. split; constructor. Qed.
@@ -2948,6 +2933,17 @@ Section Forall_Exists.
     end.
 End Forall_Exists.
 
+Lemma list_exist_dec P l :
+  (∀ x, Decision (P x)) → Decision (∃ x, x ∈ l ∧ P x).
+Proof.
+  refine (λ _, cast_if (decide (Exists P l))); by rewrite <-Exists_exists.
+Defined.
+Lemma list_forall_dec P l :
+  (∀ x, Decision (P x)) → Decision (∀ x, x ∈ l → P x).
+Proof.
+  refine (λ _, cast_if (decide (Forall P l))); by rewrite <-Forall_forall.
+Defined.
+
 Lemma forallb_True (f : A → bool) xs : forallb f xs ↔ Forall f xs.
 Proof.
   split.
-- 
GitLab