Martin Escardo 2012.

See my paper "Infinite sets that satisfy the principle of
omniscience" for a discussion of the type ℕ∞ defined here. We
observe that although we prove the omniscience in this module, it
is not needed to prove Rice's Theorem for the universe.

\begin{code}

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

module GenericConvergentSequence where

open import CurryHoward
open import Equality
open import Extensionality
open import Naturals
open import Two
open import Cantor
open import SetsAndFunctions
open import FirstProjectionInjective

\end{code}

Definition (The generic convergent sequence).
We use u,v to range over ℕ∞ and α,β to range over ₂ℕ:

\begin{code}

decreasing : ₂ℕ  Prp
decreasing α = ∀(i : )  α i  α(succ i)

ℕ∞ : Set
ℕ∞ = Σ \(α : ₂ℕ)  decreasing α

incl : ℕ∞  ₂ℕ
incl = π₀

incl-mono : ∀{u v : ℕ∞}  incl u  incl v  u  v
incl-mono {u} {v} = π₀-mono at-most-one u v
where
at-most-one : ∀{α : ₂ℕ}  ∀(p q : decreasing α)  p  q
at-most-one {α} p q = extensionality fact₂
where
open import UIP
fact₀ : ∀{i}  ∀(f g : α(succ i)    α i  )  f  g
fact₀ f g = extensionality fact₁
where
fact₁ :  r  f r  g r
fact₁ r = UIP  (f r) (g r)
fact₂ :  i  p i  q i
fact₂ i = fact₀ (p i) (q i)

Zero : ℕ∞
Zero = ((λ i  ) , λ i  id {  })

Succ : ℕ∞  ℕ∞
Succ (α , reason) = (α' , reason')
where
α' : ₂ℕ
α' 0 =
α'(succ n) = α n
reason' : decreasing α'
reason' 0 = λ r  refl
reason' (succ i) = reason i

positivity : ℕ∞
positivity u = incl u 0

isZero : ℕ∞  Prp
isZero u = positivity u

positive : ℕ∞  Prp
positive u = positivity u

isZero-Zero : isZero Zero
isZero-Zero = refl

Zero-not-Succ : ∀{u : ℕ∞}  Zero  Succ u
Zero-not-Succ {u} r = zero-is-not-one(cong positivity r)

: ℕ∞
= ((λ i  ) , λ i  id {  })

Succ-∞-is-∞ : Succ
Succ-∞-is-∞ = incl-mono(extensionality lemma)
where lemma :  i  incl(Succ ) i  incl  i
lemma 0 = refl
lemma (succ i) = refl

unique-fixed-point-of-Succ :  u  u  Succ u  u
unique-fixed-point-of-Succ u r = incl-mono(extensionality lemma)
where
fact :  i  incl u i  incl(Succ u) i
fact i = cong  w  incl w i) r
lemma :  i  incl u i
lemma 0 = fact 0
lemma (succ i) = trans (fact(succ i)) (lemma i)

Pred : ℕ∞  ℕ∞
Pred (α , reason) = (α  succ , reason  succ)

Pred-Zero-is-Zero : Pred Zero  Zero
Pred-Zero-is-Zero = refl

Pred-Succ-u-is-u : ∀{u : ℕ∞}  Pred(Succ u)  u
Pred-Succ-u-is-u {u} = refl

Pred-∞-is-∞ : Pred
Pred-∞-is-∞ = refl

Succ-mono : ∀{u v : ℕ∞}  Succ u  Succ v  u  v
Succ-mono = cong Pred

under :   ℕ∞
under 0 = Zero
under (succ n) = Succ(under n)

_≣_ : ℕ∞    Prp
u  n = u  under n

under-mono : ∀{m n : }  under m  under n  m  n
under-mono {0} {0} r = refl
under-mono {0} {succ n} r = ⊥-elim(Zero-not-Succ r)
under-mono {succ m} {0} r = ⊥-elim(Zero-not-Succ (sym r))
under-mono {succ m} {succ n} r = cong succ (under-mono {m} {n} (Succ-mono r))

under-diagonal₀ :

∀(n : )  incl(under n) n

under-diagonal₀ 0 = refl
under-diagonal₀ (succ n) = under-diagonal₀ n

under-diagonal₁ :

∀(n : )  incl(under(succ n)) n

under-diagonal₁ 0 = refl
under-diagonal₁ (succ n) = under-diagonal₁ n

isZero-equal-Zero :

∀{u : ℕ∞}  isZero u  u  Zero

isZero-equal-Zero {u} base = incl-mono(extensionality lemma)
where
lemma : ∀(i : )  incl u i  incl Zero i
lemma 0 = base
lemma (succ i) = Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (π₁ u i) (lemma i)

not-Zero-is-Succ : ∀{u : ℕ∞}  u  Zero  u  Succ(Pred u)
not-Zero-is-Succ {u} f = incl-mono(extensionality lemma)
where
lemma :  i  incl u i  incl(Succ(Pred u)) i
lemma 0 = Lemma[b≠₀→b≡₁](f  isZero-equal-Zero)
lemma (succ i) = refl

