255 lines
12 KiB
Agda
255 lines
12 KiB
Agda
{-# 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
|
||
|
||
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
|
||
|
||
orₑ : {A B C : Type} → A ∪ B → (A → C) → (B → C) → C
|
||
orₑ (inl x) f g = f x
|
||
orₑ (inr x) f g = g x
|
||
|
||
absurd : {A : Type} → Bottom → A
|
||
absurd ()
|
||
|
||
data Formula : Type where
|
||
⊥ : Formula
|
||
atom : Nat → Formula
|
||
∼_ : (p : Formula) → Formula
|
||
□_ : (p : Formula) → Formula
|
||
_∧_ : (p q : Formula) → Formula
|
||
_∨_ : (p q : Formula) → Formula
|
||
_⇒_ : (p q : Formula) → Formula
|
||
|
||
infixr 4 _⇒_
|
||
infix 19 _∧_
|
||
|
||
variable
|
||
A B C X Y Z : Formula
|
||
|
||
_⇔_ : Formula → Formula → Formula
|
||
X ⇔ Y = (X ⇒ Y) ∧ (Y ⇒ X)
|
||
|
||
⊤ : Formula
|
||
⊤ = ∼ ⊥
|
||
|
||
◇_ : Formula → Formula
|
||
◇ 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))
|
||
|
||
record M (W : Type) : Type₁ where
|
||
field
|
||
R : Rel W W
|
||
L : W → List Nat
|
||
|
||
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))) = ∃ λ y → M.R Model x y → Model , y ⊩ p -- Alias for ◇ p
|
||
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
|
||
|
||
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 _ = []
|
||
|
||
|
||
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 [])
|
||
|
||
ExampleSem : ExampleModel , 0 ⊩ □ (atom 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 ∷ []))
|
||
|
||
Context : Type
|
||
Context = List 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)
|
||
|
||
infix 8 _⊆_
|
||
_⊆_ : {A : Type} → (Γ Γ' : List A) → Type
|
||
_⊆_ {A} Γ Γ' = ∀ {X} → X ∈ Γ → X ∈ Γ'
|
||
|
||
infixr 2 _/_⊢_
|
||
data _/_⊢_ (Δ Γ : Context) : Formula → Type where
|
||
var : X ∈ Γ → Δ / Γ ⊢ X
|
||
mp : Δ / Γ ⊢ X ⇒ Y → Δ / Γ ⊢ X → Δ / Γ ⊢ Y
|
||
∧ᵢ : Δ / Γ ⊢ X → Δ / Γ ⊢ Y → Δ / Γ ⊢ X ∧ Y
|
||
∧ₑ₁ : Δ / Γ ⊢ X ∧ Y → Δ / Γ ⊢ X
|
||
∧ₑ₂ : Δ / Γ ⊢ X ∧ Y → Δ / Γ ⊢ Y
|
||
∨ᵢ₁ : Δ / Γ ⊢ X → Δ / Γ ⊢ X ∨ Y
|
||
∨ᵢ₂ : Δ / Γ ⊢ Y → Δ / Γ ⊢ X ∨ Y
|
||
∨ₑ : Δ / Γ ⊢ X ∨ Y → Δ / Γ , X ⊢ Z → Δ / Γ , Y ⊢ Z → Δ / Γ ⊢ Z
|
||
⇒ᵢ : Δ / Γ , X ⊢ Y → Δ / Γ ⊢ X ⇒ Y
|
||
¬ᵢ : Δ / Γ , 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₂)
|
||
|
||
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₁)
|
||
exchange Γ' (∧ₑ₁ x) = ∧ₑ₁ (exchange Γ' x)
|
||
exchange Γ' (∧ₑ₂ x) = ∧ₑ₂ (exchange Γ' x)
|
||
exchange Γ' (∨ᵢ₁ x) = ∨ᵢ₁ (exchange Γ' x)
|
||
exchange Γ' (∨ᵢ₂ x) = ∨ᵢ₂ (exchange Γ' x)
|
||
exchange Γ' (∨ₑ x x₁ x₂) = ∨ₑ (exchange Γ' x) (exchange (Γ' , _) x₁) (exchange (Γ' , _) x₂)
|
||
exchange Γ' (⇒ᵢ x) = ⇒ᵢ (exchange (Γ' , _) x)
|
||
exchange Γ' (¬ᵢ x) = ¬ᵢ (exchange (Γ' , _) x)
|
||
exchange Γ' (¬ₑ x x₁) = ¬ₑ (exchange Γ' x) (exchange Γ' x₁)
|
||
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 Δ' (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₁)
|
||
exchange-modal Δ' (∧ₑ₁ x) = ∧ₑ₁ (exchange-modal Δ' x)
|
||
exchange-modal Δ' (∧ₑ₂ x) = ∧ₑ₂ (exchange-modal Δ' x)
|
||
exchange-modal Δ' (∨ᵢ₁ x) = ∨ᵢ₁ (exchange-modal Δ' x)
|
||
exchange-modal Δ' (∨ᵢ₂ x) = ∨ᵢ₂ (exchange-modal Δ' x)
|
||
exchange-modal Δ' (∨ₑ x x₁ x₂) = ∨ₑ (exchange-modal Δ' x) (exchange-modal Δ' x₁) (exchange-modal Δ' x₂)
|
||
exchange-modal Δ' (⇒ᵢ x) = ⇒ᵢ (exchange-modal Δ' x)
|
||
exchange-modal Δ' (¬ᵢ x) = ¬ᵢ (exchange-modal Δ' x)
|
||
exchange-modal Δ' (¬ₑ x x₁) = ¬ₑ (exchange-modal Δ' x) (exchange-modal Δ' x₁)
|
||
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} {Γ} {Γ'} {X} x {X₁} (zero x₁ xs) = zero X Γ'
|
||
inBoth {A} {Γ} {Γ'} {X} x {X₁} (succ x₁ xs x₂) = succ X₁ Γ' (x x₂)
|
||
|
||
weak : Δ / Γ ⊢ A → Γ ⊆ Γ' → Δ / Γ' ⊢ A
|
||
weak {Δ} {Γ} {A} {Γ'} (var x) x₁ = var (x₁ x)
|
||
weak {Δ} {Γ} {A} {Γ'} (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁))
|
||
weak {Δ} {Γ} {A} {Γ'} (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁))
|
||
weak {Δ} {Γ} {A} {Γ'} (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁))
|
||
weak {Δ} {Γ} {A} {Γ'} (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁)
|
||
weak {Δ} {Γ} {A} {Γ'} (□ᵢ x) x₁ = □ᵢ x
|
||
weak {Δ} {Γ} {A} {Γ'} (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁)
|
||
|
||
weak-modal : Δ / Γ ⊢ A → Δ ⊆ Δ' → Δ' / Γ ⊢ A
|
||
weak-modal (var x) x₁ = var x
|
||
weak-modal (mp x x₂) x₁ = mp (weak-modal x x₁) (weak-modal x₂ x₁)
|
||
weak-modal (∧ᵢ x x₂) x₁ = ∧ᵢ (weak-modal x x₁) (weak-modal x₂ x₁)
|
||
weak-modal (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak-modal x x₁)
|
||
weak-modal (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak-modal x x₁)
|
||
weak-modal (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak-modal x x₁)
|
||
weak-modal (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak-modal x x₁)
|
||
weak-modal (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak-modal x x₁) (weak-modal x₂ x₁) (weak-modal x₃ x₁)
|
||
weak-modal (⇒ᵢ x) x₁ = ⇒ᵢ (weak-modal x x₁)
|
||
weak-modal (¬ᵢ x) x₁ = ¬ᵢ (weak-modal x x₁)
|
||
weak-modal (¬ₑ x x₂) x₁ = ¬ₑ (weak-modal x x₁) (weak-modal x₂ x₁)
|
||
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 : Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B
|
||
cut = {!!}
|
||
|
||
cut-modal : Δ / Γ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B
|
||
cut-modal = {!!}
|
||
|
||
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 []))))))))
|
||
|
||
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 Γ))
|
||
DedSym {Δ} {Γ} {A} {B} (mp x x₁) = {!!}
|
||
DedSym {Δ} {Γ} {A} {B} (∧ₑ₁ x) = {!!}
|
||
DedSym {Δ} {Γ} {A} {B} (∧ₑ₂ x) = {!!}
|
||
DedSym {Δ} {Γ} {A} {B} (∨ₑ x x₁ x₂) = {!!}
|
||
DedSym {Δ} {Γ} {A} {B} (⇒ᵢ x) = x
|
||
DedSym {Δ} {Γ} {A} {B} (⊥ₑ x) = weak (⊥ₑ x) λ {X} → succ X Γ
|
||
DedSym {Δ} {Γ} {A} {B} (□ₑ x 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) []))))))
|
||
|
||
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)))))))))))))
|