{-# 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

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

infixr 4 _⇒_

variable
  X Y Z : Formula

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

⊤ : Formula
⊤ = ∼ ⊥

Context : Type
Context = List Formula

variable
  Γ : Context

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

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))


infixr 2 _⊢_
data _⊢_ : Context → Formula → Type where
  var : X ∈ Γ → Γ ⊢ X
  ∧ᵢ : Γ ⊢ X → Γ ⊢ Y → Γ ⊢ X ∧ Y
  ∧ₑ₁ : Γ ⊢ X ∧ Y → Γ ⊢ X
  ∧ₑ₂ : Γ ⊢ X ∧ Y → Γ ⊢ Y
  ∨ᵢ₁ : Γ ⊢ X → Γ ⊢ X ∨ Y
  ∨ᵢ₂ : Γ ⊢ Y → Γ ⊢ X ∨ Y
  ∨ₑ : Γ ⊢ X ∨ Y → Γ , X ⊢ Z → Γ , Y ⊢ Z → Γ ⊢ Z
  mp : Γ ⊢ X ⇒ Y → Γ ⊢ X → Γ ⊢ Y 
  ⇒ᵢ : Γ , X ⊢ Y → Γ ⊢ X ⇒ Y
  ¬ᵢ : Γ , X ⊢ ⊥ → Γ ⊢ ∼ X
  ¬ₑ : Γ ⊢ X → Γ ⊢ ∼ X → Γ ⊢ ⊥
  -- TODO: entailments for ◇ and □

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

infixr 2 _,_⊩_
data _,_⊩_ {W : Type} (Model : M W) (x : W) : (p : Formula) → Type where
  top : Model , x ⊩ ⊤
  atom : {p : Nat} → p ∈ (M.L Model x) →  Model , x ⊩ atom p
  neg : {p : Formula} → ¬ (Model , x ⊩ p) → Model , x ⊩ ∼ p
  and : {p q : Formula} → Model , x ⊩ p → Model , x ⊩ q → Model , x ⊩ p ∧ q
  orl : {p q : Formula} → Model , x ⊩ p → Model , x ⊩ p ∨ q
  orr : {p q : Formula} → Model , x ⊩ q → Model , x ⊩ p ∨ q
  impl : {p q : Formula} → Model , x ⊩ p → Model , x ⊩ q → Model , x ⊩ p ⇒ q 
  -- impln : {p q : Formula} → ¬ (Model , x ⊩ p) → Model , x ⊩ p ⇒ q 
  box : {p : Formula} → (∀ (y : W) → M.R Model x y → Model , y ⊩ p) → Model , x ⊩ □ p
  dia : {p : Formula} → (∃ λ (y : W) → M.R Model x y → Model , y ⊩ p) → Model , x ⊩ ◇ p