Tehee

mambo.agda

@@ -17,6 +17,15 @@ data Σ (A : Type) (B : A -> Type) : Type where
 ∃ : {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
@@ -72,15 +81,33 @@ record M (W : Type) : Type₁ where
     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
+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) = ¬ (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 
+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 _ = []
+
+Example : ExampleModel , 0 ⊩ □ (atom 2)
+Example y zeroone = succ 2 (2 ∷ []) (zero 2 [])
+Example y zerotwo = succ 2 (2 ∷ []) (zero 2 [])
+
+Example2 : ExampleModel , 0 ⊩ ◇ (atom 1)
+Example2 = pair 1 (λ _ → zero 1 (2 ∷ []))