Mysaa/m1-internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Added automated way to extract latex from lagda files

Browse Source
This commit is contained in:
Mysaa 2023-08-05 20:33:25 +02:00
parent eb80453ef2
commit 841f6e96f1
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
6 changed files with 161 additions and 180 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
FFOL.lagda
View File

@ -16,7 +16,7 @@ module FFOL where
infixr 5 _⊢_ infixr 5 _⊢_
field field
-- We first make the base category with its terminal object --# We first make the base category with its terminal object
Con : Set ℓ¹ Con : Set ℓ¹
Sub : Con → Con → Set ℓ⁵ -- It makes a category Sub : Con → Con → Set ℓ⁵ -- It makes a category
_∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
@ -29,14 +29,14 @@ module FFOL where
ε : {Γ : Con} → Sub Γ ◇ -- The morphism from any object to the terminal ε : {Γ : Con} → Sub Γ ◇ -- The morphism from any object to the terminal
ε-u : {Γ : Con} → {σ : Sub Γ ◇} → σ ≡ ε {Γ} ε-u : {Γ : Con} → {σ : Sub Γ ◇} → σ ≡ ε {Γ}
-- Functor Con → Set called Tm --# Functor Con → Set called Tm
Tm : Con → Set ℓ² Tm : Con → Set ℓ²
_[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- Action on morphisms _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- Action on morphisms
[]t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x []t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x
[]t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ}{β : Sub Δ Γ} → {t : Tm Γ} []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ}{β : Sub Δ Γ} → {t : Tm Γ}
→ t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t
-- Tm : Set⁺ --# Tm : Set⁺
_▹ₜ : Con → Con _▹ₜ : Con → Con
πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ
πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ
@ -47,28 +47,29 @@ module FFOL where
,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ}
→ (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t) → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t)
-- Functor Con → Set called For --# Functor Con → Set called For
For : Con → Set ℓ³ For : Con → Set ℓ³
_[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- Action on morphisms _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- Action on morphisms
[]f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F []f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F
[]f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ}
→ F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f
-- Functor Con × For → Prop called Pf or ⊢ --# Functor Con × For → Prop called Pf or ⊢
_⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴ _⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴
-- Action on morphisms -- Action on morphisms
_[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f)
-- Equalities below are useless because Γ ⊢ F is in prop --# Equalities below are useless because Γ ⊢ F is in prop
-- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F}
-- → prf [ id {Γ} ]p ≡ prf -- → prf [ id {Γ} ]p ≡ prf
-- []p-∘ : {Γ Δ Ξ : Con}{α : Sub Ξ Δ}{β : Sub Δ Γ}{F : For Γ}{prf : Γ ⊢ F} -- []p-∘ : {Γ Δ Ξ : Con}{α : Sub Ξ Δ}{β : Sub Δ Γ}{F : For Γ}{prf : Γ ⊢ F}
-- → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p -- → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p
-- → Prop⁺ --# → Prop⁺
_▹ₚ_ : (Γ : Con) → For Γ → Con _▹ₚ_ : (Γ : Con) → For Γ → Con
πₚ¹ : {Γ Δ : Con}{F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ πₚ¹ : {Γ Δ : Con}{F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ
πₚ² : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) πₚ² : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f)
_,ₚ_ : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) _,ₚ_ : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
--# And its equalities
,ₚ∘πₚ : {Γ Δ : Con}{F : For Γ}{σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ ,ₚ∘πₚ : {Γ Δ : Con}{F : For Γ}{σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ
πₚ¹∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Δ ⊢ (F [ σ ]f)} πₚ¹∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Δ ⊢ (F [ σ ]f)}
→ πₚ¹ (σ ,ₚ prf) ≡ σ → πₚ¹ (σ ,ₚ prf) ≡ σ
@ -80,34 +81,35 @@ module FFOL where
{-- FORMULAE CONSTRUCTORS --} {-- FORMULAE CONSTRUCTORS --}
-- Formulas with relation on terms --# Formulas with relation on terms
R : {Γ : Con} → (t u : Tm Γ) → For Γ R : {Γ : Con} → (t u : Tm Γ) → For Γ
R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ} R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ}
→ (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t) → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t)
-- Implication --# Implication
_⇒_ : {Γ : Con} → For Γ → For Γ → For Γ _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
[]f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ}
→ (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f) → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f)
-- Forall --# Forall
∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
[]f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ}
→ (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f)) → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
--#
{-- PROOFS CONSTRUCTORS --} {-- PROOFS CONSTRUCTORS --}
-- Again, we don't have to write the _[_]p equalities as Proofs are in Prop -- Again, we don't have to write the _[_]p equalities as Proofs are in Prop
-- Lam & App --# Lam & App
lam : {Γ : Con}{F G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G) lam : {Γ : Con}{F G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
app : {Γ : Con}{F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G app : {Γ : Con}{F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G
-- ∀i and ∀e --# ∀i and ∀e
∀i : {Γ : Con}{F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) ∀i : {Γ : Con}{F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
∀e : {Γ : Con}{F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) ∀e : {Γ : Con}{F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
-- Examples --# Examples
-- Proof utils -- Proof utils
forall-in : {Γ Δ : Con} {σ : Sub Γ Δ} {A : For (Δ ▹ₜ)} → Γ ⊢ ∀∀ (A [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f) → Γ ⊢ (∀∀ A [ σ ]f) forall-in : {Γ Δ : Con} {σ : Sub Γ Δ} {A : For (Δ ▹ₜ)} → Γ ⊢ ∀∀ (A [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f) → Γ ⊢ (∀∀ A [ σ ]f)
forall-in {Γ = Γ} f = substP (λ F → Γ ⊢ F) (≡sym ([]f-∀∀)) f forall-in {Γ = Γ} f = substP (λ F → Γ ⊢ F) (≡sym ([]f-∀∀)) f

73
FFOLInitial.lagda
View File

@ -11,15 +11,16 @@ module FFOLInitial where
{-- TERM CONTEXTS - TERMS - FORMULAE - TERM SUBSTITUTIONS --} {-- TERM CONTEXTS - TERMS - FORMULAE - TERM SUBSTITUTIONS --}
-- Term contexts are isomorphic to Nat --# Term contexts are isomorphic to Nat
data Cont : Set₁ where data Cont : Set₁ where
◇t : Cont ◇t : Cont
_▹t⁰ : Cont → Cont _▹t⁰ : Cont → Cont
--#
variable variable
Γₜ Δₜ Ξₜ : Cont Γₜ Δₜ Ξₜ : Cont
-- A term variable is a de-bruijn variable, TmVar n ≈ ⟦0,n-1⟧ --# A term variable is a de-bruijn variable, TmVar n ≈ ⟦0,n-1⟧
data TmVar : Cont → Set₁ where data TmVar : Cont → Set₁ where
tvzero : TmVar (Γₜ ▹t⁰) tvzero : TmVar (Γₜ ▹t⁰)
tvnext : TmVar Γₜ → TmVar (Γₜ ▹t⁰) tvnext : TmVar Γₜ → TmVar (Γₜ ▹t⁰)
@ -28,7 +29,7 @@ module FFOLInitial where
data Tm : Cont → Set₁ where data Tm : Cont → Set₁ where
var : TmVar Γₜ → Tm Γₜ var : TmVar Γₜ → Tm Γₜ
-- Now we can define formulæ --# Now we can define formulæ
data For : Cont → Set₁ where data For : Cont → Set₁ where
R : Tm Γₜ → Tm Γₜ → For Γₜ R : Tm Γₜ → Tm Γₜ → For Γₜ
_⇒_ : For Γₜ → For Γₜ → For Γₜ _⇒_ : For Γₜ → For Γₜ → For Γₜ
@ -37,12 +38,12 @@ module FFOLInitial where
-- Then we define term substitutions --# Then we define term substitutions
data Subt : Cont → Cont → Set₁ where data Subt : Cont → Cont → Set₁ where
εₜ : Subt Γₜ ◇t εₜ : Subt Γₜ ◇t
_,ₜ_ : Subt Δₜ Γₜ → Tm Δₜ → Subt Δₜ (Γₜ ▹t⁰) _,ₜ_ : Subt Δₜ Γₜ → Tm Δₜ → Subt Δₜ (Γₜ ▹t⁰)
-- We write down the access functions from the algebra, in restricted versions --# We write down the access functions from the algebra, in restricted versions
πₜ¹ : Subt Δₜ (Γₜ ▹t⁰) → Subt Δₜ Γₜ πₜ¹ : Subt Δₜ (Γₜ ▹t⁰) → Subt Δₜ Γₜ
πₜ¹ (σₜ ,ₜ t) = σₜ πₜ¹ (σₜ ,ₜ t) = σₜ
πₜ² : Subt Δₜ (Γₜ ▹t⁰) → Tm Δₜ πₜ² : Subt Δₜ (Γₜ ▹t⁰) → Tm Δₜ
@ -56,12 +57,12 @@ module FFOLInitial where
,ₜ∘πₜ {σₜ = σₜ ,ₜ t} = refl ,ₜ∘πₜ {σₜ = σₜ ,ₜ t} = refl
-- We now define the action of term substitutions on terms --# We now define the action of term substitutions on terms
_[_]t : Tm Γₜ → Subt Δₜ Γₜ → Tm Δₜ _[_]t : Tm Γₜ → Subt Δₜ Γₜ → Tm Δₜ
var tvzero [ σ ,ₜ t ]t = t var tvzero [ σ ,ₜ t ]t = t
var (tvnext tv) [ σ ,ₜ t ]t = var tv [ σ ]t var (tvnext tv) [ σ ,ₜ t ]t = var tv [ σ ]t
-- We define weakenings of the term-context for terms --# We define weakenings of the term-context for terms
-- «A term of n variables can be seen as a term of n+1 variables» -- «A term of n variables can be seen as a term of n+1 variables»
wkₜt : Tm Γₜ → Tm (Γₜ ▹t⁰) wkₜt : Tm Γₜ → Tm (Γₜ ▹t⁰)
wkₜt (var tv) = var (tvnext tv) wkₜt (var tv) = var (tvnext tv)
@ -81,7 +82,7 @@ module FFOLInitial where
wkₜ[]t {α = α ,ₜ t} {var tvzero} = refl wkₜ[]t {α = α ,ₜ t} {var tvzero} = refl
wkₜ[]t {α = α ,ₜ t} {var (tvnext tv)} = wkₜ[]t {t = var tv} wkₜ[]t {α = α ,ₜ t} {var (tvnext tv)} = wkₜ[]t {t = var tv}
-- We can now subst on formulæ --# We can now subst on formulæ
_[_]f : For Γₜ → Subt Δₜ Γₜ → For Δₜ _[_]f : For Γₜ → Subt Δₜ Γₜ → For Δₜ
(R t u) [ σ ]f = R (t [ σ ]t) (u [ σ ]t) (R t u) [ σ ]f = R (t [ σ ]t) (u [ σ ]t)
(A ⇒ B) [ σ ]f = (A [ σ ]f) ⇒ (B [ σ ]f) (A ⇒ B) [ σ ]f = (A [ σ ]f) ⇒ (B [ σ ]f)
@ -90,7 +91,7 @@ module FFOLInitial where
-- We now can define identity and composition of term substitutions --# We now can define identity and composition of term substitutions
idₜ : Subt Γₜ Γₜ idₜ : Subt Γₜ Γₜ
idₜ {◇t} = εₜ idₜ {◇t} = εₜ
idₜ {Γₜ ▹t⁰} = lfₜσₜ (idₜ {Γₜ}) idₜ {Γₜ ▹t⁰} = lfₜσₜ (idₜ {Γₜ})
@ -98,7 +99,7 @@ module FFOLInitial where
εₜ ∘ₜ β = εₜ εₜ ∘ₜ β = εₜ
(α ,ₜ x) ∘ₜ β = (α ∘ₜ β) ,ₜ (x [ β ]t) (α ,ₜ x) ∘ₜ β = (α ∘ₜ β) ,ₜ (x [ β ]t)
-- We now have to show all their equalities (idₜ and ∘ₜ respect []t, []f, wkₜ, lfₜ, categorical rules --# We now have to show all their equalities (idₜ and ∘ₜ respect []t, []f, wkₜ, lfₜ, categorical rules
-- Substitution for terms -- Substitution for terms
[]t-id : {t : Tm Γₜ} → t [ idₜ {Γₜ} ]t ≡ t []t-id : {t : Tm Γₜ} → t [ idₜ {Γₜ} ]t ≡ t
@ -164,22 +165,23 @@ module FFOLInitial where
-- We can now define proof contexts, which are indexed by a term context --# We can now define proof contexts, which are indexed by a term context
-- i.e. we know which terms a proof context can use -- i.e. we know which terms a proof context can use
data Conp : Cont → Set₁ where data Conp : Cont → Set₁ where
◇p : Conp Γₜ ◇p : Conp Γₜ
_▹p⁰_ : Conp Γₜ → For Γₜ → Conp Γₜ _▹p⁰_ : Conp Γₜ → For Γₜ → Conp Γₜ
--#
variable variable
Γₚ Γₚ' : Conp Γₜ Γₚ Γₚ' : Conp Γₜ
Δₚ Δₚ' : Conp Δₜ Δₚ Δₚ' : Conp Δₜ
Ξₚ Ξₚ' : Conp Ξₜ Ξₚ Ξₚ' : Conp Ξₜ
-- The actions of Subt's is extended to contexts --# The actions of Subt's is extended to contexts
_[_]c : Conp Γₜ → Subt Δₜ Γₜ → Conp Δₜ _[_]c : Conp Γₜ → Subt Δₜ Γₜ → Conp Δₜ
◇p [ σₜ ]c = ◇p ◇p [ σₜ ]c = ◇p
(Γₚ ▹p⁰ A) [ σₜ ]c = (Γₚ [ σₜ ]c) ▹p⁰ (A [ σₜ ]f) (Γₚ ▹p⁰ A) [ σₜ ]c = (Γₚ [ σₜ ]c) ▹p⁰ (A [ σₜ ]f)
-- This Conp is indeed a functor --# This Conp is indeed a functor
[]c-id : Γₚ [ idₜ ]c ≡ Γₚ []c-id : Γₚ [ idₜ ]c ≡ Γₚ
[]c-id {Γₚ = ◇p} = refl []c-id {Γₚ = ◇p} = refl
[]c-id {Γₚ = Γₚ ▹p⁰ x} = cong₂ _▹p⁰_ []c-id []f-id []c-id {Γₚ = Γₚ ▹p⁰ x} = cong₂ _▹p⁰_ []c-id []f-id
@ -188,11 +190,11 @@ module FFOLInitial where
[]c-∘ {α = α} {β = β} {Ξₚ ▹p⁰ A} = cong₂ _▹p⁰_ []c-∘ []f-∘ []c-∘ {α = α} {β = β} {Ξₚ ▹p⁰ A} = cong₂ _▹p⁰_ []c-∘ []f-∘
-- We can also add a term that will not be used in the formulæ already present --# We can also add a term that will not be used in the formulæ already present
-- (that's why we use wkₜσₜ) -- (that's why we use wkₜσₜ)
_▹tp : Conp Γₜ → Conp (Γₜ ▹t⁰) _▹tp : Conp Γₜ → Conp (Γₜ ▹t⁰)
Γ ▹tp = Γ [ wkₜσₜ idₜ ]c Γ ▹tp = Γ [ wkₜσₜ idₜ ]c
-- We show how it interacts with ,ₜ and lfₜσₜ --# We show how it interacts with ,ₜ and lfₜσₜ
▹tp,ₜ : {σₜ : Subt Γₜ Δₜ}{t : Tm Γₜ} → (Γₚ ▹tp) [ σₜ ,ₜ t ]c ≡ Γₚ [ σₜ ]c ▹tp,ₜ : {σₜ : Subt Γₜ Δₜ}{t : Tm Γₜ} → (Γₚ ▹tp) [ σₜ ,ₜ t ]c ≡ Γₚ [ σₜ ]c
▹tp,ₜ {Γₚ = Γₚ} = ≡tran (≡sym []c-∘) (cong (λ ξ → Γₚ [ ξ ]c) (≡tran wkₜ∘ₜ,ₜ idlₜ)) ▹tp,ₜ {Γₚ = Γₚ} = ≡tran (≡sym []c-∘) (cong (λ ξ → Γₚ [ ξ ]c) (≡tran wkₜ∘ₜ,ₜ idlₜ))
▹tp-lfₜ : {σ : Subt Δₜ Γₜ} → ((Δₚ ▹tp) [ lfₜσₜ σ ]c) ≡ ((Δₚ [ σ ]c) ▹tp) ▹tp-lfₜ : {σ : Subt Δₜ Γₜ} → ((Δₚ ▹tp) [ lfₜσₜ σ ]c) ≡ ((Δₚ [ σ ]c) ▹tp)
@ -200,7 +202,7 @@ module FFOLInitial where
-- With those contexts, we have everything to define proofs --# With those contexts, we have everything to define proofs
data PfVar : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁ where data PfVar : (Γₜ : Cont) → (Γₚ : Conp Γₜ) → For Γₜ → Prop₁ where
pvzero : {A : For Γₜ} → PfVar Γₜ (Γₚ ▹p⁰ A) A pvzero : {A : For Γₜ} → PfVar Γₜ (Γₚ ▹p⁰ A) A
pvnext : {A B : For Γₜ} → PfVar Γₜ Γₚ A → PfVar Γₜ (Γₚ ▹p⁰ B) A pvnext : {A B : For Γₜ} → PfVar Γₜ Γₚ A → PfVar Γₜ (Γₚ ▹p⁰ B) A
@ -213,7 +215,7 @@ module FFOLInitial where
p∀∀i : {A : For (Γₜ ▹t⁰)} → Pf (Γₜ ▹t⁰) (Γₚ ▹tp) A → Pf Γₜ Γₚ (∀∀ A) p∀∀i : {A : For (Γₜ ▹t⁰)} → Pf (Γₜ ▹t⁰) (Γₚ ▹tp) A → Pf Γₜ Γₚ (∀∀ A)
-- The action on Cont's morphisms of Pf functor --# The action on Cont's morphisms of Pf functor
_[_]pvₜ : {A : For Δₜ}→ PfVar Δₜ Δₚ A → (σ : Subt Γₜ Δₜ)→ PfVar Γₜ (Δₚ [ σ ]c) (A [ σ ]f) _[_]pvₜ : {A : For Δₜ}→ PfVar Δₜ Δₚ A → (σ : Subt Γₜ Δₜ)→ PfVar Γₜ (Δₚ [ σ ]c) (A [ σ ]f)
pvzero [ σ ]pvₜ = pvzero pvzero [ σ ]pvₜ = pvzero
pvnext pv [ σ ]pvₜ = pvnext (pv [ σ ]pvₜ) pvnext pv [ σ ]pvₜ = pvnext (pv [ σ ]pvₜ)
@ -233,7 +235,7 @@ module FFOLInitial where
-- We now can create Renamings, a subcategory from (Conp,Subp) that --# We now can create Renamings, a subcategory from (Conp,Subp) that
-- A renaming from a context Γₚ to a context Δₚ means when they are seen -- A renaming from a context Γₚ to a context Δₚ means when they are seen
-- as lists, that every element of Γₚ is an element of Δₚ -- as lists, that every element of Γₚ is an element of Δₚ
-- In other words, we can prove Γₚ from Δₚ using only proof variables (var) -- In other words, we can prove Γₚ from Δₚ using only proof variables (var)
@ -241,7 +243,7 @@ module FFOLInitial where
zeroRen : Ren ◇p Γₚ zeroRen : Ren ◇p Γₚ
leftRen : {A : For Δₜ} → PfVar Δₜ Δₚ A → Ren Δₚ' Δₚ → Ren (Δₚ' ▹p⁰ A) Δₚ leftRen : {A : For Δₜ} → PfVar Δₜ Δₚ A → Ren Δₚ' Δₚ → Ren (Δₚ' ▹p⁰ A) Δₚ
-- We now show how we can extend renamings --# We now show how we can extend renamings
rightRen :{A : For Δₜ} → Ren Γₚ Δₚ → Ren Γₚ (Δₚ ▹p⁰ A) rightRen :{A : For Δₜ} → Ren Γₚ Δₚ → Ren Γₚ (Δₚ ▹p⁰ A)
rightRen zeroRen = zeroRen rightRen zeroRen = zeroRen
rightRen (leftRen x h) = leftRen (pvnext x) (rightRen h) rightRen (leftRen x h) = leftRen (pvnext x) (rightRen h)
@ -272,7 +274,7 @@ module FFOLInitial where
wkᵣp s (p∀∀i pf) = p∀∀i (wkᵣp (Ren▹tp s) pf) wkᵣp s (p∀∀i pf) = p∀∀i (wkᵣp (Ren▹tp s) pf)
-- But we need something stronger than just renamings --# But we need something stronger than just renamings
-- introducing: Proof substitutions -- introducing: Proof substitutions
-- They are basicly a list of proofs for the formulæ contained in -- They are basicly a list of proofs for the formulæ contained in
-- the goal context. -- the goal context.
@ -281,18 +283,18 @@ module FFOLInitial where
εₚ : Subp Δₚ ◇p εₚ : Subp Δₚ ◇p
_,ₚ_ : {A : For Δₜ} → (σ : Subp Δₚ Δₚ') → Pf Δₜ Δₚ A → Subp Δₚ (Δₚ' ▹p⁰ A) _,ₚ_ : {A : For Δₜ} → (σ : Subp Δₚ Δₚ') → Pf Δₜ Δₚ A → Subp Δₚ (Δₚ' ▹p⁰ A)
-- We write down the access functions from the algebra, in restricted versions --# We write down the access functions from the algebra, in restricted versions
πₚ¹ : ∀{Γₜ}{Γₚ Δₚ : Conp Γₜ} {A : For Γₜ} → Subp Δₚ (Γₚ ▹p⁰ A) → Subp Δₚ Γₚ πₚ¹ : ∀{Γₜ}{Γₚ Δₚ : Conp Γₜ} {A : For Γₜ} → Subp Δₚ (Γₚ ▹p⁰ A) → Subp Δₚ Γₚ
πₚ¹ (σₚ ,ₚ pf) = σₚ πₚ¹ (σₚ ,ₚ pf) = σₚ
πₚ² : ∀{Γₜ}{Γₚ Δₚ : Conp Γₜ} {A : For Γₜ} → Subp Δₚ (Γₚ ▹p⁰ A) → Pf Γₜ Δₚ A πₚ² : ∀{Γₜ}{Γₚ Δₚ : Conp Γₜ} {A : For Γₜ} → Subp Δₚ (Γₚ ▹p⁰ A) → Pf Γₜ Δₚ A
πₚ² (σₚ ,ₚ pf) = pf πₚ² (σₚ ,ₚ pf) = pf
-- The action of Cont's morphisms on Subp --# The action of Cont's morphisms on Subp
_[_]σₚ : Subp {Δₜ} Δₚ Δₚ' → (σ : Subt Γₜ Δₜ) → Subp {Γₜ} (Δₚ [ σ ]c) (Δₚ' [ σ ]c) _[_]σₚ : Subp {Δₜ} Δₚ Δₚ' → (σ : Subt Γₜ Δₜ) → Subp {Γₜ} (Δₚ [ σ ]c) (Δₚ' [ σ ]c)
εₚ [ σₜ ]σₚ = εₚ εₚ [ σₜ ]σₚ = εₚ
(σₚ ,ₚ pf) [ σₜ ]σₚ = (σₚ [ σₜ ]σₚ) ,ₚ (pf [ σₜ ]pₜ) (σₚ ,ₚ pf) [ σₜ ]σₚ = (σₚ [ σₜ ]σₚ) ,ₚ (pf [ σₜ ]pₜ)
-- They are indeed stronger than renamings --# They are indeed stronger than renamings
Ren→Sub : Ren Δₚ Δₚ' → Subp {Δₜ} Δₚ' Δₚ Ren→Sub : Ren Δₚ Δₚ' → Subp {Δₜ} Δₚ' Δₚ
Ren→Sub zeroRen = εₚ Ren→Sub zeroRen = εₚ
Ren→Sub (leftRen x s) = Ren→Sub s ,ₚ var x Ren→Sub (leftRen x s) = Ren→Sub s ,ₚ var x
@ -321,6 +323,7 @@ module FFOLInitial where
wkₜσₚ εₚ = εₚ wkₜσₚ εₚ = εₚ
wkₜσₚ {Δₜ = Δₜ} (_,ₚ_ {A = A} σₚ pf) = (wkₜσₚ σₚ) ,ₚ substP (λ Ξₚ → Pf (Δₜ ▹t⁰) Ξₚ (A [ wkₜσₜ idₜ ]f)) refl (_[_]pₜ {Γₜ = Δₜ ▹t⁰} pf (wkₜσₜ idₜ)) wkₜσₚ {Δₜ = Δₜ} (_,ₚ_ {A = A} σₚ pf) = (wkₜσₚ σₚ) ,ₚ substP (λ Ξₚ → Pf (Δₜ ▹t⁰) Ξₚ (A [ wkₜσₜ idₜ ]f)) refl (_[_]pₜ {Γₜ = Δₜ ▹t⁰} pf (wkₜσₜ idₜ))
--#
_[_]p : {A : For Δₜ} → Pf Δₜ Δₚ A → (σ : Subp {Δₜ} Δₚ' Δₚ) → Pf Δₜ Δₚ' A _[_]p : {A : For Δₜ} → Pf Δₜ Δₚ A → (σ : Subp {Δₜ} Δₚ' Δₚ) → Pf Δₜ Δₚ' A
var pvzero [ σ ,ₚ pf ]p = pf var pvzero [ σ ,ₚ pf ]p = pf
var (pvnext pv) [ σ ,ₚ pf ]p = var pv [ σ ]p var (pvnext pv) [ σ ,ₚ pf ]p = var pv [ σ ]p
@ -335,7 +338,7 @@ module FFOLInitial where
-- We can now define identity and composition on proof substitutions --# We can now define identity and composition on proof substitutions
idₚ : Subp {Δₜ} Δₚ Δₚ idₚ : Subp {Δₜ} Δₚ Δₚ
idₚ {Δₚ = ◇p} = εₚ idₚ {Δₚ = ◇p} = εₚ
idₚ {Δₚ = Δₚ ▹p⁰ x} = lfₚσₚ (idₚ {Δₚ = Δₚ}) idₚ {Δₚ = Δₚ ▹p⁰ x} = lfₚσₚ (idₚ {Δₚ = Δₚ})
@ -351,23 +354,25 @@ module FFOLInitial where
-- We can now merge the two notions of contexts, substitutions, and everything --# We can now merge the two notions of contexts, substitutions, and everything
record Con : Set₁ where record Con : Set₁ where
constructor con constructor con
field field
t : Cont t : Cont
p : Conp t p : Conp t
--#
variable variable
Γ Δ Ξ : Con Γ Δ Ξ : Con
--#
record Sub (Γ : Con) (Δ : Con) : Set₁ where record Sub (Γ : Con) (Δ : Con) : Set₁ where
constructor sub constructor sub
field field
t : Subt (Con.t Γ) (Con.t Δ) t : Subt (Con.t Γ) (Con.t Δ)
p : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ t ]c) p : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ t ]c)
-- We need this to apply term-substitution theorems to global substitutions --# We need this to apply term-substitution theorems to global substitutions
sub= : {Γ Δ : Con}{σₜ σₜ' : Subt (Con.t Γ) (Con.t Δ)} → sub= : {Γ Δ : Con}{σₜ σₜ' : Subt (Con.t Γ) (Con.t Δ)} →
σₜ ≡ σₜ' → σₜ ≡ σₜ' →
{σₚ : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ σₜ ]c)} {σₚ : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ σₜ ]c)}
@ -375,20 +380,20 @@ module FFOLInitial where
sub σₜ σₚ ≡ sub σₜ' σₚ' sub σₜ σₚ ≡ sub σₜ' σₚ'
sub= refl = refl sub= refl = refl
-- (Con,Sub) is a category with an initial object --# (Con,Sub) is a category with an initial object
id : Sub Γ Γ id : Sub Γ Γ
id {Γ} = sub idₜ (substP (Subp _) (≡sym []c-id) idₚ) id {Γ} = sub idₜ (substP (Subp _) (≡sym []c-id) idₚ)
_∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ _∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
sub αₜ αₚ ∘ sub βₜ βₚ = sub (αₜ ∘ₜ βₜ) (substP (Subp _) (≡sym []c-∘) (αₚ [ βₜ ]σₚ) ∘ₚ βₚ) sub αₜ αₚ ∘ sub βₜ βₚ = sub (αₜ ∘ₜ βₜ) (substP (Subp _) (≡sym []c-∘) (αₚ [ βₜ ]σₚ) ∘ₚ βₚ)
-- We have our two context extension operators --# We have our two context extension operators
_▹t : Con → Con _▹t : Con → Con
Γ ▹t = con ((Con.t Γ) ▹t⁰) (Con.p Γ ▹tp) Γ ▹t = con ((Con.t Γ) ▹t⁰) (Con.p Γ ▹tp)
_▹p_ : (Γ : Con) → For (Con.t Γ) → Con _▹p_ : (Γ : Con) → For (Con.t Γ) → Con
Γ ▹p A = con (Con.t Γ) (Con.p Γ ▹p⁰ A) Γ ▹p A = con (Con.t Γ) (Con.p Γ ▹p⁰ A)
-- We define the access function from the algebra, but defined for fully-featured substitutions --# We define the access function from the algebra, but defined for fully-featured substitutions
-- For term substitutions -- For term substitutions
πₜ¹* : {Γ Δ : Con} → Sub Δ (Γ ▹t) → Sub Δ Γ πₜ¹* : {Γ Δ : Con} → Sub Δ (Γ ▹t) → Sub Δ Γ
πₜ¹* (sub (σₜ ,ₜ t) σₚ) = sub σₜ (substP (Subp _) ▹tp,ₜ σₚ) πₜ¹* (sub (σₜ ,ₜ t) σₚ) = sub σₜ (substP (Subp _) ▹tp,ₜ σₚ)
@ -578,7 +583,7 @@ module FFOLInitial where
mForT∀∀ : {Γₜ : Cont}{A : For (Γₜ ▹t⁰)} → mForT {Γₜ} (∀∀ A) ≡ FFOL.∀∀ M (mForT {Γₜ ▹t⁰} A) mForT∀∀ : {Γₜ : Cont}{A : For (Γₜ ▹t⁰)} → mForT {Γₜ} (∀∀ A) ≡ FFOL.∀∀ M (mForT {Γₜ ▹t⁰} A)
mForT∀∀ = refl mForT∀∀ = refl
mForP∀∀ : {Γₜ : Cont}{Γₚ : Conp Γₜ}{A : For (Γₜ ▹t⁰)} → mForP {Γₜ} {Γₚ} (∀∀ A) ≡ FFOL.∀∀ M (subst (FFOL.For M) (e▹ₜP {Γₜ} {Γₚ}) (mForP {Γₜ ▹t⁰} {Γₚ ▹tp} A)) mForP∀∀ : {Γₜ : Cont}{Γₚ : Conp Γₜ}{A : For (Γₜ ▹t⁰)} → mForP {Γₜ} {Γₚ} (∀∀ A) ≡ FFOL.∀∀ M (subst (FFOL.For M) (e▹ₜP {Γₜ} {Γₚ}) (mForP {Γₜ ▹t⁰} {Γₚ ▹tp} A))
mForP∀∀ = ? mForP∀∀ = {!!}
-- mFor∀∀ : {Γ : Con}{A : For ((Con.t Γ) ▹t⁰)} → mFor {Γ} (∀∀ A) ≡ FFOL.∀∀ M (mFor {Γ ▹t} A) -- mFor∀∀ : {Γ : Con}{A : For ((Con.t Γ) ▹t⁰)} → mFor {Γ} (∀∀ A) ≡ FFOL.∀∀ M (mFor {Γ ▹t} A)
--mForL : {Γ : Con}{A : For (Con.t Γ ▹t⁰)}{t : Tm (Con.t Γ)} → FFOL._[_]f M (mFor {Γ = {!Γ ▹t!}} A) (FFOL._,ₜ_ M (FFOL.id M) (mTm {Γ = Γ} t)) ≡ mFor {Γ = Γ} (A [ idₜ ,ₜ t ]f) --mForL : {Γ : Con}{A : For (Con.t Γ ▹t⁰)}{t : Tm (Con.t Γ)} → FFOL._[_]f M (mFor {Γ = {!Γ ▹t!}} A) (FFOL._,ₜ_ M (FFOL.id M) (mTm {Γ = Γ} t)) ≡ mFor {Γ = Γ} (A [ idₜ ,ₜ t ]f)

