================================
 =                              =
 =  §3.3.2  Uniform continuity  =
 =                              =
 ================================

    Chuangjie Xu, August 2019

    Updated in February 2020

For T-definable function f : ℕᴺ → ℕ we construct a modulus of uniform
continuity, that is, a function φ : ℕᴺ → ℕ such that f is uniformly
continuous on the subspace {α : ℕᴺ | ∀i(αi ≤ δi)} with a modulus φ(δ)
for each sequence δ.

\begin{code}

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

open import Preliminaries
open import T
open import TAuxiliaries

module UniformContinuity where

\end{code}

■ Preliminaries

\begin{code}

_≤¹_ : ℕᴺ  ℕᴺ  Set
α ≤¹ β =  i  α i  β i

≤¹refl : ∀{α}  α ≤¹ α
≤¹refl i = ≤refl

✶≤¹ : {α β : ℕᴺ} {n : }  α ≤¹ tail β  n  β 0  n  α ≤¹ β
✶≤¹ u r  0      = r
✶≤¹ u r (suc i) = u i

_is-a-modulus-of-uniform-continuity-of_ : (ℕᴺ  )  (ℕᴺ  )  Set
φ is-a-modulus-of-uniform-continuity-of f =
  ∀{δ α β}  α ≤¹ δ  β ≤¹ δ  α ≡[ φ δ ] β  f α  f β

MoUC-is-extensional : {f g φ : ℕᴺ  }  (∀ α  f α  g α)
                     φ is-a-modulus-of-uniform-continuity-of g
                     φ is-a-modulus-of-uniform-continuity-of f
MoUC-is-extensional {f} {g} {φ} ex mcg {δ} {α} {β} u v em = begin
  f α ≡⟨ ex α 
  g α ≡⟨ mcg u v em 
  g β ≡⟨ sym (ex β) 
  f β 

--
-- If f is uniformly continuous on Δ = {α : ℕᴺ | ∀i(αi ≤ δi)} with a
-- modulus m, then it has a maximum image Ψ(m,f,δ) on Δ.
--
Ψ : {Γ : Cxt}  T Γ (ι  (ιᶥ  ι)  ιᶥ  ι)
Ψ = Rec · Lam (Lam (ν₁ · ν₀))
--   rec (λ f   δ  → f δ)
        · Lam (Lam (Lam (Lam (Φ · Lam (ν₃ · Lam (ν₃ · (ν₁  ν₀)) · (Tail · ν₁)) · (Head · ν₀)))))
--       (λ n   g    f    δ → Φ  (λ i → g  (λ α → f   (i ✶ α))     (tail δ))      (head δ))
-- i.e.
-- Ψ  0      f δ = f 0ʷ
-- Ψ (suc n) f δ = Φ (λ i → Ψ n (λ α → f (i ✶ α)) (tail δ)) (head δ)

Ψ-spec : {Γ : Cxt} (γ :  Γ ⟧ˣ) {f : ℕᴺ  } {δ : ℕᴺ}
        (m : )  (∀{α β}  α ≤¹ δ  β ≤¹ δ  α ≡[ m ] β  f α  f β)
         α  α ≤¹ δ  f α   Ψ ⟧ᵐ γ m f δ
