{-

An illustration of the McKinsey-Tarski translation of intuitionistic
propositional logic into the modal logic S4, or normalisation by evaluation
for the simply typed λ-calculus.

-}

module IPCMcKinseyTarski where

open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Data.String using (String)
open import Data.Unit using () renaming (⊤ to Unit ; tt to unit)
open import Function using (_∘_)
open import Relation.Binary using (Reflexive ; Transitive ; _Respects_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)


-- Propositional variables.

Atom : Set
Atom = String


-- Generic contexts.

data Cx (Ty : Set) : Set where
  ∅   : Cx Ty
  _,_ : Cx Ty → Ty → Cx Ty


-- Context extensions.

data _⊆_ {Ty : Set} : Cx Ty → Cx Ty → Set where
  refl⊆ : ∀ {Γ} → Γ ⊆ Γ
  wk⊆   : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ ⊆ (Γ′ , A)

trans⊆ : ∀ {Ty} {Γ Γ′ Γ″ : Cx Ty} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
trans⊆ η refl⊆    = η
trans⊆ η (wk⊆ η′) = wk⊆ (trans⊆ η η′)


-- Syntax.

infixl 6 _∧_
infixr 5 _⊃_
data Ty : Set where
  ι_  : Atom → Ty
  ⊤  : Ty
  _∧_ : Ty → Ty → Ty
  _⊃_ : Ty → Ty → Ty

infix 0 _⊢_
data _⊢_ : Cx Ty → Ty → Set where
  hyp  : ∀ {Γ A}                           → Γ , A ⊢ A
  wk   : ∀ {Γ A B} → Γ ⊢ A               → Γ , B ⊢ A
  unit : ∀ {Γ}                             → Γ ⊢ ⊤
  pair : ∀ {Γ A B} → Γ ⊢ A     → Γ ⊢ B → Γ ⊢ A ∧ B
  fst  : ∀ {Γ A B} → Γ ⊢ A ∧ B           → Γ ⊢ A
  snd  : ∀ {Γ A B} → Γ ⊢ A ∧ B           → Γ ⊢ B
  lam  : ∀ {Γ A B} → Γ , A ⊢ B           → Γ ⊢ A ⊃ B
  app  : ∀ {Γ A B} → Γ ⊢ A ⊃ B → Γ ⊢ A → Γ ⊢ B

mono⊢ : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ refl⊆   t = t
mono⊢ (wk⊆ η) t = wk (mono⊢ η t)


-- Intuitionistic Kripke models.

record Model : Set₁ where
  field
    World : Set

    -- Accessibility.
    _≤_    : World → World → Set
    refl≤  : Reflexive _≤_
    trans≤ : Transitive _≤_

    -- Forcing for propositional variables.
    _⊩∙_   : World → Atom → Set
    mono⊩∙ : ∀ {x} → (_⊩∙ x) Respects _≤_

open Model {{...}}


-- Semantics, after McKinsey-Tarski.

infix 0 _⊨_
_⊨_ : ∀ {{_ : Model}} → World → Ty → Set
w ⊨ (ι x) = w ⊩∙ x
w ⊨ ⊤    = Unit
w ⊨ A ∧ B = (w ⊨ A) × (w ⊨ B)
w ⊨ A ⊃ B = ∀ {w′} → w ≤ w′ → (w′ ⊨ A) → (w′ ⊨ B)

mono⊨ : ∀ {{_ : Model}} {w w′} A → w ≤ w′ → w ⊨ A → w′ ⊨ A
mono⊨ (ι x)   ξ s = mono⊩∙ ξ s
mono⊨ ⊤      ξ s = unit
mono⊨ (A ∧ B) ξ s = mono⊨ A ξ (proj₁ s) , mono⊨ B ξ (proj₂ s)
mono⊨ (A ⊃ B) ξ s = λ ξ′ a → s (trans≤ ξ ξ′) a


-- Closure over contexts.

infix 0 _⊨*_
_⊨*_ : ∀ {{_ : Model}} → World → Cx Ty → Set
w ⊨* ∅     = Unit
w ⊨* Γ , A = (w ⊨* Γ) × (w ⊨ A)

mono⊨* : ∀ {{_ : Model}} {w w′} Γ → w ≤ w′ → w ⊨* Γ → w′ ⊨* Γ
mono⊨* ∅       ξ unit    = unit
mono⊨* (Γ , A) ξ (γ , a) = mono⊨* Γ ξ γ , mono⊨ A ξ a


-- The canonical model.

instance
  ⟪IPC⟫ : Model
  ⟪IPC⟫ = record
    { World   = Cx Ty
    ; _≤_     = _⊆_
    ; refl≤   = refl⊆
    ; trans≤  = trans⊆
    ; _⊩∙_   = λ w x → w ⊢ ι x
    ; mono⊩∙ = mono⊢
    }


-- Completeness and soundness with respect to the canonical model.

mutual
  reify : ∀ {Γ} A → Γ ⊨ A → Γ ⊢ A
  reify (ι x)   s = s
  reify ⊤      s = unit
  reify (A ∧ B) s = pair (reify A (proj₁ s)) (reify B (proj₂ s))
  reify (A ⊃ B) s = lam (reify B (s (wk⊆ refl⊆) (reflect A hyp)))

  reflect : ∀ {Γ} A → Γ ⊢ A → Γ ⊨ A
  reflect (ι x)   t = t
  reflect ⊤      t = unit
  reflect (A ∧ B) t = reflect A (fst t) , reflect B (snd t)
  reflect (A ⊃ B) t = λ ξ a → reflect B (app (mono⊢ ξ t) (reify A a))


-- TODO: What is the right name for this?

id⊨* : ∀ {Γ} → Γ ⊨* Γ
id⊨* {∅}     = unit
id⊨* {Γ , A} = mono⊨* Γ (wk⊆ refl⊆) id⊨* , reflect A hyp


-- Forcing for propositions.

infix 0 _⊩_
_⊩_ : Cx Ty → Ty → Set₁
Γ ⊩ A = ∀ {{m : Model}} {w : World {{m}}} → w ⊨* Γ → w ⊨ A


-- Completeness.

quot : ∀ {Γ A} → Γ ⊩ A → Γ ⊢ A
quot {A = A} t = reify A (t id⊨*)


-- Soundness.

eval : ∀ {Γ A} → Γ ⊢ A → Γ ⊩ A
eval hyp    (γ , a) = a
eval (wk t) (γ , a) = eval t γ
eval unit         γ = unit
eval (pair t₁ t₂) γ = eval t₁ γ , eval t₂ γ
eval (fst t)      γ = proj₁ (eval t γ)
eval (snd t)      γ = proj₂ (eval t γ)
eval (lam t)      γ = λ ξ a → eval t (mono⊨* _ ξ γ , a)
eval (app t₁ t₂)  γ = (eval t₁ γ) refl≤ (eval t₂ γ)


-- TODO: What is the right name for this?

canon₁ : ∀ {Γ} A → Γ ⊩ A → Γ ⊨ A
canon₁ A = reflect A ∘ quot

canon₂ : ∀ {Γ} A → Γ ⊨ A → Γ ⊩ A
canon₂ A = eval ∘ reify A


-- Normalisation by evaluation.

norm : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A
norm = quot ∘ eval