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 0 i = 
underline (succ n) 0 = 
underline (succ n) (succ i) = underline n i 


Lemma[underline-0] : 
-------------------------------
  ∀(n : )  underline n n  
-------------------------------
Lemma[underline-0] 0 = refl
Lemma[underline-0] (succ n) = Lemma[underline-0] n 
  

Lemma[underline-1] : 
-------------------------------------
  ∀(n : )  underline(succ n) n  
-------------------------------------
Lemma[underline-1] 0 = refl
Lemma[underline-1] (succ n) = Lemma[underline-1] n 


Lemma[underline[ℕ]⊆ℕ∞] : 
-------------------------------
  ∀(n : )  underline n  ℕ∞
-------------------------------
Lemma[underline[ℕ]⊆ℕ∞] 0 i r = ⊥-elim(Lemma[b≡₁→b≠₀] r refl)
Lemma[underline[ℕ]⊆ℕ∞] (succ n) 0 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 0    x  underline 0
--------------------------------------------------
Lemma[x0≡₀→x≣underline0] {x} m base = by-induction
 where 
  by-induction : ∀(i : )  x i  
  by-induction 0 = base
  by-induction (succ i) = 
    Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (m i) (by-induction i)


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

suc : ₂ℕ  ₂ℕ
suc α 0  = 
suc α (succ n) = α n

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


Lemma[ℕ∞-closed-under-suc] : 
-------------------------------------
   (x : ₂ℕ)  x  ℕ∞  suc x  ℕ∞
-------------------------------------
Lemma[ℕ∞-closed-under-suc] x f       0  = λ 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 0 x m r s i = by-cases i
   where 
    by-cases : x  underline 1
    by-cases 0 = r
    by-cases (succ i) = by-nested-induction i
     where by-nested-induction : ∀(i : )  x(succ i)   
           by-nested-induction 0 = 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 0 = by-nested-induction (succ n) r
   where 
    by-nested-induction : ∀(n : )  x n    x 0  
    by-nested-induction 0 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 0 = Lemma[b≠₀→b≡₁] claim
   where 
    claim : x 0  
    claim r = f 0(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))