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
  α' : ₂ℕ
  α'  = ₁
  α'(succ n) = α n
  reason' : decreasing α'
  reason'  = λ r → refl
  reason' (succ i) = reason i

positivity : ℕ∞ → ₂
positivity u = incl u 

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  = 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  = fact 
  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  = 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 {} {} r = refl
under-mono {} {succ n} r = ⊥-elim(Zero-not-Succ r)
under-mono {succ m} {} 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₀  = refl
under-diagonal₀ (succ n) = under-diagonal₀ n


under-diagonal₁ :

  ∀(n : ℕ) → incl(under(succ n)) n ≡ ₁

under-diagonal₁  = 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  = 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  = 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  r s  = r
  lemma u  r s (succ i) = lemma₀ i
     where
      lemma₀ : ∀ i → incl u (succ i) ≡ ₀
      lemma₀  = s
      lemma₀ (succ i) = Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (π₁ u (succ i)) (lemma₀ i)
  lemma u (succ n) r s  = lemma₁ (succ n) r
     where
      lemma₁ : ∀ n → incl u n ≡ ₁ → positive u
      lemma₁  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  = Lemma[b≠₀→b≡₁](λ r → f  (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
  α : ₂ℕ
  α        = p(under )
  α(succ n) = min (α n) (p(under(succ n)))

  a : ℕ∞
  a = (α , λ i → Lemma[minab≤a])

  Dagger₀ : ∀(n : ℕ) → a ≡ under n → p(under n) ≡ ₀
  Dagger₀  r =  cong (λ w → incl w ) 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  = cong (λ w → incl w ) 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  = 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 ) 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}