From bcff4c47e64f1dc2890556a78ee81fbb770b2e11 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Tue, 13 Jun 2023 18:43:20 +0200 Subject: [PATCH] Added Kripke model for first order --- FinitaryFirstOrderLogic.agda | 182 +++++++++++++++++++++++++++++++++++ PropUtil.agda | 1 + 2 files changed, 183 insertions(+) diff --git a/FinitaryFirstOrderLogic.agda b/FinitaryFirstOrderLogic.agda index 6909eee..a31fee4 100644 --- a/FinitaryFirstOrderLogic.agda +++ b/FinitaryFirstOrderLogic.agda @@ -246,6 +246,188 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where ; rel = rel ; rel[] = rel[] } + + module Kripke + (World : Set) + (_≤_ : World → World → Prop) + (≤refl : {w : World} → w ≤ w ) + (≤tran : {w w' w'' : World} → w ≤ w' → w' ≤ w'' → w ≤ w'') + (TM : Set) + (REL : (n : Nat) → R n → Array TM n → World → Prop) + (RELmon : {n : Nat} → {r : R n} → {x : Array TM n} → {w w' : World} → REL n r x w → REL n r x w') + (FUN : (n : Nat) → F n → Array TM n → TM) + where + 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 γ → γ + data ◇⁰ : Set where + ◇ : Con -- The initial object of the category + ◇ = λ w → ◇⁰ + ε : {Γ : Con} → Sub ◇ Γ -- The morphism from the initial to any object + ε w () + + -- Functor Con → Set called Tm + Tm : Con → Set + Tm Γ = (w : World) → (Γ w) → TM + _[_]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 + + + _[_]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 + thm : {Γ Δ : Con} → {n : Nat} → {tz : Array (Tm Γ) n} → {σ : Sub Δ Γ} → {w : World} → {δ : Δ w} → map (λ t → t w δ) (tz [ σ ]tz) ≡ map (λ t → t w (σ w δ)) tz + thm {tz = zero} = refl + thm {tz = next x tz} {σ} {w} {δ} = substP (λ tz' → (next (x w (σ w δ)) (map (λ t → t w δ) (map (λ s w γ → s w (σ w γ)) tz))) ≡ (next (x w (σ w δ)) tz')) (thm {tz = tz}) refl -- substP (λ tz' → (next (x w (σ w δ)) (map (λ t → t δ) (map (λ s γ → s w (σ w γ)) tz))) ≡ (next (x w (σ w δ)) tz')) (thm {tz = tz}) refl + + + -- Term extension with functions + fun : {Γ : Con} → {n : Nat} → F n → Array (Tm Γ) n → Tm Γ + fun {n = n} f tz = λ w γ → FUN n f (map (λ t → t w γ) tz) + fun[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {n : Nat} → {f : F n} → {tz : Array (Tm Γ) n} → (fun f tz) [ σ ]t ≡ fun f (map (λ t → t [ σ ]t) tz) + fun[] {Γ = Γ} {Δ = Δ} {σ = σ} {n = n} {f = f} {tz = tz} = ≡fun' λ w → ≡fun λ γ → substP ((λ x → (FUN n f) x ≡ (FUN n f) (map (λ t → t w γ) (tz [ σ ]tz)))) (thm {tz = tz}) refl + + -- Tm⁺ + _▹ₜ : Con → Con + Γ ▹ₜ = λ w → (Γ w) × TM + πₜ¹ : {Γ Δ : 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 + + -- Functor Con → Set called For + For : Con → Set₁ + 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 + rel : {Γ : Con} → {n : Nat} → R n → Array (Tm Γ) n → For Γ + rel {n = n} r tz = λ w → λ γ → (REL n r) (map (λ t → t w γ) tz) w + rel[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {n : Nat} → {r : R n} → {tz : Array (Tm Γ) n} → (rel r tz) [ σ ]f ≡ rel r (map (λ t → t [ σ ]t) tz) + rel[] {σ = σ} {n = n} {r = r} {tz = tz} = ≡fun' ( λ w → ≡fun (λ γ → (substP (λ x → (REL n r) x w ≡ (REL n r) (map (λ t → t w γ) (tz [ σ ]tz)) w) thm 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 + + + -- 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 Δ Γ} → {t : Tm Γ} → (∀∀ 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 F R + tod = record + { Con = Con + ; Sub = Sub + ; _∘_ = _∘_ + ; id = id + ; ◇ = ◇ + ; ε = ε + ; Tm = Tm + ; _[_]t = _[_]t + ; []t-id = []t-id + ; []t-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {t} → []t-∘ {Γ} {Δ} {Ξ} {α} {β} {t} + ; _▹ₜ = _▹ₜ + ; πₜ¹ = πₜ¹ + ; πₜ² = πₜ² + ; _,ₜ_ = _,ₜ_ + ; πₜ²∘,ₜ = λ {Γ} {Δ} {σ} → πₜ²∘,ₜ {Γ} {Δ} {σ} + ; πₜ¹∘,ₜ = λ {Γ} {Δ} {σ} {t} → πₜ¹∘,ₜ {Γ} {Δ} {σ} {t} + ; ,ₜ∘πₜ = ,ₜ∘πₜ + ; For = For + ; _[_]f = _[_]f + ; []f-id = []f-id + ; []f-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {F} → []f-∘ {Γ} {Δ} {Ξ} {α} {β} {F} + ; _⊢_ = _⊢_ + ; _▹ₚ_ = _▹ₚ_ + ; πₚ¹ = πₚ¹ + ; πₚ² = πₚ² + ; _,ₚ_ = _,ₚ_ + ; ,ₚ∘πₚ = ,ₚ∘πₚ + ; πₚ¹∘,ₚ = λ {Γ} {Δ} {F} {σ} {p} → πₚ¹∘,ₚ {Γ} {Δ} {F} {σ} {p} + ; _⇒_ = _⇒_ + ; []f-⇒ = λ {Γ} {F} {G} {σ} → []f-⇒ {Γ} {F} {G} {σ} + ; ∀∀ = ∀∀ + ; []f-∀∀ = λ {Γ} {Δ} {F} {σ} {t} → []f-∀∀ {Γ} {Δ} {F} {σ} {t} + ; lam = lam + ; app = app + ; ∀i = ∀i + ; ∀e = ∀e + ; fun = fun + ; fun[] = fun[] + ; rel = rel + ; rel[] = rel[] + } + {- module M where diff --git a/PropUtil.agda b/PropUtil.agda index b042953..6107404 100644 --- a/PropUtil.agda +++ b/PropUtil.agda @@ -60,6 +60,7 @@ module PropUtil where ≡sym refl = refl postulate ≡fun : {ℓ ℓ' : Level} → {A : Set ℓ} → {B : Set ℓ'} → {f g : A → B} → ((x : A) → (f x ≡ g x)) → f ≡ g + postulate ≡fun' : {ℓ ℓ' : Level} → {A : Set ℓ} → {B : A → Set ℓ'} → {f g : (a : A) → B a} → ((x : A) → (f x ≡ g x)) → f ≡ g postulate subst : ∀{ℓ}{A : Set ℓ}{ℓ'}(P : A → Set ℓ'){a a' : A} → a ≡ a' → P a → P a' postulate substP : ∀{ℓ}{A : Set ℓ}{ℓ'}(P : A → Prop ℓ'){a a' : A} → a ≡ a' → P a → P a'