From 9be53b4f7f0ea78ad725581df0619a099f8e3522 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Thu, 3 Aug 2023 20:43:31 +0200 Subject: [PATCH] Tried to add a completeness proof for zol --- PropUtil.agda | 11 +++ ZOL2.lagda | 19 +++- ZOLCompleteness.lagda | 198 ++++++++++++++++++++++++++++++++++++++++++ ZOLInitial.lagda | 4 +- ZOLNormalization.agda | 3 +- 5 files changed, 229 insertions(+), 6 deletions(-) create mode 100644 ZOLCompleteness.lagda diff --git a/PropUtil.agda b/PropUtil.agda index 3da08a8..6410737 100644 --- a/PropUtil.agda +++ b/PropUtil.agda @@ -244,6 +244,12 @@ module PropUtil where a : A b : B + record _×p_ (A : Prop ℓ) (B : A → Prop ℓ') : Prop (ℓ ⊔ ℓ') where + constructor _,×p_ + field + a : A + b : B a + record _×''_ (A : Set ℓ) (B : A → Prop ℓ') : Set (ℓ ⊔ ℓ') where constructor _,×''_ field @@ -267,6 +273,11 @@ module PropUtil where proj×'₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Prop ℓ'} → (A ×' B) → B proj×'₂ p = _×'_.b p + proj×p₁ : {ℓ ℓ' : Level}{A : Prop ℓ}{B : A → Prop ℓ'} → (A ×p B) → A + proj×p₁ p = _×p_.a p + proj×p₂ : {ℓ ℓ' : Level}{A : Prop ℓ}{B : A → Prop ℓ'} → (p : A ×p B) → B (proj×p₁ p) + proj×p₂ p = _×p_.b p + proj×''₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Prop ℓ'} → (A ×'' B) → A proj×''₁ p = _×''_.a p proj×''₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Prop ℓ'} → (p : A ×'' B) → B (proj×''₁ p) diff --git a/ZOL2.lagda b/ZOL2.lagda index ecbb699..bf24fe7 100644 --- a/ZOL2.lagda +++ b/ZOL2.lagda @@ -9,7 +9,8 @@ module ZOL2 where open import ListUtil variable - ℓ¹ ℓ² ℓ³ ℓ⁴ ℓ⁵ : Level + ℓ¹ ℓ² ℓ³ ℓ⁴ : Level + ℓ¹' ℓ²' ℓ³' ℓ⁴' : Level record ZOL : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴)) where infixr 10 _∘_ @@ -77,7 +78,7 @@ module ZOL2 where lam : {Γ : Con}{F G : For Γ} → Pf (Γ ▹ₚ F) (G [ πₚ¹ id ]f) → Pf Γ (F ⇒ G) app : {Γ : Con}{F G : For Γ} → Pf Γ (F ⇒ G) → Pf Γ F → Pf Γ G - record Mapping (S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) (D : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴)) where + record Mapping (S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) (D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ¹' ⊔ ℓ²' ⊔ ℓ³' ⊔ ℓ⁴')) where field -- We first make the base category with its final object @@ -87,7 +88,7 @@ module ZOL2 where mPf : {Γ : (ZOL.Con S)} {A : ZOL.For S Γ} → ZOL.Pf S Γ A → ZOL.Pf D (mCon Γ) (mFor A) - record Morphism (S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) (D : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴)) where + record Morphism (S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) (D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ¹' ⊔ ℓ²' ⊔ ℓ³' ⊔ ℓ⁴')) where field m : Mapping S D mCon = Mapping.mCon m mSub = Mapping.mSub m @@ -101,4 +102,16 @@ module ZOL2 where e⇒ : {Γ : ZOL.Con S}{A B : ZOL.For S Γ} → mFor (ZOL._⇒_ S A B) ≡ ZOL._⇒_ D (mFor A) (mFor B) -- No equation needed for lam, app, ∀i, ∀e as their output are in prop + record TrNat {S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}} {D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}} (a : Mapping S D) (b : Mapping S D) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ¹' ⊔ ℓ²' ⊔ ℓ³' ⊔ ℓ⁴')) where + field + f : (Γ : ZOL.Con S) → ZOL.Sub D (Mapping.mCon a Γ) (Mapping.mCon b Γ) + -- Unneeded because Sub are in prop + --eq : (Γ Δ : ZOL.Con S)(σ : ZOL.Sub S Γ Δ) → (ZOL._∘_ D (f Δ) (Mapping.mSub a σ)) ≡ (ZOL._∘_ D (Mapping.mSub b σ) (f Γ)) + + _∘TrNat_ : {S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}}{D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}}{a b c : Mapping S D} → TrNat a b → TrNat b c → TrNat a c + _∘TrNat_ {D = D} α β = record { f = λ Γ → ZOL._∘_ D (TrNat.f β Γ) (TrNat.f α Γ) } + + idTrNat : {S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}}{D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}}{a : Mapping S D} → TrNat a a + idTrNat {D = D} = record { f = λ Γ → ZOL.id D } + \end{code} diff --git a/ZOLCompleteness.lagda b/ZOLCompleteness.lagda new file mode 100644 index 0000000..a3659be --- /dev/null +++ b/ZOLCompleteness.lagda @@ -0,0 +1,198 @@ +\begin{code} +{-# OPTIONS --prop --rewriting #-} + +open import PropUtil + +module ZOLCompleteness where + + open import Agda.Primitive + open import ZOL2 + open import ListUtil + + record Kripke : Set (lsuc (ℓ¹)) where + field + World : Set ℓ¹ + _-w->_ : World → World → Prop ℓ¹ -- arrows + -w->id : {w : World} → w -w-> w -- id arrow + _∘-w->_ : {w w' w'' : World} → w -w-> w' → w' -w-> w'' → w -w-> w'' -- arrow composition + + Ι : World → Prop ℓ¹ + Ι≤ : {w w' : World} → w -w-> w' → Ι w' → Ι w + + infixr 10 _∘_ + + Con : Set (lsuc ℓ¹) + Con = World → Prop ℓ¹ + Sub : Con → Con → Prop ℓ¹ + Sub Δ Γ = (w : World) → Δ w → Γ w + _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ + α ∘ β = λ w γ → α w (β w γ) + id : {Γ : Con} → Sub Γ Γ + id = λ w γ → γ + ◇ : Con -- The initial object of the category + ◇ = λ w → ⊤ + ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object + ε w Γ = tt + + + -- Functor Con → Set called For + For : Con → Set (lsuc ℓ¹) + For Γ = (w : World) → (Γ w) → Prop ℓ¹ + _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms + F [ σ ]f = λ w → λ x → F w (σ w x) + + -- Proofs + Pf : (Γ : Con) → For Γ → Prop ℓ¹ + Pf Γ F = ∀ w (γ : Γ w) → F w γ + _[_]p : {Γ Δ : Con} → {F : For Γ} → Pf Γ F → (σ : Sub Δ Γ) → Pf Δ (F [ σ ]f) -- The functor's action on morphisms + prf [ σ ]p = λ w → λ γ → prf w (σ w γ) + -- Equalities below are useless because Γ ⊢ F is in prop + -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf + -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p + + -- → Prop⁺ + _▹ₚ_ : (Γ : Con) → For Γ → Con + Γ ▹ₚ F = λ w → Γ w ×p F w + πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ + πₚ¹ σ w δ = proj×p₁ (σ w δ) + πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Pf Δ (F [ πₚ¹ σ ]f) + πₚ² σ w δ = proj×p₂ (σ w δ) + _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Pf Δ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) + (σ ,ₚ pf) w δ = (σ w δ) ,×p pf w δ + + + -- Base formula + ι : {Γ : Con} → For Γ + ι = λ w → λ γ → Ι w + + -- Implication + _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ + (F ⇒ G) w γ = {w' : World} → (s : w -w-> w') → (F w' {!s γ!}) → (G w' {!!}) + + -- Lam & App + lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → Pf (Γ ▹ₚ F) (G [ πₚ¹ id ]f) → Pf Γ (F ⇒ G) + --lam prf = λ w γ w' s h → prf w (γ ,×p h) + app : {Γ : Con} → {F G : For Γ} → Pf Γ (F ⇒ G) → Pf Γ F → Pf Γ G + --app prf prf' = λ w γ → prf w γ w -w->id (prf' w γ) + -- Again, we don't write the _[_]p equalities as everything is in Prop + + zol : ZOL + zol = record + { Con = Con + ; Sub = Sub + ; _∘_ = _∘_ + ; id = id + ; ◇ = ◇ + ; ε = ε + ; For = For + ; _[_]f = _[_]f + ; []f-id = refl + ; []f-∘ = refl + ; Pf = Pf + ; _[_]p = _[_]p + ; _▹ₚ_ = _▹ₚ_ + ; πₚ¹ = πₚ¹ + ; πₚ² = πₚ² + ; _,ₚ_ = _,ₚ_ + ; ι = ι + ; []f-ι = refl + ; _⇒_ = _⇒_ + ; []f-⇒ = refl + ; lam = lam + ; app = app + } + +\end{code} + module U where + + import ZOLInitial as I + + U : Kripke + U = record + { World = I.Con + ; _-w->_ = I.Sub + ; -w->id = I.id + ; _∘-w->_ = λ σ σ' → σ' I.∘ σ + ; Ι = λ Γ → I.Pf Γ I.ι + ; Ι≤ = λ s pf → pf I.[ s ]p + } + + open Kripke U + + y : Mapping I.zol zol + y = record + { mCon = λ Γ Δ → I.Sub Δ Γ + ; mSub = λ σ Ξ δ → σ I.∘ δ + ; mFor = λ A Ξ σ → I.Pf Ξ A + ; mPf = λ pf Ξ σ → pf I.[ σ ]p + } + m : Morphism I.zol zol + m = I.InitialMorphism.mor zol + + u : (Γ : I.Con) → Sub (Morphism.mCon m Γ) (Mapping.mCon y Γ) + q : (Γ : I.Con) → Sub (Mapping.mCon y Γ) (Morphism.mCon m Γ) + + ⟦_⟧c = Morphism.mCon m + ⟦_,_⟧f = λ A Γ → Morphism.mFor m {Γ} A + + ⟦⟧f-mon : {Γ : I.Con}{A : I.For}{w w' : World}{γ : ⟦ Γ ⟧c w}{γ' : ⟦ Γ ⟧c w'} → w -w-> w' → ⟦ A , Γ ⟧f w' γ' → ⟦ A , Γ ⟧f w γ + ⟦⟧f-mon {A = I.ι} s h = Ι≤ s h + ⟦⟧f-mon {A = A I.⇒ B} s h w'' s' h' = {!h!} + + ⟦⟧c-mon : {Γ : I.Con}{w w' : I.Con} → w -w-> w' → ⟦ Γ ⟧c w → ⟦ Γ ⟧c w' + ⟦⟧c-mon s h = {!!} + + q⁰ : {F : I.For} → {Γ : I.Con} → Pf ⟦ Γ ⟧c ⟦ F , Γ ⟧f → I.Pf Γ F + u⁰ : {F : I.For} → {Γ : I.Con} → I.Pf Γ F → Pf ⟦ Γ ⟧c ⟦ F , Γ ⟧f + + u⁰ {I.ι} h w γ = {!!} + u⁰ {A I.⇒ B} h Γ' γ Γ'' iq hF = u⁰ {B} (I.app {A = A} h (q⁰ (λ Ξ γ' → {!hF!}))) {!!} γ --{Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF)) + + q⁰ {I.ι} {Γ} h = h Γ {!!} + q⁰ {A I.⇒ B} {Γ} h = I.lam (q⁰ (λ w γ → {!h ? ? ? (I.πₚ¹ I.id)!})) --lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero))) + + u I.◇ Δ x = I.ε + u (Γ I.▹ₚ I.ι) Δ (Γu ,×p Au) = u Γ Δ Γu I.,ₚ Au + --u (Γ I.▹ₚ (A I.⇒ B)) Δ (Γu ,×p ABu) = (u Γ Δ Γu) I.,ₚ I.lam (I.πₚ² (u (Γ I.▹ₚ B) (Δ I.▹ₚ A) ({!!} ,×p {!!}))) + u (Γ I.▹ₚ (A I.⇒ B)) Δ (Γu ,×p ABu) = (u Γ Δ Γu) I.,ₚ {!!} + q .I.◇ Δ I.ε = tt + q (Γ I.▹ₚ I.ι) Δ σ = (q Γ Δ (I.πₚ¹ σ)) ,×p I.πₚ² σ + q (Γ I.▹ₚ (A I.⇒ B)) Δ σ = (q Γ Δ (I.πₚ¹ σ)) ,×p {!!} + + {- + u {Var x} h = h + u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF)) + u {F ∧∧ G} h = ⟨ (u {F} (ande₁ h)) , (u {G} (ande₂ h)) ⟩ + u {⊤⊤} h = tt + + q {Var x} h = neu⁰ h + q {F ⇒ F₁} {Γ} h = lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero))) + q {F ∧∧ G} ⟨ hF , hG ⟩ = andi (q {F} hF) (q {G} hG) + q {⊤⊤} h = true + -} + + ηu : TrNat (Morphism.m m) y + ηu = record { f = u } + ηq : TrNat y (Morphism.m m) + ηq = record { f = q } + + eq : ηu ∘TrNat ηq ≡ idTrNat + eq = {!!} + + + -- Transformation naturelle + + +\end{code} + + + -- Completeness proof + + -- We first build our universal Kripke model + + module ComplenessProof where + + -- We have a model, we construct the Universal Presheaf model of this model + import ZOLInitial as I + +\end{code} diff --git a/ZOLInitial.lagda b/ZOLInitial.lagda index e44b167..0ef457d 100644 --- a/ZOLInitial.lagda +++ b/ZOLInitial.lagda @@ -109,7 +109,7 @@ module ZOLInitial where ; app = app } - module InitialMorphism (M : ZOL {lzero} {lzero} {lzero} {lzero}) where + module InitialMorphism (M : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) where mCon : Con → (ZOL.Con M) mFor : {Γ : Con} → For → (ZOL.For M (mCon Γ)) @@ -156,7 +156,7 @@ module ZOLInitial where ; e⇒ = refl } - module InitialMorphismUniqueness {M : ZOL {lzero} {lzero} {lzero} {lzero}} {m : Morphism zol M} where + module InitialMorphismUniqueness {M : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}} {m : Morphism zol M} where open InitialMorphism M mCon≡ : {Γ : Con} → mCon Γ ≡ (Morphism.mCon m Γ) diff --git a/ZOLNormalization.agda b/ZOLNormalization.agda index b6339c9..1818d02 100644 --- a/ZOLNormalization.agda +++ b/ZOLNormalization.agda @@ -61,7 +61,8 @@ module ZOLNormalization (PV : Set) where 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)) + u {F ⇒ F₁} h {Γ'} iq hF = {!!} + --u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF)) u {F ∧∧ G} h = ⟨ (u {F} (ande₁ h)) , (u {G} (ande₂ h)) ⟩ u {⊤⊤} h = tt