module nbe where

{-
The implicational fragment of intuitionistic logic,
its soundness w.r.t. Agda (via Tarski-ish semantics),
and its soundness and completeness w.r.t. Kripke semantics,

presented here by Tillmann Rendel.


Checked with the development version of Agda,
latest commit from Tue Nov 10 17:35:20 2015 +0100,
commit hash 5297d70ee87c32dc7817d51f2c611eb7426cae8b.


Naming convention:

foo  acts on a proposition.
foo′ acts on a single formula.
foo″ acts on multiple formulae.
foo‴ is universally quantified over all models

-}

-- Relations

Relation : Set → Set → Set₁
Relation A B = A → B → Set

Reflexive : ∀ {A} → Relation A A → Set
Reflexive _~_ = ∀ {x} → x ~ x

Transitive : ∀ {A} → Relation A A → Set
Transitive _~_ = ∀ {x y z} → x ~ y → y ~ z → x ~ z

Monotone : ∀ {A} → Relation A A → (A → Set) → Set
Monotone _~_ P = ∀ {x y} → x ~ y → P x → P y

-- Propositions

postulate
  Proposition : Set

-- Formulas

data Formula : Set where
  prop : Proposition → Formula
  _⊃_ : Formula → Formula → Formula

infixr 22 _⊃_

-- Formulae

data Formulae : Set where
  ∅ : Formulae
  _,_ : Formula → Formulae → Formulae

infixr 21 _,_

data _≼_ : Relation Formulae Formulae where
  done : ∅ ≼ ∅
  drop : ∀ {A Γ Δ} →
    Γ ≼ Δ →
    Γ ≼ A , Δ
  take : ∀ {A Γ Δ} →
    Γ ≼ Δ →
    A , Γ ≼ A , Δ

≼-reflexive : Reflexive _≼_
≼-reflexive {∅} = done
≼-reflexive {A , Γ} = take ≼-reflexive

≼-transitive : Transitive _≼_
≼-transitive done done = done
≼-transitive Γ≼Δ (drop Δ≼Θ) = drop (≼-transitive Γ≼Δ Δ≼Θ)
≼-transitive (drop Γ≼Δ) (take Δ≼Θ) = drop (≼-transitive Γ≼Δ Δ≼Θ)
≼-transitive (take Γ≼Δ) (take Δ≼Θ) = take (≼-transitive Γ≼Δ Δ≼Θ)
  
data _∈_ A : Formulae → Set where
  this : ∀ {Γ} →
    A ∈ A , Γ
  that : ∀ {B Γ} →
    A ∈ Γ →
    A ∈ B , Γ

∈-monotone : ∀ {A} → Monotone _≼_ (A ∈_)
∈-monotone (done) ()
∈-monotone (drop Γ≼Δ) i = that (∈-monotone Γ≼Δ i)
∈-monotone (take Γ≼Δ) this = this
∈-monotone (take Γ≼Δ) (that i) = that (∈-monotone Γ≼Δ i)

-- Proofs

data _⊢′_ : Formulae → Formula → Set where
  assumption : ∀ {A Γ} →
    A ∈ Γ →
    Γ ⊢′ A
  ⊃E : ∀ {A B Γ} →
    Γ ⊢′ A ⊃ B →
    Γ ⊢′ A →
    Γ ⊢′ B
  ⊃I : ∀ {A B Γ} →
    A , Γ ⊢′ B →
    Γ ⊢′ A ⊃ B

_⊢_ : Formulae → Proposition → Set
_⊢_ Γ p = Γ ⊢′ prop p

data _⊢″_ (Γ : Formulae) : Formulae → Set where
  ∅ :
    Γ ⊢″ ∅
  _,_ : ∀ {A Δ} →
    Γ ⊢′ A →
    Γ ⊢″ Δ →
    Γ ⊢″ A , Δ

⊢-monotone′ : ∀ A → Monotone _≼_ (_⊢′ A)
⊢-monotone′ A Γ≼Δ (assumption A∈Γ) =
  assumption (∈-monotone Γ≼Δ A∈Γ)
⊢-monotone′ B Γ≼Δ (⊃E {A} Γ⊢′A⊃B Γ⊢′A) =
  ⊃E (⊢-monotone′ (A ⊃ B) Γ≼Δ Γ⊢′A⊃B) (⊢-monotone′ A Γ≼Δ Γ⊢′A)