Ψ-spec γ {f} {δ}  0      p α r = ≤refl' (p r ≤¹refl ≡[zero])
Ψ-spec γ {f} {δ} (suc m) p α r = ≤trans claim₁ (≤trans claim₂ claim₃)
 where
  s : head α  tail α ≤¹ δ
  s  0      = r 0
  s (suc i) = r (suc i)
  claim₀ : f α  f (head α  tail α)
  claim₀ = p r s (≡[suc] refl ≡[]-refl)
  claim₁ : f α  f (head α  tail α)
  claim₁ = ≤refl' claim₀
  q : ∀{α' β}  α' ≤¹ tail δ  β ≤¹ tail δ  α' ≡[ m ] β  f (head α  α')  f (head α  β)
  q u v em = p (✶≤¹ u (r 0)) (✶≤¹ v (r 0)) (≡[suc] refl em)
  claim₂ : f (head α  tail α)   Ψ ⟧ᵐ γ m  β  f (head α  β)) (tail δ)
  claim₂ = Ψ-spec γ m q (tail α) (r  suc)
  claim₃ :  Ψ ⟧ᵐ γ m  β  f (head α  β)) (tail δ)   Ψ ⟧ᵐ γ (suc m) f δ
  claim₃ = Φ-spec (r 0) γ  i   Ψ ⟧ᵐ γ m  β  f (i  β)) (tail δ))
  --   ⟦ Ψ ⟧ᵐ γ (suc m) f δ
  -- ≡ ⟦ Φ ⟧ᵐ γ (λ i → ⟦ Ψ ⟧ᵐ γ m (λ β → f (i ✶ β)) (tail δ)) (head δ)

\end{code}

■ A nucleus for uniform continuity

\begin{code}

 : Ty
 = (ιᶥ  ι)  (ιᶥ  ι)

η : {Γ : Cxt}  T Γ (ι  )
η = Lam (Pair · Lam ν₁ · Lam Zero)
-- λ n . ⟨ λα.n , λα.0 ⟩

κ : {Γ : Cxt}  T Γ ((ι  )    )
κ = Lam (Lam (Pair · Lam (Pr1 · (ν₂ · (Pr1 · ν₁ · ν₀)) · ν₀)
--  λ g   w →   (  ( λ α → V    (g    (V     w    α))   α )
                   · Lam (Max · (Φ · Lam (Pr2 · (ν₃ · ν₀) · ν₁) · (Ψ · (Pr2 · ν₁ · ν₀) · (Pr1 · ν₁) · ν₀)) · (Pr2 · ν₁ · ν₀))))
--               , ( λ δ → max  (Φ  (λ i → M    (g    i)   δ)    (Ψ   (M     w    δ)    (V     w)    δ))   (M     w    δ)))

--
-- Instantiate the translation by importing the following module
-- with the nucleus (Jι, η, κ)
--
open import GentzenTranslation  η κ

\end{code}

■ The generic element Ω

\begin{code}

-- Α(n) := ⟨ λα.αn , λα.n+1 ⟩
Α : {Γ : Cxt}  T Γ (ι  )
Α = Lam (Pair · Lam (ν₀ · ν₁) · Lam (Suc · ν₁))
--  λ n .     ⟨ λ α . α   n   , λ α . n+1 ⟩
Ω : {Γ : Cxt}  T Γ (  )
Ω = κ · Α

\end{code}

■ A parametrized logical relation for uniform continuity

\begin{code}

private

 V M : (ℕᴺ  ) × (ℕᴺ  )  ℕᴺ  
 V = pr₁  -- value component
 M = pr₂  -- modulus component

--
-- Base case of the logical relation
--
 : ℕᴺ   ι ⟧ʸ    ⟧ʸ  Set
 δ n w =  (n  V w δ)
         -- n is the value of w at δ
          × (∀{α β}  α ≤¹ δ  β ≤¹ δ  α ≡[ M w δ ] β  V w α  V w β)
         -- M(w,δ) is a modulus of uniform continuity of V(w) on inputs bounded by δ

--
-- η preserves the logical relation
--
 : (δ : ℕᴺ)
    {Γ : Cxt} (γ :  Γ ⟧ˣ) (n :  ι ⟧ʸ)   δ n ( η ⟧ᵐ γ n)
 δ _ n = refl ,  _ _ _  refl)

