==================================
=                                =
=  §3.3.2  Pointwise continuity  =
=                                =
==================================

Chuangjie Xu, July 2019

Updated in February 2020

We construct moduli of continuity via the monadic translation and then
verify the correctness via the Fundamental Theorem of Logical Relation.

\begin{code}

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

open import Preliminaries
open import T
open import TAuxiliaries

module Continuity where

\end{code}

■ Preliminaries

\begin{code}

_is-a-modulus-of-continuity-of_ : (ℕᴺ  )  (ℕᴺ  )  Set
φ is-a-modulus-of-continuity-of f =  α β  α ≡[ φ α ] β  f α  f β

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

\end{code}

■ A nucleus for moduli of continuity

\begin{code}

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

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

-- κ(g,w) := ⟨ λα.V(g(V(w,α)),α) , λα.max(M(g(V(w,α)),α),M(w,α)) ⟩
κ : {Γ : Cxt}  T Γ ((ι  )    )
κ = Lam (Lam (Pair · Lam (Pr1 · (ν₂ · (Pr1 · ν₁ · ν₀)) · ν₀)
--  λ g   w .  ⟨     λ α . V    (g    ( V    w    α))   α
· Lam (Max · (Pr2 · (ν₂ · (Pr1 · ν₁ · ν₀)) · ν₀) · (Pr2 · ν₁ · ν₀))))
--             ,     λ α . max  ( M    (g    ( 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 continuity

\begin{code}

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 continuity of V(w) at α

--
-- η 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 β em = trans claim₀ claim₂
where
m₀ m₁ :
m₀ = M (g (V w α)) α
m₁ = M w α
em₀ : α ≡[ m₀ ] β
em₀ = ≡[≤] em (Max-spec₀ m₀ m₁)
em₁ : α ≡[ m₁ ] β
em₁ = ≡[≤] em (Max-spec₁ m₀ m₁)
claim₀ : V (g (V w α)) α  V (g (V w α)) β
claim₀ = pr₂ (ζ (V w α)) β em₀
claim₁ : V w α  V w β
claim₁ = prf β 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
continuity given by the term M(tᴶΩ).

\begin{code}

Thm[Cont] : (t : T ε (ιᶥ  ι))
M  t  · Ω  is-a-modulus-of-continuity-of  t
Thm[Cont] t = MoC-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-continuity-of V  t  · Ω
claim₁ α = pr₂ (Cor[R] t α  {n} {w}   α {n} {w}))

\end{code}