60
Makefile
View File

@ -3,7 +3,7 @@ define extract
endef endef
define split define split
last=-1;i=1;for cur in $$(grep -n -e "--\\\\#" $(1) | cut -d':' -f1); do if [ ! "-1" -eq $$last ]; then dif=$$((cur-last-1));cat $(1) | head -n $$((cur-2)) | tail -n $$((dif-1)) > $(2)$$i$(3); i=$$((i+1)); fi; last=$$cur; done last=-1;i=1;for cur in $$(grep -n -e "--\\\\#" $(1) | cut -d':' -f1); do if [ ! "-1" -eq $$last ]; then dif=$$((cur-last-1));cat $(1) | head -n $$((cur-2)) | tail -n $$((dif)) | awk -f stripAgda.awk > $(2)$$i$(3); i=$$((i+1)); fi; last=$$cur; done
endef endef
all: report/build/M1Report.pdf all: report/build/M1Report.pdf
@ -22,63 +22,11 @@ latex/FFOLInitial.tex: FFOLInitial.lagda
report/build/M1Report.pdf: agda-tex-FFOL agda-tex-FIni agda-tex-ZOL report/build/M1Report.pdf: agda-tex-FFOL agda-tex-FIni agda-tex-ZOL
$(cd report/; latexmk -pdf -xelatex -silent -shell-escape -outdir=build/ -synctex=1 "M1Report") $(cd report/; latexmk -pdf -xelatex -silent -shell-escape -outdir=build/ -synctex=1 "M1Report")
agda-tex-FIni: latex/FFOLInitial.tex agda-tex: latex/ZOL.tex latex/FFOLInitial.tex latex/FFOL.tex
mkdir -p report/agda
1 Cont
--2
3 Tm
4 For
5 Subt
--6 Subt-accessors
7 SubtT
SubtF
IdComp
Conp
SubtC
ConpTp
Pf
Ren
Subp
SubtP
SubtS
SubpP
IdCompP
CExt
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtT.tex,'We\\ now\\ define\\ the\\ action\\ of\\ term\\ substitutions','\\>\[0\]\\<')
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtF.tex,'We\\ can\\ now\\ subst\\ on\\ formul','\\AgdaEmptyExtraSkip')
@$(call extract,latex/FFOLInitial.tex,report/agda/IIdCompT.tex,'We\\ now\\ can\\ define\\ identity\\ and\\ composition\\ of\\ term\\ substitutions','\\AgdaEmptyExtraSkip')
@$(call extract,latex/FFOLInitial.tex,report/agda/IConp.tex,'We\\ can\\ now\\ define\\ proof\\ contexts','\\>\[0\]\\<')
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtC.tex,'The\\ actions\\ of\\ Subt'"'"'s\\ is\\ extended\\ to\\ contexts','This\\ Conp\\ is\\ indeed\\ a\\ functor')
@$(call extract,latex/FFOLInitial.tex,report/agda/IConpTp.tex,'We\\ can\\ also\\ add\\ a\\ term\\ that\\ will\\ not\\ be\\ used','We\\ show\\ how\\ it\\ interacts\\ with')
@cat latex/FFOLInitial.tex | grep -A5000 -m1 'With\\ those\\ contexts,\\ we\\ have\\ everything\\ to\\ define\\ proofs' | grep -B5000 -m1 "AgdaEmptyExtraSkip" | head -n -1 | sed 's/\\>\[6\]/\\>\[0\]/g' > report/agda/IPf.tex
@$(call extract,latex/FFOLInitial.tex,report/agda/IRen.tex,'We\\ now\\ can\\ create\\ Renamings','\\>\[0\]\\<')
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubp.tex,'But\\ we\\ need\\ something\\ stronger\\ than\\ just\\ renamings','They\\ are\\ indeed\\ stronger\\ than\\ renamings')
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtP.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]pv','\\>\[0\]\\<')
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtS.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]σ','\\AgdaEmptyExtraSkip')
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubpP.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]p}}','\\AgdaEmptyExtraSkip')
@$(call extract,latex/FFOLInitial.tex,report/agda/IIdCompP.tex,'We\\ can\\ now\\ define\\ identity\\ and\\ composition\\ on\\ proof\\ substitutions','\\AgdaEmptyExtraSkip')
@cat latex/FFOLInitial.tex | grep -A5000 -m1 'We\\ can\\ now\\ merge\\ the\\ two\\ notions\\ of\\ contexts,\\ substitutions,\\ and\\ everything' | grep -B5000 -m1 '\\>\[0\]\\<' > report/agda/ICon.tex
@cat latex/FFOLInitial.tex | grep -A5000 -B1 -m1 '\\AgdaRecord{Sub}\\AgdaSpace{}%' | grep -B5000 -m1 '\\AgdaEmptyExtraSkip' > report/agda/ISub.tex
@$(call extract,latex/FFOLInitial.tex,report/agda/IIdComp.tex,'(Con,Sub)\\ is\\ a\\ category\\ with\\ an\\ initial\\ object','\\AgdaEmptyExtraSkip')
@$(call extract,latex/FFOLInitial.tex,report/agda/ICExt.tex,'We\\ have\\ our\\ two\\ context\\ extension\\ operators','\\AgdaEmptyExtraSkip')
agda-tex-FFOL: latex/FFOL.tex
mkdir -p report/agda
@$(call extract,latex/FFOL.tex,report/agda/Con.tex,'\\>\[6\]\\AgdaField{Con}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/Tm.tex,'\\>\[6\]\\AgdaField{Tm}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/Tm+.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}▹ₜ}}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/For.tex,'\\>\[6\]\\AgdaField{For}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/Pf.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}⊢\\AgdaUnderscore{}}}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/Pf+.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}▹ₚ\\AgdaUnderscore{}}}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/R.tex,'\\>\[6\]\\AgdaField{R}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/Imp.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}⇒\\AgdaUnderscore{}}}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/Forall.tex,'\\>\[6\]\\AgdaField{∀∀}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/LamApp.tex,'\\>\[6\]\\AgdaField{lam}',"AgdaEmptyExtraSkip")
@$(call extract,latex/FFOL.tex,report/agda/ForallR.tex,'\\>\[6\]\\AgdaField{∀i}',"AgdaEmptyExtraSkip")
agda-tex-ZOL: latex/ZOL.tex
mkdir -p report/agda mkdir -p report/agda
$(call split,"latex/ZOL.tex","report/agda/ZOL-",".tex") $(call split,"latex/ZOL.tex","report/agda/ZOL-",".tex")
$(call split,"latex/FFOLInitial.tex","report/agda/FFOL-I-",".tex")
$(call split,"latex/FFOL.tex","report/agda/FFOL-",".tex")
.PHONY: clean agda-tex agda-tex-FFOL agda-tex-ZOL agda-tex-FIni .PHONY: clean agda-tex agda-tex-FFOL agda-tex-ZOL agda-tex-FIni
clean: clean:

