Martin Escardo 20-21 December 2012

Development adapted from the module ConvergentSequenceSearchable.lagda:

\begin{code}

{-# OPTIONS --without-K #-}

module ConvergentSequenceInfSearchable where

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

ℕ∞-is-inf-searchable : inf-searchable ℕ∞ _≼_
ℕ∞-is-inf-searchable p = ∃-intro a (∧-intro putative-root-lemma (∧-intro lower-bound-lemma uborlb-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)

putative-root-lemma : (∃ \u → p u ≡ ₀) → p a ≡ ₀
putative-root-lemma (x , r) = lemma claim
where
lemma : ¬(∀ x → p x ≡ ₁) → p a ≡ ₀
lemma = Lemma[b≢₁→b≡₀] ∘ (contra-positive Lemma)
claim : ¬(∀ x → p x ≡ ₁)
claim f = Lemma[b≡₁→b≢₀] (f x) r

lower-bound-lemma : ∀ u → p u ≡ ₀ → a ≼ u
lower-bound-lemma u r 0 s = lemma
where
claim₀ : incl u 0 ≡ ₀ → p u ≡ α 0
claim₀ t = cong p (isZero-equal-Zero t)
claim₁ : incl u 0 ≡ ₀ → ₀ ≡ ₁
claim₁ t = trans (trans (sym r) (claim₀ t)) s
lemma : incl u 0 ≡ ₁
lemma = Lemma[b≢₀→b≡₁] (contra-positive claim₁ zero-is-not-one)

lower-bound-lemma u r (succ n) s = lemma
where
-- s : min₂ (incl a n) (p(under(succ n))) ≡ ₁
IH : incl a n ≡ ₁ → incl u n ≡ ₁
IH = lower-bound-lemma u r n
claim₀ : incl u n ≡ ₁
claim₀ = IH(Lemma[min₂ab≡₁→a≡₁] s)
claim₁ : p(under(succ n)) ≡ ₁
claim₁ = Lemma[min₂ab≡₁→b≡₁]{(incl a n)} s
claim₂ : incl u (succ n) ≡ ₀ → u ≡ under(succ n)
claim₂ = Succ-criterion claim₀
claim₃ : incl u (succ n) ≡ ₀ → p u ≡ p(under(succ n))
claim₃ t = cong p (claim₂ t)
claim₄ : incl u (succ n) ≡ ₀ → p u ≡ ₁
claim₄ t = trans (claim₃ t) claim₁
claim₅ : incl u (succ n) ≢ ₀
claim₅ t = Lemma[b≡₁→b≢₀] (claim₄ t) r
lemma : incl u (succ n) ≡ ₁
lemma = Lemma[b≢₀→b≡₁] claim₅

uborlb-lemma : ∀ l → (∀ x → p x ≡ ₀ → l ≼ x) → l ≼ a
uborlb-lemma l lower-bounder = two-equality-cases lemma₀ lemma₁
where
lemma₀ : p a ≡ ₀ → l ≼ a
lemma₀ = lower-bounder a
lemma₁ : p a ≡ ₁ → l ≼ a
lemma₁ r n x = cong (λ a → incl a n) (Claim₁ r)
\end{code}