{-# OPTIONS --no-import-sorts #-}
open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Nat
open import Agda.Builtin.List

data Bottom : Type where

¬ : Type → Type
¬ A = A → Bottom

Rel : Type → Type → Type₁
Rel A B = A → B → Type

data Σ (A : Type) (B : A -> Type) : Type where
 pair : (a : A) -> (b : B a) -> Σ A B

∃ : {A : Type} (B : A → Type) → Type
∃ {A} B = Σ A B

record _×_ (A B : Type) : Type where
  field
    fst : A
    snd : B

data _∪_ (A B : Type) : Type where
  inl : A → A ∪ B
  inr : B → A ∪ B

data Formula : Type where
  ⊥ : Formula
  atom : Nat → Formula
  ∼_ : Formula → Formula
  □_ : Formula → Formula
  _∧_ : Formula → Formula → Formula
  _∨_ : Formula → Formula → Formula
  _⇒_ : Formula → Formula → Formula

infixr 4 _⇒_
infix 19 _∧_

variable
  A B C X Y Z : Formula

_⇔_ : Formula → Formula → Formula
X ⇔ Y = (X ⇒ Y) ∧ (Y ⇒ X)

⊤ : Formula
⊤ = ∼ ⊥

◇_ : Formula → Formula
◇ p = ∼ (□ (∼ p))

infix 9 _∈_
data _∈_ {A : Type} : A → List A → Type where
  zero : (x : A) (xs : List A) → x ∈ (x ∷ xs)
  succ : {y : A} (x : A) (xs : List A) → (x ∈ xs) → (x ∈ (y ∷ xs))

record M (W : Type) : Type₁ where
  field
    R : Rel W W
    L : W → List Nat

infix 2 _,_⊩_
_,_⊩_ : {W : Type} (Model : M W) (x : W) (p : Formula) → Type 
Model , x ⊩ ⊥ = Bottom
Model , x ⊩ atom n = n ∈ M.L Model x
Model , x ⊩ (∼ (□ (∼ p))) = ∃ λ y → M.R Model x y → Model , y ⊩ p -- Alias for ◇ p
Model , x ⊩ (∼ p) = ¬ (Model , x ⊩ p)
Model , x ⊩ (p ∧ q) = (Model , x ⊩ p) × (Model , x ⊩ q)
Model , x ⊩ (p ∨ q) = (Model , x ⊩ p) ∪ (Model , x ⊩ q)
Model , x ⊩ p ⇒ q = Model , x ⊩ p → Model , x ⊩ q
Model , x ⊩ (□ p) = ∀ y → M.R Model x y → Model , y ⊩ p 

data R : Nat → Nat → Type where
  zeroone : R 0 1
  zerotwo : R 0 2
  onetwo  : R 1 2

ExampleModel : M Nat
ExampleModel .M.R = R

ExampleModel .M.L 0 = 0 ∷ []
ExampleModel .M.L 1 = 1 ∷ 2 ∷ []
ExampleModel .M.L 2 = 0 ∷ 2 ∷ []
ExampleModel .M.L _ = []

ExampleSem : ExampleModel , 0 ⊩ □ (atom 2)
ExampleSem y zeroone = succ 2 (2 ∷ []) (zero 2 [])
ExampleSem y zerotwo = succ 2 (2 ∷ []) (zero 2 [])

Example2Sem : ExampleModel , 0 ⊩ ◇ (atom 1)
Example2Sem = pair 1 (λ _ → zero 1 (2 ∷ []))

Context : Type
Context = List Formula

variable
  Γ Δ : Context

infixl 10 _,_
pattern _,_ Γ X = X ∷ Γ

infix 10 _++_
_++_ : {A : Type} → List A → List A → List A
[] ++ ys = ys
(xs , x) ++ ys = xs ++ (x ∷ ys)

infixr 2 _/_⊢_
data _/_⊢_ (Δ Γ : Context) : Formula → Type where
  var : X ∈ Γ → Δ / Γ ⊢ X
  mp : Δ / Γ ⊢ X ⇒ Y → Δ / Γ ⊢ X → Δ / Γ ⊢ Y
  ∧ᵢ : Δ / Γ ⊢ X → Δ / Γ ⊢ Y → Δ / Γ ⊢ X ∧ Y
  ∧ₑ₁ : Δ / Γ ⊢ X ∧ Y → Δ / Γ ⊢ X
  ∧ₑ₂ : Δ / Γ ⊢ X ∧ Y → Δ / Γ ⊢ Y
  ∨ᵢ₁ : Δ / Γ ⊢ X → Δ / Γ ⊢ X ∨ Y
  ∨ᵢ₂ : Δ / Γ ⊢ Y → Δ / Γ ⊢ X ∨ Y
  ∨ₑ : Δ / Γ ⊢ X ∨ Y → Δ / Γ , X ⊢ Z → Δ / Γ , Y ⊢ Z → Δ / Γ ⊢ Z
  ⇒ᵢ : Δ / Γ , X ⊢ Y → Δ / Γ ⊢ X ⇒ Y
  ¬ᵢ : Δ / Γ , X ⊢ ⊥ → Δ / Γ ⊢ ∼ X
  ¬ₑ : Δ / Γ ⊢ X → Δ / Γ ⊢ ∼ X → Δ / Γ ⊢ ⊥
  □ᵢ : [] / Δ ⊢ X → Δ / Γ ⊢ □ X
  □ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y
  -- TODO: Maybe make it KT45

K : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y)
K {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y)))))
                      (□ₑ (var (succ (□(X ⇒ Y)) ([] , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) [])))
                      (□ᵢ (mp
                        (var (zero (X ⇒ Y) ([] , X)))
                        (var (succ X ([] , X) (zero X []))))))))

ExampleSyn : [] / [] ⊢ □ X ⇒ □ (Y ⇒ X)
ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) [])) (□ᵢ (⇒ᵢ (var (succ X ([] , X) (zero X []))))))

ExampleSyn2 : [] / [] ⊢ □(A ∧ B) ⇒ (□ A ∧ □ B)
ExampleSyn2 {A} {B} = ⇒ᵢ (∧ᵢ (□ₑ (var (zero (□ (A ∧ B)) [])) (□ᵢ (∧ₑ₁ (var (zero (A ∧ B) []))))) (□ₑ (var (zero (□ (A ∧ B)) [])) (□ᵢ (∧ₑ₂ (var (zero (A ∧ B) []))))))

ExampleSyn3 : [] / [] ⊢ (□ A ∧ □ B) ⇒ □(A ∧ B)
ExampleSyn3 {A} {B} = ⇒ᵢ (□ₑ (∧ₑ₁ (var (zero ((□ A) ∧ (□ B)) []))) (□ₑ (∧ₑ₂ (var (zero ((□ A) ∧ (□ B)) []))) (□ᵢ (∧ᵢ (var (succ A ([] , A) (zero A []))) (var (zero B ([] , A)))))))