(** * Bounded Search *)

(** The main result of this file is [minimal_n], which say that if [P : nat -> Type] is a family such that each [P n] is decidable and [{n & P n}] is merely inhabited, then [{n & P n}] is inhabited.  Since [P n] is decidable, it is sufficient to prove [{n & merely (P n)}], and to do this, we prove the stronger claim that there is a *minimal* [n] satisfying [merely (P n)].  This stronger claim is a proposition, which is what makes the argument work.  Along the way, we also prove that [{ l : nat & (l <= n) * P l }] is decidable for each [n]. *)

Require Import Basics.Overture Basics.Decidable Basics.Trunc Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Sigma Types.Prod.
Require Import Truncations.Core.
Require Import Spaces.Nat.Core.

Section bounded_search.

  Context (P : nat -> Type) (P_dec : forall n, Decidable (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.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
IsHProp min_n_Type
  Proof.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
IsHProp min_n_Type
    apply ishprop_sigma_disjoint.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
forall x y : nat,
merely (P x) * merely (minimal x) ->
merely (P y) * merely (minimal y) -> x = y
    intros n n' [p m] [p' m'].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, n': nat
p: merely (P n)
m: merely (minimal n)
p': merely (P n')
m': merely (minimal n')
n = n'
    strip_truncations.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, n': nat
m': minimal n'
p': P n'
m: minimal n
p: P n
n = n'
    apply leq_antisym.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, n': nat
m': minimal n'
p': P n'
m: minimal n
p: P n
n <= n'
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, n': nat
m': minimal n'
p': P n'
m: minimal n
p: P n
n' <= n
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, n': nat
m': minimal n'
p': P n'
m: minimal n
p: P n
n <= n' exact (m n' p').
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, n': nat
m': minimal n'
p': P n'
m: minimal n
p: P n
n' <= n exact (m' n p).
  Defined.

  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).
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
k: smaller n
smaller n.+1
  Proof.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
k: smaller n
smaller n.+1
    destruct k as [l [[p m] z]].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, l: nat
p: P l
m: minimal l
z: l <= n
smaller n.+1
    exists l.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, l: nat
p: P l
m: minimal l
z: l <= n
P l * minimal l * (l <= n.+1)
    repeat split.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, l: nat
p: P l
m: minimal l
z: l <= n
P l
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, l: nat
p: P l
m: minimal l
z: l <= n
minimal l
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, l: nat
p: P l
m: minimal l
z: l <= n
l <= n.+1
    1,2: assumption.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, l: nat
p: P l
m: minimal l
z: l <= n
l <= n.+1
    exact _.
  Defined.

  Local Definition bounded_search (n : nat) : smaller n + forall l : nat, (l <= n) -> not (P l).
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
smaller n + (forall l : nat, l <= n -> ~ P l)
  Proof.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
smaller n + (forall l : nat, l <= n -> ~ P l)
    induction n as [|n IHn].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
smaller 0 + (forall l : nat, l <= 0 -> ~ P l)
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
IHn: smaller n + (forall l : nat, l <= n -> ~ P l)
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l)
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
smaller 0 + (forall l : nat, l <= 0 -> ~ P l) destruct (dec (P 0)) as [h|n].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
h: P 0
smaller 0 + (forall l : nat, l <= 0 -> ~ P l)
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: ~ P 0
smaller 0 + (forall l : nat, l <= 0 -> ~ P l)
      +
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
h: P 0
smaller 0 + (forall l : nat, l <= 0 -> ~ P l) left.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
h: P 0
smaller 0
        exact (0; (h, fun _ _ => _, _)).
      +
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: ~ P 0
smaller 0 + (forall l : nat, l <= 0 -> ~ P l) right.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: ~ P 0
forall l : nat, l <= 0 -> ~ P l
        intros l lleq0.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: ~ P 0
l: nat
lleq0: l <= 0
~ P l
        by rewrite (leq_antisym lleq0 _ : l = 0).
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
IHn: smaller n + (forall l : nat, l <= n -> ~ P l)
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l) destruct IHn as [s|n0].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
s: smaller n
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l)
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l)
      +
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
s: smaller n
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l) left; by apply smaller_S.
      +
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l) destruct (dec (P n.+1)) as [h|nP].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l)
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
nP: ~ P n.+1
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l)
        *
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l) left.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
smaller n.+1
          refine (n.+1; (h, _, _)).
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
minimal n.+1
          intros m pm.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
n.+1 <= m
          apply leq_iff_not_gt.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
~ (n.+1 > m)
          unfold gt, lt; intro leq_Sm_Sn.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
leq_Sm_Sn: m.+1 <= n.+1
Empty
          apply leq_pred' in leq_Sm_Sn.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
leq_Sm_Sn: m <= n
Empty
          destruct (n0 m leq_Sm_Sn pm).
        *
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
nP: ~ P n.+1
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l) right.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
nP: ~ P n.+1
forall l : nat, l <= n.+1 -> ~ P l
          by apply leq_ind_l.
  Defined.

  Local Definition n_to_min_n (n : nat) (Pn : P n) : min_n_Type.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Pn: P n
