diff --git a/mambo.agda b/mambo.agda index a4db8db..8d44fc6 100644 --- a/mambo.agda +++ b/mambo.agda @@ -1,10 +1,14 @@ {-# 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 +infixl 10 _,_ +data Stack (A : Type) : Type where + ∙ : Stack A + _,_ : Stack A → A → Stack A + ¬ : Type → Type ¬ A = A → Bottom @@ -58,14 +62,14 @@ X ⇔ Y = (X ⇒ Y) ∧ (Y ⇒ X) ◇ 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)) +data _∈_ {A : Type} : A → Stack A → Type where + zero : (x : A) (xs : Stack A) → x ∈ (xs , x) + succ : {y : A} (x : A) (xs : Stack A) → (x ∈ xs) → (x ∈ (xs , y)) record M (W : Type) : Type₁ where field R : Rel W W - L : W → List Nat + L : W → Stack Nat infix 2 _,_⊩_ _,_⊩_ : {W : Type} (Model : M W) (x : W) (p : Formula) → Type @@ -86,39 +90,37 @@ data R : Nat → Nat → Type where 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 _ = [] +ExampleModel .M.L 0 = ∙ , 0 +ExampleModel .M.L 1 = ∙ , 2 , 1 +ExampleModel .M.L 2 = ∙ , 2 , 0 +ExampleModel .M.L _ = ∙ KSem : ExampleModel , 0 ⊩ □ (atom 1 ⇒ atom 2) ⇒ (□ atom 1 ⇒ □ atom 2) -KSem x x₁ y zeroone = succ 2 (2 ∷ []) (zero 2 []) -KSem x x₁ y zerotwo = succ 2 (2 ∷ []) (zero 2 []) +KSem x x₁ y zeroone = succ 2 (∙ , 2) (zero 2 ∙) +KSem x x₁ y zerotwo = succ 2 (∙ , 2) (zero 2 ∙) ExampleSem : ExampleModel , 0 ⊩ □ (atom 2) -ExampleSem y zeroone = succ 2 (2 ∷ []) (zero 2 []) -ExampleSem y zerotwo = succ 2 (2 ∷ []) (zero 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 ∷ [])) +Example2Sem = pair 1 (λ _ → zero 1 (∙ , 2)) Context : Type -Context = List Formula +Context = Stack Formula variable Γ Δ Γ' Δ' : Context -infixl 10 _,_ -pattern _,_ Γ X = X ∷ Γ infix 9 _++_ -_++_ : {A : Type} → List A → List A → List A -[] ++ ys = ys -(x ∷ xs) ++ ys = x ∷ (xs ++ ys) +_++_ : {A : Type} → Stack A → Stack A → Stack A +xs ++ ∙ = xs +xs ++ ys , y = (xs ++ ys) , y infix 8 _⊆_ -_⊆_ : {A : Type} → (Γ Γ' : List A) → Type +_⊆_ : {A : Type} → (Γ Γ' : Stack A) → Type _⊆_ {A} Γ Γ' = ∀ {X} → X ∈ Γ → X ∈ Γ' infixr 2 _/_⊢_ @@ -135,18 +137,18 @@ data _/_⊢_ (Δ Γ : Context) : Formula → Type where ¬ᵢ : Δ / Γ , X ⊢ ⊥ → Δ / Γ ⊢ ∼ X ¬ₑ : Δ / Γ ⊢ ∼ X → Δ / Γ ⊢ X → Δ / Γ ⊢ ⊥ ⊥ₑ : Δ / Γ ⊢ ⊥ → Δ / Γ ⊢ X - □ᵢ : [] / Δ ⊢ X → Δ / Γ ⊢ □ X + □ᵢ : ∙ / Δ ⊢ X → Δ / Γ ⊢ □ X □ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y -- TODO: Maybe make it KT45 -inSwap : {A : Type} {X Y Z : A} (Γ Γ' : List A) → Z ∈ (Γ' ++ Γ , X , Y) → Z ∈ (Γ' ++ Γ , Y , X) -inSwap Γ [] (zero x xs) = succ x (Γ , x) (zero x Γ) -inSwap Γ [] (succ x xs (zero x₁ xs₁)) = zero x (Γ , _) -inSwap Γ [] (succ x xs (succ x₁ xs₁ x₂)) = succ x (Γ , _) (succ x Γ x₂) -inSwap Γ (Γ' , x₁) (zero x xs) = zero x₁ (Γ' ++ Γ , _ , _) -inSwap Γ (Γ' , x₁) (succ x xs x₂) = succ x (Γ' ++ Γ , _ , _) (inSwap Γ Γ' x₂) +inSwap : {A : Type} {X Y Z : A} (Γ Γ' : Stack A) → Z ∈ (Γ , X , Y ++ Γ') → Z ∈ (Γ , Y , X ++ Γ') +inSwap Γ ∙ (zero x xs) = succ x (Γ , x) (zero x Γ) +inSwap Γ ∙ (succ x xs (zero x₁ xs₁)) = zero x (Γ , _) +inSwap Γ ∙ (succ x xs (succ x₁ xs₁ x₂)) = succ x (Γ , _) (succ x Γ x₂) +inSwap Γ (Γ' , x₁) (zero x xs) = zero x₁ (Γ , _ , _ ++ Γ') +inSwap Γ (Γ' , x₁) (succ x xs x₂) = succ x (Γ , _ , _ ++ Γ') (inSwap Γ Γ' x₂) -exchange : (Γ' : Context) → Δ / Γ' ++ (Γ , A , B) ⊢ C → Δ / Γ' ++ (Γ , B , A) ⊢ C +exchange : (Γ' : Context) → Δ / (Γ , A , B) ++ Γ' ⊢ C → Δ / (Γ , B , A) ++ Γ' ⊢ C exchange Γ' (var x) = var (inSwap _ Γ' x) exchange Γ' (mp x x₁) = mp (exchange Γ' x) (exchange Γ' x₁) exchange Γ' (∧ᵢ x x₁) = ∧ᵢ (exchange Γ' x) (exchange Γ' x₁) @@ -162,7 +164,7 @@ exchange Γ' (⊥ₑ x) = ⊥ₑ (exchange Γ' x) exchange Γ' (□ᵢ x) = □ᵢ x exchange Γ' (□ₑ x x₁) = □ₑ (exchange Γ' x) (exchange Γ' x₁) -exchange-modal : (Δ' : Context) → Δ' ++ Δ , A , B / Γ ⊢ C → Δ' ++ Δ , B , A / Γ ⊢ C +exchange-modal : (Δ' : Context) → Δ , A , B ++ Δ' / Γ ⊢ C → Δ , B , A ++ Δ' / Γ ⊢ C exchange-modal Δ' (var x) = var x exchange-modal Δ' (mp x x₁) = mp (exchange-modal Δ' x) (exchange-modal Δ' x₁) exchange-modal Δ' (∧ᵢ x x₁) = ∧ᵢ (exchange-modal Δ' x) (exchange-modal Δ' x₁) @@ -178,7 +180,7 @@ exchange-modal Δ' (⊥ₑ x) = ⊥ₑ (exchange-modal Δ' x) exchange-modal Δ' (□ᵢ x) = □ᵢ (exchange Δ' x) exchange-modal Δ' (□ₑ x x₁) = □ₑ (exchange-modal Δ' x) (exchange-modal (Δ' , _) x₁) -inBoth : {A : Type} {Γ Γ' : List A} {X : A} → Γ ⊆ Γ' → (Γ , X) ⊆ (Γ' , X) +inBoth : {A : Type} {Γ Γ' : Stack A} {X : A} → Γ ⊆ Γ' → (Γ , X) ⊆ (Γ' , X) inBoth {A} {Γ} {Γ'} {X} x {X₁} (zero x₁ xs) = zero X Γ' inBoth {A} {Γ} {Γ'} {X} x {X₁} (succ x₁ xs x₂) = succ X₁ Γ' (x x₂) @@ -214,10 +216,10 @@ weak-modal (⊥ₑ x) x₁ = ⊥ₑ (weak-modal x x₁) weak-modal (□ᵢ x) x₁ = □ᵢ (weak x x₁) weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁)) -cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B -cut [] x (var x₁) = mp (⇒ᵢ (var x₁)) x -cut (Γ' , x₂) x (var (zero x₁ xs)) = var (zero x₂ (Γ' ++ _)) -cut (Γ' , x₂) x (var (succ _ xs x₃)) = weak (cut Γ' x (var x₃)) λ {X} → succ X (Γ' ++ _) +cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / (Γ , A) ++ Γ' ⊢ B → Δ / Γ ++ Γ' ⊢ B +cut ∙ x (var x₁) = mp (⇒ᵢ (var x₁)) x +cut (Γ' , x₂) x (var (zero x₁ xs)) = var (zero x₂ (_ ++ Γ')) +cut (Γ' , x₂) x (var (succ _ xs x₃)) = weak (cut Γ' x (var x₃)) λ {X} → succ X (_ ++ Γ') cut Γ' x (mp x₁ x₂) = mp (cut Γ' x x₁) (cut Γ' x x₂) cut Γ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut Γ' x x₁) (cut Γ' x x₂) cut Γ' x (∧ₑ₁ x₁) = ∧ₑ₁ (cut Γ' x x₁) @@ -232,7 +234,7 @@ cut Γ' x (⊥ₑ x₁) = ⊥ₑ (cut Γ' x x₁) cut Γ' x (□ᵢ x₁) = □ᵢ x₁ cut Γ' x (□ₑ x₁ x₂) = □ₑ (cut Γ' x x₁) (cut Γ' (weak-modal x (λ {X = X₁} → succ X₁ _)) x₂) -cut-modal : (Δ' : Context) → [] / Δ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B +cut-modal : (Δ' : Context) → ∙ / Δ ⊢ A → (Δ , A) ++ Δ' / Γ ⊢ B → Δ ++ Δ' / Γ ⊢ B cut-modal Δ' x (var x₁) = var x₁ cut-modal Δ' x (mp x₁ x₂) = mp (cut-modal Δ' x x₁) (cut-modal Δ' x x₂) cut-modal Δ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂) @@ -248,15 +250,15 @@ cut-modal Δ' x (⊥ₑ x₁) = ⊥ₑ (cut-modal Δ' x x₁) cut-modal Δ' x (□ᵢ x₁) = □ᵢ (cut Δ' x x₁) cut-modal Δ' x (□ₑ x₁ x₂) = □ₑ (cut-modal Δ' x x₁) (cut-modal (Δ' , _) x x₂) -KSym : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y) -KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y))))) - (□ₑ (var (succ (□(X ⇒ Y)) ([] , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) []))) +KSym : ∙ / ∙ ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y) +KSym {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 [])))))))) + (var (zero (X ⇒ Y) (∙ , X))) + (var (succ X (∙ , X) (zero X ∙)))))))) -MTSym : [] / [] ⊢ (A ⇒ B) ⇒ ∼ B ⇒ ∼ A -MTSym {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) ([] , (A ⇒ B) , (∼ B)) (zero (∼ B) ([] , (A ⇒ B))))) (mp (var (succ (A ⇒ B) ([] , (A ⇒ B) , (∼ B)) (succ (A ⇒ B) ([] , (A ⇒ B)) (zero (A ⇒ B) [])))) (var (zero A ([] , (A ⇒ B) , (∼ B)))))))) +MTSym : ∙ / ∙ ⊢ (A ⇒ B) ⇒ ∼ B ⇒ ∼ A +MTSym {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) (∙ , (A ⇒ B) , (∼ B)) (zero (∼ B) (∙ , (A ⇒ B))))) (mp (var (succ (A ⇒ B) (∙ , (A ⇒ B) , (∼ B)) (succ (A ⇒ B) (∙ , (A ⇒ B)) (zero (A ⇒ B) ∙)))) (var (zero A (∙ , (A ⇒ B) , (∼ B)))))))) DedSym : Δ / Γ ⊢ A ⇒ B → Δ / Γ , A ⊢ B DedSym {Δ} {Γ} {A} {B} (var x) = mp (var (succ (A ⇒ B) Γ x)) (var (zero A Γ)) @@ -271,15 +273,15 @@ DedSym {Δ} {Γ} {A} {B} (□ₑ x x₁) = mp (weak (□ₑ x x₁) (λ {X = X DedSymInv : Δ / Γ , A ⊢ B → Δ / Γ ⊢ A ⇒ B DedSymInv {Δ} {Γ} {A} {B} x = ⇒ᵢ x -ExampleSyn : [] / [] ⊢ □ X ⇒ □ (Y ⇒ X) -ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ 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) [])))))) +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))))))) +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))))))) -ExampleSyn4 : [] / [] ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B) -ExampleSyn4 {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ B)) ([] , (□ (A ⇒ B)) , (◇ A)))) (□ₑ (var (succ (□ (A ⇒ B)) ([] , (□ (A ⇒ B)) , (◇ A)) (succ (□ (A ⇒ B)) ([] , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) [])))) (¬ₑ (var (succ (∼ (□ (∼ A))) ([] , (□ (A ⇒ B)) , (◇ A)) - (zero (∼ (□ (∼ A))) ([] , (□ (A ⇒ B)))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ ( ∼ B) ([] , (∼ B) , (A ⇒ B)) (succ (∼ B) ([] , (∼ B)) (zero (∼ B) [])))) (mp (var (succ (A ⇒ B) ([] , (∼ B) , (A ⇒ B)) (zero (A ⇒ B) ([] , (∼ B))))) (var (zero A ([] , (∼ B) , (A ⇒ B))))))))))))) +ExampleSyn4 : ∙ / ∙ ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B) +ExampleSyn4 {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ B)) (∙ , (□ (A ⇒ B)) , (◇ A)))) (□ₑ (var (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B)) , (◇ A)) (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) ∙)))) (¬ₑ (var (succ (∼ (□ (∼ A))) (∙ , (□ (A ⇒ B)) , (◇ A)) + (zero (∼ (□ (∼ A))) (∙ , (□ (A ⇒ B)))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ ( ∼ B) (∙ , (∼ B) , (A ⇒ B)) (succ (∼ B) (∙ , (∼ B)) (zero (∼ B) ∙)))) (mp (var (succ (A ⇒ B) (∙ , (∼ B) , (A ⇒ B)) (zero (A ⇒ B) (∙ , (∼ B))))) (var (zero A (∙ , (∼ B) , (A ⇒ B)))))))))))))