module GenericConvergentSequence where

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

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

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

ℕ∞ : Set
ℕ∞ = ⁅ α ∶ ₂ℕ ∣ decreasing α ⁆


-- Definition (Extensional equality on ℕ∞):

_≣_ : (u v : ℕ∞)  → Prp
u ≣ v = ∀ i → incl u i ≡ incl v i

-- Definition (Extensional functions on ℕ∞).
extensional : {Z : Set} → (ℕ∞ → Z) → Prp
extensional f = ∀{u v : ℕ∞} → u ≣ v → f u ≡ f v


-- We now describe the elements of ℕ∞ explicitly.  
--
-- First the curried characteristic function of the (>) relation on ℕ,
-- seen as a function into the Cantor space.

bigger : ℕ → ₂ℕ
bigger  i = ₀
bigger (succ n)  = ₁
bigger (succ n) (succ i) = bigger n i


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


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


-- Definition (Embedding of ℕ into ℕ∞).
under : ℕ → ℕ∞
under n = bigger n || m n
 where
  m :  ∀(n : ℕ) → decreasing(bigger n)
  m  i r = ⊥-elim(Lemma[b≡₁→b≠₀] r refl)
  m (succ n)  r = refl
  m (succ n) (succ i) r = m n i r


-- Definition (Point at infinity).
∞ : ℕ∞
∞ = (λ i → ₁) || λ i r → refl


Lemma[under0] :
-------------------------------------------------------
  ∀{u : ℕ∞} → incl u  ≡ ₀ → u ≣ under 
-------------------------------------------------------
Lemma[under0] {α || m} base = by-induction
 where
  by-induction : ∀(i : ℕ) → α i ≡ ₀
  by-induction  = base
  by-induction (succ i) =
    Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] (m i) (by-induction i)


Lemma[under1] :
--------------------------------------------------------------
  ∀(u : ℕ∞) → ∀(n : ℕ) →
    incl u n ≡ ₁ → incl u(succ n) ≡ ₀ → u ≣ under(succ n)
--------------------------------------------------------------
Lemma[under1] (α || m) n r s =
 by-induction n α m r s
 where
  by-induction :
   ∀(n : ℕ) → ∀(α : ₂ℕ) → decreasing α →
                α n ≡ ₁ → α(succ n) ≡ ₀ → ∀ i → α i ≡ bigger(succ n) i
  by-induction  α m r s i = by-cases i
   where
    by-cases : ∀ i → α i ≡ bigger  i
    by-cases  = r
    by-cases (succ i) = by-nested-induction i
     where by-nested-induction : ∀(i : ℕ) → α(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) α m r s  = by-nested-induction (succ n) r
   where
    by-nested-induction : ∀(n : ℕ) → α n ≡ ₁ → α  ≡ ₁
    by-nested-induction  t = t
    by-nested-induction (succ n) t =
     by-nested-induction n (m n t)
  by-induction (succ n) α m r s (succ i) =
   by-induction n (α ∘ succ) (m ∘ succ) r s i


Lemma[ℕ∞∖under[ℕ]⊆[∞]] :
------------------------------------------------------
  ∀(u : ℕ∞) → (∀(n : ℕ) → ¬(u ≣ under n)) → u ≣ ∞
------------------------------------------------------
Lemma[ℕ∞∖under[ℕ]⊆[∞]] u f = Lemma
 where
  Lemma : ∀(n : ℕ) → incl u n ≡ ₁
  Lemma  = Lemma[b≠₀→b≡₁] claim
   where
    claim : incl u  ≠ ₀
    claim r = f  (Lemma[under0] {u} r)
  Lemma (succ n) = Lemma[b≠₀→b≡₁] claim
   where
    IH : incl u n ≡ ₁
    IH = Lemma n

    claim : incl u(succ n) ≠ ₀
    claim r = f(succ n)(Lemma[under1] u n IH r)


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

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

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

   Lemma : p u ≠ ₀
   Lemma t = (Claim-∞ t)(Lemma[ℕ∞∖under[ℕ]⊆[∞]] u (Claim' t))