module GenericConvergentSequence where

open import Logic
open import Equality
open import Naturals
open import Two
open import Cantor

-- Definition (The generic convergent sequence).
ℕ∞ : ₂ℕ → Ω
ℕ∞ x = ∀(i : ℕ) → x i ≥ x(succ i)
-- We use x,y,z to range over ℕ∞ and α,β to range over ₂ℕ.


-- Definition (Set membership).
_∈_ : {X : Set} → X → (A : X → Ω) → Ω
x ∈ A = A x


-- We now describe the elements of ℕ∞ explicitly.  The following is
-- the characteristic function of the (>) relation on ℕ, viewed in a
-- different way.

-- Definition (Embedding of ℕ into ℕ∞).
underline : ℕ → ₂ℕ
underline  i = ₀
underline (succ n)  = ₁
underline (succ n) (succ i) = underline n i


Lemma[underline-0] :
-------------------------------
  ∀(n : ℕ) → underline n n ≡ ₀
-------------------------------
Lemma[underline-0]  = refl
Lemma[underline-0] (succ n) = Lemma[underline-0] n


Lemma[underline-1] :
-------------------------------------
  ∀(n : ℕ) → underline(succ n) n ≡ ₁
-------------------------------------
Lemma[underline-1]  = refl
Lemma[underline-1] (succ n) = Lemma[underline-1] n


Lemma[underline[ℕ]⊆ℕ∞] :
-------------------------------
  ∀(n : ℕ) → underline n ∈ ℕ∞
-------------------------------
Lemma[underline[ℕ]⊆ℕ∞]  i r = ⊥-elim(Lemma[b≡₁→b≠₀] r refl)
Lemma[underline[ℕ]⊆ℕ∞] (succ n)  r = refl
Lemma[underline[ℕ]⊆ℕ∞] (succ n) (succ i) r = Lemma[underline[ℕ]⊆ℕ∞] n i r


-- Definition (Infinity).
∞ : ₂ℕ
∞ = λ i → ₁


Lemma[∞∈ℕ∞] :
---------
  ∞ ∈ ℕ∞
---------
Lemma[∞∈ℕ∞] i r = refl


Lemma[x0≡₀→x≣underline0] :
--------------------------------------------------
  ∀{x : ₂ℕ} → x ∈ ℕ∞ → x  ≡ ₀ → x ≣ underline 
--------------------------------------------------
Lemma[x0≡₀→x≣underline0] {x} m base = by-induction
 where
  by-induction : ∀(i : ℕ) → x i ≡ ₀
  by-induction  = base
  by-induction (succ i) =
    Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (m i) (by-induction i)


-- Definition (Successor and predecessor functions on ℕ∞).

suc : ₂ℕ → ₂ℕ
suc α   = ₁
suc α (succ n) = α n

prd : ₂ℕ → ₂ℕ
prd α n = α(succ n)


Lemma[ℕ∞-closed-under-suc] :
-------------------------------------
  ∀ (x : ₂ℕ) → x ∈ ℕ∞ → suc x ∈ ℕ∞
-------------------------------------
Lemma[ℕ∞-closed-under-suc] x f         = λ r → refl
Lemma[ℕ∞-closed-under-suc] x f (succ i) = f i


Lemma[ℕ∞-closed-under-prd] :
-----------------------------------
  ∀ {x : ₂ℕ} → x ∈ ℕ∞ → prd x ∈ ℕ∞
-----------------------------------
Lemma[ℕ∞-closed-under-prd] {x} f  = f ∘ succ


Lemma[prd∞=∞] :
-----------
  prd ∞ ≡ ∞
-----------
Lemma[prd∞=∞] = refl

Lemma[prd∘suc=id] :
----------------
  prd ∘ suc ≡ id
---------------
Lemma[prd∘suc=id] = refl


-- Exercise: ∀ (n : ℕ) → suc(underline n) ≣ underline(succ n)


Lemma[xn≡₁→x[n+1]≡₀→x≣underline[n+1]] :
---------------------------------------------------
  ∀{x : ₂ℕ} → x ∈ ℕ∞ → ∀{n : ℕ} →
    x n ≡ ₁ → x(succ n) ≡ ₀ → x ≣ underline(succ n)
---------------------------------------------------
Lemma[xn≡₁→x[n+1]≡₀→x≣underline[n+1]] {x} m {n} r s =
 by-induction n x m r s
 where
  by-induction :  ∀(n : ℕ) →
                  ∀(x : ₂ℕ) → x ∈ ℕ∞ →
                    x n ≡ ₁ → x(succ n) ≡ ₀ → x ≣ underline(succ n)
  by-induction  x m r s i = by-cases i
   where
    by-cases : x ≣ underline 
    by-cases  = r
    by-cases (succ i) = by-nested-induction i
     where by-nested-induction : ∀(i : ℕ) → x(succ i) ≡ ₀
           by-nested-induction  = s
           by-nested-induction (succ i) =
            Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (m (succ i)) (by-nested-induction i)
  by-induction (succ n) x m r s  = by-nested-induction (succ n) r
   where
    by-nested-induction : ∀(n : ℕ) → x n ≡ ₁ → x  ≡ ₁
    by-nested-induction  t = t
    by-nested-induction (succ n) t =
     by-nested-induction n (m n t)
  by-induction (succ n) x m r s (succ i) =
   by-induction n (prd x) (Lemma[ℕ∞-closed-under-prd] m) r s i


Lemma[ℕ∞∖underline[ℕ]⊆[∞]] :
---------------------------------------------
  ∀(x : ₂ℕ) → x ∈ ℕ∞ →
   (∀(n : ℕ) → ¬(x ≣ underline n)) → x ≣ ∞
---------------------------------------------
Lemma[ℕ∞∖underline[ℕ]⊆[∞]] x m f = Lemma
 where
  Lemma : ∀(n : ℕ) → x n ≡ ₁
  Lemma  = Lemma[b≠₀→b≡₁] claim
   where
    claim : x  ≠ ₀
    claim r = f (Lemma[x0≡₀→x≣underline0] m r)
  Lemma (succ n) = Lemma[b≠₀→b≡₁] claim
   where
    IH : x n ≡ ₁
    IH = Lemma n

    claim : x(succ n) ≠ ₀
    claim r =
     f(succ n)(Lemma[xn≡₁→x[n+1]≡₀→x≣underline[n+1]] m IH r)


Lemma[density] :
-------------------------------------
  ∀(p : ₂ℕ → ₂) → extensional p →
 (∀(n : ℕ) → p(underline n) ≡ ₁) →
  p ∞ ≡ ₁ →
  ∀(x : ₂ℕ) → x ∈ ℕ∞ → p x ≡ ₁
-------------------------------------
Lemma[density] p extensionality-of-p f r x m = Lemma[b≠₀→b≡₁] Lemma
 where
  Claim : ∀(n : ℕ) → p x ≡ ₀ → ¬(x ≣ underline n)
  Claim n = (contra-positive
              (λ s → transitivity(extensionality-of-p s) (f n)))
           ∘ Lemma[b≡₀→b≠₁]

  Claim' : p x ≡ ₀ → ∀(n : ℕ) → ¬(x ≣ underline n)
  Claim' g n = Claim n g

  Claim-∞ : p x ≡ ₀ → ¬(x ≣ ∞)
  Claim-∞ = (contra-positive
              (λ s → transitivity(extensionality-of-p s) r))
           ∘ Lemma[b≡₀→b≠₁]

  Lemma : p x ≠ ₀
  Lemma t = (Claim-∞ t)(Lemma[ℕ∞∖underline[ℕ]⊆[∞]] x m (Claim' t))