Martin Escardo 20-21 December 2012

Development adapted from the module ConvergentSequenceSearchable.lagda:

Not only is ℕ∞ searchable, but, moreover, minimal witnesses can be
found.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module ConvergentSequenceInfSearchable where

open import SpartanMLTT
open import Naturals
open import Two
open import InfSearchable
open import GenericConvergentSequence

ℕ∞-is-inf-searchable : inf-searchable ℕ∞ _≼_
ℕ∞-is-inf-searchable p = a , (putative-root-lemma , (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 =  ap  w  incl w 0) r
  Dagger₀ (succ n) r = trans w t
   where 
    s : α n  
    s = trans (ap  w  incl w n) r) (under-diagonal₁ n)
    t : α(succ n)  
    t = trans (ap  w  incl w(succ n)) r) (under-diagonal₀ n)
    w : p(under(succ n))  α(succ n)
    w = sym(ap b  min𝟚 b (p(under(succ n)))) s)

  Dagger₁ : a    (n : )  p(under n)  
  Dagger₁ r 0 = ap  w  incl w 0) r
  Dagger₁ r (succ n) = trans w t
   where 
    s : α n  
    s = ap  w  incl w n) r
    t : α(succ n)  
    t = ap  w  incl w (succ n)) r
    w : p(under(succ n))  α(succ n)
    w = sym(ap 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 (ap 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 (ap 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 = ap 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 = ap 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 = ap  a  incl a n) (Claim₁ r)
\end{code}