=================================
 =                               =
 =  Example: uniform continuity  =
 =                               =
 =================================

    Chuangjie Xu, August 2019

\begin{code}

{-# OPTIONS --without-K --safe #-}

open import Preliminaries
open import T

module UniformContinuity where

\end{code}

■ Preliminaries

\begin{code}

_≪_ : ℕᴺ → ℕᴺ → Set
α ≪ β = ∀ i → α i ≤ β i

0ʷ≪ : {α : ℕᴺ} → 0ʷ ≪ α
0ʷ≪ = λ i → ≤zero

_✶_ : {A : Set} → A → A ᴺ → A ᴺ
(a ✶ u)         = a
(a ✶ u) (succ i) = u i

✶≪ : {α θ : ℕᴺ} {n : ℕ} → α ≪ tail θ → n ≤ θ  → (n ✶ α) ≪ θ
✶≪ u r         = r
✶≪ u r (succ i) = u i

--
-- maximum image of uniformly continuous functions
--
MI : (ℕᴺ → ℕ) → ℕᴺ → ℕ → ℕ
MI f θ         = f 0ʷ
MI f θ (succ m) = φ (λ i → MI (λ α → f (i ✶ α)) (tail θ) m) (head θ)

MI-spec : {f : ℕᴺ → ℕ} {θ : ℕᴺ}
        → (m : ℕ) → ((α β : ℕᴺ) → α ≪ θ → β ≪ θ → α ≡[ m ] β → f α ≡ f β)
        → (α : ℕᴺ) → α ≪ θ → f α ≤ MI f θ m
MI-spec  p α u = ≤refl' (p α 0ʷ u 0ʷ≪ ≡[zero])
MI-spec {f} {θ} (succ m) p α u = ≤trans claim₁ (≤trans claim₂ claim₃)
 where
  w : (head α ✶ tail α) ≪ θ
  w         = u 
  w (succ i) = u (succ i)
  claim₀ : f α ≡ f (head α ✶ tail α)
  claim₀ = p α (head α ✶ tail α) u w (≡[succ] refl ≡[]-refl)
  claim₁ : f α ≤ f (head α ✶ tail α)
  claim₁ = ≤refl' claim₀
  p' : (α' β : ℕᴺ) → α' ≪ tail θ → β ≪ tail θ → α' ≡[ m ] β → f (α  ✶ α') ≡ f (α  ✶ β)
  p' α' β u' v em = p (α  ✶ α') (α  ✶ β) (✶≪ u' (u )) (✶≪ v (u )) (≡[succ] refl em)
  claim₂ : f (head α ✶ tail α) ≤ MI (λ β → f (α  ✶ β)) (tail θ) m
  claim₂ = MI-spec m p' (tail α) (u ∘ succ)
  claim₃ : MI (λ β → f (α  ✶ β)) (tail θ) m ≤ MI f θ (succ m)
  claim₃ = φ-spec {α } {θ } (u )

\end{code}

■ A nucleus for moduli of uniform continuity

\begin{code}

ℕᴶ : Set
ℕᴶ = (ℕᴺ → ℕ) × (ℕᴺ → ℕ)

V = pr₁
M = pr₂

η : ℕ → ℕᴶ
η n = (λ α → n) , (λ γ → )

κ : (ℕ → ℕᴶ) → ℕᴶ → ℕᴶ
κ g x = (λ α → V (g (V x α)) α)
      , (λ γ → max (M x γ) (φ (λ i → M (g i) γ) (MI (V x) γ (M x γ))))

Ω : ℕᴶ → ℕᴶ
Ω = κ (λ n → (λ α → α n) , (λ γ → succ n))

⟪_⟫ʸ : Ty → Set
⟪ ι ⟫ʸ     = ℕᴶ
⟪ σ ⇾ τ ⟫ʸ = ⟪ σ ⟫ʸ → ⟪ τ ⟫ʸ

KE : {ρ : Ty} → (ℕ → ⟪ ρ ⟫ʸ) → ℕᴶ → ⟪ ρ ⟫ʸ
KE {ι}     g = κ g
KE {_ ⇾ ρ} g = λ n a → KE (λ x → g x a) n

⟪_⟫ˣ : Cxt → Set
⟪ ε ⟫ˣ     = 𝟙
⟪ Γ ₊ ρ ⟫ˣ = ⟪ Γ ⟫ˣ × ⟪ ρ ⟫ʸ

_₍_₎ᴶ : {Γ : Cxt} {ρ : Ty} → ⟪ Γ ⟫ˣ → ∥ ρ ∈ Γ ∥ → ⟪ ρ ⟫ʸ
(_ , a) ₍ zero ₎ᴶ   = a
(γ , _) ₍ succ i ₎ᴶ = γ ₍ i ₎ᴶ

⟪_⟫ᵐ : {Γ : Cxt} {σ : Ty} → T Γ σ → ⟪ Γ ⟫ˣ → ⟪ σ ⟫ʸ
⟪ Var i ⟫ᵐ γ = γ ₍ i ₎ᴶ
⟪ Lam t ⟫ᵐ γ = λ a → ⟪ t ⟫ᵐ (γ , a)
⟪ f · a ⟫ᵐ γ = ⟪ f ⟫ᵐ γ (⟪ a ⟫ᵐ γ)
⟪ Zero ⟫ᵐ  _ = η 
⟪ Succ ⟫ᵐ  _ = λ x → (succ ∘ V x , M x)
⟪ Rec ⟫ᵐ   _ = λ a f → KE (rec a (f ∘ η))

infix  _ᴶ

_ᴶ : {ρ : Ty} → T ε ρ → ⟪ ρ ⟫ʸ
t ᴶ = ⟪ t ⟫ᵐ ⋆

\end{code}

■ Theorem: For any f : ℕᴺ → ℕ of T, the term M (fᴶ Ω) is a modulus of
           uniformly continuous of f.

\begin{code}

Mᵘᶜ : T ε ((ι ⇾ ι) ⇾ ι) → ℕᴺ → ℕ
Mᵘᶜ f = M ((f ᴶ) Ω)

Theorem : (f : T ε ((ι ⇾ ι) ⇾ ι))
        → (θ α β : ℕᴺ) → α ≪ θ → β ≪ θ → α ≡[ Mᵘᶜ f θ ] β → ⟦ f ⟧ α ≡ ⟦ f ⟧ β

\end{code}

■ Proof

\begin{code}

R : {ρ : Ty} → ℕᴺ → ⟪ ρ ⟫ʸ → ⟦ ρ ⟧ʸ → Set
R {ι}     θ w n = (V w θ ≡ n)
                × ((α β : ℕᴺ) → α ≪ θ → β ≪ θ → α ≡[ M w θ ] β → V w α ≡ V w β)
R {σ ⇾ τ} θ f g = (x : ⟪ σ ⟫ʸ) (y : ⟦ σ ⟧ʸ) → R θ x y → R θ (f x) (g y)

R[KE] : {ρ : Ty} {θ : ℕᴺ}
      → {f : ℕ → ⟪ ρ ⟫ʸ} {g : ℕ → ⟦ ρ ⟧ʸ}
      → ((i : ℕ) → R θ (f i) (g i))
      → R θ (KE f) g
R[KE] {ι} {θ} {f} {g} ζ w n (e , p) = eq , pr
 where
  eq : V (f (V w θ)) θ ≡ g n
  eq = begin
       V (f (V w θ)) θ ≡⟨ pr₁ (ζ (V w θ)) ⟩
       g (V w θ)       ≡⟨ ap g e ⟩
       g n             ∎
  pr : (α β : ℕᴺ) → α ≪ θ → β ≪ θ → α ≡[ M (KE f w) θ ] β
     → V (f (V w α)) α ≡ V (f (V w β)) β
  pr α β u v em = begin
                  V (f (V w α)) α ≡⟨ ap (λ x → V (f x) α) claim₀ ⟩
                  V (f (V w β)) α ≡⟨ pr₂ (ζ (V w β)) α β u v (≡[≤] em claim₂) ⟩
                  V (f (V w β)) β ∎
   where
    claim₀ : V w α ≡ V w β
    claim₀ = p α β u v (≡[≤] em (Max-spec₀ _ _))
    claim₁ : M (f (V w β)) θ ≤ φ (λ i → M (f i) θ) (MI (V w) θ (M w θ))
    claim₁ = φ-spec (MI-spec (M w θ) p β v)
    claim₂ : M (f (V w β)) θ ≤ M (KE f w) θ
    claim₂ = ≤trans claim₁ (Max-spec₁ (M w θ) _)
R[KE] {σ ⇾ τ} ζ _ _ χ _ _ ξ = R[KE] (λ i → ζ i _ _ ξ) _ _ χ

Rˣ : {Γ : Cxt} → ℕᴺ → ⟪ Γ ⟫ˣ → ⟦ Γ ⟧ˣ → Set
Rˣ {ε}     θ  ⋆       ⋆      = 𝟙
Rˣ {Γ ₊ ρ} θ (δ , x) (γ , y) = Rˣ θ δ γ × R θ x y

R[Var] : {Γ : Cxt} {ρ : Ty} {δ : ⟪ Γ ⟫ˣ} {γ : ⟦ Γ ⟧ˣ} {θ : ℕᴺ}
       → Rˣ θ δ γ → (i : ∥ ρ ∈ Γ ∥) → R θ (δ ₍ i ₎ᴶ) (γ ₍ i ₎)
R[Var] (_ , χ)  zero    = χ
R[Var] (ζ , _) (succ i) = R[Var] ζ i

R[η] : {n : ℕ} {θ : ℕᴺ} → R θ (η n) n
R[η] = refl , (λ _ _ _ _ _ → refl)

Lemma[R] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ) (θ : ℕᴺ)
         → {δ : ⟪ Γ ⟫ˣ} {γ : ⟦ Γ ⟧ˣ} → Rˣ θ δ γ
         → R θ (⟪ t ⟫ᵐ δ) (⟦ t ⟧ᵐ γ)