--
-- κ preserves the logical relation
--
 : (δ : ℕᴺ)
    {Γ : Cxt} (γ :  Γ ⟧ˣ) {f :  ι  ι ⟧ʸ} {g :  ι   ⟧ʸ}
    (∀ i   δ (f i) (g i))   {n w}   δ n w   δ (f n) ( κ ⟧ᵐ γ g w)
 δ γ {f} {g} ζ {n} {w} (e , prf) = trans e₀ e₁ , goal
 where
  e₀ : f n  V (g n) δ
  e₀ = pr₁ (ζ n)
  e₁ : V (g n) δ  V (g (V w δ)) δ
  e₁ = ap  x  V (g x) δ) e
  m : 
  m = M ( κ ⟧ᵐ γ g w) δ
  goal : ∀{α β}  α ≤¹ δ  β ≤¹ δ  α ≡[ m ] β
        V (g (V w α)) α  V (g (V w β)) β
  goal {α} {β} u v em = trans claim₀ claim₂
   where
    m₀ m₁ m₂ : 
    m₀ = M (g (V w α)) δ
    m₁ =  Φ ⟧ᵐ γ  i  M (g i) δ) ( Ψ ⟧ᵐ γ (M w δ) (V w) δ)
    m₂ = M w δ
    m₀≤m₁ : m₀  m₁
    m₀≤m₁ = Φ-spec (Ψ-spec γ (M w δ) prf α u) γ  i  M (g i) δ)
    m₀≤m : m₀  m
    m₀≤m = ≤trans m₀≤m₁ (Max-spec₀ m₁ m₂)
    em₀ : α ≡[ m₀ ] β
    em₀ = ≡[≤] em m₀≤m
    em₂ : α ≡[ m₂ ] β
    em₂ = ≡[≤] em (Max-spec₁ m₁ m₂)
    claim₀ : V (g (V w α)) α  V (g (V w α)) β
    claim₀ = pr₂ (ζ (V w α)) u v em₀
    claim₁ : V w α  V w β
    claim₁ = prf u v em₂
    claim₂ : V (g (V w α)) β  V (g (V w β)) β
    claim₂ = ap  x  V (g x) β) claim₁

--
-- Ω preserves the logical relation
--
 : (δ : ℕᴺ)
    ∀{n w}   δ n w   δ (δ n) ( Ω  w)
 -- i.e.  R δ δ ⟦ Ω ⟧
 δ {n} {w} =  δ  claim {n} {w}
 where
  claim :  i   δ (δ i) ( Α  i)
  claim i = refl ,  _ _ em  ≡[]-< em ≤refl)

--
-- Extend Rι to R for all types of T
--
R : ℕᴺ  {ρ : Ty}   ρ ⟧ʸ    ρ ⟩ᴶ ⟧ʸ  Set
R δ = LR._R_
 where
  import LogicalRelation  η κ ( δ) ( δ) ( δ) as LR

--
-- Corollary of the Fundamental Theorem of Logical Relation
--
Cor[R] : {ρ : Ty} (t : T ε ρ) (δ : ℕᴺ)  R δ  t   t  
Cor[R] t δ = LR.FTLR t 
 where
  import LogicalRelation  η κ ( δ) ( δ) ( δ) as LR

\end{code}

■ Theorem: Every closed term t : ℕᴺ ⇾ ℕ of T has a modulus of
           uniform continuity given by the term M(tᴶΩ).

\begin{code}

Thm[UC] : (t : T ε (ιᶥ  ι))
         M  t  · Ω  is-a-modulus-of-uniform-continuity-of  t 
Thm[UC] t = MoUC-is-extensional claim₀ claim₁
 where
  claim₀ :  α   t  α  V  t  · Ω  α
  claim₀ α = pr₁ (Cor[R] t α  {n} {w}   α {n} {w}))
  claim₁ : M  t  · Ω  is-a-modulus-of-uniform-continuity-of V  t  · Ω 
  claim₁ {δ} = pr₂ (Cor[R] t δ  {n} {w}   δ {n} {w}))


Mᵘᶜ : T ε (ιᶥ  ι)
     ℕᴺ  
Mᵘᶜ t = M  t  · Ω 

\end{code}