```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))
```