From 841f6e96f13ad1f5f6e9c07f0c83683161b2f0c9 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Sat, 5 Aug 2023 20:33:25 +0200 Subject: [PATCH] Added automated way to extract latex from lagda files --- FFOL.lagda | 28 +++++---- FFOLInitial.lagda | 73 +++++++++++----------- Makefile | 60 ++---------------- report/M1Report.tex | 145 +++++++++++++++++++++----------------------- report/header.tex | 2 +- stripAgda.awk | 33 ++++++++++ 6 files changed, 161 insertions(+), 180 deletions(-) create mode 100644 stripAgda.awk diff --git a/FFOL.lagda b/FFOL.lagda index 59a2a7a..3a09c36 100644 --- a/FFOL.lagda +++ b/FFOL.lagda @@ -16,7 +16,7 @@ module FFOL where infixr 5 _⊢_ field - -- We first make the base category with its terminal object + --# We first make the base category with its terminal object Con : Set ℓ¹ Sub : Con → Con → Set ℓ⁵ -- It makes a category _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ @@ -29,14 +29,14 @@ module FFOL where ε : {Γ : Con} → Sub Γ ◇ -- The morphism from any object to the terminal ε-u : {Γ : Con} → {σ : Sub Γ ◇} → σ ≡ ε {Γ} - -- Functor Con → Set called Tm + --# Functor Con → Set called Tm Tm : Con → Set ℓ² _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- Action on morphisms []t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ}{β : Sub Δ Γ} → {t : Tm Γ} → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t - -- Tm : Set⁺ + --# Tm : Set⁺ _▹ₜ : Con → Con πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ @@ -47,28 +47,29 @@ module FFOL where ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t) - -- Functor Con → Set called For + --# Functor Con → Set called For For : Con → Set ℓ³ _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- Action on morphisms []f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f - -- Functor Con × For → Prop called Pf or ⊢ + --# Functor Con × For → Prop called Pf or ⊢ _⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴ -- Action on morphisms _[_]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} -- → prf [ id {Γ} ]p ≡ prf -- []p-∘ : {Γ Δ Ξ : Con}{α : Sub Ξ Δ}{β : Sub Δ Γ}{F : For Γ}{prf : Γ ⊢ F} -- → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p - -- → Prop⁺ + --# → Prop⁺ _▹ₚ_ : (Γ : Con) → For Γ → Con πₚ¹ : {Γ Δ : Con}{F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ πₚ² : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) _,ₚ_ : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) + --# And its equalities ,ₚ∘πₚ : {Γ Δ : Con}{F : For Γ}{σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ πₚ¹∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ (σ ,ₚ prf) ≡ σ @@ -80,34 +81,35 @@ module FFOL where {-- FORMULAE CONSTRUCTORS --} - -- Formulas with relation on terms + --# Formulas with relation on terms R : {Γ : Con} → (t u : Tm Γ) → For Γ R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ} → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t) - -- Implication + --# Implication _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f) - -- Forall + --# Forall ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f)) + --# {-- PROOFS CONSTRUCTORS --} -- 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) app : {Γ : Con}{F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G - -- ∀i and ∀e + --# ∀i and ∀e ∀i : {Γ : Con}{F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) ∀e : {Γ : Con}{F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) - -- Examples + --# Examples -- Proof utils forall-in : {Γ Δ : Con} {σ : Sub Γ Δ} {A : For (Δ ▹ₜ)} → Γ ⊢ ∀∀ (A [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f) → Γ ⊢ (∀∀ A [ σ ]f) forall-in {Γ = Γ} f = substP (λ F → Γ ⊢ F) (≡sym ([]f-∀∀)) f diff --git a/FFOLInitial.lagda b/FFOLInitial.lagda index a40c239..03038ba 100644 --- a/FFOLInitial.lagda +++ b/FFOLInitial.lagda @@ -11,15 +11,16 @@ module FFOLInitial where {-- TERM CONTEXTS - TERMS - FORMULAE - TERM SUBSTITUTIONS --} - -- Term contexts are isomorphic to Nat + --# Term contexts are isomorphic to Nat data Cont : Set₁ where ◇t : Cont _▹t⁰ : Cont → Cont - + + --# variable Γₜ Δₜ Ξₜ : 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 tvzero : TmVar (Γₜ ▹t⁰) tvnext : TmVar Γₜ → TmVar (Γₜ ▹t⁰) @@ -28,7 +29,7 @@ module FFOLInitial where data Tm : Cont → Set₁ where var : TmVar Γₜ → Tm Γₜ - -- Now we can define formulæ + --# Now we can define formulæ data For : Cont → Set₁ where R : Tm Γₜ → Tm Γₜ → 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 εₜ : 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 Δₜ Γₜ πₜ¹ (σₜ ,ₜ t) = σₜ πₜ² : Subt Δₜ (Γₜ ▹t⁰) → Tm Δₜ @@ -56,12 +57,12 @@ module FFOLInitial where ,ₜ∘πₜ {σₜ = σₜ ,ₜ 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 Δₜ var tvzero [ σ ,ₜ t ]t = 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» wkₜt : Tm Γₜ → Tm (Γₜ ▹t⁰) wkₜt (var tv) = var (tvnext tv) @@ -81,7 +82,7 @@ module FFOLInitial where wkₜ[]t {α = α ,ₜ t} {var tvzero} = refl 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 Δₜ (R t u) [ σ ]f = R (t [ σ ]t) (u [ σ ]t) (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ₜ {◇t} = εₜ idₜ {Γₜ ▹t⁰} = lfₜσₜ (idₜ {Γₜ}) @@ -98,7 +99,7 @@ module FFOLInitial where εₜ ∘ₜ β = εₜ (α ,ₜ 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 []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 data Conp : Cont → Set₁ where ◇p : Conp Γₜ _▹p⁰_ : Conp Γₜ → For Γₜ → Conp Γₜ - + + --# variable Γₚ Γₚ' : 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 Δₜ ◇p [ σₜ ]c = ◇p (Γₚ ▹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 {Γₚ = ◇p} = refl []c-id {Γₚ = Γₚ ▹p⁰ x} = cong₂ _▹p⁰_ []c-id []f-id @@ -188,11 +190,11 @@ module FFOLInitial where []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ₜσₜ) _▹tp : Conp Γₜ → Conp (Γₜ ▹t⁰) Γ ▹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,ₜ {Γₚ = Γₚ} = ≡tran (≡sym []c-∘) (cong (λ ξ → Γₚ [ ξ ]c) (≡tran wkₜ∘ₜ,ₜ idlₜ)) ▹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 pvzero : {A : For Γₜ} → PfVar Γₜ (Γₚ ▹p⁰ A) 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) - -- 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) pvzero [ σ ]pvₜ = pvzero 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 -- as lists, that every element of Γₚ is an element of Δₚ -- In other words, we can prove Γₚ from Δₚ using only proof variables (var) @@ -241,7 +243,7 @@ module FFOLInitial where zeroRen : Ren ◇p Γₚ 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 zeroRen = zeroRen 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) - -- But we need something stronger than just renamings + --# But we need something stronger than just renamings -- introducing: Proof substitutions -- They are basicly a list of proofs for the formulæ contained in -- the goal context. @@ -281,18 +283,18 @@ module FFOLInitial where εₚ : Subp Δₚ ◇p _,ₚ_ : {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 Δₚ Γₚ πₚ¹ (σₚ ,ₚ pf) = σₚ πₚ² : ∀{Γₜ}{Γₚ Δₚ : Conp Γₜ} {A : For Γₜ} → Subp Δₚ (Γₚ ▹p⁰ A) → Pf Γₜ Δₚ A πₚ² (σₚ ,ₚ pf) = pf - -- The action of Cont's morphisms on Subp + --# The action of Cont's morphisms on Subp _[_]σₚ : Subp {Δₜ} Δₚ Δₚ' → (σ : Subt Γₜ Δₜ) → Subp {Γₜ} (Δₚ [ σ ]c) (Δₚ' [ σ ]c) εₚ [ σₜ ]σₚ = εₚ (σₚ ,ₚ pf) [ σₜ ]σₚ = (σₚ [ σₜ ]σₚ) ,ₚ (pf [ σₜ ]pₜ) - -- They are indeed stronger than renamings + --# They are indeed stronger than renamings Ren→Sub : Ren Δₚ Δₚ' → Subp {Δₜ} Δₚ' Δₚ Ren→Sub zeroRen = εₚ Ren→Sub (leftRen x s) = Ren→Sub s ,ₚ var x @@ -321,6 +323,7 @@ module FFOLInitial where wkₜσₚ εₚ = εₚ 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 var pvzero [ σ ,ₚ pf ]p = pf 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ₚ {Δₚ = ◇p} = εₚ 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 constructor con field t : Cont p : Conp t - + + --# variable Γ Δ Ξ : Con - + + --# record Sub (Γ : Con) (Δ : Con) : Set₁ where constructor sub field t : Subt (Con.t Γ) (Con.t Δ) 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 Δ)} → σₜ ≡ σₜ' → {σₚ : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ σₜ ]c)} @@ -375,20 +380,20 @@ module FFOLInitial where sub σₜ σₚ ≡ sub σₜ' σₚ' 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ₜ (substP (Subp _) (≡sym []c-id) idₚ) _∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ 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 Γ) ▹t⁰) (Con.p Γ ▹tp) _▹p_ : (Γ : Con) → For (Con.t Γ) → Con Γ ▹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 πₜ¹* : {Γ Δ : Con} → Sub Δ (Γ ▹t) → Sub Δ Γ πₜ¹* (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∀∀ = refl 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) --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) diff --git a/Makefile b/Makefile index 0d8a705..f61a71c 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ define extract endef 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 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 $(cd report/; latexmk -pdf -xelatex -silent -shell-escape -outdir=build/ -synctex=1 "M1Report") -agda-tex-FIni: latex/FFOLInitial.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 +agda-tex: latex/ZOL.tex latex/FFOLInitial.tex latex/FFOL.tex mkdir -p report/agda $(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 clean: diff --git a/report/M1Report.tex b/report/M1Report.tex index fa27e8b..4e22b66 100644 --- a/report/M1Report.tex +++ b/report/M1Report.tex @@ -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. - \begin{tcolorbox} - \begin{AgdaSuppressSpace} - %\agda{agda/ZOL-Con.tex} - \end{AgdaSuppressSpace} - \vspace{-5.5ex} - \end{tcolorbox} - \subsection{Normalization for Infinitary First Order Logic} \begin{figure} @@ -141,22 +134,22 @@ We will first define this category, its initial object, and every rule that these components should obey. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/Con.tex} - \vspace{-7.5ex} + + \agda{agda/FFOL-1.tex} + \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. - \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} - \vspace{-2ex} - \agda{agda/Tm.tex} + + \agda{agda/FFOL-2.tex} \agdasep - \agda{agda/For.tex} + \agda{agda/FFOL-4.tex} \agdasep - \agda{agda/Pf.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-5.tex} + \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$. @@ -164,14 +157,14 @@ Please ignore the \verb*|substP| for now, this notion will be explained in \autoref{sec:transport-hell}. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/Tm+.tex} - \vspace{-7.5ex} + + \agda{agda/FFOL-3.tex} + \end{tcolorbox} \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/Pf+.tex} - \vspace{-7.5ex} + + \agda{agda/FFOL-7.tex} + \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). @@ -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. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/R.tex} + + \agda{agda/FFOL-9.tex} \agdasep - \agda{agda/Imp.tex} + \agda{agda/FFOL-10.tex} \agdasep - \agda{agda/Forall.tex} + \agda{agda/FFOL-11.tex} \agdasep - \agda{agda/LamApp.tex} + \agda{agda/FFOL-13.tex} \agdasep - \agda{agda/ForallR.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-14.tex} + \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. @@ -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). \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/ICont.tex} - \vspace{-7.5ex} + + \agda{agda/FFOL-I-1.tex} + \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. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/ITm.tex} + + \agda{agda/FFOL-I-3.tex} \agdasep - \agda{agda/IFor.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-I-4.tex} + \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. @@ -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. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/ISubt.tex} + + \agda{agda/FFOL-I-5.tex} \agdasep - \agda{agda/ISubtT.tex} + \agda{agda/FFOL-I-7.tex} \agdasep - \agda{agda/ISubTF.tex} + \agda{agda/FFOL-I-9.tex} \agdasep - \agda{agda/IIdCompT.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-I-10.tex} + \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. @@ -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}$. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/IConp.tex} + + \agda{agda/FFOL-I-12.tex} \agdasep - \agda{agda/ISubtC.tex} + \agda{agda/FFOL-I-14.tex} \agdasep - \agda{agda/IConpTp.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-I-16.tex} + \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. @@ -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[σ]$. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/IPf.tex} + + \agda{agda/FFOL-I-18.tex} \agdasep - \agda{agda/ISubtP.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-I-19.tex} + \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$. @@ -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$. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/IRen.tex} - \vspace{-7.5ex} + + \agda{agda/FFOL-I-20.tex} + \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. @@ -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. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/ISubp.tex} + + \agda{agda/FFOL-I-22.tex} \agdasep - \agda{agda/ISubtS.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-I-24.tex} + \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}$. @@ -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. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/ISubpP.tex} - \vspace{-7.5ex} + + \agda{agda/FFOL-I-26.tex} + \end{tcolorbox} 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}. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/IIdCompP.tex} - \vspace{-7.5ex} + + \agda{agda/FFOL-I-27.tex} + \end{tcolorbox} 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. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/ICon.tex} + + \agda{agda/FFOL-I-28.tex} \agdasep - \agda{agda/ISub.tex} - \vspace{-13.5ex} - \begin{center}\rule{0.9\linewidth}{0.4pt}\end{center} - \vspace{-3ex} + \agda{agda/FFOL-I-30.tex} + + \agdasep + \begin{code} \>[4]\AgdaOperator{\AgdaField{\AgdaUnderscore{}[\AgdaUnderscore{}]p}}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% @@ -348,18 +341,18 @@ \AgdaBound{σ}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{]p}}\<% \end{code} - \vspace{-5ex} + \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. \begin{tcolorbox} - \vspace{-2ex} - \agda{agda/IIdComp.tex} - \vspace{-3ex} + + \agda{agda/FFOL-I-32.tex} + \agdasep - \agda{agda/ICExt.tex} - \vspace{-7.5ex} + \agda{agda/FFOL-I-33.tex} + \end{tcolorbox} \subsection{Transport Hell} diff --git a/report/header.tex b/report/header.tex index 012cf4c..2ce361b 100644 --- a/report/header.tex +++ b/report/header.tex @@ -108,7 +108,7 @@ % Agda Config \usepackage{agda} -%\AgdaNoSpaceAroundCode{} +\AgdaNoSpaceAroundCode{} \usepackage{newunicodechar} \newunicodechar{∘}{\ensuremath{\mathnormal{\circ}}} \newunicodechar{≡}{\ensuremath{\mathnormal{\equiv}}} diff --git a/stripAgda.awk b/stripAgda.awk new file mode 100644 index 0000000..323d95b --- /dev/null +++ b/stripAgda.awk @@ -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 + } +}