positive-is-not-Zero : ∀{u : ℕ∞}  positive u  u  Zero
positive-is-not-Zero {u} r s = lemma r
where
lemma : ¬(positive u)
lemma = Lemma[b≡₀→b≠₁](cong positivity s)

positive-equal-Succ :

∀{u : ℕ∞}  positive u  u  Succ(Pred u)

positive-equal-Succ r =
not-Zero-is-Succ (positive-is-not-Zero r)

Succ-criterion :

∀{u : ℕ∞}  ∀{n}  incl u n    incl u(succ n)    u  Succ(under n)

Succ-criterion {u} {n} r s = incl-mono(extensionality(lemma u n r s))
where
lemma :  u   n  incl u n    incl u(succ n)
i  incl u i  incl (Succ(under n)) i
lemma u 0 r s 0 = r
lemma u 0 r s (succ i) = lemma₀ i
where
lemma₀ :  i  incl u (succ i)
lemma₀ 0 = s
lemma₀ (succ i) = Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (π₁ u (succ i)) (lemma₀ i)
lemma u (succ n) r s 0 = lemma₁ (succ n) r
where
lemma₁ :  n  incl u n    positive u
lemma₁ 0 t = t
lemma₁ (succ n) t = lemma₁ n (π₁ u n t)
lemma u (succ n) r s (succ i) = lemma (Pred u) n r s i

∞-is-not-ℕ : ∀(n : )    under n
∞-is-not-ℕ n s =
zero-is-not-one (sym(trans (cong  w  incl w n) s) (under-diagonal₀ n)))

not-ℕ-is-∞ :

∀{u : ℕ∞}  (∀(n : )  u  under n)  u

not-ℕ-is-∞ {u} f = incl-mono(extensionality lemma)
where
lemma : ∀(n : )  incl u n
lemma 0 = Lemma[b≠₀→b≡₁] r  f 0 (isZero-equal-Zero r))
lemma (succ n) = Lemma[b≠₀→b≡₁] r  f(succ n)(Succ-criterion (lemma n) r))

ℕ∞-density :

∀{p : ℕ∞  }  (∀ n  p(under n)  )  p      u  p u

ℕ∞-density {p} f r u = Lemma[b≠₀→b≡₁] lemma
where
claim : p u    ∀(n : )  u  under n
claim g n = contra-positive  s  trans(cong p s) (f n))(Lemma[b≡₀→b≠₁] g)

claim-∞ : p u    u
claim-∞ = (contra-positive  s  trans(cong p s) r))  Lemma[b≡₀→b≠₁]

lemma : p u
lemma t = claim-∞ t (not-ℕ-is-∞(claim t))

ℕ∞-searchable :

∀(p : ℕ∞  )   \a  p a     u  p u

ℕ∞-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)

ℕ∞-omniscient :

∀(p : ℕ∞  )  ( \u  p u  )  (∀ u  p u  )

ℕ∞-omniscient p = two-equality-cases case₀ case₁
where
e :  \a  p a     u  p u
e = ℕ∞-searchable p

a : ℕ∞
a = ∃-witness e

case₀ : p a    ( \u  p u  )  (∀ u  p u  )
case₀ r = ∨-intro₀(∃-intro a r)

case₁ : p a    ( \u  p u  )  (∀ u  p u  )
case₁ r = ∨-intro₁(∃-elim e r)

\end{code}

There should be a better proof of the following. The idea is simple:
by the above development, u = under 0 if and only if incl u 0 ≡ 0, and
u ≡ under(n+1) if and only incl u n ≡ ₁ and incl u (n+1) ≡ ₀.

\begin{code}

finite-isolated :

∀(u : ℕ∞)  ∀(n : )  u  under n    u  under n

finite-isolated u 0 = two-equality-cases lemma₀ lemma₁
where
lemma₀ : isZero u  u  Zero  u  Zero
lemma₀ r = in₀(isZero-equal-Zero r)
lemma₁ : positive u  u  Zero  u  Zero
lemma₁ r = in₁(contra-positive fact (Lemma[b≡₁→b≠₀] r))
where fact : u  Zero  isZero u
fact r = cong  u  incl u 0) r
finite-isolated u (succ n) = two-equality-cases lemma₀ lemma₁
where
lemma₀ :  incl u n    u  under(succ n)  u  under(succ n)
lemma₀ r = in₁(contra-positive lemma (Lemma[b≡₀→b≠₁] r))
where
lemma : u  under(succ n)  incl u n
lemma r = trans (cong  v  incl v n) r) (under-diagonal₁ n)
lemma₁ :  incl u n    u  under(succ n)  u  under(succ n)
lemma₁ r = two-equality-cases lemma₁₀ lemma₁₁
where
lemma₁₀ :  incl u (succ n)    u  under(succ n)  u  under(succ n)
lemma₁₀ s = in₀(Succ-criterion r s)
lemma₁₁ :  incl u (succ n)    u  under(succ n)  u  under(succ n)
lemma₁₁ s = in₁ (contra-positive lemma (Lemma[b≡₁→b≠₀] s))
where
lemma : u  under(succ n)  incl u (succ n)
lemma r = trans (cong  v  incl v (succ n)) r) (under-diagonal₀(succ n))

\end{code}