From 8d1df370ca785bb9fd696b00e7413962fb6ca4ef Mon Sep 17 00:00:00 2001 From: Mysaa Date: Thu, 25 May 2023 20:33:23 +0200 Subject: [PATCH] Tidied files up, changed messy prop.agda into a beautiful Readme.agda --- ListUtil.agda | 27 ++++++++ Normalization.agda | 135 --------------------------------------- PropositionalKripke.agda | 72 ++++++++++++--------- PropositionalLogic.agda | 123 +++++++++++++++++++++++++++-------- Readme.agda | 129 +++++++++++++++++++++++++++++++++++++ prop.agda | 99 ---------------------------- 6 files changed, 297 insertions(+), 288 deletions(-) create mode 100644 ListUtil.agda delete mode 100644 Normalization.agda create mode 100644 Readme.agda delete mode 100644 prop.agda diff --git a/ListUtil.agda b/ListUtil.agda new file mode 100644 index 0000000..a5bf401 --- /dev/null +++ b/ListUtil.agda @@ -0,0 +1,27 @@ +{-# OPTIONS --prop #-} + +module ListUtil where + + open import Data.List using (List; _∷_; []) public + + private + variable + T : Set₀ + L : List T + L' : List T + A : T + B : T + + + -- Definition of sublists + -- Similar definition : {L L' : List T} → L ⊆ L' ++ L + data _⊆_ : List T → List T → Prop where + zero⊆ : L ⊆ L + next⊆ : L ⊆ L' → L ⊆ (A ∷ L') + + -- One useful lemma + retro⊆ : {L L' : List T} → {A : T} → (A ∷ L) ⊆ L' → L ⊆ L' + retro⊆ {L' = []} () -- Impossible to have «A∷L ⊆ []» + retro⊆ {L' = B ∷ L'} zero⊆ = next⊆ zero⊆ + retro⊆ {L' = B ∷ L'} (next⊆ h) = next⊆ (retro⊆ h) + diff --git a/Normalization.agda b/Normalization.agda deleted file mode 100644 index 434ac33..0000000 --- a/Normalization.agda +++ /dev/null @@ -1,135 +0,0 @@ -{-# OPTIONS --prop #-} - -module Normalization (PV : Set) where - - open import PropUtil - open import PropositionalLogic PV - open import PropositionalKripke PV - - private - variable - A : Form - B : Form - F : Form - G : Form - Γ : Con - Γ' : Con - x : PV - - -- ⊢⁰ are neutral forms - -- ⊢* are normal forms - mutual - data _⊢⁰_ : Con → Form → Prop where - zero : (A ∷ Γ) ⊢⁰ A - next : Γ ⊢⁰ A → (B ∷ Γ) ⊢⁰ A - app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B - data _⊢*_ : Con → Form → Prop where - neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x - lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B) - - ⊢⁰→⊢ : Γ ⊢⁰ F → Γ ⊢ F - ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F - ⊢⁰→⊢ zero = zero - ⊢⁰→⊢ (next h) = next (⊢⁰→⊢ h) - ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x) - ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x - ⊢*→⊢ (lam h) = lam (⊢*→⊢ h) - - private - data _⊆_ : Con → Con → Prop where - zero⊆ : Γ ⊆ Γ - next⊆ : Γ ⊆ Γ' → Γ ⊆ (A ∷ Γ') - retro⊆ : {Γ Γ' : Con} → {A : Form} → (A ∷ Γ) ⊆ Γ' → Γ ⊆ Γ' - retro⊆ {Γ' = []} () -- Impossible to have «A∷Γ ⊆ []» - retro⊆ {Γ' = x ∷ Γ'} zero⊆ = next⊆ zero⊆ - retro⊆ {Γ' = x ∷ Γ'} (next⊆ h) = next⊆ (retro⊆ h) - - - -- Extension of ⊢⁰ to contexts - _⊢⁺⁰_ : Con → Con → Prop - Γ ⊢⁺⁰ [] = ⊤ - Γ ⊢⁺⁰ (F ∷ Γ') = (Γ ⊢⁰ F) ∧ (Γ ⊢⁺⁰ Γ') - infix 5 _⊢⁺⁰_ - - -- This relation is reflexive - private -- Lemma showing that the relation respects ⊆ - mon⊆≤⁰ : Γ' ⊆ Γ → Γ ⊢⁺⁰ Γ' - mon⊆≤⁰ {[]} sub = tt - mon⊆≤⁰ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆≤⁰ (next⊆ zero⊆) ⟩ - mon⊆≤⁰ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆≤⁰ sub)) ) , mon⊆≤⁰ (next⊆ (retro⊆ sub)) ⟩ - - refl⊢⁺⁰ : Γ ⊢⁺⁰ Γ - refl⊢⁺⁰ {[]} = tt - refl⊢⁺⁰ {x ∷ Γ} = ⟨ zero , mon⊆≤⁰ (next⊆ zero⊆) ⟩ - - -- A useful lemma, that we can add hypotheses - addhyp⊢⁺⁰ : Γ ⊢⁺⁰ Γ' → (A ∷ Γ) ⊢⁺⁰ Γ' - addhyp⊢⁺⁰ {Γ' = []} h = tt - addhyp⊢⁺⁰ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁺⁰ (proj₂ h) ⟩ - - - {- We use a slightly different Universal Kripke Model -} - module UniversalKripke⁰ where - Worlds = Con - _≤_ : Con → Con → Prop - Γ ≤ Η = Η ⊢⁺⁰ Γ - _⊩_ : Con → PV → Prop - Γ ⊩ x = Γ ⊢⁰ Var x - - refl≤ = refl⊢⁺⁰ - - -- Proving transitivity - halftran≤* : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺⁰ Γ' → Γ' ⊢* F → Γ ⊢* F - halftran≤⁰ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺⁰ Γ' → Γ' ⊢⁰ F → Γ ⊢⁰ F - halftran≤* h⁺ (neu⁰ x) = neu⁰ (halftran≤⁰ h⁺ x) - halftran≤* h⁺ (lam h) = lam (halftran≤* ⟨ zero , addhyp⊢⁺⁰ h⁺ ⟩ h) - halftran≤⁰ h⁺ zero = proj₁ h⁺ - halftran≤⁰ h⁺ (next h) = halftran≤⁰ (proj₂ 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 : PV} → w ⊩ x → w' ⊩ x - mon⊩ h h' = halftran≤⁰ h h' - - - ⊢*Var : Γ ⊢* Var x → Γ ⊢⁰ Var x - ⊢*Var (neu⁰ x) = x - - UK⁰ : Kripke - UK⁰ = record {UniversalKripke⁰} - open Kripke UK⁰ - open UniversalKripke⁰ using (halftran≤⁰) - - -- quote - ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F - -- unquote - ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F - - ⊢→⊩ᶠ {Var x} h = h - ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran≤⁰ iq h) (⊩ᶠ→⊢ hF)) - ⊩ᶠ→⊢ {Var x} h = neu⁰ h - ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺⁰ refl⊢⁺⁰) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) - - ---⊩ᶠ→⊢ {F ⇒ G} {Γ} h = lam (⊩ᶠ→⊢ {G} (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) - - {- - ⊩ᶠ→⊢ {F} zero = neu⁰ zero - ⊩ᶠ→⊢ {Var x} (next h) = neu⁰ (next {!!}) - ⊩ᶠ→⊢ {F ⇒ G} (next h) = neu⁰ (next {!!}) - ⊩ᶠ→⊢ {F ⇒ G} (lam h) = lam (⊩ᶠ→⊢ h) - ⊩ᶠ→⊢ {Var x} (app h h₁) = neu⁰ (app {!⊩ᶠ→⊢ h!} (⊩ᶠ→⊢ h₁)) - ⊩ᶠ→⊢ {F ⇒ G} (app h h₁) = neu⁰ (app {!!} (⊩ᶠ→⊢ h₁)) - -} - - {- - ⊩ᶠ→⊢ {Var x} zero = neu⁰ zero - ⊩ᶠ→⊢ {Var x} (next h) = neu⁰ (next (⊢*Var (⊩ᶠ→⊢ {Var x} h))) - ⊩ᶠ→⊢ {Var x} (app {A = A} h h₁) = {!!} - -- neu⁰ (app {A = A} {!!} (⊩ᶠ→⊢ (CompletenessProof.⊢→⊩ᶠ h₁))) - ⊩ᶠ→⊢ {F ⇒ G} {Γ} h = lam (⊩ᶠ→⊢ {G} (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) - -} - - diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda index 4f80c36..3eb86bc 100644 --- a/PropositionalKripke.agda +++ b/PropositionalKripke.agda @@ -2,6 +2,7 @@ module PropositionalKripke (PV : Set) where + open import ListUtil open import PropUtil open import PropositionalLogic PV @@ -37,7 +38,7 @@ module PropositionalKripke (PV : Set) where _⊩ᶠ_ : Worlds → Form → Prop w ⊩ᶠ Var x = w ⊩ x w ⊩ᶠ (fp ⇒ fq) = {w' : Worlds} → w ≤ w' → w' ⊩ᶠ fp → w' ⊩ᶠ fq - + _⊩ᶜ_ : Worlds → Con → Prop w ⊩ᶜ [] = ⊤ w ⊩ᶜ (p ∷ c) = (w ⊩ᶠ p) ∧ (w ⊩ᶜ c) @@ -66,43 +67,56 @@ module PropositionalKripke (PV : Set) where - {- Universal Kripke -} - - module UniversalKripke where - Worlds = Con - _≤_ : Con → Con → Prop - Γ ≤ Η = Η ⊢⁺ Γ - _⊩_ : Con → PV → Prop - Γ ⊩ x = Γ ⊢ Var x - - refl≤ = refl⊢⁺ - - -- Proving transitivity - halftran≤ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F - halftran≤ h⁺ zero = proj₁ h⁺ - halftran≤ h⁺ (next 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 : PV} → w ⊩ x → w' ⊩ x - mon⊩ h h' = halftran≤ h h' - - UK : Kripke - UK = record {UniversalKripke} module CompletenessProof where + + -- First, we define the Universal Kripke Model with (⊢⁺)⁻¹ as world order + UK : Kripke + UK = record { + Worlds = Con; + _≤_ = λ x y → y ⊢⁺ x; + refl≤ = refl⊢⁺; + tran≤ = λ ΓΓ' Γ'Γ'' → tran⊢⁺ Γ'Γ'' ΓΓ'; + _⊩_ = λ Γ x → Γ ⊢ Var x; + mon⊩ = λ ba bx → halftran⊢⁺ ba bx + } open Kripke UK - open UniversalKripke using (halftran≤) + -- Now we can prove that ⊩ᶠ and ⊢ act in the same way ⊩ᶠ→⊢ : {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)) + ⊢→⊩ᶠ {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 (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) + -- Finally, we can deduce completeness of the Kripke model completeness : {F : Form} → [] ⊫ F → [] ⊢ F completeness {F} ⊫F = ⊩ᶠ→⊢ (⊫F tt) + + module NormalizationProof where + + -- First we define the Universal model with (⊢⁰⁺)⁻¹ as world order + -- It is slightly different from the last Model, but proofs are the same + UK⁰ : Kripke + UK⁰ = record { + Worlds = Con; + _≤_ = λ x y → y ⊢⁰⁺ x; + refl≤ = refl⊢⁰⁺; + tran≤ = λ ΓΓ' Γ'Γ'' → tran⊢⁰⁺ Γ'Γ'' ΓΓ'; + _⊩_ = λ Γ x → Γ ⊢⁰ Var x; + mon⊩ = λ ba bx → halftran⊢⁰⁺⁰ ba bx + } + open Kripke UK⁰ + + -- We can now prove the normalization, i.e. the quote and function exists + -- The mutual proofs are exactly the same as the ones used in completeness + -- quote + ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F + -- unquote + ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F + + ⊢→⊩ᶠ {Var x} h = h + ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran⊢⁰⁺⁰ iq h) (⊩ᶠ→⊢ hF)) + ⊩ᶠ→⊢ {Var x} h = neu⁰ h + ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) diff --git a/PropositionalLogic.agda b/PropositionalLogic.agda index 473e2d1..8360ad7 100644 --- a/PropositionalLogic.agda +++ b/PropositionalLogic.agda @@ -3,17 +3,14 @@ module PropositionalLogic (PV : Set) where open import PropUtil - open import Data.List using (List; _∷_; []) public - + open import ListUtil + data Form : Set where Var : PV → Form _⇒_ : Form → Form → Form infixr 8 _⇒_ - data _≡_ : {A : Set} → A → A → Prop where - refl : {A : Set} → {x : A} → x ≡ x - {- Contexts -} Con = List Form @@ -24,20 +21,15 @@ module PropositionalLogic (PV : Set) where B : Form B' : Form C : Form + F : Form + G : Form Γ : Con Γ' : Con + x : PV - -- Definition of subcontexts (directly included) - -- Similar definition : {Γ' : Con} → Γ ⊆ Γ' ++ Γ - private - data _⊆_ : Con → Con → Prop where - zero⊆ : Γ ⊆ Γ - next⊆ : Γ ⊆ Γ' → Γ ⊆ (A ∷ Γ') - retro⊆ : {Γ Γ' : Con} → {A : Form} → (A ∷ Γ) ⊆ Γ' → Γ ⊆ Γ' - retro⊆ {Γ' = []} () -- Impossible to have «A∷Γ ⊆ []» - retro⊆ {Γ' = x ∷ Γ'} zero⊆ = next⊆ zero⊆ - retro⊆ {Γ' = x ∷ Γ'} (next⊆ h) = next⊆ (retro⊆ h) + + {--- DEFINITION OF ⊢ ---} data _⊢_ : Con → Form → Prop where zero : (A ∷ Γ) ⊢ A @@ -52,23 +44,101 @@ module PropositionalLogic (PV : Set) where Γ ⊢⁺ [] = ⊤ Γ ⊢⁺ (F ∷ Γ') = (Γ ⊢ F) ∧ (Γ ⊢⁺ Γ') infix 5 _⊢⁺_ - - -- This relation is reflexive - private -- Lemma showing that the relation respects ⊆ - mon⊆≤ : Γ' ⊆ Γ → Γ ⊢⁺ Γ' - mon⊆≤ {[]} sub = tt - mon⊆≤ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆≤ (next⊆ zero⊆) ⟩ - mon⊆≤ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆≤ sub)) ) , mon⊆≤ (next⊆ (retro⊆ sub)) ⟩ + -- The relation respects ⊆ + mon⊆⊢⁺ : Γ' ⊆ Γ → Γ ⊢⁺ Γ' + mon⊆⊢⁺ {[]} sub = tt + mon⊆⊢⁺ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆⊢⁺ (next⊆ zero⊆) ⟩ + mon⊆⊢⁺ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆⊢⁺ sub)) ) , mon⊆⊢⁺ (next⊆ (retro⊆ sub)) ⟩ + + -- The relation is reflexive refl⊢⁺ : Γ ⊢⁺ Γ refl⊢⁺ {[]} = tt - refl⊢⁺ {x ∷ Γ} = ⟨ zero , mon⊆≤ (next⊆ zero⊆) ⟩ + refl⊢⁺ {x ∷ Γ} = ⟨ zero , mon⊆⊢⁺ (next⊆ zero⊆) ⟩ - -- A useful lemma, that we can add hypotheses + -- We can add hypotheses to the left addhyp⊢⁺ : Γ ⊢⁺ Γ' → (A ∷ Γ) ⊢⁺ Γ' addhyp⊢⁺ {Γ' = []} h = tt addhyp⊢⁺ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁺ (proj₂ h) ⟩ - + + -- The relation respects ⊢ + halftran⊢⁺ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁺ Γ' → Γ' ⊢ F → Γ ⊢ F + halftran⊢⁺ h⁺ zero = proj₁ h⁺ + halftran⊢⁺ h⁺ (next 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') + + -- The relation is transitive + tran⊢⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁺ Γ' → Γ' ⊢⁺ Γ'' → Γ ⊢⁺ Γ'' + tran⊢⁺ {Γ'' = []} h h' = tt + tran⊢⁺ {Γ'' = x ∷ Γ*} h h' = ⟨ halftran⊢⁺ h (proj₁ h') , tran⊢⁺ h (proj₂ h') ⟩ + + + + {--- DEFINITIONS OF ⊢⁰ and ⊢* ---} + + -- ⊢⁰ are neutral forms + -- ⊢* are normal forms + mutual + data _⊢⁰_ : Con → Form → Prop where + zero : (A ∷ Γ) ⊢⁰ A + next : Γ ⊢⁰ A → (B ∷ Γ) ⊢⁰ A + app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B + data _⊢*_ : Con → Form → Prop where + neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x + lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B) + infix 5 _⊢⁰_ + infix 5 _⊢*_ + + -- Both are tighter than ⊢ + ⊢⁰→⊢ : Γ ⊢⁰ F → Γ ⊢ F + ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F + ⊢⁰→⊢ zero = zero + ⊢⁰→⊢ (next h) = next (⊢⁰→⊢ h) + ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x) + ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x + ⊢*→⊢ (lam h) = lam (⊢*→⊢ h) + + -- Extension of ⊢⁰ to contexts + -- i.e. there is a neutral proof for any element + _⊢⁰⁺_ : Con → Con → Prop + Γ ⊢⁰⁺ [] = ⊤ + Γ ⊢⁰⁺ (F ∷ Γ') = (Γ ⊢⁰ F) ∧ (Γ ⊢⁰⁺ Γ') + infix 5 _⊢⁰⁺_ + + -- The relation respects ⊆ + mon⊆⊢⁰⁺ : Γ' ⊆ Γ → Γ ⊢⁰⁺ Γ' + mon⊆⊢⁰⁺ {[]} sub = tt + mon⊆⊢⁰⁺ {x ∷ Γ} zero⊆ = ⟨ zero , mon⊆⊢⁰⁺ (next⊆ zero⊆) ⟩ + mon⊆⊢⁰⁺ {x ∷ Γ} (next⊆ sub) = ⟨ (next (proj₁ (mon⊆⊢⁰⁺ sub)) ) , mon⊆⊢⁰⁺ (next⊆ (retro⊆ sub)) ⟩ + + -- This relation is reflexive + refl⊢⁰⁺ : Γ ⊢⁰⁺ Γ + refl⊢⁰⁺ {[]} = tt + refl⊢⁰⁺ {x ∷ Γ} = ⟨ zero , mon⊆⊢⁰⁺ (next⊆ zero⊆) ⟩ + + -- A useful lemma, that we can add hypotheses + addhyp⊢⁰⁺ : Γ ⊢⁰⁺ Γ' → (A ∷ Γ) ⊢⁰⁺ Γ' + addhyp⊢⁰⁺ {Γ' = []} h = tt + addhyp⊢⁰⁺ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁰⁺ (proj₂ h) ⟩ + + -- The relation preserves ⊢⁰ and ⊢* + halftran⊢⁰⁺* : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁰⁺ Γ' → Γ' ⊢* F → Γ ⊢* F + halftran⊢⁰⁺⁰ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰ F → Γ ⊢⁰ F + halftran⊢⁰⁺* h⁺ (neu⁰ x) = neu⁰ (halftran⊢⁰⁺⁰ h⁺ x) + halftran⊢⁰⁺* h⁺ (lam h) = lam (halftran⊢⁰⁺* ⟨ zero , addhyp⊢⁰⁺ h⁺ ⟩ h) + halftran⊢⁰⁺⁰ h⁺ zero = proj₁ h⁺ + halftran⊢⁰⁺⁰ h⁺ (next h) = halftran⊢⁰⁺⁰ (proj₂ h⁺) h + halftran⊢⁰⁺⁰ h⁺ (app h h') = app (halftran⊢⁰⁺⁰ h⁺ h) (halftran⊢⁰⁺* h⁺ h') + + -- The relation is transitive + tran⊢⁰⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰⁺ Γ'' → Γ ⊢⁰⁺ Γ'' + tran⊢⁰⁺ {Γ'' = []} h h' = tt + tran⊢⁰⁺ {Γ'' = x ∷ Γ} h h' = ⟨ halftran⊢⁰⁺⁰ h (proj₁ h') , tran⊢⁰⁺ h (proj₂ h') ⟩ + + + + {--- Simple translation with in an Environment ---} Env = PV → Prop @@ -88,6 +158,9 @@ module PropositionalLogic (PV : Set) where ⟦ app th₁ th₂ ⟧ᵈ = λ p → ⟦ th₁ ⟧ᵈ p (⟦ th₂ ⟧ᵈ p) + + + {--- Combinatory Logic ---} data ⊢sk : Form → Prop where diff --git a/Readme.agda b/Readme.agda new file mode 100644 index 0000000..ca1e730 --- /dev/null +++ b/Readme.agda @@ -0,0 +1,129 @@ +{-# OPTIONS --prop #-} +module Readme where + +-- We will use String as propositional variables +open import Agda.Builtin.String using (String) +open import ListUtil +open import PropUtil + +-- We can use the basic propositional logic +open import PropositionalLogic String + +-- Here is an example of a propositional formula and its proof +-- The formula is (Q → R) → (P → Q) → P → R +d-C : [] ⊢ ((Var "Q") ⇒ (Var "R")) ⇒ ((Var "P") ⇒ (Var "Q")) ⇒ (Var "P") ⇒ (Var "R") +d-C = lam (lam (lam (app (next (next zero)) (app (next zero) zero)))) + +-- We can with the basic interpretation ⟦_⟧ prove that some formulæ are not provable +-- For example, we can disprove (P → Q) → P 's provability as we can construct an +-- environnement where the statement doesn't hold + +ρ₀ : Env +ρ₀ "P" = ⊥ +ρ₀ "Q" = ⊤ +ρ₀ _ = ⊥ + +cex-d : ([] ⊢ (((Var "P") ⇒ (Var "Q")) ⇒ (Var "P"))) → ⊥ +cex-d h = ⟦ h ⟧ᵈ {ρ₀} tt λ x → tt + +-- But this is not enough to show the non-provability of every non-provable statement. +-- Let's take as an example Pierce formula : ((P → Q) → P) → P +-- This statement is equivalent to the law of excluded middle (Tertium Non Datur) +-- We show that fact in Agda's proposition system + +Pierce = {P Q : Prop} → ((P → Q) → P) → P +TND : Prop → Prop +TND P = P ∨ (¬ P) + +-- Lemma: The double negation of the TND is always true +-- (You cannot show that having neither a proposition nor its negation is impossible +nnTND : {P : Prop} → ¬ (¬ (P ∨ ¬ P)) +nnTND ntnd = ntnd (inj₂ λ p → ntnd (inj₁ p)) +P→TND : Pierce → {P : Prop} → TND P +P→TND pierce {P} = pierce {TND P} {⊥} (λ p → case⊥ (nnTND p)) +TND→P : ({P : Prop} → TND P) → Pierce +TND→P tnd {P} {Q} pqp = dis (tnd {P}) (λ p → p) (λ np → pqp (λ p → case⊥ (np p))) + + +-- So we have to use a model that is more powerful : Kripke models +-- With those models, one can describe a frame in which the pierce formula doesn't hold +-- As we have that any proven formula is *true* in a kripke model, this shows +-- that the Pierce formula cannot be proven + +-- We import the general definition of Kripke models +open import PropositionalKripke String + +-- We will now create a specific Kripke model in which Pierce formula doesn't hold + +module PierceDisproof where + + 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} + open Kripke PierceW + open PierceWorld using (w₁ ; w₂ ; w₁₁ ; w₁₂ ; w₂₂ ; w₂A) + + -- Now we can write the «instance» of the Pierce formula which doesn't hold in our world + PierceF : Form + PierceF = (((Var "A" ⇒ Var "B") ⇒ Var "A") ⇒ Var "A") + + -- Now we show that it does not hold in w₁ but holds in w₂ + Pierce⊥w₁ : ¬(w₁ ⊩ᶠ PierceF) + Pierce⊤w₂ : w₂ ⊩ᶠ PierceF + + -- A does not hold in w₁ + NotAw₁ : ¬(w₁ ⊩ᶠ (Var "A")) + NotAw₁ () + -- B does not hold in w₂ while A holds + NotBw₂ : ¬(w₂ ⊩ᶠ (Var "B")) + NotBw₂ () + -- Therefore, (A → B) does not hold in w₁ + NotABw₁ : ¬(w₁ ⊩ᶠ (Var "A" ⇒ Var "B")) + NotABw₁ h = NotBw₂ (h w₁₂ w₂A) + -- So the hypothesis of the pierce formula does hold in w₁ + -- as its premice does not hold in w₁ and its conclusion does hold in w₂ + PierceHypw₁ : w₁ ⊩ᶠ ((Var "A" ⇒ Var "B") ⇒ Var "A") + PierceHypw₁ w₁₁ x = case⊥ (NotABw₁ x) + PierceHypw₁ w₁₂ x = w₂A + -- So, as the conclusion of the pierce formula does not hold in w₁, the pierce formula doesn't hold. + Pierce⊥w₁ h = case⊥ (NotAw₁ (h w₁₁ PierceHypw₁)) + -- Finally, the formula holds in w₂ as its conclusion is true + Pierce⊤w₂ w₂₂ h₂ = w₂A + + -- So, if pierce formula would be provable, it would hold in w₁, which it doesn't + -- therefore it is not provable CQFD + PierceNotProvable : ¬([] ⊢ PierceF) + PierceNotProvable h = Pierce⊥w₁ (⟦ h ⟧ {w₁} tt) + + + + + + + + + + + + + + diff --git a/prop.agda b/prop.agda deleted file mode 100644 index 02576e9..0000000 --- a/prop.agda +++ /dev/null @@ -1,99 +0,0 @@ -{-# OPTIONS --prop #-} -module prop where - - -open import Agda.Builtin.String using (String) -open import Data.String.Properties using (_==_) -open import Data.List using (List; _∷_; []) - - - -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 -ρ₀ "P" = ⊥ -ρ₀ "Q" = ⊤ -ρ₀ _ = ⊥ - -cex-d : ([] ⊢ (((Var "P") [⇒] (Var "Q")) [⇒] (Var "P"))) → ⊥ -cex-d h = ⟦ h ⟧d {ρ₀} tt λ x → tt - - - -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 -} - - -{- 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) - - - - - - - - - - - - - -