Mambo

mambo.agda

@@ -0,0 +1,79 @@
+{-# 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₁
+Rel A = A → A → Type
+
+record _×_ (A B : Type) : Type where
+  field
+    fst : A
+    snd : 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 → Γ ⊢ ⊥
+  -- ¬¬ₑ : Γ ⊢ ¬ ¬ X → Γ ⊢ X
+  -- Unsure if i want classical logic
+  -- 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) : Formula → Type where
+  top : Model , x ⊩ ⊤
+  atom : {p : Nat} → p ∈ (M.L Model x) →  Model , x ⊩ atom p
+  -- TODO: The rest :D