From 6f40106128e2e40306602bfc8182436427213777 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Jul 2021 10:01:08 +0200
Subject: [PATCH] add lemma list_in_dec

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

diff --git a/theories/list.v b/theories/list.v
index 29e1b750..c68da7b5 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -939,6 +939,21 @@ 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.
-- 
GitLab