NbE for K modal logic

modalNbE.agda

{-# OPTIONS --cubical #-}

module modalNbE where

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Cubical.Foundations.Everything renaming (cong to ap)
open import Cubical.Data.Sigma

-- Data Structures

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level

infixl 20 _⊹_
data 𝐶𝑡𝑥 (ty : Type ℓ) : Type ℓ where
  ∅ : 𝐶𝑡𝑥 ty
  _⊹_ : 𝐶𝑡𝑥 ty → ty → 𝐶𝑡𝑥 ty

data 𝑉𝑎𝑟 (ty : Type ℓ) : (Γ : 𝐶𝑡𝑥 ty) (A : ty) → Type ℓ where
  𝑧𝑣 : {Γ : 𝐶𝑡𝑥 ty} {A : ty} → 𝑉𝑎𝑟 ty (Γ ⊹ A) A
  𝑠𝑣 : {Γ : 𝐶𝑡𝑥 ty} {A B : ty} → 𝑉𝑎𝑟 ty Γ A → 𝑉𝑎𝑟 ty (Γ ⊹ B) A

infixl 20 _⊕_
data 𝐸𝑙𝑠 {ty : Type ℓ₁} (el : ty → Type ℓ₂) : (Γ : 𝐶𝑡𝑥 ty) → Type (ℓ₁ ⊔ ℓ₂) where
  ! : 𝐸𝑙𝑠 el ∅
  _⊕_ : {Γ : 𝐶𝑡𝑥 ty} {A : ty} → 𝐸𝑙𝑠 el Γ → el A → 𝐸𝑙𝑠 el (Γ ⊹ A)

𝑇𝑚𝑠 : {ty : Type ℓ₁} (tm : 𝐶𝑡𝑥 ty → ty → Type ℓ₂) (Γ Δ : 𝐶𝑡𝑥 ty) → Type (ℓ₁ ⊔ ℓ₂)
𝑇𝑚𝑠 tm Γ Δ = 𝐸𝑙𝑠 (tm Γ) Δ

𝑅𝑒𝑛 : (ty : Type ℓ) → 𝐶𝑡𝑥 ty → 𝐶𝑡𝑥 ty → Type ℓ
𝑅𝑒𝑛 ty = 𝑇𝑚𝑠 (𝑉𝑎𝑟 ty)

map𝐶𝑡𝑥 : {ty₁ : Type ℓ₁} {ty₂ : Type ℓ₂} (f : ty₁ → ty₂) (Γ : 𝐶𝑡𝑥 ty₁) → 𝐶𝑡𝑥 ty₂
map𝐶𝑡𝑥 f ∅ = ∅
map𝐶𝑡𝑥 f (Γ ⊹ A) = map𝐶𝑡𝑥 f Γ ⊹ f A

map𝐸𝑙𝑠 : {ty : Type ℓ₁} {Δ : 𝐶𝑡𝑥 ty} {el₁ : ty → Type ℓ₂} {el₂ : ty → Type ℓ₃}
  (f : {A : ty} → el₁ A → el₂ A) → 𝐸𝑙𝑠 el₁ Δ → 𝐸𝑙𝑠 el₂ Δ
map𝐸𝑙𝑠 f ! = !
map𝐸𝑙𝑠 f (σ ⊕ t) = map𝐸𝑙𝑠 f σ ⊕ f t

π𝐸𝑙𝑠 : {ty : Type ℓ₁} {el : ty → Type ℓ₂} {Γ : 𝐶𝑡𝑥 ty} {A : ty} →
  𝐸𝑙𝑠 el (Γ ⊹ A) → 𝐸𝑙𝑠 el Γ
π𝐸𝑙𝑠 (σ ⊕ t) = σ

𝑧𝐸𝑙𝑠 : {ty : Type ℓ₁} {el : ty → Type ℓ₂} {Γ : 𝐶𝑡𝑥 ty} {A : ty} →
  𝐸𝑙𝑠 el (Γ ⊹ A) → el A
𝑧𝐸𝑙𝑠 (σ ⊕ t) = t

derive : {ty : Type ℓ₁} {el : ty → Type ℓ₂} {Γ : 𝐶𝑡𝑥 ty} {A : ty} →
  𝐸𝑙𝑠 el Γ → 𝑉𝑎𝑟 ty Γ A → el A
derive σ 𝑧𝑣 = 𝑧𝐸𝑙𝑠 σ
derive σ (𝑠𝑣 v) = derive (π𝐸𝑙𝑠 σ) v

_⊹⊹_ : {ty : Type ℓ} → 𝐶𝑡𝑥 ty → 𝐶𝑡𝑥 ty → 𝐶𝑡𝑥 ty
Γ ⊹⊹ ∅ = Γ
Γ ⊹⊹ (Δ ⊹ A) = (Γ ⊹⊹ Δ) ⊹ A

_⊕⊕-f_ : {ty : Type ℓ₁} {el : ty → Type ℓ₂} {Γ Δ : 𝐶𝑡𝑥 ty} {f : ty → ty} →
  𝐸𝑙𝑠 el (map𝐶𝑡𝑥 f Γ) → 𝐸𝑙𝑠 el (map𝐶𝑡𝑥 f Δ) → 𝐸𝑙𝑠 el (map𝐶𝑡𝑥 f (Γ ⊹⊹ Δ))
_⊕⊕-f_ {Δ = ∅} σ ! = σ
_⊕⊕-f_ {Δ = Δ ⊹ A} σ (τ ⊕ t) = (σ ⊕⊕-f τ) ⊕ t

module _ {ty : Type ℓ} where
  private
    ctx = 𝐶𝑡𝑥 ty
    ren = 𝑅𝑒𝑛 ty
    var = 𝑉𝑎𝑟 ty

  W₁𝑅𝑒𝑛 : {Γ Δ : ctx} (A : ty) → ren Γ Δ → ren (Γ ⊹ A) Δ
  W₁𝑅𝑒𝑛 A = map𝐸𝑙𝑠 𝑠𝑣

  W₂𝑅𝑒𝑛 : {Γ Δ : ctx} (A : ty) → ren Γ Δ → ren (Γ ⊹ A) (Δ ⊹ A)
  W₂𝑅𝑒𝑛 A σ = W₁𝑅𝑒𝑛 A σ ⊕ 𝑧𝑣

  id𝑅𝑒𝑛 : (Γ : ctx) → ren Γ Γ
  id𝑅𝑒𝑛 ∅ = !
  id𝑅𝑒𝑛 (Γ ⊹ A) = W₂𝑅𝑒𝑛 A (id𝑅𝑒𝑛 Γ)

  π𝑅𝑒𝑛 : {Γ : ctx} {A : ty} → ren (Γ ⊹ A) Γ
  π𝑅𝑒𝑛 {Γ} {A} = π𝐸𝑙𝑠 (id𝑅𝑒𝑛 (Γ ⊹ A))

  π₁𝑅𝑒𝑛 : (Γ Δ : ctx) → ren (Γ ⊹⊹ Δ) Γ
  π₁𝑅𝑒𝑛 Γ ∅ = id𝑅𝑒𝑛 Γ
  π₁𝑅𝑒𝑛 Γ (Δ ⊹ A) = W₁𝑅𝑒𝑛 A (π₁𝑅𝑒𝑛 Γ Δ)

  π₂𝑅𝑒𝑛 : (Γ Δ : ctx) → ren (Γ ⊹⊹ Δ) Δ
  π₂𝑅𝑒𝑛 Γ ∅ = !
  π₂𝑅𝑒𝑛 Γ (Δ ⊹ A) = W₂𝑅𝑒𝑛 A (π₂𝑅𝑒𝑛 Γ Δ) 

  infix 30 _[_]𝑅
  _[_]𝑅 : {Γ Δ : ctx} {A : ty} → var Δ A → ren Γ Δ → var Γ A
  v [ σ ]𝑅 = derive σ v

  infixl 30 _∘𝑅𝑒𝑛_
  _∘𝑅𝑒𝑛_ : {Γ Δ Σ : ctx} → ren Δ Σ → ren Γ Δ → ren Γ Σ
  σ ∘𝑅𝑒𝑛 τ = map𝐸𝑙𝑠 _[ τ ]𝑅 σ

-- Syntax

infixr 20 _⇒_
data Ty : Type where
  Base : Ty
  _⇒_ : Ty → Ty → Ty
  □ : Ty → Ty

Ctx = 𝐶𝑡𝑥 Ty
Var = 𝑉𝑎𝑟 Ty
Ren = 𝑅𝑒𝑛 Ty

infixl 30 Box_With_

data Tm : Ctx → Ty → Type
Tms = 𝑇𝑚𝑠 Tm

data Tm where
  V : {Γ : Ctx} {A : Ty} → Var Γ A → Tm Γ A
  Lam : {Γ : Ctx} {A B : Ty} → Tm (Γ ⊹ A) B → Tm Γ (A ⇒ B)
  App : {Γ : Ctx} {A B : Ty} → Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
  Box_With_ : {Γ Δ : Ctx} {A : Ty} →
    Tm Δ A → Tms Γ (map𝐶𝑡𝑥 □ Δ) → Tm Γ (□ A)

-- NbE

data Ne : Ctx → Ty → Type
data Nf : Ctx → Ty → Type

Nes = 𝑇𝑚𝑠 Ne

infixl 30 BOX_WITH_
data Ne where
  VN : {Γ : Ctx} {A : Ty} → Var Γ A → Ne Γ A
  APP : {Γ : Ctx} {A B : Ty} → Ne Γ (A ⇒ B) → Nf Γ A → Ne Γ B

data Nf where
  NEU : {Γ : Ctx} → Ne Γ Base → Nf Γ Base
  LAM : {Γ : Ctx} {A B : Ty} → Nf (Γ ⊹ A) B → Nf Γ (A ⇒ B)
  BOX_WITH_ : {Γ Δ : Ctx} {A : Ty} →
    Nf Δ A → Nes Γ (map𝐶𝑡𝑥 □ Δ) → Nf Γ (□ A)

infixl 20 _[_]Ne _[_]Nf

{-# TERMINATING #-}
_[_]Ne : {Δ Γ : Ctx} {A : Ty} → Ne Γ A → Ren Δ Γ → Ne Δ A
_[_]Nf : {Δ Γ : Ctx} {A : Ty} → Nf Γ A → Ren Δ Γ → Nf Δ A

VN v [ σ ]Ne = VN (derive σ v)
APP M N [ σ ]Ne = APP (M [ σ ]Ne) (N [ σ ]Nf)

NEU M [ σ ]Nf = NEU (M [ σ ]Ne)
LAM {A = A} N [ σ ]Nf = LAM (N [ W₂𝑅𝑒𝑛 A σ ]Nf)
BOX N WITH τ [ σ ]Nf = BOX N WITH (map𝐸𝑙𝑠 _[ σ ]Ne τ)

_∘NeR_ : {Γ Δ Σ : Ctx} → Nes Δ Σ → Ren Γ Δ → Nes Γ Σ
σ ∘NeR τ = map𝐸𝑙𝑠 _[ τ ]Ne σ

El : Ctx → Ty → Type
El Γ Base = Nf Γ Base
El Γ (A ⇒ B) = {Δ : Ctx} → Ren Δ Γ → El Δ A → El Δ B
El Γ (□ A) = Σ Ctx (λ Δ → Nes Γ (map𝐶𝑡𝑥 □ Δ) × El Δ A)

Els : Ctx → Ctx → Type
Els Δ Γ = 𝑇𝑚𝑠 El Δ Γ

q : {Γ : Ctx} {A : Ty} → El Γ A → Nf Γ A
u : {Γ : Ctx} {A : Ty} → Ne Γ A → El Γ A

q {A = Base} N = N
q {A = A ⇒ B} 𝒻 = LAM (q (𝒻 π𝑅𝑒𝑛 (u (VN 𝑧𝑣))))
q {A = □ A} (Δ , σ , 𝓈) = BOX q 𝓈 WITH σ

u {A = Base} M = NEU M
u {A = A ⇒ B} M σ 𝓈 = u (APP (M [ σ ]Ne) (q 𝓈))
u {A = □ A} M = (∅ ⊹ A) , (! ⊕ M), u (VN 𝑧𝑣)

_[_]El : {Δ Γ : Ctx} {A : Ty} → El Γ A → Ren Δ Γ → El Δ A
_[_]El {A = Base} N σ = N [ σ ]Nf
_[_]El {A = A ⇒ B} 𝒻 σ τ 𝓈 = 𝒻 (σ ∘𝑅𝑒𝑛 τ) 𝓈
_[_]El {A = □ A} (Δ , τ , 𝓈) σ = Δ , τ ∘NeR σ , 𝓈

unify : {Γ Δ : Ctx} → Els Γ (map𝐶𝑡𝑥 □ Δ) →
  Σ Ctx (λ Σ → Nes Γ (map𝐶𝑡𝑥 □ Σ) × Els Σ Δ)
unify {Δ = ∅} ! = ∅ , ! , !
unify {Δ = _ ⊹ _} (𝓈s ⊕ 𝓈)  with unify 𝓈s | 𝓈
... | (Γ , σ , 𝓈s) | (Δ , τ , 𝓈) =
  (Γ ⊹⊹ Δ) , (σ ⊕⊕-f τ) , (map𝐸𝑙𝑠 _[ π₁𝑅𝑒𝑛 Γ Δ ]El 𝓈s) ⊕ (𝓈 [ π₂𝑅𝑒𝑛 Γ Δ ]El)

{-# TERMINATING #-}
eval : {Γ Δ : Ctx} {A : Ty} → Tm Δ A → Els Γ Δ → El Γ A
eval (V v) 𝓈s = derive 𝓈s v
eval (Lam t) 𝓈s σ 𝓈 = eval t (map𝐸𝑙𝑠 _[ σ ]El 𝓈s ⊕ 𝓈)
eval {Γ} (App t s) 𝓈s = eval t 𝓈s (id𝑅𝑒𝑛 Γ) (eval s 𝓈s)
eval (Box t With σ) 𝓈s with unify (map𝐸𝑙𝑠 (λ s → eval s 𝓈s) σ)
... | (Δ , τ , 𝓉s) = Δ , τ , eval t 𝓉s

norm : {Γ : Ctx} {A : Ty} → Tm Γ A → Nf Γ A
norm {Γ} t = q (eval t (map𝐸𝑙𝑠 (u ∘ VN) (id𝑅𝑒𝑛 Γ)))

-- Some tests

{-# TERMINATING #-}
ιNe : {Γ : Ctx} {A : Ty} → Ne Γ A → Tm Γ A
ιNf : {Γ : Ctx} {A : Ty} → Nf Γ A → Tm Γ A

ιNe (VN v) = V v
ιNe (APP M N) = App (ιNe M) (ιNf N)

ιNf (NEU M) = ιNe M
ιNf (LAM N) = Lam (ιNf N)
ιNf (BOX N WITH σ) = Box (ιNf N) With map𝐸𝑙𝑠 ιNe σ

K : {Γ : Ctx} {A B : Ty} → Tm Γ (□ (A ⇒ B) ⇒ □ A ⇒ □ B)
K = Lam (Lam (Box (App (V (𝑠𝑣 𝑧𝑣)) (V 𝑧𝑣)) With (! ⊕ V (𝑠𝑣 𝑧𝑣) ⊕ V 𝑧𝑣)))

eg0 = K {∅} {Base} {Base}
val0 = ιNf (norm eg0)

eg1 : Tm (∅ ⊹ □ (Base ⇒ Base) ⊹ □ Base) (□ Base)
eg1 = Box (App (V (𝑠𝑣 𝑧𝑣)) (V 𝑧𝑣)) With
  (! ⊕ V (𝑠𝑣 𝑧𝑣) ⊕ Box App (V (𝑠𝑣 𝑧𝑣)) (V 𝑧𝑣) With (! ⊕ V (𝑠𝑣 𝑧𝑣) ⊕ V 𝑧𝑣))
val1 = ιNf (norm eg1)