Removed the Kripke model

2023-07-20 11:03:52 +02:00 · 2023-07-20 11:03:52 +02:00 · 2534ebf85e
commit 2534ebf85e
parent fbf699b63e
3 changed files with 3 additions and 212 deletions
--- a/FFOLCompleteness.agda
+++ b/FFOLCompleteness.agda
@ -239,7 +239,7 @@ module FFOLCompleteness where
    app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G
    app prf prf' = λ w γ → prf w γ w id-a (prf' w γ)
    -- Again, we don't write the _[_]p equalities as everything is in Prop
-                                                                      
+vv                                                                      
    -- ∀i and ∀e
    ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
    ∀i p w γ = λ t → p w (γ ,× t)
--- a/FinitaryFirstOrderLogic.agda
+++ b/FinitaryFirstOrderLogic.agda
@ -317,214 +317,3 @@ module FinitaryFirstOrderLogic where
    -- (((∀ 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 ◇◇ h t h' = h (λ h'' → h' (h'' t))
-
-  record Kripke : Set (lsuc (ℓ¹)) where
-    field
-      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≤ : {w w' : World} → w ≤ w' → TM w → TM w'
-      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 ℓ¹
-    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 Tm
-    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 γ)
-    []t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x
-    []t-id = refl
-    []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {t : Tm Γ} → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t
-    []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
-    []tz-∘ {tz = zero} = refl
-    []tz-∘ {α = α} {β = β} {tz = next x tz} = substP (λ tz' → (next ((x [ β ]t) [ α ]t) tz') ≡ (((next x tz) [ β ]tz) [ α ]tz)) (≡sym ([]tz-∘ {α = α} {β = β} {tz = tz})) refl
-    []tz-id : {Γ : Con} → {n : Nat} → {tz : Array (Tm Γ) n} → tz [ id ]tz ≡ tz
-    []tz-id {tz = zero} = refl
-    []tz-id {tz = next x tz} = substP (λ tz' → next x tz' ≡ next x tz) (≡sym ([]tz-id {tz = tz})) refl
-    
-    -- Tm⁺
-    _▹ₜ : Con → Con
-    Γ ▹ₜ = λ w → (Γ w) × (TM w)
-    πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ
-    πₜ¹ σ = λ w → λ x → proj×₁ (σ w x)
-    πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ
-    πₜ² σ = λ w → λ x → proj×₂ (σ w x) 
-    _,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹ₜ)
-    σ ,ₜ t = λ w → λ x → (σ w x) ,× (t w x)
-    πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t
-    πₜ²∘,ₜ {σ = σ} {t} = refl {a = t}
-    πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ
-    πₜ¹∘,ₜ = refl
-    ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ
-    ,ₜ∘πₜ = refl
-    ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t)
-    ,ₜ∘ = refl
-                                                                    
-    -- 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)
-    []f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F
-    []f-id = refl
-    []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f
-    []f-∘ = refl
-
-    -- Formulas with relation on terms
-    R : {Γ : Con} → Tm Γ → Tm Γ → For Γ
-    R t u = λ w → λ γ → REL w (t w γ) (u w γ)
-    R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ} → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t)
-    R[] {σ = σ} = cong₂ R refl refl
-
-                                                                                                        
-    -- Proofs
-    _⊢_ : (Γ : 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 γ)
-    -- 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) ×'' (F w)
-    πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ
-    πₚ¹ σ w δ = proj×''₁ (σ w δ)
-    πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f)
-    πₚ² σ w δ = proj×''₂ (σ w δ)
-    _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
-    _,ₚ_ {F = F} σ pf w δ = (σ w δ) ,×'' pf w δ
-    ,ₚ∘πₚ : {Γ Δ : Con} → {F : For Γ} → {σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ
-    ,ₚ∘πₚ = refl
-    πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ {Γ} {Δ} {F} (σ ,ₚ prf) ≡ σ
-    πₚ¹∘,ₚ = refl
-    ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} →
-      (_,ₚ_  {F = F} σ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym ([]f-∘ {α = δ} {β = σ} {F = F})) (prf [ δ ]p))
-    ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} = refl
-    
-                                                                                                      
-                                                                                                      
-    -- Implication
-    _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
-    F ⇒ G = λ w → λ γ → (∀ w' → w ≤ w' → (F w γ) → (G w γ))
-    []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f)
-    []f-⇒ = refl
-    
-    -- Forall
-    ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
-    ∀∀ F = λ w → λ γ → ∀ t → F w (γ ,× t)
-    []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
-    []f-∀∀ = refl
-                                                                                                                           
-    -- Lam & App
-    lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
-    lam prf = λ w γ w' s h → prf w (γ ,×'' h)
-    app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G
-    app prf prf' = λ w γ → prf w γ w ≤refl (prf' w γ)
-    -- Again, we don't write the _[_]p equalities as everything is in Prop
-                                                                      
-    -- ∀i and ∀e
-    ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
-    ∀i p w γ = λ t → p w (γ ,× t)
-    ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
-    ∀e p {t} w γ = p w γ (t w γ)
-
-
-    tod : FFOL
-    tod = record
-      { Con = Con
-      ; Sub = Sub
-      ; _∘_ = _∘_
-      ; ∘-ass = refl
-      ; id = id
-      ; idl = refl
-      ; idr = refl
-      ; ◇ = ◇
-      ; ε = ε
-      ; ε-u = refl
-      ; Tm = Tm
-      ; _[_]t = _[_]t
-      ; []t-id = []t-id
-      ; []t-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {t} → []t-∘ {Γ} {Δ} {Ξ} {α} {β} {t}
-      ; _▹ₜ = _▹ₜ
-      ; πₜ¹ = πₜ¹
-      ; πₜ² = πₜ²
-      ; _,ₜ_ = _,ₜ_
-      ; πₜ²∘,ₜ = λ {Γ} {Δ} {σ} → πₜ²∘,ₜ {Γ} {Δ} {σ}
-      ; πₜ¹∘,ₜ = λ {Γ} {Δ} {σ} {t} → πₜ¹∘,ₜ {Γ} {Δ} {σ} {t}
-      ; ,ₜ∘πₜ = ,ₜ∘πₜ
-      ; ,ₜ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {t} → ,ₜ∘ {Γ} {Δ} {Ξ} {σ} {δ} {t}
-      ; For = For
-      ; _[_]f = _[_]f
-      ; []f-id = []f-id
-      ; []f-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {F} → []f-∘ {Γ} {Δ} {Ξ} {α} {β} {F}
-      ; _⊢_ = _⊢_
-      ; _[_]p = _[_]p
-      ; _▹ₚ_ = _▹ₚ_
-      ; πₚ¹ = πₚ¹
-      ; πₚ² = πₚ²
-      ; _,ₚ_ = _,ₚ_
-      ; ,ₚ∘πₚ = ,ₚ∘πₚ
-      ; πₚ¹∘,ₚ = λ {Γ} {Δ} {F} {σ} {p} → πₚ¹∘,ₚ {Γ} {Δ} {F} {σ} {p}
-      ; ,ₚ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} → ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf}
-      ; _⇒_ = _⇒_
-      ; []f-⇒ = λ {Γ} {F} {G} {σ} → []f-⇒ {Γ} {F} {G} {σ}
-      ; ∀∀ = ∀∀
-      ; []f-∀∀ = λ {Γ} {Δ} {F} {σ} → []f-∀∀ {Γ} {Δ} {F} {σ}
-      ; lam = lam
-      ; app = app
-      ; ∀i = ∀i
-      ; ∀e = ∀e
-      ; R = R
-      ; R[] = λ {Γ} {Δ} {σ} {t} {u} → R[] {Γ} {Δ} {σ} {t} {u}
-      }
-
-
-  {-
-  -- 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≤ = {!!}
-           }
-  -}
--- a/PropUtil.agda
+++ b/PropUtil.agda
@ -162,10 +162,12 @@ module PropUtil where
    {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))
+  
  substppoly : {ℓ ℓ' ℓ'' ℓ''' : Level}{A : Set ℓ}{P : A → Set ℓ'}{R : A → Set ℓ''}{Q : A → Set ℓ'''}{α β : A}
    {eq : α ≡ β}{f : {ξ : A} → R ξ → Q ξ → P ξ} {x : R α} {y : Q α}
    → coe (cong P eq) (f {α} x y) ≡ f {β} (coe (cong R eq) x) (coe (cong Q eq) y)
  substppoly {eq = refl} {f}{x}{y} = ≡tran coerefl (cong₂ f (≡sym coerefl) (≡sym coerefl))
+  
  substfpoly' : {ℓ ℓ' ℓ'' : Level}{A B : Set ℓ}{P R : A → Set ℓ'}{Q : B → Prop ℓ''}{α β : A}{γ δ : B}
    {eq : α ≡ β}{eq' : γ ≡ δ} {f : {ξ : A}{ι : B} → R ξ → Q ι → P ξ} {x : R α} {y : Q γ}
    → coe (cong P eq) (f {α} {γ} x y) ≡ f {β} {δ} (coe (cong R eq) x) (substP Q eq' y)