From 971517861e4de4e1de6d9af1a7c24086d259470e Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 15 Jan 2025 16:38:18 -0500
Subject: [PATCH] BoundedSearch: add decidable_search

---
 theories/BoundedSearch.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/BoundedSearch.v b/theories/BoundedSearch.v
index 8c3332e316..994402289e 100644
--- a/theories/BoundedSearch.v
+++ b/theories/BoundedSearch.v
@@ -71,6 +71,17 @@ Section bounded_search.
              rewrite eqlSn; assumption.
   Defined.
 
+  (** Should we include [minimal l] in the condition as well? *)
+  Definition decidable_search (n : nat) : Decidable { l : nat & (l <= n) * P l }.
+  Proof.
+    destruct (bounded_search n) as [s | no_l].
+    - destruct s as [l [[Pl min] l_leq_n]].
+      exact (inl (l; (l_leq_n, Pl))).
+    - right.
+      intros [l [l_leq_n Pl]].
+      exact (no_l l l_leq_n Pl).
+  Defined.
+
   Local Definition n_to_min_n (n : nat) (Pn : P n) : min_n_Type.
   Proof.
     assert (smaller n + forall l, (l <= n) -> not (P l)) as X by apply bounded_search.