Lemma[R] (Var i) θ ζ = R[Var] ζ i
Lemma[R] (Lam t) θ ζ = λ _ _ χ → Lemma[R] t θ (ζ , χ)
Lemma[R] (f · a) θ ζ = Lemma[R] f θ ζ _ _ (Lemma[R] a θ ζ)
Lemma[R] Zero    _ _ = R[η]
Lemma[R] Succ    _ _ = λ _ _ χ → ap succ (pr₁ χ)
                               , λ α β u v em → ap succ (pr₂ χ α β u v em)
Lemma[R] Rec     _ _ = λ _ _ χ _ _ ξ → R[KE] (ind χ λ _ p → ξ _ _ R[η] _ _ p)

R[Ω] : (θ : ℕᴺ) → R θ Ω θ
R[Ω] θ (f , Mᶠ) n (e , p) = eq , pr
 where
  eq : θ (f θ) ≡ θ n
  eq = ap θ e
  pr : (α β : ℕᴺ) → α ≪ θ → β ≪ θ
     → α ≡[ M (Ω (f , Mᶠ)) θ ] β → α (f α) ≡ β (f β)
  pr α β u v em = begin
                  α (f α) ≡⟨ ≡[]-< em claim₁ ⟩
                  β (f α) ≡⟨ ap β claim₂ ⟩
                  β (f β) ∎
   where
    claim₀ : f α < φ succ (MI f θ (Mᶠ θ))
    claim₀ = φ-spec (MI-spec (Mᶠ θ) p α u)
    claim₁ : f α < M (Ω (f , Mᶠ)) θ
    claim₁ = ≤trans claim₀ (Max-spec₁ (Mᶠ θ) _)
    claim₂ : f α ≡ f β
    claim₂ = p α β u v (≡[≤] em (Max-spec₀ _ _))

