BoundedSearch: add decidable_search

HoTT · Jan 15, 2025 · 9715178 · 9715178
1 parent e235678
commit 9715178
Showing 1 changed file with 11 additions and 0 deletions.
diff --git 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.