By Martin Escardo, 2 September 2011.

Modified in December 2011 assuming the axiom of extensionality (which
is not used directly in this module, but instead in
GenericConvergentSequence).

We prove that the generic convergent sequence ℕ∞ is searchable, which
amounts to Theorem-3·6 of the paper

http://www.cs.bham.ac.uk/~mhe/papers/omniscient.pdf,
http://www.cs.bham.ac.uk/~mhe/.talks/dagstuhl2011/omniscient.pdf

and conclude as a corollary that it is searchable and satisfies the
principle of omniscience.

\begin{code}

module ConvergentSequenceSearchable where

\end{code}

(Continuity axioms and the fan principle are not assumed.)

\begin{code}

open import CurryHoward
open import Equality
open import Naturals
open import Two
open import Cantor
open import GenericConvergentSequence
open import SetsAndFunctions
open import Searchable

\end{code}

This is the main theorem proved in this module:

\begin{code}

ℕ∞-is-searchable : searchable ℕ∞
ℕ∞-is-searchable p = ∃-intro a Lemma
where
α : ₂ℕ
α 0       = p(under 0)
α(succ n) = min (α n) (p(under(succ n)))

a : ℕ∞
a = (α , λ i → Lemma[minab≤a])

Dagger₀ : ∀(n : ℕ) → a ≡ under n → p(under n) ≡ ₀
Dagger₀ 0 r =  cong (λ w → incl w 0) r
Dagger₀ (succ n) r = trans w t
where
s : α n ≡ ₁
s = trans (cong (λ w → incl w n) r) (under-diagonal₁ n)

t : α(succ n) ≡ ₀
t = trans (cong (λ w → incl w(succ n)) r) (under-diagonal₀ n)

w : p(under(succ n)) ≡ α(succ n)
w = sym(cong(λ b → min b (p(under(succ n)))) s)

Dagger₁ : a ≡ ∞ → ∀(n : ℕ) → p(under n) ≡ ₁
Dagger₁ r 0 = cong (λ w → incl w 0) r
Dagger₁ r (succ n) = trans w t
where
s : α n ≡ ₁
s = cong (λ w → incl w n) r

t : α(succ n) ≡ ₁
t = cong (λ w → incl w (succ n)) r

w : p(under(succ n)) ≡ α(succ n)
w = sym(cong(λ b → min b (p(under(succ n)))) s)

Claim₀ : p a ≡ ₁ → ∀(n : ℕ) → a ≠ under n
Claim₀ r n s = Lemma[b≡₁→b≠₀] r (Lemma s)
where
Lemma : a ≡ under n → p a ≡ ₀
Lemma t = trans (cong p t) (Dagger₀ n t)

Claim₁ : p a ≡ ₁ → a ≡ ∞
Claim₁ r = not-ℕ-is-∞ (Claim₀ r)

Claim₂ : p a ≡ ₁ → ∀(n : ℕ) → p(under n) ≡ ₁
Claim₂ r = Dagger₁(Claim₁ r)

Claim₃ : p a ≡ ₁ → p ∞ ≡ ₁
Claim₃ r = Lemma[x≡y→x≡z→z≡y] r (cong p (Claim₁ r))

Lemma : p a ≡ ₁ → ∀(v : ℕ∞) → p v ≡ ₁
Lemma r = ℕ∞-density (Claim₂ r) (Claim₃ r)

\end{code}

Corollary:

\begin{code}

open import Omniscience

ℕ∞-is-omniscient : omniscient ℕ∞
ℕ∞-is-omniscient = searchable-implies-omniscient ℕ∞-is-searchable

\end{code}