Lemma[≐] : (f : T ε ((ι ⇾ ι) ⇾ ι))
         → (α : ℕᴺ) → V ((f ᴶ) Ω) α ≡ ⟦ f ⟧ α
Lemma[≐] f α = pr₁ (Lemma[R] f α ⋆ Ω α (R[Ω] α))

Lemma[UC] : (f : T ε ((ι ⇾ ι) ⇾ ι))
          → (θ α β : ℕᴺ) → α ≪ θ → β ≪ θ → α ≡[ Mᵘᶜ f θ ] β
          → V ((f ᴶ) Ω) α ≡ V ((f ᴶ) Ω) β
Lemma[UC] f θ = pr₂ (Lemma[R] f θ ⋆ Ω θ (R[Ω] θ))

{-
Theorem : (f : T ε ((ι ⇾ ι) ⇾ ι))
        → (θ α β : ℕᴺ) → α ≪ θ → β ≪ θ → α ≡[ Mᵘᶜ f θ ] β → ⟦ f ⟧ α ≡ ⟦ f ⟧ β
-}
Theorem f θ α β u v em = begin
                         ⟦ f ⟧ α       ≡⟨ sym (Lemma[≐] f α) ⟩
                         V ((f ᴶ) Ω) α ≡⟨ Lemma[UC] f θ α β u v em ⟩
                         V ((f ᴶ) Ω) β ≡⟨ Lemma[≐] f β ⟩
                         ⟦ f ⟧ β       ∎

\end{code}