Separated Syntax in another file to make Agda faster
Added some proof examples that works for the Tarski model Rewrite (again) of the syntax, still not working
This commit is contained in:
parent
ab7e77e833
commit
21bdad22a9
GPG Key ID:
7054D5D6A90F084F
285
FFOLInitial.agda
Normal file
285
FFOLInitial.agda
Normal file
@ -0,0 +1,285 @@
|
||||
{-# OPTIONS --prop #-}
|
||||
|
||||
open import PropUtil
|
||||
|
||||
module FFOLInitial (F : Nat → Set) (R : Nat → Set) where
|
||||
|
||||
open import FinitaryFirstOrderLogic F R
|
||||
open import Agda.Primitive
|
||||
open import ListUtil
|
||||
|
||||
variable
|
||||
n : Nat
|
||||
|
||||
-- First definition of terms and term contexts --
|
||||
data Cont : Set₁ where
|
||||
◇t : Cont
|
||||
_▹t⁰ : Cont → Cont
|
||||
variable
|
||||
Γₜ Δₜ Ξₜ : Cont
|
||||
data TmVar : Cont → Set₁ where
|
||||
tvzero : TmVar (Γₜ ▹t⁰)
|
||||
tvnext : TmVar Γₜ → TmVar (Γₜ ▹t⁰)
|
||||
|
||||
data Tm : Cont → Set₁ where
|
||||
var : TmVar Γₜ → Tm Γₜ
|
||||
fun : F n → Array (Tm Γₜ) n → Tm Γₜ
|
||||
|
||||
-- Now we can define formulæ
|
||||
data For : Cont → Set₁ where
|
||||
rel : R n → Array (Tm Γₜ) n → For Γₜ
|
||||
_⇒_ : For Γₜ → For Γₜ → For Γₜ
|
||||
∀∀ : For (Γₜ ▹t⁰) → For Γₜ
|
||||
|
||||
-- Then we define term substitutions, and the application of them on terms and formulæ
|
||||
data Subt : Cont → Cont → Set₁ where
|
||||
εₜ : Subt Γₜ ◇t
|
||||
wk▹t : Subt Δₜ Γₜ → Tm Δₜ → Subt Δₜ (Γₜ ▹t⁰)
|
||||
|
||||
-- We subst on terms
|
||||
_[_]t : Tm Γₜ → Subt Δₜ Γₜ → Tm Δₜ
|
||||
_[_]tz : Array (Tm Γₜ) n → Subt Δₜ Γₜ → Array (Tm Δₜ) n
|
||||
var tvzero [ wk▹t σ t ]t = t
|
||||
var (tvnext tv) [ wk▹t σ t ]t = var tv [ σ ]t
|
||||
fun f tz [ σ ]t = fun f (tz [ σ ]tz)
|
||||
zero [ σ ]tz = zero
|
||||
next t tz [ σ ]tz = next (t [ σ ]t) (tz [ σ ]tz)
|
||||
|
||||
-- We define liftings on term variables
|
||||
-- A term of n variables is a term of n+1 variables
|
||||
liftt : Tm Γₜ → Tm (Γₜ ▹t⁰)
|
||||
-- Same for a term array
|
||||
lifttz : Array (Tm Γₜ) n → Array (Tm (Γₜ ▹t⁰)) n
|
||||
liftt (var tv) = var (tvnext tv)
|
||||
liftt (fun f tz) = fun f (lifttz tz)
|
||||
lifttz zero = zero
|
||||
lifttz (next t tz) = next (liftt t) (lifttz tz)
|
||||
-- From a substitution into n variables, we construct a substitution from n+1 variables to n+1 variables which maps it to itself
|
||||
-- i.e. 0 -> 0 and for all i ->(old) σ(i) we get i+1 -> σ(i)+1
|
||||
lift : Subt Δₜ Γₜ → Subt (Δₜ ▹t⁰) (Γₜ ▹t⁰)
|
||||
lift εₜ = wk▹t εₜ (var tvzero)
|
||||
lift (wk▹t σ t) = wk▹t (lift σ) (liftt t)
|
||||
-- From a substition into n variables, we get a substitution into n+1 variables which don't use the last one
|
||||
llift : Subt Δₜ Γₜ → Subt (Δₜ ▹t⁰) Γₜ
|
||||
llift εₜ = εₜ
|
||||
llift (wk▹t σ t) = wk▹t (llift σ) (liftt t)
|
||||
|
||||
-- We subst on formulæ
|
||||
_[_]f : For Γₜ → Subt Δₜ Γₜ → For Δₜ
|
||||
(rel r tz) [ σ ]f = rel r ((map (λ t → t [ σ ]t) tz))
|
||||
(A ⇒ B) [ σ ]f = (A [ σ ]f) ⇒ (B [ σ ]f)
|
||||
(∀∀ A) [ σ ]f = ∀∀ (A [ lift σ ]f)
|
||||
|
||||
-- We now can define identity on term substitutions
|
||||
idₜ : Subt Γₜ Γₜ
|
||||
idₜ {◇t} = εₜ
|
||||
idₜ {Γₜ ▹t⁰} = lift idₜ
|
||||
|
||||
_∘ₜ_ : Subt Δₜ Γₜ → Subt Ξₜ Δₜ → Subt Ξₜ Γₜ
|
||||
εₜ ∘ₜ β = εₜ
|
||||
wk▹t α x ∘ₜ β = wk▹t (α ∘ₜ β) (x [ β ]t)
|
||||
|
||||
-- We have the access functions from the algebra, in restricted versions
|
||||
πₜ¹ : Subt Δₜ (Γₜ ▹t⁰) → Subt Δₜ Γₜ
|
||||
πₜ¹ (wk▹t σₜ t) = σₜ
|
||||
πₜ² : Subt Δₜ (Γₜ ▹t⁰) → Tm Δₜ
|
||||
πₜ² (wk▹t σₜ t) = t
|
||||
_,ₜ_ : Subt Δₜ Γₜ → Tm Δₜ → Subt Δₜ (Γₜ ▹t⁰)
|
||||
σₜ ,ₜ t = wk▹t σₜ t
|
||||
|
||||
-- And their equalities (the fact that there are reciprocical)
|
||||
πₜ²∘,ₜ : {σₜ : Subt Δₜ Γₜ} → {t : Tm Δₜ} → πₜ² (σₜ ,ₜ t) ≡ t
|
||||
πₜ²∘,ₜ = refl
|
||||
πₜ¹∘,ₜ : {σₜ : Subt Δₜ Γₜ} → {t : Tm Δₜ} → πₜ¹ (σₜ ,ₜ t) ≡ σₜ
|
||||
πₜ¹∘,ₜ = refl
|
||||
,ₜ∘πₜ : {σₜ : Subt Δₜ (Γₜ ▹t⁰)} → (πₜ¹ σₜ) ,ₜ (πₜ² σₜ) ≡ σₜ
|
||||
,ₜ∘πₜ {σₜ = wk▹t σₜ t} = refl
|
||||
|
||||
-- We can also prove the substitution equalities
|
||||
lem1 : lift (idₜ {Γₜ}) ≡ wk▹t {!!} {!!}
|
||||
[]t-id : {t : Tm Γₜ} → t [ idₜ {Γₜ} ]t ≡ t
|
||||
[]tz-id : {tz : Array (Tm Γₜ) n} → tz [ idₜ {Γₜ} ]tz ≡ tz
|
||||
[]t-id {◇t ▹t⁰} {var tvzero} = refl
|
||||
[]t-id {(Γₜ ▹t⁰) ▹t⁰} {var tv} = {!!}
|
||||
[]t-id {Γₜ} {fun f tz} = substP (λ tz' → fun f tz' ≡ fun f tz) (≡sym []tz-id) refl
|
||||
[]tz-id {tz = zero} = refl
|
||||
[]tz-id {tz = next x tz} = substP (λ tz' → (next (x [ idₜ ]t) tz') ≡ next x tz) (≡sym []tz-id) (substP (λ x' → next x' tz ≡ next x tz) (≡sym []t-id) refl)
|
||||
[]t-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → {t : Tm Γₜ} → t [ β ∘ₜ α ]t ≡ (t [ β ]t) [ α ]t
|
||||
[]t-∘ {α = α} {β = β} {t = t} = {!!}
|
||||
fun[] : {σ : Subt Δₜ Γₜ} → {f : F n} → {tz : Array (Tm Γₜ) n} → (fun f tz) [ σ ]t ≡ fun f (map (λ t → t [ σ ]t) tz)
|
||||
[]f-id : {F : For Γₜ} → F [ idₜ {Γₜ} ]f ≡ F
|
||||
[]f-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → {F : For Γₜ} → F [ β ∘ₜ α ]f ≡ (F [ β ]f) [ α ]f
|
||||
rel[] : {σ : Subt Δₜ Γₜ} → {r : R n} → {tz : Array (Tm Γₜ) n} → (rel r tz) [ σ ]f ≡ rel r (map (λ t → t [ σ ]t) tz)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
data Conp : Cont → Set₁ -- pu tit in Prop
|
||||
variable
|
||||
Γₚ : Conp Γₜ
|
||||
Δₚ : Conp Δₜ
|
||||
Ξₚ : Conp Ξₜ
|
||||
|
||||
data Conp where
|
||||
◇p : Conp Γₜ
|
||||
_▹p⁰_ : Conp Γₜ → For Γₜ → Conp Γₜ
|
||||
record Con : Set₁ where
|
||||
constructor con
|
||||
field
|
||||
t : Cont
|
||||
p : Conp t
|
||||
|
||||
◇ : Con
|
||||
◇ = con ◇t ◇p
|
||||
|
||||
|
||||
_▹p_ : (Γ : Con) → For (Con.t Γ) → Con
|
||||
Γ ▹p A = con (Con.t Γ) (Con.p Γ ▹p⁰ A)
|
||||
|
||||
variable
|
||||
Γ Δ Ξ : Con
|
||||
|
||||
|
||||
|
||||
-- We can add term, that will not be used in the formulæ already present
|
||||
-- (that's why we use llift)
|
||||
_▹tp : Conp Γₜ → Conp (Γₜ ▹t⁰)
|
||||
◇p ▹tp = ◇p
|
||||
(Γₚ ▹p⁰ A) ▹tp = (Γₚ ▹tp) ▹p⁰ (A [ llift idₜ ]f)
|
||||
|
||||
_▹t : Con → Con
|
||||
Γ ▹t = con ((Con.t Γ) ▹t⁰) (Con.p Γ ▹tp)
|
||||
|
||||
data PfVar : (Γ : Con) → For (Con.t Γ) → Set₁ where
|
||||
pvzero : {A : For (Con.t Γ)} → PfVar (Γ ▹p A) A
|
||||
pvnext : {A B : For (Con.t Γ)} → PfVar Γ A → PfVar (Γ ▹p B) A
|
||||
|
||||
data Pf : (Γ : Con) → For (Con.t Γ) → Prop₁ where
|
||||
var : {A : For (Con.t Γ)} → PfVar Γ A → Pf Γ A
|
||||
app : {A B : For (Con.t Γ)} → Pf Γ (A ⇒ B) → Pf Γ A → Pf Γ B
|
||||
lam : {A B : For (Con.t Γ)} → Pf (Γ ▹p A) B → Pf Γ (A ⇒ B)
|
||||
|
||||
--p∀∀e : {A : For Γ} → Pf Γ (∀∀ A) → Pf Γ (A [ t , id ])
|
||||
--p∀∀i : {A : For (Γ ▹t)} → Pf (Γ [?]) A → Pf Γ (∀∀ A)
|
||||
data Sub : Con → Con → Set₁
|
||||
subt : Sub Δ Γ → Subt (Con.t Δ) (Con.t Γ)
|
||||
data Sub where
|
||||
εₚ : Subt (Con.t Δ) Γₜ → Sub Δ (con Γₜ ◇p) -- Γₜ → Δₜ ≡≡> (Γₜ,◇p) → (Δₜ,Δₚ)
|
||||
-- If i tell you by what you should replace a missing proof of A, then you can
|
||||
-- prove anything that uses a proof of A
|
||||
wk▹p : {A : For (Con.t Γ)} → (σ : Sub Δ Γ) → Pf Δ (A [ subt σ ]f) → Sub Δ (Γ ▹p A)
|
||||
subt (εₚ σₜ) = σₜ
|
||||
subt (wk▹p σ pf) = subt σ
|
||||
|
||||
-- lifts
|
||||
--liftpt : Pf Δ (A [ subt σ ]f) → Pf Δ ((A [ llift idₜ ]f) [ subt (σ ,ₜ t) ]f)
|
||||
{-
|
||||
-- The functions made for accessing the terms of Sub, needed for the algebra
|
||||
πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹t) → Sub Δ Γ
|
||||
πₜ¹ σ = {!!}
|
||||
πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹t) → Tm (Con.t Δ)
|
||||
πₜ² σ = {!!}
|
||||
_,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm (Con.t Δ) → Sub Δ (Γ ▹t)
|
||||
llift∘,ₜ : {σ : Sub Δ Γ} → {A : For (Con.t Γ)} → {t : Tm (Con.t Δ)} → (A [ llift idₜ ]f) [ subt (σ ,ₜ t) ]f ≡ A [ subt σ ]f
|
||||
llift∘,ₜ {A = rel x x₁} = {!!}
|
||||
llift∘,ₜ {A = A ⇒ A₁} = {!!}
|
||||
llift∘,ₜ {A = ∀∀ A} = {!substrefl!}
|
||||
(εₚ σₜ) ,ₜ t = εₚ (wk▹t σₜ t)
|
||||
_,ₜ_ {Γ = ΓpA} {Δ = Δ} (wk▹p σ pf) t = wk▹p (σ ,ₜ t) (substP (λ a → Pf Δ a) llift∘,ₜ {!pf!})
|
||||
πₚ¹ : {A : Con.t Γ} → Sub Δ (Γ ▹p A) → Sub Δ Γ
|
||||
πₚ¹ Γₚ (wk▹p Γₚ' σ pf) = σ
|
||||
πₚ² : {A : Con.t Γ} → (σ : Sub Δ (Γ ▹p A)) → Pf Δ (A [ subt (πₚ¹ (Con.p Γ) σ) ]f)
|
||||
πₚ² Γₚ (wk▹p Γₚ' σ pf) = pf
|
||||
_,ₚ_ : {A : Con.t Γ} → (σ : Sub Δ Γ) → Pf Δ (A [ subt σ ]f) → Sub Δ (Γ ▹p A)
|
||||
_,ₚ_ = wk▹p
|
||||
-}
|
||||
|
||||
|
||||
{-
|
||||
-- We subst on proofs
|
||||
_,ₚ_ : {F : For (Con.t Γ)} → (σ : Sub Δ Γ) → Pf Δ (F [ subt σ ]f) → Sub Δ (Γ ▹p F)
|
||||
_,ₚ_ {Γ} σ pf = wk▹p (Con.p Γ) σ pf
|
||||
sub▹p : (σ : Sub (con Δₜ Δₚ) (con Γₜ Γₚ)) → Sub (con Δₜ (Δₚ ▹p⁰ (A [ subt σ ]f))) (con Γₜ (Γₚ ▹p⁰ A))
|
||||
p[] : Pf Γ A → (σ : Sub Δ Γ) → Pf Δ (A [ subt σ ]f)
|
||||
sub▹p Γₚ (εₚ σₜ) = wk▹p Γₚ (εₚ σₜ) (var pvzero)
|
||||
sub▹p Γₚ (wk▹p p σ pf) = {!!}
|
||||
test : (σ : Sub Δ Γ) → Sub (Δ ▹p (A [ subt σ ]f)) (Γ ▹p A)
|
||||
p[] Γₚ (var pvzero) (wk▹p p σ pf) = pf
|
||||
p[] Γₚ (var (pvnext pv)) (wk▹p p σ pf) = p[] Γₚ (var pv) σ
|
||||
p[] Γₚ (app pf pf') σ = app (p[] Γₚ pf σ) (p[] Γₚ pf' σ)
|
||||
p[] Γₚ (lam pf) σ = lam (p[] {!\!} {!!} (sub▹p {!!} {!σ!}))
|
||||
-}
|
||||
|
||||
{-
|
||||
idₚ : Subp Γₚ Γₚ
|
||||
idₚ {Γₚ = ◇p} = εₚ
|
||||
idₚ {Γₚ = Γₚ ▹p⁰ A} = wk▹p Γₚ (liftₚ Γₚ idₚ) (var pvzero)
|
||||
|
||||
ε : Sub Γ ◇
|
||||
ε = sub εₜ εₚ
|
||||
|
||||
id : Sub Γ Γ
|
||||
id = sub idₜ idₚ
|
||||
|
||||
_∘ₜ_ : Subt Δₜ Ξₜ → Subt Γₜ Δₜ → Subt Γₜ Ξₜ
|
||||
εₜ ∘ₜ εₜ = εₜ
|
||||
εₜ ∘ₜ wk▹t β x = εₜ
|
||||
(wk▹t α t) ∘ₜ β = wk▹t (α ∘ₜ β) (t [ β ]t)
|
||||
|
||||
_∘ₚ_ : Subp Δₚ Ξₚ → Subp Γₚ Δₚ → Subp Γₚ Ξₚ
|
||||
εₚ ∘ₚ βₚ = εₚ
|
||||
wk▹p p αₚ x ∘ₚ βₚ = {!wk▹p ? ? ?!}
|
||||
|
||||
_∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
|
||||
sub αₜ αₚ ∘ (sub βₜ βₚ) = sub (αₜ ∘ₜ βₜ) {!!}
|
||||
-}
|
||||
|
||||
imod : FFOL {lsuc lzero} {lsuc lzero} {lsuc lzero} {lsuc lzero} F R
|
||||
imod = record
|
||||
{ Con = Con
|
||||
; Sub = Sub
|
||||
; _∘_ = {!!}
|
||||
; id = {!!}
|
||||
; ◇ = ◇
|
||||
; ε = {!!}
|
||||
; Tm = λ Γ → Tm (Con.t Γ)
|
||||
; _[_]t = λ t σ → t [ subt σ ]t
|
||||
; []t-id = {!!}
|
||||
; []t-∘ = {!!}
|
||||
; fun = fun
|
||||
; fun[] = {!!}
|
||||
; _▹ₜ = _▹t
|
||||
; πₜ¹ = {!!}
|
||||
; πₜ² = {!!}
|
||||
; _,ₜ_ = {!!}
|
||||
; πₜ²∘,ₜ = {!!}
|
||||
; πₜ¹∘,ₜ = {!!}
|
||||
; ,ₜ∘πₜ = {!!}
|
||||
; For = λ Γ → For (Con.t Γ)
|
||||
; _[_]f = λ A σ → A [ subt σ ]f
|
||||
; []f-id = {!!}
|
||||
; []f-∘ = {!!}
|
||||
; rel = rel
|
||||
; rel[] = {!!}
|
||||
; _⊢_ = λ Γ A → Pf Γ A
|
||||
; _▹ₚ_ = _▹p_
|
||||
; πₚ¹ = {!!}
|
||||
; πₚ² = {!!}
|
||||
; _,ₚ_ = {!!}
|
||||
; ,ₚ∘πₚ = {!!}
|
||||
; πₚ¹∘,ₚ = {!!}
|
||||
; _⇒_ = _⇒_
|
||||
; []f-⇒ = {!!}
|
||||
; ∀∀ = ∀∀
|
||||
; []f-∀∀ = {!!}
|
||||
; lam = {!!}
|
||||
; app = app
|
||||
; ∀i = {!!}
|
||||
; ∀e = {!!}
|
||||
}
|
||||
|
||||
@ -84,151 +84,6 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
|
||||
∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
|
||||
∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
|
||||
|
||||
module Initial where
|
||||
|
||||
data Con : Set₁
|
||||
data For : Con → Set₁
|
||||
data Con where -- isom integer ≡ number of terms in the context
|
||||
◇ : Con
|
||||
_▹t : Con → Con
|
||||
_▹p_ : (Γ : Con) → For Γ → Con
|
||||
|
||||
variable
|
||||
Γ Δ Ξ : Con
|
||||
n : Nat
|
||||
A : For Γ
|
||||
|
||||
data TmVar : Con → Set₁ where
|
||||
tvzero : TmVar (Γ ▹t)
|
||||
tvnext : TmVar Γ → TmVar (Γ ▹t)
|
||||
tvdisc : TmVar Γ → TmVar (Γ ▹p A)
|
||||
|
||||
data Tm : Con → Set₁ where
|
||||
var : TmVar Γ → Tm Γ
|
||||
fun : F n → Array (Tm Γ) n → Tm Γ
|
||||
|
||||
data For where
|
||||
rel : R n → Array (Tm Γ) n → For Γ
|
||||
_⇒_ : For Γ → For Γ → For Γ
|
||||
∀∀ : For (Γ ▹t) → For Γ
|
||||
|
||||
data PfVar : Con → For Γ → Set₁ where
|
||||
pvzero : {A : For Γ} → PfVar (Γ ▹p A) A
|
||||
pvnext : {A : For Δ} → {B : For Γ} → PfVar Γ A → PfVar (Γ ▹p B) A
|
||||
pvdisc : {A : For Δ} → PfVar Γ A → PfVar (Γ ▹t) A
|
||||
|
||||
data Pf : Con → For Γ → Prop₁ where
|
||||
var : {A : For Δ} → PfVar Γ A → Pf Γ A
|
||||
app : {A B : For Δ} → Pf Γ (A ⇒ B) → Pf Γ A → Pf Γ B
|
||||
lam : {A B : For Γ} → Pf (Γ ▹p A) B → Pf Γ (A ⇒ B)
|
||||
--p∀∀e : {A : For Γ} → Pf Γ (∀∀ A) → Pf Γ (A [ t , id ])
|
||||
--p∀∀i : {A : For (Γ ▹t)} → Pf (Γ [?]) A → Pf Γ (∀∀ A)
|
||||
|
||||
data Sub : Con → Con → Set₁ where -- TODO replace with prop
|
||||
ε : Sub Γ ◇
|
||||
wk▹t : Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹t)
|
||||
wk▹p : Sub Δ Γ → Pf Δ A → Sub Δ (Γ ▹p A)
|
||||
|
||||
-- We subst on terms
|
||||
_[_]t : Tm Γ → Sub Δ Γ → Tm Δ
|
||||
_[_]tz : Array (Tm Γ) n → Sub Δ Γ → Array (Tm Δ) n
|
||||
|
||||
var tvzero [ wk▹t σ t ]t = t
|
||||
var (tvnext tv) [ wk▹t σ x ]t = var tv [ σ ]t
|
||||
var (tvdisc tv) [ wk▹p σ x ]t = var tv [ σ ]t
|
||||
fun f tz [ σ ]t = fun f (tz [ σ ]tz)
|
||||
zero [ σ ]tz = zero
|
||||
next t tz [ σ ]tz = next (t [ σ ]t) (tz [ σ ]tz)
|
||||
|
||||
-- We subst on proofs
|
||||
_[_]p : Pf Γ A → Sub Δ Γ → Pf Δ A
|
||||
_[_]p = {!!}
|
||||
|
||||
-- We subst on formulæ
|
||||
_[_]f : For Γ → Sub Δ Γ → For Δ
|
||||
_[_]f = {!!}
|
||||
|
||||
|
||||
_∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
|
||||
ε ∘ β = ε
|
||||
wk▹t α t ∘ β = wk▹t (α ∘ β) (t [ β ]t)
|
||||
wk▹p α pf ∘ β = wk▹p (α ∘ β) (pf [ β ]p)
|
||||
|
||||
pgcd : Con → Con → Con
|
||||
pgcd ◇ Δ = ◇
|
||||
pgcd (Γ ▹t) ◇ = ◇
|
||||
pgcd (Γ ▹t) (Δ ▹t) = pgcd Γ Δ
|
||||
pgcd (Γ ▹t) (Δ ▹p x) = pgcd Γ Δ
|
||||
pgcd (Γ ▹p x) ◇ = ◇
|
||||
pgcd (Γ ▹p x) (Δ ▹t) = pgcd Γ Δ
|
||||
pgcd (Γ ▹p x) (Δ ▹p x₁) = pgcd Γ Δ
|
||||
|
||||
|
||||
len : Con → Nat
|
||||
len ◇ = 0
|
||||
len (Γ ▹t) = succ (len Γ)
|
||||
len (Γ ▹p A) = succ (len Γ)
|
||||
|
||||
lift▹tPf : Pf Γ A → Pf (Γ ▹t) A
|
||||
lift▹tPf (var x) = var (pvdisc x)
|
||||
lift▹tPf (app p p₁) = app (lift▹tPf p) (lift▹tPf p₁)
|
||||
lift▹tPf (lam p) = {!!}
|
||||
lift▹t : Sub Γ Δ → Sub (Γ ▹t) Δ
|
||||
lift▹t ε = ε
|
||||
lift▹t (wk▹t σ t) = wk▹t (lift▹t σ) (var tvzero)
|
||||
lift▹t (wk▹p {A = A} σ x) = wk▹p (lift▹t σ) (var (pvdisc {!x!}))
|
||||
|
||||
id : Sub Γ Γ
|
||||
id {◇} = ε
|
||||
id {Γ ▹t} = wk▹t {!!} (var tvzero)
|
||||
id {◇ ▹p A} = wk▹p ε (var pvzero)
|
||||
id {(Γ ▹t) ▹p A} = wk▹p (wk▹t {!!} (var (tvdisc tvzero))) (var pvzero)
|
||||
id {(Γ ▹p x) ▹p A} = wk▹p {!!} (var pvzero)
|
||||
|
||||
|
||||
imod : FFOL {lsuc lzero} {lsuc lzero} {lsuc lzero} {lsuc lzero} F R
|
||||
imod = record
|
||||
{ Con = Con
|
||||
; Sub = Sub
|
||||
; _∘_ = _∘_
|
||||
; id = id
|
||||
; ◇ = ◇
|
||||
; ε = ε
|
||||
; Tm = Tm
|
||||
; _[_]t = _[_]t
|
||||
; []t-id = {!!}
|
||||
; []t-∘ = {!!}
|
||||
; fun = fun
|
||||
; fun[] = {!!}
|
||||
; _▹ₜ = _▹t
|
||||
; πₜ¹ = {!!}
|
||||
; πₜ² = {!!}
|
||||
; _,ₜ_ = {!!}
|
||||
; πₜ²∘,ₜ = {!!}
|
||||
; πₜ¹∘,ₜ = {!!}
|
||||
; ,ₜ∘πₜ = {!!}
|
||||
; For = For
|
||||
; _[_]f = {!!}
|
||||
; []f-id = {!!}
|
||||
; []f-∘ = {!!}
|
||||
; rel = rel
|
||||
; rel[] = {!!}
|
||||
; _⊢_ = λ (Γ : Con) (A : For Γ) → Pf Γ A
|
||||
; _▹ₚ_ = _▹p_
|
||||
; πₚ¹ = {!!}
|
||||
; πₚ² = {!!}
|
||||
; _,ₚ_ = {!!}
|
||||
; ,ₚ∘πₚ = {!!}
|
||||
; πₚ¹∘,ₚ = {!!}
|
||||
; _⇒_ = _⇒_
|
||||
; []f-⇒ = {!!}
|
||||
; ∀∀ = ∀∀
|
||||
; []f-∀∀ = {!!}
|
||||
; lam = {!!}
|
||||
; app = app
|
||||
; ∀i = {!!}
|
||||
; ∀e = {!!}
|
||||
}
|
||||
record Tarski : Set₁ where
|
||||
field
|
||||
TM : Set
|
||||
@ -397,6 +252,25 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
|
||||
; rel[] = rel[]
|
||||
}
|
||||
|
||||
|
||||
-- (∀ x ∀ y . A(x,y)) ⇒ ∀ y ∀ x . A(y,x)
|
||||
-- both sides are ∀ ∀ A (0,1)
|
||||
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 _ 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 _ h t = h t t
|
||||
-- ∀ x . A (x) ⇒ ∀ x y . A(x)
|
||||
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 ◇◇ h t h' = h (λ h'' → h' (h'' t))
|
||||
|
||||
record Kripke : Set₁ where
|
||||
field
|
||||
World : Set
|
||||
@ -583,5 +457,5 @@ module FinitaryFirstOrderLogic (F : Nat → Set) (R : Nat → Set) where
|
||||
-- Completeness proof
|
||||
|
||||
-- We first build our universal Kripke model
|
||||
|
||||
|
||||
|
||||
|
||||
@ -52,6 +52,8 @@ module PropUtil where
|
||||
h $ t = h t
|
||||
|
||||
open import Agda.Primitive
|
||||
postulate _≈_ : ∀{ℓ}{A : Set ℓ}(a : A) → A → Set ℓ
|
||||
{-# BUILTIN REWRITE _≈_ #-}
|
||||
infix 3 _≡_
|
||||
data _≡_ {ℓ}{A : Set ℓ}(a : A) : A → Prop ℓ where
|
||||
refl : a ≡ a
|
||||
@ -65,6 +67,9 @@ module PropUtil where
|
||||
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'
|
||||
|
||||
postulate substrefl : ∀{ℓ}{A : Set ℓ}{ℓ'}{P : A → Set ℓ'}{a : A}{e : a ≡ a}{p : P a} → subst P e p ≈ p
|
||||
{-# REWRITE substrefl #-}
|
||||
|
||||
{-# BUILTIN EQUALITY _≡_ #-}
|
||||
|
||||
data Nat : Set where
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user