⊢-monotone′ (A ⊃ B) Γ≼Δ (⊃I A,Γ⊢′B) =
  ⊃I (⊢-monotone′ B (take Γ≼Δ) A,Γ⊢′B)

⊢-monotone : ∀ p → Monotone _≼_ (_⊢ p)
⊢-monotone p = ⊢-monotone′ (prop p)

⊢-monotone″ : ∀ Θ → Monotone _≼_ (_⊢″ Θ)
⊢-monotone″ ∅ Γ≼Δ ∅ = ∅
⊢-monotone″ (A , Θ) Γ≼Δ (Γ⊢A , Γ⊢Θ) =
  ⊢-monotone′ A Γ≼Δ Γ⊢A , ⊢-monotone″ Θ Γ≼Δ Γ⊢Θ

≼→⊢″ : ∀ {Γ Δ} → Δ ≼ Γ → Γ ⊢″ Δ
≼→⊢″ done = ∅
≼→⊢″ (drop Δ≼Γ) =  ⊢-monotone″ _ (drop ≼-reflexive) (≼→⊢″ Δ≼Γ)
≼→⊢″ (take Δ≼Γ) = assumption this , ≼→⊢″ (drop Δ≼Γ)

-- Truth à la Tarski

record ⊤ : Set where
  constructor tt

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    prj₁ : A
    prj₂ : B

record Tarski : Set₁ where
  field _⊨_ : Proposition → Set

open Tarski

_⊨′_ : Tarski → Formula  → Set
M ⊨′ prop p = M ⊨ p
M ⊨′ A ⊃ B = M ⊨′ A → M ⊨′ B

_⊨″_ : Tarski → Formulae → Set
M ⊨″ ∅ = ⊤
M ⊨″ A , Γ = (M ⊨′ A) × (M ⊨″ Γ)

_⊨‴_ : Formulae → Formula → Set₁
Γ ⊨‴ A = ∀ {M} → M ⊨″ Γ → M ⊨′ A

∈→⊨‴ : ∀ {Γ A} → A ∈ Γ → Γ ⊨‴ A
∈→⊨‴ this (M⊧A , M⊧Γ) = M⊧A
∈→⊨‴ (that A∈Γ) (M⊧B , M⊧Γ) = ∈→⊨‴ A∈Γ M⊧Γ

⊢→⊨‴ : ∀ {Γ A} → Γ ⊢′ A → Γ ⊨‴ A
⊢→⊨‴ (assumption i) ρ = ∈→⊨‴ i ρ
⊢→⊨‴ (⊃E p q) ρ = (⊢→⊨‴ p ρ) (⊢→⊨‴ q ρ)
⊢→⊨‴ (⊃I p) ρ x = ⊢→⊨‴ p (x , ρ)

-- Truth à la Kripke

record Kripke : Set₁ where
  -- set of worlds
  field World : Set

  -- reflexive and transitive reachability
  field _≤_ : Relation World World
  field reflexive : Reflexive _≤_
  field transitive : Transitive _≤_

  -- forcing of propositions
  field _⊩_ : World → Proposition → Set
  field monotone : ∀ p → Monotone _≤_ (_⊩ p)

  -- forcing of formulae
  _⊩′_ : World → Formula → Set
  w ⊩′ prop p = w ⊩ p
  w ⊩′ A ⊃ B = ∀ {u} → w ≤ u → u  ⊩′ A → u ⊩′ B

  monotone′ : ∀ A → Monotone _≤_ (_⊩′ A)
  monotone′ (prop p) = monotone p
  monotone′ (A ⊃ B) w≤u f u≤v v⊩A = f (transitive w≤u u≤v) v⊩A

  -- forcing of formula sets
  _⊩″_ : World → Formulae → Set
  w ⊩″ ∅ = ⊤
  w ⊩″ A , Γ = (w ⊩′ A) × (w ⊩″ Γ)

  monotone″ : ∀ Γ → Monotone _≤_ (_⊩″ Γ)
  monotone″ ∅ w≤u w⊩Γ = tt
  monotone″ (A , Γ) w≤u (w⊩A , w⊩Γ) =
    monotone′ A w≤u w⊩A , monotone″ Γ w≤u w⊩Γ

forces = Kripke._⊩_
forces′ = Kripke._⊩′_
forces″ = Kripke._⊩″_

