BoundedSearch.v

Require Import HoTT.Basics HoTT.Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Truncations.Core.
Require Import HoTT.Spaces.Nat.Core.

Section bounded_search.

  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.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
IsHProp min_n_Type
  Proof.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
IsHProp min_n_Type
    apply ishprop_sigma_disjoint.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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
P_inhab: {n : nat & 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
P_inhab: {n : nat & 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
P_inhab: {n : nat & 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
P_inhab: {n : nat & 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
P_inhab: {n : nat & 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)
P_inhab: hexists (fun n : nat => P n)
n: nat
k: smaller n
smaller n.+1
  Proof.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
smaller 0 + (forall l : nat, l <= 0 -> ~ P l)
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
smaller 0 + (forall l : nat, l <= 0 -> ~ P l) assert (P 0 + not (P 0)) as X; [apply P_dec |].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
X: P 0 + ~ P 0
smaller 0 + (forall l : nat, l <= 0 -> ~ P l)
      destruct X as [h|].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
h: P 0
smaller 0
        refine (0;(h,_,_)).P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
h: P 0
minimal 0
        *P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
h: P 0
minimal 0 intros ? ?.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
h: P 0
m: nat
X: P m
0 <= m exact _.
      +P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
n: ~ P 0
l: nat
lleq0: l <= 0
~ P l
        assert (l0 : l = 0) by rapply leq_antisym.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: ~ P 0
l: nat
lleq0: l <= 0
l0: l = 0
~ P l
        rewrite l0; assumption.
    -P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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 [|n0].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
n: nat
s: smaller n
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l) left.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
s: smaller n
smaller n.+1 apply smaller_S.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
s: smaller n
smaller n assumption.
      +P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l) assert (P (n.+1) + not (P (n.+1))) as X by apply P_dec.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
X: P n.+1 + ~ P n.+1
smaller n.+1 + (forall l : nat, l <= n.+1 -> ~ P l)
        destruct X as [h|].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
minimal n.+1
          --P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
n.+1 <= m
             assert ((n.+1 <= m)+(n.+1>m)) as X by apply leq_dichot.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
X: (n.+1 <= m) + (n.+1 > m)
n.+1 <= m
             destruct X as [leqSnm|ltmSn].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
leqSnm: n.+1 <= m
n.+1 <= m
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
ltmSn: n.+1 > m
n.+1 <= m
             ++P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
leqSnm: n.+1 <= m
n.+1 <= m assumption.
             ++P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
ltmSn: n.+1 > m
n.+1 <= m unfold gt, lt in ltmSn.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
ltmSn: m.+1 <= n.+1
n.+1 <= m
                assert (m <= n) as X by rapply leq_S_n.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
h: P n.+1
m: nat
pm: P m
ltmSn: m.+1 <= n.+1
X: m <= n
n.+1 <= m
                destruct (n0 m X pm).
        *P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ 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)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
forall l : nat, l <= n.+1 -> ~ P l intros l q.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
~ P l
          assert ((l <= n) + (l > n)) as X by apply leq_dichot.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
X: (l <= n) + (l > n)
~ P l
          destruct X as [h|h].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
h: l <= n
~ P l
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
h: l > n
~ P l
          --P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
h: l <= n
~ P l exact (n0 l h).
          --P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
h: l > n
~ P l unfold lt in h.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
h: l > n
~ P l
             assert (eqlSn : l = n.+1) by (apply leq_antisym; assumption).P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
n0: forall l : nat, l <= n -> ~ P l
n1: ~ P n.+1
l: nat
q: l <= n.+1
h: l > n
eqlSn: l = n.+1
~ P l
             rewrite eqlSn; assumption.
  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)
P_inhab: hexists (fun n : nat => P n)
n: nat
Pn: P n
min_n_Type
  Proof.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P 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.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
Pn: P n
X: smaller n + (forall l : nat, l <= n -> ~ P l)
min_n_Type
    destruct X as [[l [[Pl ml] leqln]]|none].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
Pn: P n
l: nat
Pl: P l
ml: minimal l
leqln: l <= n
min_n_Type
P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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)
P_inhab: hexists (fun n : nat => P n)
n: nat
Pn: P n
l: nat
Pl: P l
ml: minimal l
leqln: l <= n
min_n_Type exact (l;(tr Pl,tr ml)).
    -P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => 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 : min_n_Type.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
min_n_Type
  Proof.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
min_n_Type
    refine (Trunc_rec _ P_inhab).P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
{n : nat & P n} -> min_n_Type
    intros [n Pn].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
Pn: P n
min_n_Type exact (n_to_min_n n Pn).
  Defined.

  Definition minimal_n : { n : nat & P n }.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
{n : nat & P n}
  Proof.P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
{n : nat & P n}
    destruct prop_n_to_min_n as [n pl].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
pl: merely (P n) * merely (minimal n)
{n : nat & P n} destruct pl as [p _].P: nat -> Type
P_dec: forall n : nat, Decidable (P n)
P_inhab: hexists (fun n : nat => P n)
n: nat
p: merely (P n)
{n : nat & P n}
    exact (n; fst merely_inhabited_iff_inhabited_stable p).
  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 (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}.X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
{x : X & P x}
  Proof.X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
{x : X & P x}
    set (P' n := P (e n)).X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
{x : X & P x}
    assert (P'_dec : forall n, Decidable (P' n)) by apply _.X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec: forall n : nat, Decidable (P' n)
{x : X & P x}
    assert (P'_inhab : hexists (fun n => P' n)).X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec: forall n : nat, Decidable (P' n)
hexists (fun n : nat => P' n)
X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec: forall n : nat, Decidable (P' n)
P'_inhab: hexists (fun n : nat => P' n)
{x : X & P x}
    {X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec: forall n : nat, Decidable (P' n)
hexists (fun n : nat => P' n)
      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: forall n : nat, Decidable (P' n)
P_inhab: {x : X & P x}
hexists (fun n : nat => P' n) 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: forall n : nat, Decidable (P' n)
P_inhab: {x : X & P x}
{n : nat & P' n}
      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: forall n : nat, Decidable (P' n)
P_inhab: {x : X & P x}
x: X
p: P x
{n : nat & P' n}
      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: forall n : nat, Decidable (P' n)
P_inhab: {x : 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: forall n : nat, Decidable (P' n)
P_inhab: {x : 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: forall n : nat, Decidable (P' n)
P_inhab: {x : 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 (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec: forall n : nat, Decidable (P' n)
P'_inhab: hexists (fun n : nat => P' n)
{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 (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec: forall n : nat, Decidable (P' n)
P'_inhab: hexists (fun n : nat => P' n)
n: nat
p': P' n
{x : X & P x}
    exists (e n).X: Type
e: nat <~> X
P: X -> Type
P_dec: forall x : X, Decidable (P x)
P_inhab: hexists (fun x : X => P x)
P':= fun n : nat => P (e n): nat -> Type
P'_dec: forall n : nat, Decidable (P' n)
P'_inhab: hexists (fun n : nat => P' n)
n: nat
p': P' n
P (e n) exact p'.
  Defined.

End bounded_search_alt_type.