From 422dcf67f0d7871cabd638d72e2e91da98b9fdfa Mon Sep 17 00:00:00 2001 From: Mysaa Date: Tue, 30 May 2023 14:02:01 +0200 Subject: [PATCH] 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₁)