Library UniMath.Combinatorics.BoundedSearch

Auke Booij Nov. 2017
If P is a decidable predicate on the natural numbers, then from the existence of a natural number satisfying P , we can find a natural number satisfying P .

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.MoreFoundations.Propositions.

Section constr_indef_descr.
Context
(P : nat hProp)
(P_dec : n : nat, P n ⨿ ¬ P n)
(P_inhab : n : nat, P n).

Local Definition minimal (n : nat) : UU := m : nat, P m (n m).
Local Definition isapropminimal (n : nat) : isaprop (minimal n).
Proof.
apply impred_isaprop.
intros m.
apply isapropimpl.
apply isasetbool.
Defined.

Local Definition min_n_UU : UU := n : nat, P n × minimal n.

Local Definition isapropmin_n : isaprop min_n_UU.
Proof.
apply isaproptotal2.
- intros n.
apply isapropdirprod. apply (P n).
apply isapropminimal.
- intros n n' k k'.
induction k as [p m], k' as [p' m'].
apply isantisymmnatleh.
+ exact (m n' p').
+ exact (m' n p).
Defined.

Local Definition min_n : hProp := make_hProp min_n_UU isapropmin_n.

Local Definition smaller (n : nat) := l : nat, P l × minimal l × (l n)%nat.

Local Definition smaller_S (n : nat) (k : smaller n) : smaller (S n).
Proof.
induction k as [l pmz].
induction pmz as [p mz].
induction mz as [m z].
refine (l,,p,,m,,_).
refine (istransnatgth _ _ _ _ _).
apply natgthsnn.
apply z.
Defined.

Local Definition bounded_search (n : nat) : smaller n ⨿ l : nat, (l n)%nat ¬ P l.
Proof.
induction n.
- assert (P 0 ⨿ ¬ P 0) as X.
apply P_dec.
induction X as [h|].
+ apply ii1.
refine (O,,h,,_,,_).
× intros ? ?. apply natleh0n.
× apply isreflnatleh.
+ apply ii2. intros l lleq0.
assert (H : l = O).
{ apply natleh0tois0. assumption. }
rewrite H. assumption.
- induction IHn as [|n0].
+ apply ii1. apply smaller_S. assumption.
+ assert (P (S n) ⨿ ¬ P (S n)) as X.
apply P_dec.
induction X as [h|].
× refine (ii1 (S n,,h,,_,,_)).
-- intros m q.
assert (((S n) > m)%nat ⨿ (S n m)) as X.
apply natgthorleh.
induction X as [h0|].
++ apply fromempty.
refine (n0 m h0 q).
++ assumption.
-- apply isreflnatleh.
× apply ii2. intros l q.
assert ((l > n)%nat ⨿ (l n)) as X.
apply natgthorleh.
induction X as [h|h].
-- assert (H : l = S n).
apply isantisymmnatgeh. apply h. apply q. rewrite H. assumption.
-- exact (n0 l h).
Defined.

Local Definition n_to_min_n (n : nat) (p : P n) : min_n.
Proof.
assert (smaller n ⨿ l : nat, (l n)%nat ¬ P l) as X.
apply bounded_search.
induction X as [lqmz|none].
- induction lqmz as [l qmz].
induction qmz as [q mz].
induction mz as [m z].
refine (l,,q,,m).
- apply fromempty.
refine (none n (isreflnatgeh _ ) p).
Defined.

Local Definition prop_n_to_min_n : min_n.
Proof.
refine (@hinhuniv ( n : nat, P n) _ _ _).
- induction 1 as [n p]. exact (n_to_min_n n p).
- exact P_inhab.
Defined.

Definition minimal_n : n : nat, P n.
Proof.
induction prop_n_to_min_n as [n pl]. induction pl as [p _].
exact (n,,p).
Defined.

End constr_indef_descr.