145
report/M1Report.tex
View File

@ -71,13 +71,6 @@
Unfortunately, Agda cannot understand SOGATs directly (yet). So we have to convert this SOGAT into a GAT. I will describe the process in this section, each line of the SOGAT giving birth to a set of sorts, constructors and equations in the GAT. Unfortunately, Agda cannot understand SOGATs directly (yet). So we have to convert this SOGAT into a GAT. I will describe the process in this section, each line of the SOGAT giving birth to a set of sorts, constructors and equations in the GAT.
\begin{tcolorbox}
\begin{AgdaSuppressSpace}
%\agda{agda/ZOL-Con.tex}
\end{AgdaSuppressSpace}
\vspace{-5.5ex}
\end{tcolorbox}
\subsection{Normalization for Infinitary First Order Logic} \subsection{Normalization for Infinitary First Order Logic}
\begin{figure} \begin{figure}
@ -141,22 +134,22 @@
We will first define this category, its initial object, and every rule that these components should obey. We will first define this category, its initial object, and every rule that these components should obey.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/Con.tex} \agda{agda/FFOL-1.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
We can now define terms, formulæ and proofs, which are functors from $\bCon$ to $\bSet$ (and proofs are a more complex functor from $\bCon$ to XXXXX). For each of them, we define the action of the functors on morphisms, and we also write the equalities that describe the functionality. We can now define terms, formulæ and proofs, which are functors from $\bCon$ to $\bSet$ (and proofs are a more complex functor from $\bCon$ to XXXXX). For each of them, we define the action of the functors on morphisms, and we also write the equalities that describe the functionality.
\def\agdasep{\vspace{-10.5ex}\begin{center}\rule{0.9\linewidth}{0.4pt}\end{center}\vspace{-3.5ex}} \def\agdasep{\begin{center}\vspace{-2.5ex}\rule{0.9\linewidth}{0.4pt}\vspace{-1ex}\end{center}}
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/Tm.tex} \agda{agda/FFOL-2.tex}
\agdasep \agdasep
\agda{agda/For.tex} \agda{agda/FFOL-4.tex}
\agdasep \agdasep
\agda{agda/Pf.tex} \agda{agda/FFOL-5.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
Then we define our context extensions. We also have constructors for substitutions to extended contexts. This constructor should work as a product, which means that we have two \enquote{projections} that can revert the mapping. The constructor should finally be consistent with $\circ$. Then we define our context extensions. We also have constructors for substitutions to extended contexts. This constructor should work as a product, which means that we have two \enquote{projections} that can revert the mapping. The constructor should finally be consistent with $\circ$.
@ -164,14 +157,14 @@
Please ignore the \verb*|substP| for now, this notion will be explained in \autoref{sec:transport-hell}. Please ignore the \verb*|substP| for now, this notion will be explained in \autoref{sec:transport-hell}.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/Tm+.tex} \agda{agda/FFOL-3.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/Pf+.tex} \agda{agda/FFOL-7.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
Finally, with those context extensions, we can define our operators on functions and proofs. Those operators have to commute with the images of substitutions (the equations are unneeded for proof operators, as they are in prop). Finally, with those context extensions, we can define our operators on functions and proofs. Those operators have to commute with the images of substitutions (the equations are unneeded for proof operators, as they are in prop).
@ -179,17 +172,17 @@
We can take a closer look at where our apparently strictly positive application should be ($\lam$ and $\foralli$). We can see that instead of an application, we only have a formula (or a proof) that goes from an extended context to a base contexts. This \enquote{removal} of the term variable stands for the strictly positive function that would have taken a term/proof as a parameter. We can take a closer look at where our apparently strictly positive application should be ($\lam$ and $\foralli$). We can see that instead of an application, we only have a formula (or a proof) that goes from an extended context to a base contexts. This \enquote{removal} of the term variable stands for the strictly positive function that would have taken a term/proof as a parameter.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/R.tex} \agda{agda/FFOL-9.tex}
\agdasep \agdasep
\agda{agda/Imp.tex} \agda{agda/FFOL-10.tex}
\agdasep \agdasep
\agda{agda/Forall.tex} \agda{agda/FFOL-11.tex}
\agdasep \agdasep
\agda{agda/LamApp.tex} \agda{agda/FFOL-13.tex}
\agdasep \agdasep
\agda{agda/ForallR.tex} \agda{agda/FFOL-14.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
We now have a generalized algebraic theory that describes all the models of Predicate logic. A model is indeed an implementation of the agda record described above. We now have a generalized algebraic theory that describes all the models of Predicate logic. A model is indeed an implementation of the agda record described above.
@ -206,19 +199,19 @@
So, we first define the term contexts, which simply describes how many terms they are in the context (therefore, it is isomorphic to Nat). So, we first define the term contexts, which simply describes how many terms they are in the context (therefore, it is isomorphic to Nat).
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/ICont.tex} \agda{agda/FFOL-I-1.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
Then, we can define terms (which can only be term variables in our simplified version), and formulæ (with only one binary relation). They are both indexed only on a term context, and we will need make them $\bCon \rightarrow \bSet$ rather than $\textbf{Cont} \rightarrow \bSet$. But this will be only a trivial extraction of the $\textbf{Cont}$ inside the $\bCon$, as we can notice that the terms and formulæ defined by a context doesn't depend on the proof variables available. We simply give the constructors described in the algebra. Then, we can define terms (which can only be term variables in our simplified version), and formulæ (with only one binary relation). They are both indexed only on a term context, and we will need make them $\bCon \rightarrow \bSet$ rather than $\textbf{Cont} \rightarrow \bSet$. But this will be only a trivial extraction of the $\textbf{Cont}$ inside the $\bCon$, as we can notice that the terms and formulæ defined by a context doesn't depend on the proof variables available. We simply give the constructors described in the algebra.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/ITm.tex} \agda{agda/FFOL-I-3.tex}
\agdasep \agdasep
\agda{agda/IFor.tex} \agda{agda/FFOL-I-4.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
We now can define term substitutions. The algebra gives us two ways of constructing them: with $,_t$ and as a morphism from the initial object. That's how we make our constructor The two projections $\pi_t^1$ and $\pi_t^2$ are then simply obtained by destroying the $,_t$ constructor and getting the first or second term. The equalities between $\pi_t¹$, $\pi_t²$ and $,_t$ can be proven easily in that layout. We now can define term substitutions. The algebra gives us two ways of constructing them: with $,_t$ and as a morphism from the initial object. That's how we make our constructor The two projections $\pi_t^1$ and $\pi_t^2$ are then simply obtained by destroying the $,_t$ constructor and getting the first or second term. The equalities between $\pi_t¹$, $\pi_t²$ and $,_t$ can be proven easily in that layout.
@ -232,15 +225,15 @@
You can see we use some helper functions that are called $\operatorname{wk}_t$ and $\operatorname{lf}_t$. Those stands for weakening and lifting. I don't show their definitions here, because they are only helper functions, but $\operatorname{wk}_t$ means that from something going from a context $\Gamma$, we create something going from the context $\Gamma \triangleright_t$ that does not uses the added variable. $\operatorname{lf}_t$ means that we add one variable in the source, one variable in the goal, and that this variable is mapped to itself. You can see we use some helper functions that are called $\operatorname{wk}_t$ and $\operatorname{lf}_t$. Those stands for weakening and lifting. I don't show their definitions here, because they are only helper functions, but $\operatorname{wk}_t$ means that from something going from a context $\Gamma$, we create something going from the context $\Gamma \triangleright_t$ that does not uses the added variable. $\operatorname{lf}_t$ means that we add one variable in the source, one variable in the goal, and that this variable is mapped to itself.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/ISubt.tex} \agda{agda/FFOL-I-5.tex}
\agdasep \agdasep
\agda{agda/ISubtT.tex} \agda{agda/FFOL-I-7.tex}
\agdasep \agdasep
\agda{agda/ISubTF.tex} \agda{agda/FFOL-I-9.tex}
\agdasep \agdasep
\agda{agda/IIdCompT.tex} \agda{agda/FFOL-I-10.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
We can now start creating the other category. For that, we can define the base set of the category like we did with term contexts. But this time, our extension constructor has another parameter: The formula the added proof proves. Therefore, we have a dependency of $\operatorname{Conp}$ on $\operatorname{Cont}$, because formula is defined in conp. We can now start creating the other category. For that, we can define the base set of the category like we did with term contexts. But this time, our extension constructor has another parameter: The formula the added proof proves. Therefore, we have a dependency of $\operatorname{Conp}$ on $\operatorname{Cont}$, because formula is defined in conp.
@ -250,13 +243,13 @@
We will finally create another operator on $\textbf{Conp}$: $\triangleright tp$. This operator does a term extension of a proof context, which doesn't add any information to the proofs, it only adds one unused variable to them (we substitute all the proofs with $\operatorname{wk}_t \operatorname{id}_t$). It can be understood as the action of the general $\triangleright_t$ functor on $\textbf{Conp}$. We will finally create another operator on $\textbf{Conp}$: $\triangleright tp$. This operator does a term extension of a proof context, which doesn't add any information to the proofs, it only adds one unused variable to them (we substitute all the proofs with $\operatorname{wk}_t \operatorname{id}_t$). It can be understood as the action of the general $\triangleright_t$ functor on $\textbf{Conp}$.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/IConp.tex} \agda{agda/FFOL-I-12.tex}
\agdasep \agdasep
\agda{agda/ISubtC.tex} \agda{agda/FFOL-I-14.tex}
\agdasep \agdasep
\agda{agda/IConpTp.tex} \agda{agda/FFOL-I-16.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
We now have everything we need to define proofs. As we are in the syntax, the only constructors for proofs will be those defined in the algebra, plus proof variables. These definitions are pretty straightforward as they are directly induced from the algebra. You can notice that we have separated term and proof contexts in the definitions, but it is only for the sake of readability, because operations on proofs will often modify the proof context without changing the term context. We now have everything we need to define proofs. As we are in the syntax, the only constructors for proofs will be those defined in the algebra, plus proof variables. These definitions are pretty straightforward as they are directly induced from the algebra. You can notice that we have separated term and proof contexts in the definitions, but it is only for the sake of readability, because operations on proofs will often modify the proof context without changing the term context.
@ -264,11 +257,11 @@
We also define the action of term-substitutions on proofs (because Pf is a functor that is indexed by $\textbf{Cont}$). Terms substitutions does nothing to the proofs, they only affect formulæ and terms, which you cannot find inside a proof. So it is only changing the type of a proof from $\Pf Δ_t\;Δ_p\;A$ to $\Pf Γ_t\;Δ_p[σ]\; A[σ]$. We also define the action of term-substitutions on proofs (because Pf is a functor that is indexed by $\textbf{Cont}$). Terms substitutions does nothing to the proofs, they only affect formulæ and terms, which you cannot find inside a proof. So it is only changing the type of a proof from $\Pf Δ_t\;Δ_p\;A$ to $\Pf Γ_t\;Δ_p[σ]\; A[σ]$.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/IPf.tex} \agda{agda/FFOL-I-18.tex}
\agdasep \agdasep
\agda{agda/ISubtP.tex} \agda{agda/FFOL-I-19.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
Before we can define proof substitutions, we need to define a weaker version of them, that are called \emph{renamings}. A renaming from a proof context $Γ_p$ to a proof context $Δ_p$ that have the same term-context, is a way of re-ordering, duplicating or deleting the proofs contained inside of $Δ_p$. If we were to understand proof contexts as list of formulæ, then a renaming from $Γ_p$ to $Δ_p$ would be a witness that each formula in $Δ_p$ is contained at least one time in $Γ_p$. That's why we use $\operatorname{PfVar}$, as $\operatorname{PfVar} Γ_t Γ_p A$ is a witness that proof-context $Γ_p$ contains the formula $A$. Before we can define proof substitutions, we need to define a weaker version of them, that are called \emph{renamings}. A renaming from a proof context $Γ_p$ to a proof context $Δ_p$ that have the same term-context, is a way of re-ordering, duplicating or deleting the proofs contained inside of $Δ_p$. If we were to understand proof contexts as list of formulæ, then a renaming from $Γ_p$ to $Δ_p$ would be a witness that each formula in $Δ_p$ is contained at least one time in $Γ_p$. That's why we use $\operatorname{PfVar}$, as $\operatorname{PfVar} Γ_t Γ_p A$ is a witness that proof-context $Γ_p$ contains the formula $A$.
@ -276,9 +269,9 @@
For these renamings, we make some constructors, for example the identity renaming, or the weakening of a renaming. We will finally make a operator that weakens a proof in $Γ_p$ with a renaming from $Γ_p$ to $Δ_p$ into a proof in $Δ_p$. For these renamings, we make some constructors, for example the identity renaming, or the weakening of a renaming. We will finally make a operator that weakens a proof in $Γ_p$ with a renaming from $Γ_p$ to $Δ_p$ into a proof in $Δ_p$.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/IRen.tex} \agda{agda/FFOL-I-20.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
Now, we are defining a complete proof substitution, that can also be understood as a list a proofs of the formulæ described in the goal proof-context. Now, we are defining a complete proof substitution, that can also be understood as a list a proofs of the formulæ described in the goal proof-context.
@ -288,11 +281,11 @@
Again, these substitutions are a functor over the category $\textbf{Cont}$, so we have to construct the action on morphisms, which is simply applying the transformations to all the proofs contained in the substitution. Again, these substitutions are a functor over the category $\textbf{Cont}$, so we have to construct the action on morphisms, which is simply applying the transformations to all the proofs contained in the substitution.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/ISubp.tex} \agda{agda/FFOL-I-22.tex}
\agdasep \agdasep
\agda{agda/ISubtS.tex} \agda{agda/FFOL-I-24.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
With this new kind of substitution, we can substitute on proofs (that's what they're for). In other words, we have to describe the action of the $\Pf$ functor on the morphisms of the category $\textbf{Conp}$. With this new kind of substitution, we can substitute on proofs (that's what they're for). In other words, we have to describe the action of the $\Pf$ functor on the morphisms of the category $\textbf{Conp}$.
@ -302,9 +295,9 @@
Again, we have defined $\operatorname{wk}_p$ and $\operatorname{lf}_p$. The former will add an unused proof variable (an assumption) in a substitution, and the latter adds a formula in the goal which is proven using an assumption. Again, we have defined $\operatorname{wk}_p$ and $\operatorname{lf}_p$. The former will add an unused proof variable (an assumption) in a substitution, and the latter adds a formula in the goal which is proven using an assumption.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/ISubpP.tex} \agda{agda/FFOL-I-26.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
This definition of proof substitutions allows us to define the categorical operators for proof substitutions. This definition of proof substitutions allows us to define the categorical operators for proof substitutions.
@ -314,9 +307,9 @@
The proofs of these laws contains a lot of transports, which will be described more precisely in \autoref{sec:transport-hell}. The proofs of these laws contains a lot of transports, which will be described more precisely in \autoref{sec:transport-hell}.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/IIdCompP.tex} \agda{agda/FFOL-I-27.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
The last step is to merge our two kinds of contexts and substitutions in order to match the algebra. The last step is to merge our two kinds of contexts and substitutions in order to match the algebra.
@ -324,13 +317,13 @@
For contexts, we simply have a record type. But for substitutions, we defined Subp to only describe substitutions between Conp{\footnotesize s} with \emph{the same Conp}. Our solution is to understand global substitutions as a sequence of substitutions, first on terms, and then on proofs. That's why the \enquote{proof} part of the substitution can only be applyed to proofs on $\Delta_p [t]p$, i.e. proofs that have already been term-substituted by the \enquote{term} part of the substitution. The definition of the algebra's substitution is given after, and you can see that substitutions works exactly as described, first, the proof and everything inside is substituted using the \enquote{term} part of the substitution, and only after that the \enquote{proof} part of the substitution is applied. For contexts, we simply have a record type. But for substitutions, we defined Subp to only describe substitutions between Conp{\footnotesize s} with \emph{the same Conp}. Our solution is to understand global substitutions as a sequence of substitutions, first on terms, and then on proofs. That's why the \enquote{proof} part of the substitution can only be applyed to proofs on $\Delta_p [t]p$, i.e. proofs that have already been term-substituted by the \enquote{term} part of the substitution. The definition of the algebra's substitution is given after, and you can see that substitutions works exactly as described, first, the proof and everything inside is substituted using the \enquote{term} part of the substitution, and only after that the \enquote{proof} part of the substitution is applied.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/ICon.tex} \agda{agda/FFOL-I-28.tex}
\agdasep \agdasep
\agda{agda/ISub.tex} \agda{agda/FFOL-I-30.tex}
\vspace{-13.5ex}
\begin{center}\rule{0.9\linewidth}{0.4pt}\end{center} \agdasep
\vspace{-3ex}
\begin{code} \begin{code}
\>[4]\AgdaOperator{\AgdaField{\AgdaUnderscore{}[\AgdaUnderscore{}]p}}\AgdaSpace{}% \>[4]\AgdaOperator{\AgdaField{\AgdaUnderscore{}[\AgdaUnderscore{}]p}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}%
@ -348,18 +341,18 @@
\AgdaBound{σ}\AgdaSpace{}% \AgdaBound{σ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]p}}\<% \AgdaOperator{\AgdaFunction{]p}}\<%
\end{code} \end{code}
\vspace{-5ex}
\end{tcolorbox} \end{tcolorbox}
And we can finally define our categorical operators for the merged version. They are only concatenation of the previously defined operators, so no hard logic here. Those constructions are obviously followed by equations needed for the algebra. And we can finally define our categorical operators for the merged version. They are only concatenation of the previously defined operators, so no hard logic here. Those constructions are obviously followed by equations needed for the algebra.
\begin{tcolorbox} \begin{tcolorbox}
\vspace{-2ex}
\agda{agda/IIdComp.tex} \agda{agda/FFOL-I-32.tex}
\vspace{-3ex}
\agdasep \agdasep
\agda{agda/ICExt.tex} \agda{agda/FFOL-I-33.tex}
\vspace{-7.5ex}
\end{tcolorbox} \end{tcolorbox}
\subsection{Transport Hell} \subsection{Transport Hell}