syntax forces M w p =  w ⊩₍ M ₎ p
syntax forces′ M w A = w ⊩′₍ M ₎ A
syntax forces″ M w Γ = w ⊩″₍ M ₎ Γ

_⊩‴_ : Formulae → Formula → Set₁
Γ ⊩‴ A = ∀ {M w} → w ⊩″₍ M ₎ Γ → w ⊩′₍ M ₎ A

-- soundness
∈→⊩‴ : ∀ {Γ A} → A ∈ Γ → Γ ⊩‴ A
∈→⊩‴ this (w⊩A , w⊩Γ) = w⊩A
∈→⊩‴ (that A∈Γ) (w⊩B , w⊩Γ) = ∈→⊩‴ A∈Γ w⊩Γ

⊢→⊩′ : ∀ Γ A → Γ ⊢′ A → Γ ⊩‴ A
⊢→⊩′ Γ A (assumption A∈Γ) w⊩Γ = ∈→⊩‴ A∈Γ w⊩Γ
⊢→⊩′ Γ B (⊃E {A} Γ⊢A⊃B Γ⊢A) {M} w⊩Γ = (⊢→⊩′ Γ (A ⊃ B) Γ⊢A⊃B w⊩Γ) (Kripke.reflexive M) (⊢→⊩′ Γ A Γ⊢A w⊩Γ)
⊢→⊩′ Γ (A ⊃ B) (⊃I A,Γ⊢B) {M} w⊩Γ w≤u w⊩A = ⊢→⊩′ (A , Γ) B A,Γ⊢B (w⊩A , (Kripke.monotone″ M Γ w≤u w⊩Γ))

-- term model
terms : Kripke
terms = record
  { World = Formulae
  ; _≤_ = _≼_
  ; reflexive = ≼-reflexive
  ; transitive = ≼-transitive
  ; _⊩_ = _⊢_
  ; monotone = ⊢-monotone
  }

-- type-directed partial evaluation
module _ where
  open Kripke terms

  -- for propositions
  ↑ : ∀ {Γ} p → Γ ⊢ p → Γ ⊩ p
  ↓ : ∀ {Γ} p → Γ ⊩ p → Γ ⊢ p

  ↑ p Γ⊢p = Γ⊢p
  ↓ p Γ⊩p = Γ⊩p

  -- for a single formula
  ↑′ : ∀ {Γ} A → Γ ⊢′ A → Γ ⊩′ A
  ↓′ : ∀ {Γ} A → Γ ⊩′ A → Γ ⊢′ A

  ↑′ (prop p) Γ⊢p = ↑ p Γ⊢p
  ↑′ (A ⊃ B) Γ⊢A⊃B Γ≼Δ Δ⊩A = ↑′ B (⊃E (⊢-monotone′ (A ⊃ B) Γ≼Δ Γ⊢A⊃B) (↓′ A Δ⊩A))

  ↓′ (prop p) Γ⊩p = ↓ p Γ⊩p
  ↓′ (A ⊃ B) Γ⊩A = ⊃I (↓′ B (Γ⊩A (drop ≼-reflexive) (↑′ A (assumption this))))

  -- for multiple formulae
  ↑″ : ∀ {Γ} Δ → Γ ⊢″ Δ → Γ ⊩″ Δ
  ↑″ ∅ x = tt
  ↑″ (A , Δ) (Γ⊢A , Γ⊢Δ) = ↑′ A Γ⊢A , ↑″ Δ Γ⊢Δ

  ↓″ : ∀ {Γ} Δ → Γ ⊩″ Δ → Γ ⊢″ Δ
  ↓″ ∅ tt = ∅
  ↓″ (A , Δ) (Γ⊩A , Γ⊩Δ) = ↓′ A Γ⊩A , ↓″ Δ Γ⊩Δ

-- soundess and completeness

sound : ∀ Γ A → Γ ⊢′ A → (∀ M w → w ⊩″₍ M ₎ Γ → w ⊩′₍ M ₎ A)
sound Γ A Γ⊢A M w w⊩Γ = ⊢→⊩′ Γ A Γ⊢A w⊩Γ

complete : ∀ Γ A → (∀ M w → w ⊩″₍ M ₎ Γ → w ⊩′₍ M ₎ A) → Γ ⊢′ A
complete Γ A f = ↓′ A (f terms Γ (↑″ Γ (≼→⊢″ ≼-reflexive)))