From 1d4cda091ee22c46b65a7c445c273d0c1a2df0c1 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Tue, 25 Jul 2023 15:46:40 +0200 Subject: [PATCH] Trying Presheaf model --- FFOLCompleteness.agda | 110 ++++++++++++++++++++++++++++++++++++------ FFOLInitial.agda | 47 ++++++++++++++++-- PropUtil.agda | 8 +-- 3 files changed, 142 insertions(+), 23 deletions(-) diff --git a/FFOLCompleteness.agda b/FFOLCompleteness.agda index e122dff..41defce 100644 --- a/FFOLCompleteness.agda +++ b/FFOLCompleteness.agda @@ -296,6 +296,45 @@ module FFOLCompleteness where ; R[] = refl } + record Presheaf' : Set (lsuc (ℓ¹)) where + field + World : Set ℓ¹ + Arr : World → World → Set ℓ¹ -- arrows + id-a : {w : World} → Arr w w -- id arrow + _∘a_ : {w w' w'' : World} → Arr w w' → Arr w' w'' → Arr w w'' -- arrow composition + ∘a-ass : {w w' w'' w''' : World}{a : Arr w w'}{b : Arr w' w''}{c : Arr w'' w'''} + → ((a ∘a b) ∘a c) ≡ (a ∘a (b ∘a c)) + idl-a : {w w' : World} → {a : Arr w w'} → (id-a {w}) ∘a a ≡ a + idr-a : {w w' : World} → {a : Arr w w'} → a ∘a (id-a {w'}) ≡ a + TM : World → Set ℓ¹ + TM≤ : {w w' : World} → Arr w w' → TM w' → TM w + REL : (w : World) → TM w → TM w → Set ℓ¹ + REL≤ : {w w' : World} → {t u : TM w'} → (eq : Arr w w') → REL w' t u → REL w (TM≤ eq t) (TM≤ eq u) + + {- + -- Now we try to interpret formulæ and contexts + import FFOLInitial as I + _⊩ᶠ_ : World → (I.For I.◇t) → Set ℓ¹ + w ⊩ᶠ I.R t u = REL w {!!} {!!} + w ⊩ᶠ (A I.⇒ B) = ∀ (w' : World) → Arr w w' → w' ⊩ᶠ A → w' ⊩ᶠ B + w ⊩ᶠ I.∀∀ A = ∀ (t : TM w) → {!!} + -} + + + + record Kripke : Set (lsuc (ℓ¹)) where + field + World : Set ℓ¹ + Arr : World → World → Prop ℓ¹ -- arrows + id-a : {w : World} → Arr w w -- id arrow + _∘a_ : {w w' w'' : World} → Arr w w' → Arr w' w'' → Arr w w'' -- arrow composition + -- associativity and id rules are trivial cause arrows are in prop + TM : World → Set ℓ¹ + TM≤ : {w w' : World} → Arr w w' → TM w' → TM w + REL : (w : World) → TM w → TM w → Prop ℓ¹ + REL≤ : {w w' : World} → {t u : TM w'} → (eq : Arr w w') → REL w' t u → REL w (TM≤ eq t) (TM≤ eq u) + + -- Completeness proof -- We first build our universal Kripke model @@ -305,26 +344,67 @@ module FFOLCompleteness where -- We have a model, we construct the Universal Presheaf model of this model import FFOLInitial as I - UniversalPresheaf : Presheaf + UniversalPresheaf : Kripke UniversalPresheaf = record - { World = I.Con - ; Arr = I.Sub - ; id-a = I.id - ; _∘a_ = λ σ σ' → σ' I.∘ σ - ; ∘a-ass = ≡sym I.∘-ass - ; idl-a = I.idr - ; idr-a = I.idl - ; TM = λ Γ → I.Tm (I.Con.t Γ) - ; TM≤ = λ σ t → t I.[ I.Sub.t σ ]t - ; REL = λ Γ t u → I.Pf Γ (I.r t u) - ; REL≤ = λ σ pf → (pf I.[ I.Sub.t σ ]pₜ) I.[ I.Sub.p σ ]p + { World = (Γₜ : I.Cont) → I.Conp Γₜ + ; Arr = λ w₁ w₂ → (Γₜ : I.Cont) → (I.Pf* Γₜ (w₂ Γₜ) (w₁ Γₜ)) + ; id-a = λ {w} Γₜ → I.Pf*-id + ; _∘a_ = λ σ₁ σ₂ Γₜ → I.Pf*-∘ (σ₁ Γₜ) (σ₂ Γₜ) + --; ∘a-ass = λ {w} → ≡fun' (λ Γₜ → ≡sym (I.∘ₚ-ass {Γₚ = w Γₜ})) + --; idl-a = λ {w} {w'} → ≡fun' (λ Γₜ → I.idrₚ {Γₚ = w Γₜ} {Δₚ = w' Γₜ}) + --; idr-a = λ {w} {w'} → ≡fun' (λ Γₜ → I.idlₚ {Γₚ = w Γₜ} {Δₚ = w' Γₜ}) + ; TM = λ w → (Γₜ : I.Cont) → (I.Tm Γₜ) + ; TM≤ = λ σ t → t + ; REL = λ w t u → (Γₜ : I.Cont) → I.Pf Γₜ (w Γₜ) (I.R (t Γₜ) (u Γₜ)) + ; REL≤ = λ σ pf → λ Γₜ → I.Pf*Pf {!!} (pf Γₜ) } -- I.xx are from initial, xx are from up - open Presheaf UniversalPresheaf + open Kripke UniversalPresheaf + + -- We now create the forcing relation for our Universal presheaf + -- We need the world to depend of a term context (i guess), so i think i cannot make it so + -- the forcing relation works for every Kripke Model. + _⊩f_ : (w : World) → {Γₜ : I.Cont} → I.For Γₜ → Prop₁ + _⊩f_ w {Γₜ} (I.R t v) = I.Pf Γₜ (w Γₜ) (I.R t v) + w ⊩f (A I.⇒ B) = ∀ w' → Arr w w' → w' ⊩f A → w' ⊩f B + w ⊩f I.∀∀ A = w ⊩f A + + ⊩f-mon : {w w' : World} → Arr w w' → {Γₜ : I.Cont} → {A : I.For Γₜ} → w ⊩f A → w' ⊩f A + ⊩f-mon s {Γₜ} {I.R t v} wh = I.Pf*Pf (s Γₜ) wh + ⊩f-mon s {A = A I.⇒ B} wh w'' s' w''h = wh w'' (s ∘a s' ) w''h + ⊩f-mon s {A = I.∀∀ A} wh = ⊩f-mon s {A = A} wh + + ⊩fPf : {Γₜ : I.Cont}{w : World}{A : I.For Γₜ} → w ⊩f A → I.Pf Γₜ (w Γₜ) A + ⊩fPf {A = I.R t v} pf = pf + ⊩fPf {A = A I.⇒ A₁} pf = {!I.app!} + ⊩fPf {A = I.∀∀ A} pf = I.p∀∀i (substP (λ X → I.Pf _ X A) {!!} (⊩fPf pf)) + + + _⊩c_ : (w : World) → {Γₜ : I.Cont} → I.Conp Γₜ → Prop₁ + w ⊩c I.◇p = ⊤ + w ⊩c (Γₚ I.▹p⁰ A) = (w ⊩c Γₚ) ∧ (w ⊩f A) + + ⊩c-mon : {w w' : World} → Arr w w' → {Γₜ : I.Cont} → {Γₚ : I.Conp Γₜ} → w ⊩c Γₚ → w' ⊩c Γₚ + ⊩c-mon s {Γₚ = I.◇p} wh = tt + ⊩c-mon s {Γₜ} {Γₚ = Γₚ I.▹p⁰ A} wh = ⟨ (⊩c-mon s (proj₁ wh)) , ⊩f-mon s {Γₜ} {A} (proj₂ wh) ⟩ + + ⊩cPf* : {Γₜ : I.Cont}{w : World}{Γₚ : I.Conp Γₜ} → w ⊩c Γₚ → I.Pf* Γₜ (w Γₜ) Γₚ + ⊩cPf* {Γₚ = I.◇p} h = tt + ⊩cPf* {Γₚ = Γₚ I.▹p⁰ x} h = ⟨ (⊩cPf* (proj₁ h)) , {!proj₂ h!} ⟩ + + _⊫_ : {Γₜ : I.Cont} → (I.Conp Γₜ) → I.For Γₜ → Prop₁ + Γₚ ⊫ A = ∀ w → w ⊩c Γₚ → w ⊩f A -- Now we want to show universality of this model, that is -- if you have a proof in UP, you have the same in I. + + u : {Γₜ : I.Cont}{Γₚ : I.Conp Γₜ}{A : I.For Γₜ} → I.Pf Γₜ Γₚ A → Γₚ ⊫ A + q : {Γₜ : I.Cont}{Γₚ : I.Conp Γₜ}{A : I.For Γₜ} → Γₚ ⊫ A → I.Pf Γₜ Γₚ A - q : {Γ : Con}{A : For Γ} → Γ ⊢ A → I.Pf {!!} {!!} - u : {Γ : Con}{A : For Γ} → I.Pf {!!} {!!} → Γ ⊢ A + u {A = I.R t s} pf w wh = {!!} + u {A = A I.⇒ B} pf w wh w' s w'h = u {A = B} (I.app pf (q λ w'' w''h → {!!})) w' (⊩c-mon s wh) + u {A = I.∀∀ A} pf w wh = {!!} + q {A = I.R t s} h = {!!} + q {A = A I.⇒ B} h = {!!} + q {A = I.∀∀ A} h = {!!} diff --git a/FFOLInitial.agda b/FFOLInitial.agda index 64aa127..b14a44b 100644 --- a/FFOLInitial.agda +++ b/FFOLInitial.agda @@ -200,7 +200,7 @@ module FFOLInitial where -- With those contexts, we have everything to define proofs - data PfVar : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Set₁ where + data PfVar : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁ where pvzero : {A : For Γₜ} → PfVar Γₜ (Γₚ ▹p⁰ A) A pvnext : {A B : For Γₜ} → PfVar Γₜ Γₚ A → PfVar Γₜ (Γₚ ▹p⁰ B) A @@ -389,9 +389,6 @@ module FFOLInitial where {f = λ {W} ξ pf → _,ₚ_ ξ pf}{x = σₚ [ α ∘ₜ β ]σₚ}{y = pf [ α ∘ₜ β ]pₜ}) )) - - - -- How ∘ₚ and ∘ₜ interact to make associativity (to be proven later for Sub) ∘ₚₜ-ass⁰ : @@ -645,3 +642,45 @@ module FFOLInitial where ; ∀e = λ {Γ} {F} pf {t} → p∀∀e pf } + + -- We define normal and neutral forms + data Ne : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁ + data Nf : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁ + data Ne where + var : {A : For Γₜ} → PfVar Γₜ Γₚ A → Ne Γₜ Γₚ A + app : {A B : For Γₜ} → Ne Γₜ Γₚ (A ⇒ B) → Nf Γₜ Γₚ A → Ne Γₜ Γₚ B + p∀∀e : {A : For (Γₜ ▹t⁰)} → {t : Tm Γₜ} → Ne Γₜ Γₚ (∀∀ A) → Ne Γₜ Γₚ (A [ idₜ ,ₜ t ]f) + data Nf where + R : {t u : Tm Γₜ} → Ne Γₜ Γₚ (R t u) → Nf Γₜ Γₚ (R t u) + lam : {A B : For Γₜ} → Nf Γₜ (Γₚ ▹p⁰ A) B → Nf Γₜ Γₚ (A ⇒ B) + p∀∀i : {A : For (Γₜ ▹t⁰)} → Nf (Γₜ ▹t⁰) (Γₚ ▹tp) A → Nf Γₜ Γₚ (∀∀ A) + + + Pf* : (Γₜ : Cont) → Conp Γₜ → Conp Γₜ → Prop₁ + Pf* Γₜ Γₚ ◇p = ⊤ + Pf* Γₜ Γₚ (Γₚ' ▹p⁰ A) = (Pf* Γₜ Γₚ Γₚ') ∧ (Pf Γₜ Γₚ A) + + Sub→Pf* : {Γₜ : Cont} {Γₚ Γₚ' : Conp Γₜ} → Subp {Γₜ} Γₚ Γₚ' → Pf* Γₜ Γₚ Γₚ' + Sub→Pf* εₚ = tt + Sub→Pf* (σₚ ,ₚ pf) = ⟨ (Sub→Pf* σₚ) , pf ⟩ + Pf*-id : {Γₜ : Cont} {Γₚ : Conp Γₜ} → Pf* Γₜ Γₚ Γₚ + Pf*-id = Sub→Pf* idₚ + + Pf*▹p : {Γₜ : Cont}{Γₚ Γₚ' : Conp Γₜ}{A : For Γₜ} → Pf* Γₜ Γₚ Γₚ' → Pf* Γₜ (Γₚ ▹p⁰ A) Γₚ' + Pf*▹p {Γₚ' = ◇p} s = tt + Pf*▹p {Γₚ' = Γₚ' ▹p⁰ x} s = ⟨ (Pf*▹p (proj₁ s)) , (wkᵣp (rightRen reflRen) (proj₂ s)) ⟩ + Pf*▹tp : {Γₜ : Cont}{Γₚ Γₚ' : Conp Γₜ} → Pf* Γₜ Γₚ Γₚ' → Pf* (Γₜ ▹t⁰) (Γₚ ▹tp) (Γₚ' ▹tp) + Pf*▹tp {Γₚ' = ◇p} s = tt + Pf*▹tp {Γₚ' = Γₚ' ▹p⁰ A} s = ⟨ Pf*▹tp (proj₁ s) , (proj₂ s) [ wkₜσₜ idₜ ]pₜ ⟩ + + Pf*Pf : {Γₜ : Cont} {Γₚ Γₚ' : Conp Γₜ} {A : For Γₜ} → Pf* Γₜ Γₚ Γₚ' → Pf Γₜ Γₚ' A → Pf Γₜ Γₚ A + Pf*Pf s (var pvzero) = proj₂ s + Pf*Pf s (var (pvnext pv)) = Pf*Pf (proj₁ s) (var pv) + Pf*Pf s (app p p') = app (Pf*Pf s p) (Pf*Pf s p') + Pf*Pf s (lam p) = lam (Pf*Pf (⟨ (Pf*▹p s) , (var pvzero) ⟩) p) + Pf*Pf s (p∀∀e p) = p∀∀e (Pf*Pf s p) + Pf*Pf s (p∀∀i p) = p∀∀i (Pf*Pf (Pf*▹tp s) p) + + Pf*-∘ : {Γₜ : Cont} {Γₚ Δₚ Ξₚ : Conp Γₜ} → Pf* Γₜ Δₚ Ξₚ → Pf* Γₜ Γₚ Δₚ → Pf* Γₜ Γₚ Ξₚ + Pf*-∘ {Ξₚ = ◇p} α β = tt + Pf*-∘ {Ξₚ = Ξₚ ▹p⁰ A} α β = ⟨ Pf*-∘ (proj₁ α) β , Pf*Pf β (proj₂ α) ⟩ diff --git a/PropUtil.agda b/PropUtil.agda index 4f4268c..4d46499 100644 --- a/PropUtil.agda +++ b/PropUtil.agda @@ -13,7 +13,7 @@ module PropUtil where -- ⊥ is a data with no constructor -- ⊤ is a record with one always-available constructor data ⊥ : Prop where - record ⊤ : Prop where + record ⊤ : Prop ℓ where constructor tt @@ -21,7 +21,7 @@ module PropUtil where inj₁ : {P Q : Prop} → P → P ∨ Q inj₂ : {P Q : Prop} → Q → P ∨ Q - record _∧_ (P Q : Prop) : Prop where + record _∧_ (P Q : Prop ℓ) : Prop ℓ where constructor ⟨_,_⟩ field p : P @@ -31,9 +31,9 @@ module PropUtil where infixr 11 _∨_ -- ∧ elimination - proj₁ : {P Q : Prop} → P ∧ Q → P + proj₁ : {P Q : Prop ℓ} → P ∧ Q → P proj₁ pq = _∧_.p pq - proj₂ : {P Q : Prop} → P ∧ Q → Q + proj₂ : {P Q : Prop ℓ} → P ∧ Q → Q proj₂ pq = _∧_.q pq -- ∨ elimination