commit ef0d5a51d7ff6c6f8e775be4eccfc4dae905df23 Author: Mysaa Date: Tue May 23 18:27:34 2023 +0200 First commit, a functional proof completeness of kripke structure for propositional logic diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..a64485f --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +*.agdai +*~ + diff --git a/prop.agda b/prop.agda new file mode 100644 index 0000000..d67c032 --- /dev/null +++ b/prop.agda @@ -0,0 +1,308 @@ +{-# OPTIONS --prop #-} +module prop where + + +open import Agda.Builtin.String using (String) +open import Data.String.Properties using (_==_) +open import Data.List using (List; _∷_; []) + + +{- Prop -} + +-- ⊥ is a data with no constructor +-- ⊤ is a record with one always-available constructor +data ⊥ : Prop where +record ⊤ : Prop where + constructor tt +data _∨_ : Prop → Prop → Prop where + inj₁ : {P Q : Prop} → P → P ∨ Q + inj₂ : {P Q : Prop} → Q → P ∨ Q +record _∧_ (P Q : Prop) : Prop where + constructor ⟨_,_⟩ + field + p : P + q : Q +infixr 10 _∧_ +infixr 11 _∨_ +-- ∧ elimination +proj₁ : {P Q : Prop} → P ∧ Q → P +proj₁ pq = _∧_.p pq +proj₂ : {P Q : Prop} → P ∧ Q → Q +proj₂ pq = _∧_.q pq +-- ¬ is a shorthand for « → ⊥ » +¬ : Prop → Prop +¬ P = P → ⊥ +case⊥ : {P : Prop} → ⊥ → P +case⊥ () +-- ∨ elimination +dis : {P Q S : Prop} → (P ∨ Q) → (P → S) → (Q → S) → S +dis (inj₁ p) ps qs = ps p +dis (inj₂ q) ps qs = qs q + + +_⇔_ : Prop → Prop → Prop +P ⇔ Q = (P → Q) ∧ (Q → P) + + +data Form : Set where + Var : String → Form + _[⇒]_ : Form → Form → Form + +infixr 8 _[⇒]_ + +data _≡_ : {A : Set} → A → A → Prop where + refl : {A : Set} → {x : A} → x ≡ x + +Con = List Form + +variable + A : Form + B : Form + C : Form + F : Form + G : Form + Γ : Con + Η : Con + x : String + y : String + +data _⊢_ : Con → Form → Prop where + zero : (F ∷ Γ) ⊢ F + succ : Γ ⊢ F → (G ∷ Γ) ⊢ F + lam : (F ∷ Γ) ⊢ G → Γ ⊢ (F [⇒] G) + app : Γ ⊢ (F [⇒] G) → Γ ⊢ F → Γ ⊢ G + +infixr 5 _⊢_ + +d-C : [] ⊢ ((Var "Q") [⇒] (Var "R")) [⇒] ((Var "P") [⇒] (Var "Q")) [⇒] (Var "P") [⇒] (Var "R") +d-C = lam (lam (lam (app (succ (succ zero)) (app (succ zero) zero)))) + +Env = String → Prop + +⟦_⟧F : Form → Env → Prop +⟦ Var x ⟧F ρ = ρ x +⟦ A [⇒] B ⟧F ρ = (⟦ A ⟧F ρ) → (⟦ B ⟧F ρ) + +⟦_⟧C : Con → Env → Prop +⟦ [] ⟧C ρ = ⊤ +⟦ A ∷ Γ ⟧C ρ = (⟦ A ⟧F ρ) ∧ (⟦ Γ ⟧C ρ) + +⟦_⟧d : Γ ⊢ F → {ρ : Env} → ⟦ Γ ⟧C ρ → ⟦ F ⟧F ρ +⟦ zero ⟧d p = proj₁ p +⟦ succ th ⟧d p = ⟦ th ⟧d (proj₂ p) +⟦ lam th ⟧d = λ pₐ p₀ → ⟦ th ⟧d ⟨ p₀ , pₐ ⟩ +⟦ app th₁ th₂ ⟧d = λ p → ⟦ th₁ ⟧d p (⟦ th₂ ⟧d p) + +ρ₀ : Env +ρ₀ "P" = ⊥ +ρ₀ "Q" = ⊤ +ρ₀ _ = ⊥ + +cex-d : ([] ⊢ (((Var "P") [⇒] (Var "Q")) [⇒] (Var "P"))) → ⊥ +cex-d h = ⟦ h ⟧d {ρ₀} tt λ x → tt + +data ⊢sk : Form → Prop where + SS : ⊢sk ((A [⇒] B [⇒] C) [⇒] (A [⇒] B) [⇒] A [⇒] C) + KK : ⊢sk (A [⇒] B [⇒] A) + app : ⊢sk (A [⇒] B) → ⊢sk A → ⊢sk B + +thm : ([] ⊢ A) ⇔ ⊢sk A +thm₁ : ⊢sk A → ([] ⊢ A) +thm₁ SS = lam (lam (lam ( app (app (succ (succ zero)) zero) (app (succ zero) zero)))) +thm₁ KK = lam (lam (succ zero)) +thm₁ (app x x₁) = app (thm₁ x) (thm₁ x₁) + +data _⊢skC_ : Con → Form → Prop where + zero : (A ∷ Γ) ⊢skC A + suc : Γ ⊢skC A → (B ∷ Γ) ⊢skC A + SS : Γ ⊢skC ((A [⇒] B [⇒] C) [⇒] (A [⇒] B) [⇒] A [⇒] C) + KK : Γ ⊢skC (A [⇒] B [⇒] A) + app : Γ ⊢skC (A [⇒] B) → Γ ⊢skC A → Γ ⊢skC B + +skC→sk : [] ⊢skC A → ⊢sk A +skC→sk SS = SS +skC→sk KK = KK +skC→sk (app d e) = app (skC→sk d) (skC→sk e) + + +lam-sk : (A ∷ Γ) ⊢skC B → Γ ⊢skC (A [⇒] B) +lam-sk-zero : Γ ⊢skC (A [⇒] A) +lam-sk-zero {A = A} = app (app SS KK) (KK {B = A}) +lam-sk zero = lam-sk-zero +lam-sk (suc x) = app KK x +lam-sk SS = app KK SS +lam-sk KK = app KK KK +lam-sk (app x₁ x₂) = app (app SS (lam-sk x₁)) (lam-sk x₂) + +⊢→⊢skC : Γ ⊢ A → Γ ⊢skC A +⊢→⊢skC zero = zero +⊢→⊢skC (succ x) = suc (⊢→⊢skC x) +⊢→⊢skC (lam x) = lam-sk (⊢→⊢skC x) +⊢→⊢skC (app x x₁) = app (⊢→⊢skC x) (⊢→⊢skC x₁) + +thm = ⟨ (λ x → skC→sk (⊢→⊢skC x)) , thm₁ ⟩ + + +Pierce = {P Q : Prop} → ((P → Q) → P) → P +TND : Prop → Prop +TND P = P ∨ (¬ P) + +P→TND : Pierce → {P : Prop} → TND P +nnTND : {P : Prop} → ¬ (¬ (P ∨ ¬ P)) +nnTND ntnd = ntnd (inj₂ λ p → ntnd (inj₁ p)) +P→TND pierce {P} = pierce {TND P} {⊥} (λ p → case⊥ (nnTND p)) + + + +{- Kripke Models -} + +record Kripke : Set₁ where + field + Worlds : Set₀ + _≤_ : Worlds → Worlds → Prop + refl≤ : {w : Worlds} → w ≤ w + tran≤ : {a b c : Worlds} → a ≤ b → b ≤ c → a ≤ c + _⊩_ : Worlds → String → Prop + mon⊩ : {a b : Worlds} → a ≤ b → {p : String} → a ⊩ p → b ⊩ p + {- Extending ⊩ to Formulas and Contexts -} + _⊩ᶠ_ : Worlds → Form → Prop + w ⊩ᶠ Var x = w ⊩ x + w ⊩ᶠ (fp [⇒] fq) = {w' : Worlds} → w ≤ w' → w' ⊩ᶠ fp → w' ⊩ᶠ fq + mon⊩ᶠ : {a b : Worlds} → a ≤ b → a ⊩ᶠ A → b ⊩ᶠ A + mon⊩ᶠ {Var x} ab aA = mon⊩ ab aA + mon⊩ᶠ {A [⇒] A₁} ab aA bc cA = aA (tran≤ ab bc) cA + _⊩ᶜ_ : Worlds → Con → Prop + w ⊩ᶜ [] = ⊤ + w ⊩ᶜ (p ∷ c) = (w ⊩ᶠ p) ∧ (w ⊩ᶜ c) + mon⊩ᶜ : {a b : Worlds} → a ≤ b → a ⊩ᶜ Γ → b ⊩ᶜ Γ + mon⊩ᶜ {[]} ab aΓ = aΓ + mon⊩ᶜ {A ∷ Γ} ab aΓ = ⟨ mon⊩ᶠ {A} ab (proj₁ aΓ) , mon⊩ᶜ ab (proj₂ aΓ) ⟩ + _⊫_ : Con → Form → Prop + Γ ⊫ F = {w : Worlds} → w ⊩ᶜ Γ → w ⊩ᶠ F + {- Soundness -} + ⟦_⟧ : Γ ⊢ A → Γ ⊫ A + ⟦ zero ⟧ = proj₁ + ⟦ succ p ⟧ = λ x → ⟦ p ⟧ (proj₂ x) + ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩ + ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ) + +{- Pierce is not provable -} + +module PierceWorld where + data Worlds : Set where + w₁ w₂ : Worlds + data _≤_ : Worlds → Worlds → Prop where + w₁₁ : w₁ ≤ w₁ + w₁₂ : w₁ ≤ w₂ + w₂₂ : w₂ ≤ w₂ + data _⊩_ : Worlds → String → Prop where + w₂A : w₂ ⊩ "A" + + refl≤ : {w : Worlds} → w ≤ w + refl≤ {w₁} = w₁₁ + refl≤ {w₂} = w₂₂ + tran≤ : {w w' w'' : Worlds} → w ≤ w' → w' ≤ w'' → w ≤ w'' + tran≤ w₁₁ z = z + tran≤ w₁₂ w₂₂ = w₁₂ + tran≤ w₂₂ w₂₂ = w₂₂ + mon⊩ : {a b : Worlds} → a ≤ b → {p : String} → a ⊩ p → b ⊩ p + mon⊩ w₂₂ w₂A = w₂A + +PierceW : Kripke +PierceW = record {PierceWorld} + +FaultyPierce : Form +FaultyPierce = (((Var "A" [⇒] Var "B") [⇒] Var "A") [⇒] Var "A") + +{- Pierce formula is false in world 1 -} +Pierce⊥w₁ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ FaultyPierce) +PierceHypw₁ : Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ ((Var "A" [⇒] Var "B") [⇒] Var "A") +NotAw₁ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ (Var "A")) +NotAw₁ () +NotBw₂ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₂ (Var "B")) +NotBw₂ () +NotABw₁ : ¬(Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ (Var "A" [⇒] Var "B")) +NotABw₁ h = NotBw₂ (h PierceWorld.w₁₂ PierceWorld.w₂A) +PierceHypw₁ PierceWorld.w₁₁ x = case⊥ (NotABw₁ x) +PierceHypw₁ PierceWorld.w₁₂ x = PierceWorld.w₂A +Pierce⊥w₁ h = case⊥ (NotAw₁ (h PierceWorld.w₁₁ PierceHypw₁)) +{- Pierce formula is true in world 2 -} +Pierce⊤w₂ : Kripke._⊩ᶠ_ PierceW PierceWorld.w₂ FaultyPierce +Pierce⊤w₂ PierceWorld.w₂₂ h₂ = PierceWorld.w₂A +PierceImpliesw₁ : ([] ⊢ FaultyPierce) → (Kripke._⊩ᶠ_ PierceW PierceWorld.w₁ FaultyPierce) +PierceImpliesw₁ h = Kripke.⟦_⟧ PierceW h {PierceWorld.w₁} tt +NotProvable : ¬([] ⊢ FaultyPierce) +NotProvable h = Pierce⊥w₁ (PierceImpliesw₁ h) + +{- Universal Kripke -} +-- Extension of ⊢ to contexts +_⊢⁺_ : Con → Con → Prop +Γ ⊢⁺ [] = ⊤ +Γ ⊢⁺ (F ∷ Γ') = (Γ ⊢ F) ∧ (Γ ⊢⁺ Γ') + +module UniversalKripke where + Worlds = Con + _≤_ : Con → Con → Prop + Γ ≤ Η = Η ⊢⁺ Γ + _⊩_ : Con → String → Prop + Γ ⊩ x = Γ ⊢ Var x + + data _⊆_ : Con → Con → Prop where + zero⊆ : Γ ⊆ Γ + next⊆ : Γ ⊆ Η → Γ ⊆ (F ∷ Η) + retro⊆ : {Γ Γ' : Con} → {F : Form} → (F ∷ Γ) ⊆ Γ' → Γ ⊆ Γ' + retro⊆ {Γ' = []} () -- Impossible to have «F∷Γ ⊆ []» + retro⊆ {Γ' = x ∷ Γ'} zero⊆ = next⊆ zero⊆ + retro⊆ {Γ' = x ∷ Γ'} (next⊆ h) = next⊆ (retro⊆ h) + mon⊆≤ : {Γ Γ' : Con} → Γ' ⊆ Γ → Γ ⊢⁺ Γ' + mon⊆≤ {[]} zero⊆ = tt + mon⊆≤ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆≤ (next⊆ zero⊆) ⟩ + mon⊆≤ {x ∷ Γ} {[]} (next⊆ sub) = tt + mon⊆≤ {x ∷ Γ} {y ∷ Γ'} (next⊆ sub) = ⟨ succ (proj₁ (mon⊆≤ sub)) , mon⊆≤ (next⊆ (retro⊆ sub)) ⟩ + + refl≤ : {Γ : Con} → Γ ⊢⁺ Γ + refl≤ = mon⊆≤ zero⊆ + addhyp : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → (F ∷ Γ) ⊢⁺ Γ' + addhyp {Γ' = []} h = tt + addhyp {Γ' = x ∷ Γ'} h = ⟨ succ (proj₁ h) , addhyp (proj₂ h) ⟩ + halftran≤ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F + halftran≤ h⁺ zero = proj₁ h⁺ + halftran≤ h⁺ (succ h) = halftran≤ (proj₂ h⁺) h + halftran≤ h⁺ (lam h) = lam (halftran≤ ⟨ zero , addhyp h⁺ ⟩ h) + halftran≤ h⁺ (app h h') = app (halftran≤ h⁺ h) (halftran≤ h⁺ h') + tran≤ : {Γ Γ' Γ'' : Con} → Γ ≤ Γ' → Γ' ≤ Γ'' → Γ ≤ Γ'' + tran≤ {[]} h h' = tt + tran≤ {x ∷ Γ} h h' = ⟨ halftran≤ h' (proj₁ h) , tran≤ (proj₂ h) h' ⟩ + + mon⊩ : {w w' : Con} → w ≤ w' → {x : String} → w ⊩ x → w' ⊩ x + mon⊩ h h' = halftran≤ h h' + +UK : Kripke +UK = record {UniversalKripke} + +module CompletenessProof where + open Kripke UK + open UniversalKripke using (mon⊆≤ ; zero⊆ ; next⊆ ; halftran≤ ; addhyp) + + ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢ F + ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢ F → Γ ⊩ᶠ F + ⊢→⊩ᶠ {Var x} h = h + ⊢→⊩ᶠ {F [⇒] F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran≤ (addhyp iq) h) zero)) (⊩ᶠ→⊢ hF)) + ⊩ᶠ→⊢ {Var x} h = h + ⊩ᶠ→⊢ {F [⇒] F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (mon⊆≤ (next⊆ zero⊆)) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) + + completeness : {F : Form} → [] ⊫ F → [] ⊢ F + completeness {F} ⊫F = ⊩ᶠ→⊢ (⊫F tt) + + + + + + + + + + + + + diff --git a/tests/test2.agda b/tests/test2.agda new file mode 100644 index 0000000..b1f823f --- /dev/null +++ b/tests/test2.agda @@ -0,0 +1,13 @@ +module test2 where + +open import Data.Nat using (ℕ) +open import Data.Vec using (Vec; _∷_) +open import Data.Fin using (Fin; zero; suc) + +variable + A : Set + n : ℕ + +lookup : Vec A n → Fin n → A +lookup (a ∷ as) zero = a +lookup (a ∷ as) (suc i) = lookup as i diff --git a/tests/test3.agda b/tests/test3.agda new file mode 100644 index 0000000..e76d26e --- /dev/null +++ b/tests/test3.agda @@ -0,0 +1,16 @@ +module test3 where + +open import Data.Nat using (ℕ; _+_) +open import Relation.Binary.PropositionalEquality using (_≡_) + ++-assoc : Set ++-assoc = ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z + +open import Data.Nat using (zero; suc) +open import Relation.Binary.PropositionalEquality using (refl; cong) + ++-assoc-proof : +-assoc + ++-assoc-proof zero y z = refl ++-assoc-proof (suc x') y z = cong suc (+-assoc-proof x' y z) + diff --git a/tests/tests.agda b/tests/tests.agda new file mode 100644 index 0000000..8d63eca --- /dev/null +++ b/tests/tests.agda @@ -0,0 +1,17 @@ +data Greeting : Set where + hello : Greeting + +greet : Greeting +greet = hello + +module hello-world-dep where + +open import Data.Nat using (ℕ; zero; suc) + +data Vec (A : Set) : ℕ → Set where + [] : Vec A zero + _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n) + +infixr 5 _∷_ + +