Timings for BoundedSearch.v
Require Import HoTT.Basics HoTT.Types.
Require Import HoTT.Truncations.Core.
Require Import HoTT.Spaces.Nat.Core.
Context (P : nat -> Type)
(P_dec : forall n, Decidable (P n))
(P_inhab : hexists (fun n => P n)).
(** We open type_scope again after nat_scope in order to use the product type notation. *)
Local Open Scope nat_scope.
Local Open Scope type_scope.
Local Definition minimal (n : nat) : Type := forall m : nat, P m -> n <= m.
(** If we assume [Funext], then [minimal n] is a proposition. But to avoid needing [Funext], we propositionally truncate it. *)
Local Definition min_n_Type : Type := { n : nat & merely (P n) * merely (minimal n) }.
Local Instance ishpropmin_n : IsHProp min_n_Type.
apply ishprop_sigma_disjoint.
intros n n' [p m] [p' m'].
Local Definition smaller (n : nat) := { l : nat & P l * minimal l * (l <= n) }.
Local Definition smaller_S (n : nat) (k : smaller n) : smaller (S n).
destruct k as [l [[p m] z]].
Local Definition bounded_search (n : nat) : smaller n + forall l : nat, (l <= n) -> not (P l).
assert (P 0 + not (P 0)) as X; [apply P_dec |].
assert (l0 : l = 0) by rapply leq_antisym.
assert (P (n.+1) + not (P (n.+1))) as X by apply P_dec.
assert ((n.+1 <= m)+(n.+1>m)) as X by apply leq_dichot.
destruct X as [leqSnm|ltmSn].
assert (m <= n) as X by rapply leq_S_n.
assert ((l <= n) + (l > n)) as X by apply leq_dichot.
assert (eqlSn : l = n.+1) by (apply leq_antisym; assumption).
rewrite eqlSn; assumption.
Local Definition n_to_min_n (n : nat) (Pn : P n) : min_n_Type.
assert (smaller n + forall l, (l <= n) -> not (P l)) as X by apply bounded_search.
destruct X as [[l [[Pl ml] leqln]]|none].
destruct (none n (leq_refl n) Pn).
Local Definition prop_n_to_min_n : min_n_Type.
refine (Trunc_rec _ P_inhab).
Definition minimal_n : { n : nat & P n }.
destruct prop_n_to_min_n as [n pl].
exact (n; fst merely_inhabited_iff_inhabited_stable p).
Section bounded_search_alt_type.
Context (X : Type)
(e : nat <~> X)
(P : X -> Type)
(P_dec : forall x, Decidable (P x))
(P_inhab : hexists (fun x => P x)).
(** Bounded search works for types equivalent to the naturals even without full univalence. *)
Definition minimal_n_alt_type : {x : X & P x}.
assert (P'_dec : forall n, Decidable (P' n)) by apply _.
assert (P'_inhab : hexists (fun n => P' n)).
destruct P_inhab as [x p].
destruct (minimal_n P' P'_dec P'_inhab) as [n p'].
End bounded_search_alt_type.