2
report/header.tex
View File

@ -108,7 +108,7 @@
% Agda Config % Agda Config
\usepackage{agda} \usepackage{agda}
%\AgdaNoSpaceAroundCode{} \AgdaNoSpaceAroundCode{}
\usepackage{newunicodechar} \usepackage{newunicodechar}
\newunicodechar{∘}{\ensuremath{\mathnormal{\circ}}} \newunicodechar{∘}{\ensuremath{\mathnormal{\circ}}}
\newunicodechar{≡}{\ensuremath{\mathnormal{\equiv}}} \newunicodechar{≡}{\ensuremath{\mathnormal{\equiv}}}

33
stripAgda.awk Normal file
View File

@ -0,0 +1,33 @@
BEGIN {
b=1
}
/\\>\[2\]\\AgdaComment{--\\#}\\<%/ {
b=2
}
/^\\\\\[\\AgdaEmptyExtraSkip\]%$/ {
agg=agg""((agg=="")?"":"\n")""$0
b=0
}
/^%$/ {
agg=agg""((agg=="")?"":"\n")""$0
b=0
}
/^\\\\$/ {
agg=agg""((agg=="")?"":"\n")""((b==2)?"":$0)
b=0
}
/^\\>\[0\]\\<%$/ {
agg=agg""((agg=="")?"":"\n")""$0
b=0
}
// {
if (b==1){
if(agg!=""){
print agg
}
agg=""
print $0
}else if (b==0){
b=1
}
}