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 #-}

module ConvergentSequenceSearchable where


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


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


This is the main theorem proved in this module:


ℕ∞-is-searchable : searchable ℕ∞
ℕ∞-is-searchable p = ∃-intro 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 =  cong  w  incl w 0) r
  Dagger₀ (succ n) r = trans w t
    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
    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)
    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)




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)