min_n_Type
  Proof.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Pn: P n
min_n_Type
    destruct (bounded_search n) as [[l [[Pl ml] _]] | none].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Pn: P n
l: nat
Pl: P l
ml: minimal l
min_n_Type
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Pn: P n
none: forall l : nat, l <= n -> ~ P l
min_n_Type
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Pn: P n
l: nat
Pl: P l
ml: minimal l
min_n_Type exact (l; (tr Pl, tr ml)).
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Pn: P n
none: forall l : nat, l <= n -> ~ P l
min_n_Type destruct (none n (leq_refl n) Pn).
  Defined.

  Local Definition prop_n_to_min_n (P_inhab : hexists P) : min_n_Type.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists P
min_n_Type
  Proof.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists P
min_n_Type
    strip_truncations.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: {x : _ & P x}
min_n_Type
    exact (n_to_min_n (P_inhab.1) (P_inhab.2)).
  Defined.

  Definition minimal_n (P_inhab : hexists P) : { n : nat & P n }.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists P
{n : nat & P n}
  Proof.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists P
{n : nat & P n}
    destruct (prop_n_to_min_n P_inhab) as [n [p _]].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists P
n: nat
p: merely (P n)
{n : nat & P n}
    exact (n; fst merely_inhabited_iff_inhabited_stable p).
  Defined.

  (** As a consequence of [bounded_search] we deduce that bounded existence is decidable.  See also [decidable_exists_bounded_nat] in Spaces/Lists/Theory.v for a similar result with different dependencies. *)
  Definition decidable_search (n : nat) : Decidable { l : nat & (l <= n) * P l }.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Decidable {l : nat & (l <= n) * P l}
  Proof.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
Decidable {l : nat & (l <= n) * P l}
    destruct (bounded_search n) as [s | no_l].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
s: smaller n
Decidable {l : nat & (l <= n) * P l}
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
no_l: forall l : nat, l <= n -> ~ P l
Decidable {l : nat & (l <= n) * P l}
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
s: smaller n
Decidable {l : nat & (l <= n) * P l} destruct s as [l [[Pl min] l_leq_n]].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n, l: nat
Pl: P l
min: minimal l
l_leq_n: l <= n
Decidable {l : nat & (l <= n) * P l}
      exact (inl (l; (l_leq_n, Pl))).
    -
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
no_l: forall l : nat, l <= n -> ~ P l
Decidable {l : nat & (l <= n) * P l} right.
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
no_l: forall l : nat, l <= n -> ~ P l
~ {l : nat & (l <= n) * P l}
      intros [l [l_leq_n Pl]].
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
n: nat
no_l: forall l : nat, l <= n -> ~ P l
l: nat
l_leq_n: l <= n
Pl: P l
Empty
      exact (no_l l l_leq_n Pl).
  Defined.

End bounded_search.

Section bounded_search_alt_type.

  Context (X : Type)
          (e : nat <~> X)
          (P : X -> Type)
          (P_dec : forall x, Decidable (P x))
          (P_inhab : hexists P).

  (** Bounded search works for types equivalent to the naturals even without full univalence. *)
  Definition minimal_n_alt_type : {x : X & P x}.
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
{x : X & P x}
  Proof.
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
{x : X & P x}
    pose (P' n := P (e n)).
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
P':= fun n : nat => P (e n): nat -> Type
{x : X & P x}
    pose (P'_dec n := P_dec (e n) : Decidable (P' n)).
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
{x : X & P x}
    assert (P'_inhab : hexists P').
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
hexists P'
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P'_inhab: hexists P'
{x : X & P x}
    {
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
hexists P'
      strip_truncations.
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P_inhab: {x : _ & P x}
hexists P' apply tr.
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P_inhab: {x : _ & P x}
{x : _ & P' x}
      destruct P_inhab as [x p].
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P_inhab: {x : _ & P x}
x: X
p: P x
{x : _ & P' x}
      exists (e ^-1 x).
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P_inhab: {x : _ & P x}
x: X
p: P x
P' (e^-1 x)
      unfold P'.
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P_inhab: {x : _ & P x}
x: X
p: P x
P (e (e^-1 x))
      rewrite (eisretr e).
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P_inhab: {x : _ & P x}
x: X
p: P x
P x exact p.
    }
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P'_inhab: hexists P'
{x : X & P x}
    destruct (minimal_n P' P'_dec P'_inhab) as [n p'].
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists P
P':= fun n : nat => P (e n): nat -> Type
P'_dec:= fun n : nat => P_dec (e n) : Decidable (P' n): forall n : nat, Decidable (P' n)
P'_inhab: hexists P'
n: nat
p': P' n
{x : X & P x}
    exact ((e n); p').
  Defined.

End bounded_search_alt_type.