From a8978652533d249e0bf7dfa31a30f8e4e82c9331 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Fri, 14 Jul 2023 16:22:05 +0200 Subject: [PATCH] Added Agda new version, some progress --- FFOLInitial.agda | 70 +++++++++++++++++++++------ FinitaryFirstOrderLogic.agda | 92 ++++++++++++++++++++++++------------ ListUtil.agda | 2 +- PropUtil.agda | 42 +++++++++++----- 4 files changed, 149 insertions(+), 57 deletions(-) diff --git a/FFOLInitial.agda b/FFOLInitial.agda index 405903a..53a2974 100644 --- a/FFOLInitial.agda +++ b/FFOLInitial.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --prop #-} +{-# OPTIONS --prop --rewriting #-} open import PropUtil @@ -129,6 +129,9 @@ module FFOLInitial where σ-idr : {α : Subt Δₜ Γₜ} → α ∘ₜ idₜ ≡ α σ-idr {α = εₜ} = refl σ-idr {α = α ,ₜ x} = cong₂ _,ₜ_ σ-idr []t-id + ∘ₜ-ass : {Γₜ Δₜ Ξₜ Ψₜ : Cont}{α : Subt Γₜ Δₜ}{β : Subt Δₜ Ξₜ}{γ : Subt Ξₜ Ψₜ} → (γ ∘ₜ β) ∘ₜ α ≡ γ ∘ₜ (β ∘ₜ α) + ∘ₜ-ass {α = α} {β} {εₜ} = refl + ∘ₜ-ass {α = α} {β} {γ ,ₜ x} = cong₂ _,ₜ_ ∘ₜ-ass (≡sym ([]t-∘ {t = x})) []f-∀∀ : {A : For (Γₜ ▹t⁰)} → {σₜ : Subt Δₜ Γₜ} → (∀∀ A) [ σₜ ]f ≡ (∀∀ (A [ (σₜ ∘ₜ πₜ¹ idₜ) ,ₜ πₜ² idₜ ]f)) []f-∀∀ {A = A} = cong ∀∀ (cong (_[_]f A) (cong₂ _,ₜ_ (≡tran (cong wkₜσt (≡sym σ-idr)) (≡sym lem3)) refl)) @@ -299,11 +302,32 @@ module FFOLInitial where _∘ₚ_ : {Γₚ Δₚ Ξₚ : Conp Δₜ} → Subp {Δₜ} Δₚ Ξₚ → Subp {Δₜ} Γₚ Δₚ → Subp {Δₜ} Γₚ Ξₚ εₚ ∘ₚ β = εₚ (α ,ₚ pf) ∘ₚ β = (α ∘ₚ β) ,ₚ (pf [ β ]p) + idlₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} → (idₚ {Δₚ = Δₚ}) ∘ₚ σₚ ≡ σₚ + idlₚ {Δₚ = ◇p} = ? + idlₚ {Δₚ = Δₚ ▹p⁰ x} = ? + idrₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} → σₚ ∘ₚ (idₚ {Δₚ = Γₚ}) ≡ σₚ + idrₚ = {!!} id : Sub Γ Γ id {Γ} = sub idₜ (subst (Subp _) (≡sym []c-id) idₚ) _∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ sub αₜ αₚ ∘ sub βₜ βₚ = sub (αₜ ∘ₜ βₜ) (subst (Subp _) (≡sym []c-∘) (αₚ [ βₜ ]σₚ) ∘ₚ βₚ) + idl : {Γ Δ : Con} {σ : Sub Γ Δ} → (id {Δ}) ∘ σ ≡ σ + idl {σ = sub σₜ σₚ} = cong₂' sub σ-idl {!!} + idr : {Γ Δ : Con} {σ : Sub Γ Δ} → σ ∘ (id {Γ}) ≡ σ + idr {σ = sub σₜ σₚ} = cong₂' sub σ-idr {!!} + {- + ∘ₚ-ass : + {Γₜ Δₜ Ξₜ Ψₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Ξₜ}{Ψₚ : Conp Ψₜ} + {αₜ : Subt Γₜ Δₜ}{βₜ : Subt Δₜ Ξₜ}{γₜ : Subt Ξₜ Ψₜ}{γₚ : Subp Ξₚ (Ψₚ [ γₜ ]c)}{βₚ : Subp Δₚ (Ξₚ [ βₜ ]c)}{αₚ : Subp Γₚ (Δₚ [ αₜ ]c)} + {eq₁ : Subp (Δₚ [ αₜ ]c) ((Ψₚ [ γₜ ∘ₜ βₜ ]c)[ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c)} + {eq₂ : Subp (Ξₚ [ βₜ ]c) ((Ψₚ [ γₜ ]c)[ βₜ ]c) ≡ Subp (Ξₚ [ βₜ ]c) (Ψₚ [ γₜ ∘ₜ βₜ ]c)} + {eq₃ : Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ∘ₜ αₜ ]c) ≡ {!Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)!}} + {eq₄ : Subp (Δₚ [ αₜ ]c) ((Ξₚ [ βₜ ]c) [ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ξₚ [ βₜ ∘ₜ αₜ ]c)} + → (coe eq₁ (((coe eq₂ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ) ≡ (coe eq₃ (γₚ [ βₜ ∘ₜ αₜ ]σₚ)) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ) ∘ₚ αₚ)) + -} + postulate ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α) + -- ∘-ass {Γ}{Δ}{Ξ}{Ψ}{α = sub αₜ αₚ} {β = sub βₜ βₚ} {γ = sub γₜ γₚ} = {!Subp (Con.p Ξ [ βₜ ∘ₜ αₜ ]c) (Con.p Ψ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)!} -- SUB-ization @@ -332,15 +356,20 @@ module FFOLInitial where --lemG eq ε= {!!} substf : {ℓ ℓ' : Level}{A : Set ℓ}{P : A → Set ℓ'}{Q : A → Set ℓ'}{a b c d : A}{eqa : a ≡ a}{eqb : b ≡ b}{eqcd : c ≡ d}{eqdc : d ≡ c}{f : P a → P b}{g : P b → Q c}{x : P a} → g (subst P eqb (f (subst P eqa x))) ≡ subst Q eqdc (subst Q eqcd (g (f x))) substf {P = P} {Q = Q} {eqcd = refl} {f = f} {g = g} = ≡tran² (cong g (≡tran (substrefl {P = P} {e = refl}) (cong f (substrefl {P = P} {e = refl})))) (≡sym (substrefl {P = Q} {e = refl})) (≡sym (substrefl {P = Q} {e = refl})) - lemG : {σₜ : Subt Γₜ Ξₜ}{δₜ : Subt Δₜ Γₜ}{σₚ : Subp Γₚ (Ξₚ [ σₜ ]c)}{δₚ : Subp Δₚ (Γₚ [ δₜ ]c)}{t : Tm Γₜ} - {eq₁ : Subp (Γₚ [ δₜ ]c) (((Ξₚ ▹tp) [ σₜ ,ₜ t ]c) [ δₜ ]c) ≡ Subp (Γₚ [ δₜ ]c) ((Ξₚ ▹tp) [ (σₜ ∘ₜ δₜ) ,ₜ (t [ δₜ ]t) ]c)} - {eq₂ : Subp Γₚ (Ξₚ [ σₜ ]c) ≡ Subp Γₚ ((Ξₚ ▹tp) [ σₜ ,ₜ t ]c)} - {eq₃ : Subp Δₚ (Ξₚ [ σₜ ∘ₜ δₜ ]c) ≡ Subp Δₚ ((Ξₚ ▹tp) [ (σₜ ∘ₜ δₜ) ,ₜ (t [ δₜ ]t)]c)} - {eq₄ : Subp (Γₚ [ δₜ ]c) ((Ξₚ [ σₜ ]c) [ δₜ ]c) ≡ Subp (Γₚ [ δₜ ]c) (Ξₚ [ σₜ ∘ₜ δₜ ]c)} - → (coe eq₁ ((coe eq₂ σₚ) [ δₜ ]σₚ)) ∘ₚ δₚ ≡ coe eq₃ ((coe eq₄ (σₚ [ δₜ ]σₚ)) ∘ₚ δₚ) - lemG {σₜ = σₜ} {δₜ} {σₚ} {δₚ} {t} {eq₁} {eq₂} {eq₃} {eq₄} = {!eq₁!} - ,ₜ∘* {Γ} {Δ} {Ξ} {sub σₜ σₚ} {sub δₜ δₚ} {t} = cong (sub ((σₜ ∘ₜ δₜ) ,ₜ (t [ δₜ ]t))) lemG - + + ,ₜ∘* {Γ} {Δ} {Ξ} {sub σₜ σₚ} {sub δₜ δₚ} {t} = cong (sub ((σₜ ∘ₜ δₜ) ,ₜ (t [ δₜ ]t))) + (substfgpoly + {P = Subp {Con.t Δ} (Con.p Δ)} + {Q = Subp {Con.t Δ} ((Con.p Γ) [ δₜ ]c)} + {R = Subp {Con.t Γ} (Con.p Γ)} + {F = λ X → X [ δₜ ]c} + {eq₁ = ≡sym lemA} + {eq₂ = ≡sym []c-∘} + {eq₃ = ≡sym []c-∘} + {eq₄ = ≡sym lemA} + {g = λ σₚ → σₚ ∘ₚ δₚ} + {f = λ σₚ → σₚ [ δₜ ]σₚ} + {x = σₚ}) πₚ¹* : {Γ Δ : Con} {A : For (Con.t Γ)} → Sub Δ (Γ ▹p A) → Sub Δ Γ πₚ¹* (sub σₜ (σₚ ,ₚ pf)) = sub σₜ σₚ @@ -350,10 +379,19 @@ module FFOLInitial where sub σₜ σₚ ,ₚ* pf = sub σₜ (σₚ ,ₚ pf) ,ₚ∘πₚ : {Γ Δ : Con} → {F : For (Con.t Γ)} → {σ : Sub Δ (Γ ▹p F)} → (πₚ¹* σ) ,ₚ* (πₚ² σ) ≡ σ - ,ₚ∘πₚ {σ = sub σₜ (σₚ ,ₚ pf)} = refl - ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For (Con.t Ξ)}{prf : Pf Γ (F [ Sub.t σ ]f)} → (σ ,ₚ* prf) ∘ δ ≡ (σ ∘ δ) ,ₚ* (substP (λ F → Pf Δ F) (≡sym []f-∘) ((prf [ Sub.t δ ]pₜ) [ Sub.p δ ]p)) - ,ₚ∘ {Γ = Γ} {Δ = Δ} {σ = sub σₜ σₚ} {sub δₜ δₚ} {F = A} = cong (sub (σₜ ∘ₜ δₜ)) {!!} - + ,ₚ∘πₚ {σ = sub σₜ (σₚ ,ₚ p)} = refl + --funlol : {Γₜ Δₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Ξₜ}{σₜ : Subt Γₜ Ξₜ}{δₜ : Subt Δₜ Γₜ}{δₚ : Subp Δₚ (Γₚ [ δₜ ]c)}{A : For Ξₜ}{prf : Pf (con Δₜ (Γₚ [ δₜ ]c)) ((A [ σₜ ∘ₜ δₜ ]f))} → Subp {Δₜ} (Γₚ [ δₜ ]c) ((Ξₚ [ σₜ ∘ₜ δₜ ]c) ▹p⁰ ((A [ σₜ ]f) [ δₜ ]f)) → Subp {Δₜ} (Δₚ) ((Ξₚ [ σₜ ∘ₜ δₜ ]c) ▹p⁰ (A [ σₜ ∘ₜ δₜ ]f)) + --funlol {Γₚ = Γₚ} {Ξₚ = Ξₚ} {σₜ = σₜ} {δₜ = δₜ} {δₚ = δₚ} {prf = prf} (ξ ,ₚ pf) = ((subst (λ X → Subp (Γₚ [ δₜ ]c) ((Ξₚ [ σₜ ∘ₜ δₜ ]c) ▹p⁰ X)) (≡sym []f-∘) ξ) ,ₚ ?) ∘ₚ δₚ + postulate ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For (Con.t Ξ)}{prf : Pf Γ (F [ Sub.t σ ]f)} → (σ ,ₚ* prf) ∘ δ ≡ (σ ∘ δ) ,ₚ* (substP (λ F → Pf Δ F) (≡sym []f-∘) ((prf [ Sub.t δ ]pₜ) [ Sub.p δ ]p)) + {-,ₚ∘ {Γ = Γ} {Δ = Δ} {σ = sub σₜ σₚ} {sub δₜ δₚ} {F = A} {prf} = cong (sub (σₜ ∘ₜ δₜ)) (cong {!funlol!} + (substfpoly + {P = λ X → Subp (Con.p Γ [ δₜ ]c) (X ▹p⁰ ((A [ σₜ ]f) [ δₜ ]f))} + {R = λ X → Subp (Con.p Γ [ δₜ ]c) X} + {eq = ≡sym []c-∘} + {f = λ ξ → ξ ,ₚ (prf [ δₜ ]pₜ)} + {x = σₚ [ δₜ ]σₚ} + )) + -} --_,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹t) --πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t --πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ @@ -375,9 +413,13 @@ module FFOLInitial where { Con = Con ; Sub = Sub ; _∘_ = _∘_ + ; ∘-ass = ∘-ass ; id = id + ; idl = {!!} + ; idr = {!!} ; ◇ = ◇ ; ε = sub εₜ εₚ + ; ε-u = {!!} ; Tm = λ Γ → Tm (Con.t Γ) ; _[_]t = λ t σ → t [ Sub.t σ ]t ; []t-id = []t-id diff --git a/FinitaryFirstOrderLogic.agda b/FinitaryFirstOrderLogic.agda index 02d8223..50f7058 100644 --- a/FinitaryFirstOrderLogic.agda +++ b/FinitaryFirstOrderLogic.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --prop #-} +{-# OPTIONS --prop --rewriting #-} open import PropUtil @@ -15,11 +15,15 @@ module FinitaryFirstOrderLogic where infixr 5 _⊢_ field Con : Set ℓ¹ - Sub : Con → Con → Set ℓ⁵ -- It makes a posetal category + Sub : Con → Con → Set ℓ⁵ -- It makes a category _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ + ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α) id : {Γ : Con} → Sub Γ Γ + idl : {Γ Δ : Con} {σ : Sub Γ Δ} → (id {Δ}) ∘ σ ≡ σ + idr : {Γ Δ : Con} {σ : Sub Γ Δ} → σ ∘ (id {Γ}) ≡ σ ◇ : Con -- The initial object of the category ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object + ε-u : {Γ : Con} → {σ : Sub Γ ◇} → σ ≡ ε {Γ} -- Functor Con → Set called Tm Tm : Con → Set ℓ² @@ -27,7 +31,7 @@ module FinitaryFirstOrderLogic where []t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {t : Tm Γ} → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t - -- Tm⁺ + -- Tm : Set+ _▹ₜ : Con → Con πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ @@ -137,11 +141,11 @@ module FinitaryFirstOrderLogic where f ∘ g = λ x → f (g x) id : {Γ : Con} → Sub Γ Γ id = λ x → x - record ◇ : Con where - constructor ◇◇ - ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object - ε Γ = ◇◇ - + ε : {Γ : Con} → Sub Γ ⊤ₛ -- The morphism from the initial to any object + ε Γ = ttₛ + ε-u : {Γ : Con} → {σ : Sub Γ ⊤ₛ} → σ ≡ ε {Γ} + ε-u = refl + -- Functor Con → Set called Tm Tm : Con → Set Tm Γ = Γ → TM @@ -251,9 +255,13 @@ module FinitaryFirstOrderLogic where { Con = Con ; Sub = Sub ; _∘_ = _∘_ + ; ∘-ass = refl ; id = id - ; ◇ = ◇ + ; idl = refl + ; idr = refl + ; ◇ = ⊤ₛ ; ε = ε + ; ε-u = refl ; Tm = Tm ; _[_]t = _[_]t ; []t-id = []t-id @@ -294,49 +302,47 @@ module FinitaryFirstOrderLogic where -- (∀ x ∀ y . A(x,y)) ⇒ ∀ y ∀ x . A(y,x) -- both sides are ∀ ∀ A (0,1) - ex1 : {A : For (◇ ▹ₜ ▹ₜ)} → ◇ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (∀∀ A))) + ex1 : {A : For (⊤ₛ ▹ₜ ▹ₜ)} → ⊤ₛ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (∀∀ A))) ex1 _ hyp = hyp -- (A ⇒ ∀ x . B(x)) ⇒ ∀ x . A ⇒ B(x) - ex2 : {A : For ◇} → {B : For (◇ ▹ₜ)} → ◇ ⊢ ((A ⇒ (∀∀ B)) ⇒ (∀∀ ((A [ πₜ¹ id ]f) ⇒ B))) + ex2 : {A : For ⊤ₛ} → {B : For (⊤ₛ ▹ₜ)} → ⊤ₛ ⊢ ((A ⇒ (∀∀ B)) ⇒ (∀∀ ((A [ πₜ¹ id ]f) ⇒ B))) ex2 _ h t h' = h h' t -- ∀ x y . A(x,y) ⇒ ∀ x . A(x,x) -- For simplicity, I swiched positions of parameters of A (somehow...) - ex3 : {A : For (◇ ▹ₜ ▹ₜ)} → ◇ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (A [ id ,ₜ (πₜ² id) ]f))) + ex3 : {A : For (⊤ₛ ▹ₜ ▹ₜ)} → ⊤ₛ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (A [ id ,ₜ (πₜ² id) ]f))) ex3 _ h t = h t t -- ∀ x . A (x) ⇒ ∀ x y . A(x) - ex4 : {A : For (◇ ▹ₜ)} → ◇ ⊢ ((∀∀ A) ⇒ (∀∀ (∀∀ (A [ ε ,ₜ (πₜ² (πₜ¹ id)) ]f)))) + ex4 : {A : For (⊤ₛ ▹ₜ)} → ⊤ₛ ⊢ ((∀∀ A) ⇒ (∀∀ (∀∀ (A [ ε ,ₜ (πₜ² (πₜ¹ id)) ]f)))) ex4 {A} ◇◇ x t t' = x t -- (((∀ x . A (x)) ⇒ B)⇒ B) ⇒ ∀ x . ((A (x) ⇒ B) ⇒ B) - ex5 : {A : For (◇ ▹ₜ)} → {B : For ◇} → ◇ ⊢ ((((∀∀ A) ⇒ B) ⇒ B) ⇒ (∀∀ ((A ⇒ (B [ πₜ¹ id ]f)) ⇒ (B [ πₜ¹ id ]f)))) + ex5 : {A : For (⊤ₛ ▹ₜ)} → {B : For ⊤ₛ} → ⊤ₛ ⊢ ((((∀∀ A) ⇒ B) ⇒ B) ⇒ (∀∀ ((A ⇒ (B [ πₜ¹ id ]f)) ⇒ (B [ πₜ¹ id ]f)))) ex5 ◇◇ h t h' = h (λ h'' → h' (h'' t)) - record Kripke : Set₁ where + record Kripke : Set (lsuc (ℓ¹)) where field - World : Set + World : Set ℓ¹ _≤_ : World → World → Prop ≤refl : {w : World} → w ≤ w ≤tran : {w w' w'' : World} → w ≤ w' → w' ≤ w'' → w ≤ w' - TM : World → Set + TM : World → Set ℓ¹ TM≤ : {w w' : World} → w ≤ w' → TM w → TM w' - REL : (w : World) → TM w → TM w → Prop + REL : (w : World) → TM w → TM w → Prop ℓ¹ REL≤ : {w w' : World} → {t u : TM w} → (eq : w ≤ w') → REL w t u → REL w' (TM≤ eq t) (TM≤ eq u) infixr 10 _∘_ - Con = World → Set - Sub : Con → Con → Set + Con = World → Set ℓ¹ + Sub : Con → Con → Set ℓ¹ Sub Δ Γ = (w : World) → Δ w → Γ w _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ α ∘ β = λ w γ → α w (β w γ) id : {Γ : Con} → Sub Γ Γ id = λ w γ → γ - record ◇⁰ : Set where - constructor ◇◇⁰ ◇ : Con -- The initial object of the category - ◇ = λ w → ◇⁰ + ◇ = λ w → ⊤ₛ ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object - ε w Γ = ◇◇⁰ + ε w Γ = ttₛ -- Functor Con → Set called Tm - Tm : Con → Set + Tm : Con → Set ℓ¹ Tm Γ = (w : World) → (Γ w) → TM w _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms t [ σ ]t = λ w → λ γ → t w (σ w γ) @@ -346,7 +352,7 @@ module FinitaryFirstOrderLogic where []t-∘ = refl - + -- We simply define « bulk _[σ]t » (that acts on *n* terms from *Tm Γ*) _[_]tz : {Γ Δ : Con} → {n : Nat} → Array (Tm Γ) n → Sub Δ Γ → Array (Tm Δ) n tz [ σ ]tz = map (λ s → s [ σ ]t) tz []tz-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {n : Nat} → {tz : Array (Tm Γ) n} → tz [ β ∘ α ]tz ≡ tz [ β ]tz [ α ]tz @@ -375,8 +381,8 @@ module FinitaryFirstOrderLogic where ,ₜ∘ = refl -- Functor Con → Set called For - For : Con → Set₁ - For Γ = (w : World) → (Γ w) → Prop + 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) []f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F @@ -392,7 +398,7 @@ module FinitaryFirstOrderLogic where -- Proofs - _⊢_ : (Γ : Con) → For Γ → Prop + _⊢_ : (Γ : Con) → For Γ → Prop ℓ¹ Γ ⊢ F = ∀ w (γ : Γ w) → F w γ _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms prf [ σ ]p = λ w → λ γ → prf w (σ w γ) @@ -450,9 +456,13 @@ module FinitaryFirstOrderLogic where { Con = Con ; Sub = Sub ; _∘_ = _∘_ + ; ∘-ass = refl ; id = id + ; idl = refl + ; idr = refl ; ◇ = ◇ ; ε = ε + ; ε-u = refl ; Tm = Tm ; _[_]t = _[_]t ; []t-id = []t-id @@ -491,8 +501,30 @@ module FinitaryFirstOrderLogic where } + {- -- Completeness proof -- We first build our universal Kripke model - + module ComplenessProof (M : FFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} {ℓ⁵}) where + + -- We have a model, we construct the Universal Kripke model of this model + + World : Set ℓ¹ + World = FFOL.Con M + + _≤_ : World → World → Prop + Γ ≤ Δ = {!FFOL.Sub M Δ Γ!} + + UK : Kripke + UK = record + { World = World + ; _≤_ = λ Δ Γ → {!FFOL.Sub M Δ Γ!} + ; ≤refl = {!FFOL.id M!} + ; ≤tran = {!FFOL.∘ M!} + ; TM = {!!} + ; TM≤ = {!!} + ; REL = {!!} + ; REL≤ = {!!} + } + -} diff --git a/ListUtil.agda b/ListUtil.agda index 79e688c..b857d4e 100644 --- a/ListUtil.agda +++ b/ListUtil.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --prop #-} +{-# OPTIONS --prop --rewriting #-} module ListUtil where diff --git a/PropUtil.agda b/PropUtil.agda index da69503..ebada6f 100644 --- a/PropUtil.agda +++ b/PropUtil.agda @@ -2,6 +2,14 @@ module PropUtil where + open import Agda.Primitive + variable ℓ ℓ' : Level + + data ⊥ₛ : Set where + record ⊤ₛ : Set ℓ where + constructor ttₛ + + -- ⊥ is a data with no constructor -- ⊤ is a record with one always-available constructor data ⊥ : Prop where @@ -56,7 +64,6 @@ module PropUtil where - open import Agda.Primitive postulate _≈_ : ∀{ℓ}{A : Set ℓ}(a : A) → A → Set ℓ infix 3 _≡_ data _≡_ {ℓ}{A : Set ℓ}(a : A) : A → Prop ℓ where @@ -124,9 +131,22 @@ module PropUtil where substreflrefl : {ℓ ℓ' : Level}{A : Set ℓ}{P : A → Set ℓ'}{a : A}{e : a ≡ a}{p : P a} → subst P e (subst P e p) ≡ p substreflrefl {P = P} {a} {e} {p} = ≡tran (substrefl {P = P} {a = a} {e = e} {p = subst P e p}) (substrefl {P = P} {a = a} {e = e} {p = p}) + cong₂' : {ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : A → Set ℓ'}{C : Set ℓ''} → (f : (a : A) → B a → C) → {a a' : A} {b : B a} {b' : B a'} → (eq : a ≡ a') → subst B eq b ≡ b' → f a b ≡ f a' b' + cong₂' f {a} refl refl = cong (f a) (≡sym coerefl) + congsubst : {ℓ ℓ' : Level}{A : Set ℓ}{P : A → Set ℓ'}{a a' : A}{e : a ≡ a}{p : P a}{p' : P a} → p ≡ p' → subst P e p ≡ subst P e p' congsubst {P = P} {e = refl} h = cong (subst P refl) h - + + substfpoly : {ℓ ℓ' : Level}{A : Set ℓ}{P R : A → Set ℓ'}{α β : A} + {eq : α ≡ β} {f : {ξ : A} → R ξ → P ξ} {x : R α} + → coe (cong P eq) (f {α} x) ≡ f (coe (cong R eq) x) + substfpoly {eq = refl} {f} = ≡tran coerefl (cong f (≡sym coerefl)) + + substfgpoly : {ℓ ℓ' : Level}{A B : Set ℓ} {P Q : A → Set ℓ'} {R : B → Set ℓ'} {F : B → A} {α β : A} {ε φ : B} + {eq₁ : α ≡ β} {eq₂ : F ε ≡ α} {eq₃ : F φ ≡ β} {eq₄ : ε ≡ φ} + {g : {a : A} → Q a → P a} {f : {b : B} → R b → Q (F b)} {x : R ε} + → g {β} (subst Q eq₃ (f {φ} (subst R eq₄ x))) ≡ subst P eq₁ (g {α} (subst Q eq₂ (f {ε} x))) + substfgpoly {P = P} {Q} {R} {eq₁ = refl} {refl} {refl} {refl} {g} {f} = ≡tran³ (cong g (substrefl {P = Q} {e = refl})) (cong g (cong f (substrefl {P = R} {e = refl}))) (cong g (≡sym (substrefl {P = Q} {e = refl}))) (≡sym (substrefl {P = P} {e = refl})) {-# BUILTIN EQUALITY _≡_ #-} @@ -145,16 +165,14 @@ module PropUtil where succ : Nat → Nat {-# BUILTIN NATURAL Nat #-} - variable - ℓ ℓ' : Level - record _×_ (A : Set ℓ) (B : Set ℓ) : Set ℓ where + record _×_ (A : Set ℓ) (B : Set ℓ') : Set (ℓ ⊔ ℓ') where constructor _,×_ field a : A b : B - record _×'_ (A : Set ℓ) (B : Prop ℓ) : Set ℓ where + record _×'_ (A : Set ℓ) (B : Prop ℓ') : Set (ℓ ⊔ ℓ') where constructor _,×'_ field a : A @@ -166,19 +184,19 @@ module PropUtil where a : A b : B a - proj×₁ : {A B : Set} → (A × B) → A + proj×₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (A × B) → A proj×₁ p = _×_.a p - proj×₂ : {A B : Set} → (A × B) → B + proj×₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (A × B) → B proj×₂ p = _×_.b p - proj×'₁ : {A : Set} → {B : Prop} → (A ×' B) → A + proj×'₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Prop ℓ'} → (A ×' B) → A proj×'₁ p = _×'_.a p - proj×'₂ : {A : Set} → {B : Prop} → (A ×' B) → B + proj×'₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Prop ℓ'} → (A ×' B) → B proj×'₂ p = _×'_.b p - proj×''₁ : {A : Set} → {B : A → Prop} → (A ×'' B) → A + proj×''₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Prop ℓ'} → (A ×'' B) → A proj×''₁ p = _×''_.a p - proj×''₂ : {A : Set} → {B : A → Prop} → (p : A ×'' B) → B (proj×''₁ p) + proj×''₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Prop ℓ'} → (p : A ×'' B) → B (proj×''₁ p) proj×''₂ p = _×''_.b p