Mjapp

mambo.agda

@@ -47,35 +47,11 @@ X ⇔ Y = (X ⇒ Y) ∧ (Y ⇒ X)
 ⊤ : Formula
 ⊤ = ∼ ⊥
 
-Context : Type
-Context = List Formula
-
-variable
-  Γ : Context
-
-infixl 10 _,_
-pattern _,_ Γ X = X ∷ Γ
-
+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))
 
-
-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
@@ -111,3 +87,38 @@ Example y zerotwo = succ 2 (2 ∷ []) (zero 2 [])
 
 Example2 : ExampleModel , 0 ⊩ ◇ (atom 1)
 Example2 = 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)
+
+boxed : Context → Context
+boxed [] = []
+boxed (xs , x) =  boxed xs , □ x
+
+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 ∈ Δ → Γ ++ boxed Δ ⊢ Y
+  □ᵢ : X ∈ Δ → Γ ++ boxed Δ ⊢ □ X
+  -- TODO: Add ◇