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

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

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


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

module ConvergentSequenceSearchable where


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


open import Naturals
open import Two 
open import GenericConvergentSequence
open import SpartanMLTT
open import Searchable


This is the main theorem proved in this module:


ℕ∞-is-searchable : searchable ℕ∞
ℕ∞-is-searchable p = a , Lemma
  α :   𝟚
  α 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
    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
    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)
    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)




open import Omniscience

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

open import DiscreteAndSeparated

ℕ∞→ℕ-has-decidable-equality : discrete(ℕ∞  )
ℕ∞→ℕ-has-decidable-equality = omniscient-discrete-discrete ℕ∞-is-omniscient  u  ℕ-discrete)