From 422dcf67f0d7871cabd638d72e2e91da98b9fdfa Mon Sep 17 00:00:00 2001 From: Mysaa Date: Tue, 30 May 2023 14:02:01 +0200 Subject: [PATCH 1/2] Started merging zero and next into a one and only proof constructor, so normal forms are now unique. Added a lot of relations on lists in order to study different kinds of morphisms --- ListUtil.agda | 66 ++++++++++++++++++++++++- PropositionalKripke.agda | 25 ++++++++++ PropositionalLogic.agda | 104 ++++++++++++++++++++++++--------------- 3 files changed, 153 insertions(+), 42 deletions(-) diff --git a/ListUtil.agda b/ListUtil.agda index a5bf401..a7dbad0 100644 --- a/ListUtil.agda +++ b/ListUtil.agda @@ -13,7 +13,20 @@ module ListUtil where B : T - -- Definition of sublists + -- Definition of list appartenance + -- The definition uses reflexivity and never any kind of equality + infix 3 _∈_ + data _∈_ : T → List T → Prop where + zero∈ : A ∈ A ∷ L + next∈ : A ∈ L → A ∈ B ∷ L + + {- RELATIONS BETWEEN LISTS -} + + -- We have the following relations + -- ↗ ⊂⁰ ↘ + -- ⊆ → ⊂ → ⊂⁺ → ∈* + infix 4 _⊆_ _⊂_ _⊂⁺_ _⊂⁰_ _∈*_ + {- ⊆ : We can remove elements but only from the head of the list -} -- Similar definition : {L L' : List T} → L ⊆ L' ++ L data _⊆_ : List T → List T → Prop where zero⊆ : L ⊆ L @@ -25,3 +38,54 @@ module ListUtil where retro⊆ {L' = B ∷ L'} zero⊆ = next⊆ zero⊆ retro⊆ {L' = B ∷ L'} (next⊆ h) = next⊆ (retro⊆ h) + {- ⊂ : We can remove elements anywhere on the list, no duplicates, no reordering -} + data _⊂_ : List T → List T → Prop where + zero⊂ : [] ⊂ L + both⊂ : L ⊂ L' → (A ∷ L) ⊂ (A ∷ L') + next⊂ : L ⊂ L' → L ⊂ (A ∷ L') + + {- ⊂⁰ : We can remove elements and reorder the list, as long as we don't duplicate the elements -} + -----> We do not have unicity of derivation ([A,A] ⊂⁰ [A,A] can be prove by identity or by swapping its two elements + --> We could do with some counting function, but ... it would not be nice, would it ? + data _⊂⁰_ : List T → List T → Prop where + zero⊂⁰ : _⊂⁰_ {T} [] [] + next⊂⁰ : L ⊂⁰ L' → L ⊂⁰ A ∷ L' + both⊂⁰ : L ⊂⁰ L' → A ∷ L ⊂⁰ A ∷ L' + swap⊂⁰ : L ⊂⁰ A ∷ B ∷ L' → L ⊂⁰ B ∷ A ∷ L' + error : L ⊂⁰ L' + -- TODOTODOTODOTODO Fix this definition + {- ⊂⁺ : We can remove and duplicate elements, as long as we don't change the order -} + data _⊂⁺_ : List T → List T → Prop where + zero⊂⁺ : _⊂⁺_ {T} [] [] + next⊂⁺ : L ⊂⁺ L' → L ⊂⁺ A ∷ L' + dup⊂⁺ : A ∷ L ⊂⁺ L' → A ∷ L ⊂⁺ A ∷ L' + {- ∈* : We can remove or duplicate elements and we can change their order -} + -- The weakest of all relations on lists + -- L ∈* L' if all elements of L exists in L' (no consideration for order nor duplication) + data _∈*_ : List T → List T → Prop where + zero∈* : [] ∈* L + next∈* : A ∈ L → L' ∈* L → (A ∷ L') ∈* L + + -- Founding principle + mon∈∈* : A ∈ L → L ∈* L' → A ∈ L' + mon∈∈* zero∈ (next∈* x hl) = x + mon∈∈* (next∈ ha) (next∈* x hl) = mon∈∈* ha hl + + -- We show that the relation is reflexive and is implied by ⊆ + refl∈* : L ∈* L + ⊆→∈* : L ⊆ L' → L ∈* L' + refl∈* {L = []} = zero∈* + refl∈* {L = x ∷ L} = next∈* zero∈ (⊆→∈* (next⊆ zero⊆)) + ⊆→∈* zero⊆ = refl∈* + ⊆→∈* {L = []} (next⊆ h) = zero∈* + ⊆→∈* {L = x ∷ L} (next⊆ h) = next∈* (next∈ (mon∈∈* zero∈ (⊆→∈* h))) (⊆→∈* (retro⊆ (next⊆ h))) + + -- Allows to grow ∈* to the right + right∈* : L ∈* L' → L ∈* (A ∷ L') + right∈* zero∈* = zero∈* + right∈* (next∈* x h) = next∈* (next∈ x) (right∈* h) + + -- Allows to grow ∈* from both sides + both∈* : L ∈* L' → (A ∷ L) ∈* (A ∷ L') + both∈* zero∈* = next∈* zero∈ zero∈* + both∈* (next∈* x h) = next∈* zero∈ (next∈* (next∈ x) (right∈* h)) diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda index 3eb86bc..574f2c8 100644 --- a/PropositionalKripke.agda +++ b/PropositionalKripke.agda @@ -120,3 +120,28 @@ module PropositionalKripke (PV : Set) where ⊢→⊩ᶠ {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))) + + module OtherProofs where + + -- We will try to define the Kripke models using the following embeddings + + -- Strongest is using the ⊢⁺ relation directly + + -- -> See module CompletenessProof + + -- We can also use the relation ⊢⁰⁺, which is compatible with ⊢⁰ and ⊢* + + -- -> See module NormalizationProof + + + + {- Renamings -} + + {- Weakening anywhere, order preserving, duplication authorized -} + + {- Weakening anywhere, no duplication, order preserving -} + + + {- Weakening at the end -} + + -- This is exactly our relation ⊆ diff --git a/PropositionalLogic.agda b/PropositionalLogic.agda index 8360ad7..9853cc9 100644 --- a/PropositionalLogic.agda +++ b/PropositionalLogic.agda @@ -25,6 +25,7 @@ module PropositionalLogic (PV : Set) where G : Form Γ : Con Γ' : Con + Γ'' : Con x : PV @@ -32,12 +33,21 @@ module PropositionalLogic (PV : Set) where {--- DEFINITION OF ⊢ ---} data _⊢_ : Con → Form → Prop where - zero : (A ∷ Γ) ⊢ A - next : Γ ⊢ A → (B ∷ Γ) ⊢ A + zero : A ∈ Γ → Γ ⊢ A lam : (A ∷ Γ) ⊢ B → Γ ⊢ (A ⇒ B) app : Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B - infix 5 _⊢_ + + zero⊢ : (A ∷ Γ) ⊢ A + zero⊢ = zero zero∈ + one⊢ : (B ∷ A ∷ Γ) ⊢ A + one⊢ = zero (next∈ zero∈) + + -- We can add hypotheses to a proof + addhyp⊢ : Γ ∈* Γ' → Γ ⊢ A → Γ' ⊢ A + addhyp⊢ s (zero x) = zero (mon∈∈* x s) + addhyp⊢ s (lam h) = lam (addhyp⊢ (both∈* s) h) + addhyp⊢ s (app h h₁) = app (addhyp⊢ s h) (addhyp⊢ s h₁) -- Extension of ⊢ to contexts _⊢⁺_ : Con → Con → Prop @@ -45,28 +55,32 @@ module PropositionalLogic (PV : Set) where Γ ⊢⁺ (F ∷ Γ') = (Γ ⊢ F) ∧ (Γ ⊢⁺ Γ') infix 5 _⊢⁺_ + -- We show that the relation respects ∈* + + mon∈*⊢⁺ : Γ' ∈* Γ → Γ ⊢⁺ Γ' + mon∈*⊢⁺ zero∈* = tt + mon∈*⊢⁺ (next∈* x h) = ⟨ (zero x) , (mon∈*⊢⁺ h) ⟩ + -- 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)) ⟩ + mon⊆⊢⁺ h = mon∈*⊢⁺ (⊆→∈* h) -- The relation is reflexive refl⊢⁺ : Γ ⊢⁺ Γ refl⊢⁺ {[]} = tt - refl⊢⁺ {x ∷ Γ} = ⟨ zero , mon⊆⊢⁺ (next⊆ zero⊆) ⟩ - - -- We can add hypotheses to the left - addhyp⊢⁺ : Γ ⊢⁺ Γ' → (A ∷ Γ) ⊢⁺ Γ' - addhyp⊢⁺ {Γ' = []} h = tt - addhyp⊢⁺ {Γ' = A ∷ Γ'} h = ⟨ next (proj₁ h) , addhyp⊢⁺ (proj₂ h) ⟩ + refl⊢⁺ {x ∷ Γ} = ⟨ zero⊢ , mon⊆⊢⁺ (next⊆ zero⊆) ⟩ + -- We can add hypotheses to to a proof + addhyp⊢⁺ : Γ ∈* Γ' → Γ ⊢⁺ Γ'' → Γ' ⊢⁺ Γ'' + addhyp⊢⁺ {Γ'' = []} s h = tt + addhyp⊢⁺ {Γ'' = x ∷ Γ''} s ⟨ Γx , ΓΓ'' ⟩ = ⟨ addhyp⊢ s Γx , addhyp⊢⁺ s ΓΓ'' ⟩ + -- 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') + halftran⊢⁺ {Γ' = F ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺ + halftran⊢⁺ {Γ' = F ∷ Γ'} h⁺ (zero (next∈ x)) = halftran⊢⁺ (proj₂ h⁺) (zero x) + halftran⊢⁺ h⁺ (lam h) = lam (halftran⊢⁺ ⟨ (zero zero∈) , (addhyp⊢⁺ (right∈* refl∈*) h⁺) ⟩ h) + halftran⊢⁺ h⁺ (app h h₁) = app (halftran⊢⁺ h⁺ h) (halftran⊢⁺ h⁺ h₁) -- The relation is transitive tran⊢⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁺ Γ' → Γ' ⊢⁺ Γ'' → Γ ⊢⁺ Γ'' @@ -81,8 +95,7 @@ module PropositionalLogic (PV : Set) where -- ⊢* are normal forms mutual data _⊢⁰_ : Con → Form → Prop where - zero : (A ∷ Γ) ⊢⁰ A - next : Γ ⊢⁰ A → (B ∷ Γ) ⊢⁰ A + zero : A ∈ Γ → Γ ⊢⁰ A app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B data _⊢*_ : Con → Form → Prop where neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x @@ -93,42 +106,53 @@ module PropositionalLogic (PV : Set) where -- Both are tighter than ⊢ ⊢⁰→⊢ : Γ ⊢⁰ F → Γ ⊢ F ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F - ⊢⁰→⊢ zero = zero - ⊢⁰→⊢ (next h) = next (⊢⁰→⊢ h) + ⊢⁰→⊢ (zero h) = zero h ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x) ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x ⊢*→⊢ (lam h) = lam (⊢*→⊢ h) + -- We can add hypotheses to a proof + addhyp⊢⁰ : Γ ∈* Γ' → Γ ⊢⁰ A → Γ' ⊢⁰ A + addhyp⊢* : Γ ∈* Γ' → Γ ⊢* A → Γ' ⊢* A + addhyp⊢⁰ s (zero x) = zero (mon∈∈* x s) + addhyp⊢⁰ s (app h h₁) = app (addhyp⊢⁰ s h) (addhyp⊢* s h₁) + addhyp⊢* s (neu⁰ x) = neu⁰ (addhyp⊢⁰ s x) + addhyp⊢* s (lam h) = lam (addhyp⊢* (both∈* s) 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∈*⊢⁰⁺ zero∈* = tt + mon∈*⊢⁰⁺ (next∈* x h) = ⟨ (zero x) , (mon∈*⊢⁰⁺ h) ⟩ + -- 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)) ⟩ + mon⊆⊢⁰⁺ h = mon∈*⊢⁰⁺ (⊆→∈* h) -- This relation is reflexive refl⊢⁰⁺ : Γ ⊢⁰⁺ Γ refl⊢⁰⁺ {[]} = tt - refl⊢⁰⁺ {x ∷ Γ} = ⟨ zero , mon⊆⊢⁰⁺ (next⊆ zero⊆) ⟩ + refl⊢⁰⁺ {x ∷ Γ} = ⟨ zero 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) ⟩ + addhyp⊢⁰⁺ : Γ ∈* Γ' → Γ ⊢⁰⁺ Γ'' → Γ' ⊢⁰⁺ Γ'' + addhyp⊢⁰⁺ {Γ'' = []} s h = tt + addhyp⊢⁰⁺ {Γ'' = A ∷ Γ'} s ⟨ Γx , ΓΓ'' ⟩ = ⟨ addhyp⊢⁰ s Γx , addhyp⊢⁰⁺ s ΓΓ'' ⟩ -- 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⁺ (lam h) = lam (halftran⊢⁰⁺* ⟨ zero zero∈ , addhyp⊢⁰⁺ (right∈* refl∈*) h⁺ ⟩ h) + halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺ + halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero (next∈ h)) = halftran⊢⁰⁺⁰ (proj₂ h⁺) (zero h) halftran⊢⁰⁺⁰ h⁺ (app h h') = app (halftran⊢⁰⁺⁰ h⁺ h) (halftran⊢⁰⁺* h⁺ h') -- The relation is transitive @@ -152,8 +176,8 @@ module PropositionalLogic (PV : Set) where ⟦ A ∷ Γ ⟧ᶜ ρ = (⟦ A ⟧ᶠ ρ) ∧ (⟦ Γ ⟧ᶜ ρ) ⟦_⟧ᵈ : Γ ⊢ A → {ρ : Env} → ⟦ Γ ⟧ᶜ ρ → ⟦ A ⟧ᶠ ρ - ⟦ zero ⟧ᵈ p = proj₁ p - ⟦ next th ⟧ᵈ p = ⟦ th ⟧ᵈ (proj₂ p) + ⟦_⟧ᵈ {x ∷ Γ} (zero zero∈) p = proj₁ p + ⟦_⟧ᵈ {x ∷ Γ} (zero (next∈ h)) p = ⟦ zero h ⟧ᵈ (proj₂ p) ⟦ lam th ⟧ᵈ = λ pₐ p₀ → ⟦ th ⟧ᵈ ⟨ p₀ , pₐ ⟩ ⟦ app th₁ th₂ ⟧ᵈ = λ p → ⟦ th₁ ⟧ᵈ p (⟦ th₂ ⟧ᵈ p) @@ -169,8 +193,7 @@ module PropositionalLogic (PV : Set) where app : ⊢sk (A ⇒ B) → ⊢sk A → ⊢sk B data _⊢skC_ : Con → Form → Prop where - zero : (A ∷ Γ) ⊢skC A - next : Γ ⊢skC A → (B ∷ Γ) ⊢skC A + zero : A ∈ Γ → Γ ⊢skC A SS : Γ ⊢skC ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C) KK : Γ ⊢skC (A ⇒ B ⇒ A) app : Γ ⊢skC (A ⇒ B) → Γ ⊢skC A → Γ ⊢skC B @@ -180,8 +203,8 @@ module PropositionalLogic (PV : Set) where ⊢⇔⊢sk : ([] ⊢ A) ⇔ ⊢sk A ⊢sk→⊢ : ⊢sk A → ([] ⊢ A) - ⊢sk→⊢ SS = lam (lam (lam ( app (app (next (next zero)) zero) (app (next zero) zero)))) - ⊢sk→⊢ KK = lam (lam (next zero)) + ⊢sk→⊢ SS = lam (lam (lam ( app (app (zero (next∈ (next∈ zero∈))) (zero zero∈)) (app (zero (next∈ zero∈)) (zero zero∈))))) + ⊢sk→⊢ KK = lam (lam (zero (next∈ zero∈))) ⊢sk→⊢ (app x x₁) = app (⊢sk→⊢ x) (⊢sk→⊢ x₁) skC→sk : [] ⊢skC A → ⊢sk A @@ -193,15 +216,14 @@ module PropositionalLogic (PV : Set) where 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 (next x) = app KK x + lam-sk (zero zero∈) = lam-sk-zero + lam-sk (zero (next∈ h)) = app KK (zero h) 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 (next x) = next (⊢→⊢skC x) + ⊢→⊢skC (zero h) = zero h ⊢→⊢skC (lam x) = lam-sk (⊢→⊢skC x) ⊢→⊢skC (app x x₁) = app (⊢→⊢skC x) (⊢→⊢skC x₁) From 28b7faac052f4ed135f3f06a5e16c8f4867492c4 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Wed, 31 May 2023 13:59:33 +0200 Subject: [PATCH 2/2] Added a generalized version of the Normalization proof --- ListUtil.agda | 65 +++++++++++-- Prop.agda | 46 ---------- PropUtil.agda | 6 ++ PropositionalKripke.agda | 46 +++++++--- PropositionalKripkeGeneral.agda | 157 ++++++++++++++++++++++++++++++++ Readme.agda | 44 +++++++-- 6 files changed, 286 insertions(+), 78 deletions(-) delete mode 100644 Prop.agda create mode 100644 PropositionalKripkeGeneral.agda diff --git a/ListUtil.agda b/ListUtil.agda index a7dbad0..d54c224 100644 --- a/ListUtil.agda +++ b/ListUtil.agda @@ -9,6 +9,7 @@ module ListUtil where T : Set₀ L : List T L' : List T + L'' : List T A : T B : T @@ -38,12 +39,33 @@ module ListUtil where retro⊆ {L' = B ∷ L'} zero⊆ = next⊆ zero⊆ retro⊆ {L' = B ∷ L'} (next⊆ h) = next⊆ (retro⊆ h) + refl⊆ : L ⊆ L + refl⊆ = zero⊆ + + tran⊆ : L ⊆ L' → L' ⊆ L'' → L ⊆ L'' + tran⊆ zero⊆ h2 = h2 + tran⊆ (next⊆ h1) h2 = tran⊆ h1 (retro⊆ h2) + {- ⊂ : We can remove elements anywhere on the list, no duplicates, no reordering -} data _⊂_ : List T → List T → Prop where zero⊂ : [] ⊂ L both⊂ : L ⊂ L' → (A ∷ L) ⊂ (A ∷ L') next⊂ : L ⊂ L' → L ⊂ (A ∷ L') - + + ⊆→⊂ : L ⊆ L' → L ⊂ L' + refl⊂ : L ⊂ L + ⊆→⊂ {L = []} h = zero⊂ + ⊆→⊂ {L = x ∷ L} zero⊆ = both⊂ (refl⊂) + ⊆→⊂ {L = x ∷ L} (next⊆ h) = next⊂ (⊆→⊂ h) + refl⊂ = ⊆→⊂ refl⊆ + + tran⊂ : L ⊂ L' → L' ⊂ L'' → L ⊂ L'' + tran⊂ zero⊂ h2 = zero⊂ + tran⊂ (both⊂ h1) (both⊂ h2) = both⊂ (tran⊂ h1 h2) + tran⊂ (both⊂ h1) (next⊂ h2) = next⊂ (tran⊂ (both⊂ h1) h2) + tran⊂ (next⊂ h1) (both⊂ h2) = next⊂ (tran⊂ h1 h2) + tran⊂ (next⊂ h1) (next⊂ h2) = next⊂ (tran⊂ (next⊂ h1) h2) + {- ⊂⁰ : We can remove elements and reorder the list, as long as we don't duplicate the elements -} -----> We do not have unicity of derivation ([A,A] ⊂⁰ [A,A] can be prove by identity or by swapping its two elements --> We could do with some counting function, but ... it would not be nice, would it ? @@ -58,7 +80,27 @@ module ListUtil where data _⊂⁺_ : List T → List T → Prop where zero⊂⁺ : _⊂⁺_ {T} [] [] next⊂⁺ : L ⊂⁺ L' → L ⊂⁺ A ∷ L' - dup⊂⁺ : A ∷ L ⊂⁺ L' → A ∷ L ⊂⁺ A ∷ L' + dup⊂⁺ : L ⊂⁺ A ∷ L' → A ∷ L ⊂⁺ A ∷ L' + + ⊂→⊂⁺ : L ⊂ L' → L ⊂⁺ L' + ⊂→⊂⁺ {L' = []} zero⊂ = zero⊂⁺ + ⊂→⊂⁺ {L' = x ∷ L'} zero⊂ = next⊂⁺ (⊂→⊂⁺ zero⊂) + ⊂→⊂⁺ (both⊂ h) = dup⊂⁺ (next⊂⁺ (⊂→⊂⁺ h)) + ⊂→⊂⁺ (next⊂ h) = next⊂⁺ (⊂→⊂⁺ h) + refl⊂⁺ : L ⊂⁺ L + refl⊂⁺ = ⊂→⊂⁺ refl⊂ + tran⊂⁺ : L ⊂⁺ L' → L' ⊂⁺ L'' → L ⊂⁺ L'' + tran⊂⁺ zero⊂⁺ zero⊂⁺ = zero⊂⁺ + tran⊂⁺ zero⊂⁺ (next⊂⁺ h2) = next⊂⁺ h2 + tran⊂⁺ (next⊂⁺ h1) (next⊂⁺ h2) = next⊂⁺ (tran⊂⁺ (next⊂⁺ h1) h2) + tran⊂⁺ (next⊂⁺ h1) (dup⊂⁺ h2) = tran⊂⁺ h1 h2 + tran⊂⁺ (dup⊂⁺ h1) (next⊂⁺ h2) = next⊂⁺ (tran⊂⁺ (dup⊂⁺ h1) h2) + tran⊂⁺ (dup⊂⁺ h1) (dup⊂⁺ h2) = dup⊂⁺ (tran⊂⁺ h1 (dup⊂⁺ h2)) + + retro⊂⁺ : A ∷ L ⊂⁺ L' → L ⊂⁺ L' + retro⊂⁺ (next⊂⁺ h) = next⊂⁺ (retro⊂⁺ h) + retro⊂⁺ (dup⊂⁺ h) = h + {- ∈* : We can remove or duplicate elements and we can change their order -} -- The weakest of all relations on lists -- L ∈* L' if all elements of L exists in L' (no consideration for order nor duplication) @@ -73,19 +115,26 @@ module ListUtil where -- We show that the relation is reflexive and is implied by ⊆ refl∈* : L ∈* L - ⊆→∈* : L ⊆ L' → L ∈* L' + ⊂⁺→∈* : L ⊂⁺ L' → L ∈* L' refl∈* {L = []} = zero∈* - refl∈* {L = x ∷ L} = next∈* zero∈ (⊆→∈* (next⊆ zero⊆)) - ⊆→∈* zero⊆ = refl∈* - ⊆→∈* {L = []} (next⊆ h) = zero∈* - ⊆→∈* {L = x ∷ L} (next⊆ h) = next∈* (next∈ (mon∈∈* zero∈ (⊆→∈* h))) (⊆→∈* (retro⊆ (next⊆ h))) + refl∈* {L = x ∷ L} = next∈* zero∈ (⊂⁺→∈* (next⊂⁺ refl⊂⁺)) + ⊂⁺→∈* zero⊂⁺ = refl∈* + ⊂⁺→∈* {L = []} (next⊂⁺ h) = zero∈* + ⊂⁺→∈* {L = x ∷ L} (next⊂⁺ h) = next∈* (next∈ (mon∈∈* zero∈ (⊂⁺→∈* h))) (⊂⁺→∈* (retro⊂⁺ (next⊂⁺ h))) + ⊂⁺→∈* (dup⊂⁺ h) = next∈* zero∈ (⊂⁺→∈* h) -- Allows to grow ∈* to the right right∈* : L ∈* L' → L ∈* (A ∷ L') right∈* zero∈* = zero∈* right∈* (next∈* x h) = next∈* (next∈ x) (right∈* h) - -- Allows to grow ∈* from both sides both∈* : L ∈* L' → (A ∷ L) ∈* (A ∷ L') both∈* zero∈* = next∈* zero∈ zero∈* both∈* (next∈* x h) = next∈* zero∈ (next∈* (next∈ x) (right∈* h)) + + tran∈* : L ∈* L' → L' ∈* L'' → L ∈* L'' + tran∈* {L = []} = λ x x₁ → zero∈* + tran∈* {L = x ∷ L} (next∈* x₁ h1) h2 = next∈* (mon∈∈* x₁ h2) (tran∈* h1 h2) + + ⊆→∈* : L ⊆ L' → L ∈* L' + ⊆→∈* h = ⊂⁺→∈* (⊂→⊂⁺ (⊆→⊂ h)) diff --git a/Prop.agda b/Prop.agda deleted file mode 100644 index ab70ae5..0000000 --- a/Prop.agda +++ /dev/null @@ -1,46 +0,0 @@ -{-# OPTIONS --prop #-} - -module Prop where - - -- ⊥ 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 → ⊥ - - -- ⊥ elimination - 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 - - - -- ⇔ shorthand - _⇔_ : Prop → Prop → Prop - P ⇔ Q = (P → Q) ∧ (Q → P) diff --git a/PropUtil.agda b/PropUtil.agda index 69d105c..99b77d2 100644 --- a/PropUtil.agda +++ b/PropUtil.agda @@ -44,3 +44,9 @@ module PropUtil where -- ⇔ shorthand _⇔_ : Prop → Prop → Prop P ⇔ Q = (P → Q) ∧ (Q → P) + + + -- Syntactic sugar for writing applications + infixr 200 _$_ + _$_ : {T U : Prop} → (T → U) → T → U + h $ t = h t diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda index 574f2c8..32a4639 100644 --- a/PropositionalKripke.agda +++ b/PropositionalKripke.agda @@ -58,8 +58,8 @@ module PropositionalKripke (PV : Set) where {- Soundness -} ⟦_⟧ : Γ ⊢ F → Γ ⊫ F - ⟦ zero ⟧ = proj₁ - ⟦ next p ⟧ = λ x → ⟦ p ⟧ (proj₂ x) + ⟦ zero zero∈ ⟧ wΓ = proj₁ wΓ + ⟦ zero (next∈ h) ⟧ wΓ = ⟦ zero h ⟧ (proj₂ wΓ) ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩ ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ) @@ -81,21 +81,21 @@ module PropositionalKripke (PV : Set) where mon⊩ = λ ba bx → halftran⊢⁺ ba bx } open Kripke UK - + -- 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⊢⁺ (right∈* refl∈*) iq) h) (zero zero∈))) (⊩ᶠ→⊢ hF)) ⊩ᶠ→⊢ {Var x} h = h - ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) + ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ (right∈* refl∈*) refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero 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 @@ -119,7 +119,7 @@ module PropositionalKripke (PV : Set) where ⊢→⊩ᶠ {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 ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ (right∈* refl∈*) refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈)))) module OtherProofs where @@ -132,16 +132,34 @@ module PropositionalKripke (PV : Set) where -- We can also use the relation ⊢⁰⁺, which is compatible with ⊢⁰ and ⊢* -- -> See module NormalizationProof - + - {- Renamings -} - - {- Weakening anywhere, order preserving, duplication authorized -} - - {- Weakening anywhere, no duplication, order preserving -} + {- Renamings : ∈* -} + UK∈* : Kripke + UK∈* = record { + Worlds = Con; + _≤_ = _∈*_; + refl≤ = refl∈*; + tran≤ = tran∈*; + _⊩_ = λ Γ x → Γ ⊢ Var x; + mon⊩ = λ x x₁ → addhyp⊢ x x₁ + } + {- + {- Weakening anywhere, order preserving, duplication authorized : ⊂⁺ -} + UK⊂⁺ : Kripke + UK⊂⁺ = record { + Worlds = Con; + _≤_ = _⊂⁺_; + refl≤ = refl⊂⁺; + tran≤ = tran⊂⁺; + _⊩_ = λ Γ x → Γ ⊢ Var x; + mon⊩ = λ x x₁ → addhyp⊢ x x₁ + } + -} + {- Weakening anywhere, no duplication, order preserving : ⊂ -} - {- Weakening at the end -} + {- Weakening at the end : ⊆-} -- This is exactly our relation ⊆ diff --git a/PropositionalKripkeGeneral.agda b/PropositionalKripkeGeneral.agda new file mode 100644 index 0000000..3796b1e --- /dev/null +++ b/PropositionalKripkeGeneral.agda @@ -0,0 +1,157 @@ +{-# OPTIONS --prop #-} + +module PropositionalKripkeGeneral (PV : Set) where + + open import ListUtil + open import PropUtil + open import PropositionalLogic PV using (Form; Var; _⇒_; Con) + + open import PropositionalKripke PV using (Kripke) + + record Preorder (T : Set₀) : Set₁ where + constructor order + field + _≤_ : T → T → Prop + refl≤ : {a : T} → a ≤ a + tran≤ : {a b c : T} → a ≤ b → b ≤ c → a ≤ c + + [_]ᵒᵖ : {T : Set₀} → Preorder T → Preorder T + [_]ᵒᵖ o = order (λ a b → (Preorder._≤_ o) b a) (Preorder.refl≤ o) (λ h₁ h₂ → (Preorder.tran≤ o) h₂ h₁) + + record NormalAndNeutral : Set₁ where + field + _⊢⁰_ : Con → Form → Prop + _⊢*_ : Con → Form → Prop + zero : {Γ : Con} → {F : Form} → (F ∷ Γ) ⊢⁰ F + app : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ⇒ G) → Γ ⊢* F → Γ ⊢⁰ G + neu⁰ : {Γ : Con} → {x : PV} → Γ ⊢⁰ Var x → Γ ⊢* Var x + lam : {Γ : Con} → {F G : Form} → (F ∷ Γ) ⊢* G → Γ ⊢* (F ⇒ G) + + record NormalizationFrame : Set₁ where + field + o : Preorder Con + nn : NormalAndNeutral + retro : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (Preorder._≤_ o) Γ (F ∷ Δ) + ⊢tran : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (NormalAndNeutral._⊢⁰_ nn) Γ F → (NormalAndNeutral._⊢⁰_ nn) Δ F + + open Preorder o + open NormalAndNeutral nn + + all : Con → PV → Prop + all Γ x = ⊤ + + UK : Kripke + UK = record { + Worlds = Con; + _≤_ = _≤_; + refl≤ = refl≤; + tran≤ = tran≤; + _⊩_ = λ Γ x → Γ ⊢⁰ Var x; + mon⊩ = λ Γ h → ⊢tran Γ h + } + + open Kripke UK + + -- q is quote, u is unquote + q : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F + u : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F + + u {Var x} h = h + u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF)) + q {Var x} h = neu⁰ h + q {F ⇒ F₁} {Γ} h = lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero))) + + + + + module NormalizationTests where + + {- Now using our records -} + open import PropositionalLogic PV hiding (Form; Var; _⇒_; Con) + + + ClassicNN : NormalAndNeutral + ClassicNN = record + { + _⊢⁰_ = _⊢⁰_ ; + _⊢*_ = _⊢*_ ; + zero = zero zero∈ ; + app = app ; + neu⁰ = neu⁰ ; + lam = lam + } + + BiggestNN : NormalAndNeutral + BiggestNN = record + { + _⊢⁰_ = _⊢_ ; + _⊢*_ = _⊢_ ; + zero = zero zero∈ ; + app = app ; + neu⁰ = λ x → x ; + lam = lam + } + + PO⊢⁺ = [ order {Con} _⊢⁺_ refl⊢⁺ tran⊢⁺ ]ᵒᵖ + PO⊢⁰⁺ = [ order {Con} _⊢⁰⁺_ refl⊢⁰⁺ tran⊢⁰⁺ ]ᵒᵖ + PO∈* = order {Con} _∈*_ refl∈* tran∈* + PO⊂⁺ = order {Con} _⊂⁺_ refl⊂⁺ tran⊂⁺ + PO⊂ = order {Con} _⊂_ refl⊂ tran⊂ + PO⊆ = order {Con} _⊆_ refl⊆ tran⊆ + + -- Completeness Proofs + Frame⊢ : NormalizationFrame + Frame⊢ = record + { + o = PO⊢⁺ ; + nn = BiggestNN ; + retro = λ s → addhyp⊢⁺ (right∈* refl∈*) s ; + ⊢tran = halftran⊢⁺ + } + + Frame⊢⁰ : NormalizationFrame + Frame⊢⁰ = record + { + o = PO⊢⁰⁺ ; + nn = ClassicNN ; + retro = λ s → addhyp⊢⁰⁺ (right∈* refl∈*) s ; + ⊢tran = halftran⊢⁰⁺⁰ + } + + Frame∈* : NormalizationFrame + Frame∈* = record + { + o = PO∈* ; + nn = ClassicNN ; + retro = right∈* ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ s) h + } + + Frame⊂⁺ : NormalizationFrame + Frame⊂⁺ = record + { + o = PO⊂⁺ ; + nn = ClassicNN ; + retro = next⊂⁺ ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* s) h + } + + Frame⊂ : NormalizationFrame + Frame⊂ = record + { + o = PO⊂ ; + nn = ClassicNN ; + retro = next⊂ ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ s) h + } + + Frame⊆ : NormalizationFrame + Frame⊆ = record + { + o = PO⊆ ; + nn = ClassicNN ; + retro = next⊆ ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ $ ⊆→⊂ s) h + } + + diff --git a/Readme.agda b/Readme.agda index ca1e730..6af3a4e 100644 --- a/Readme.agda +++ b/Readme.agda @@ -12,7 +12,7 @@ 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)))) +d-C = lam (lam (lam (app (zero $ next∈ $ next∈ zero∈) (app (zero $ next∈ zero∈) (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 @@ -115,15 +115,39 @@ module PierceDisproof where PierceNotProvable h = Pierce⊥w₁ (⟦ h ⟧ {w₁} tt) - - - - - - - - - +module CompletenessAndNormalization where + -- With Kripke models, we can even prove completeness + -- Using the Universal Kripke Model + + completenessQuote = CompletenessProof.⊩ᶠ→⊢ + completenessUnquote = CompletenessProof.⊢→⊩ᶠ + + -- With a slightly different universal model (using normal and neutral forms), + -- we can make a normalization proof + normalizationQuote = NormalizationProof.⊩ᶠ→⊢ + normalizationUnquote = NormalizationProof.⊢→⊩ᶠ + + -- This normalization proof has been made in the biggest Kripke model possible + -- that is, the one using the relation ⊢⁰⁺ + -- But we can also prove it with tighter relations: ∈*, ⊂⁺, ⊂, ⊆ + + -- As all those proofs are really similar, we created a NormalizationFrame structure + -- that computes most of the proof with only a few lemmas + open import PropositionalKripkeGeneral String + + -- We now have access to quote and unquote functions with this + u1 = NormalizationFrame.u NormalizationTests.Frame⊢ + q1 = NormalizationFrame.q NormalizationTests.Frame⊢ + u2 = NormalizationFrame.u NormalizationTests.Frame⊢⁰ + q2 = NormalizationFrame.q NormalizationTests.Frame⊢⁰ + u3 = NormalizationFrame.u NormalizationTests.Frame∈* + q3 = NormalizationFrame.q NormalizationTests.Frame∈* + u4 = NormalizationFrame.u NormalizationTests.Frame⊂⁺ + q4 = NormalizationFrame.q NormalizationTests.Frame⊂⁺ + u5 = NormalizationFrame.u NormalizationTests.Frame⊂ + q5 = NormalizationFrame.q NormalizationTests.Frame⊂ + u6 = NormalizationFrame.u NormalizationTests.Frame⊆ + q6 = NormalizationFrame.q NormalizationTests.Frame⊆