From e9eedbff2da0bb76787296c91a5c648743ba7816 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Sun, 30 Jul 2023 19:07:51 +0200 Subject: [PATCH] Added Agda code in latex, plus beginning of an introduction --- .gitignore | 3 + FFOL.agda => FFOL.lagda | 61 ++++++---- FFOLInitial.agda => FFOLInitial.lagda | 23 ++-- Makefile | 57 +++++++++ report/M1Report.tex | 160 +++++++++++++++++++++++++- report/header.tex | 49 ++++++-- 6 files changed, 311 insertions(+), 42 deletions(-) rename FFOL.agda => FFOL.lagda (89%) rename FFOLInitial.agda => FFOLInitial.lagda (99%) create mode 100644 Makefile diff --git a/.gitignore b/.gitignore index 867ffb9..0378d97 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,6 @@ .\#* *.kate-swp /report/build/ +/report/agda/ +/report/agda.sty +/latex diff --git a/FFOL.agda b/FFOL.lagda similarity index 89% rename from FFOL.agda rename to FFOL.lagda index 29eb939..2058d2d 100644 --- a/FFOL.agda +++ b/FFOL.lagda @@ -1,3 +1,4 @@ +\begin{code} {-# OPTIONS --prop --rewriting #-} open import PropUtil @@ -19,7 +20,8 @@ module FFOL where Con : Set ℓ¹ Sub : Con → Con → Set ℓ⁵ -- It makes a category _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ - ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α) + ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} + → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α) id : {Γ : Con} → Sub Γ Γ idl : {Γ Δ : Con} {σ : Sub Γ Δ} → (id {Δ}) ∘ σ ≡ σ idr : {Γ Δ : Con} {σ : Sub Γ Δ} → σ ∘ (id {Γ}) ≡ σ @@ -29,9 +31,10 @@ module FFOL where -- Functor Con → Set called Tm Tm : Con → Set ℓ² - _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms + _[_]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 + []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ}{β : Sub Δ Γ} → {t : Tm Γ} + → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t -- Tm : Set⁺ _▹ₜ : Con → Con @@ -41,56 +44,67 @@ module FFOL where πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ - ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t) + ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} + → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t) -- Functor Con → Set called For For : Con → Set ℓ³ - _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms + _[_]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 + []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} + → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f -- Functor Con × For → Prop called Pf or ⊢ _⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴ - _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms + -- Action on morphisms + _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- 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 + -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} + -- → prf [ id {Γ} ]p ≡ prf + -- []p-∘ : {Γ Δ Ξ : Con}{α : Sub Ξ Δ}{β : Sub Δ Γ}{F : For Γ}{prf : Γ ⊢ F} + -- → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p -- → Prop⁺ _▹ₚ_ : (Γ : Con) → For Γ → Con - πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ - πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) - _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) - ,ₚ∘πₚ : {Γ Δ : Con} → {F : For Γ} → {σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ - πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ (σ ,ₚ prf) ≡ σ + πₚ¹ : {Γ Δ : Con}{F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ + πₚ² : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) + _,ₚ_ : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) + ,ₚ∘πₚ : {Γ Δ : Con}{F : For Γ}{σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ + πₚ¹∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Δ ⊢ (F [ σ ]f)} + → πₚ¹ (σ ,ₚ prf) ≡ σ -- Equality below is useless because Γ ⊢ F is in Prop - -- πₚ²∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ² (σ ,ₚ prf) ≡ prf - ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} → (σ ,ₚ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym []f-∘) (prf [ δ ]p)) + -- πₚ²∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Δ ⊢ (F [ σ ]f)} + -- → πₚ² (σ ,ₚ prf) ≡ prf + ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} + → (σ ,ₚ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym []f-∘) (prf [ δ ]p)) {-- FORMULAE CONSTRUCTORS --} -- 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) + R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ} + → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t) -- Implication _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ - []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f) + []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} + → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f) -- Forall ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ - []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f)) + []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 : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G) - app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G + lam : {Γ : Con}{F G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G) + app : {Γ : Con}{F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G -- ∀i and ∀e - ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) - ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) + ∀i : {Γ : Con}{F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) + ∀e : {Γ : Con}{F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) -- Examples @@ -363,3 +377,4 @@ module FFOL where -- (((∀ 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)) +\end{code} diff --git a/FFOLInitial.agda b/FFOLInitial.lagda similarity index 99% rename from FFOLInitial.agda rename to FFOLInitial.lagda index c1d975b..0463ec5 100644 --- a/FFOLInitial.agda +++ b/FFOLInitial.lagda @@ -1,3 +1,4 @@ +\begin{code} {-# OPTIONS --prop --rewriting #-} open import PropUtil @@ -219,8 +220,8 @@ module FFOLInitial where -- We now can create Renamings, a subcategory from (Conp,Subp) that - -- A renaming from a context Γₚ to a context Δₚ means that when they are seen as lists, - -- that every element of Γₚ is an element of Δₚ + -- 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) data Ren : Conp Γₜ → Conp Γₜ → Set₁ where zeroRen : Ren ◇p Γₚ @@ -722,24 +723,26 @@ module FFOLInitial where (substP (λ X → (M FFOL.▹ₚ (M FFOL.▹ₜ) (mCon (con Γₜ Γₚ))) X ≡ (M FFOL.▹ₜ) ((M FFOL.▹ₚ mCon (con Γₜ Γₚ)) (mFor A))) (≡tran (coeshift {!!}) - (cong (λ X → subst (FFOL.For M) _ (FFOL._[_]f M (mFor A) (mSub (sub (wkₜσₜ idₜ) X)))) (≡sym (coecoe-coe {eq1 = ?} {x = idₚ {Δₚ = Γₚ}})))) + (cong (λ X → subst (FFOL.For M) _ (FFOL._[_]f M (mFor A) (mSub (sub (wkₜσₜ idₜ) X)))) (≡sym (coecoe-coe {eq1 = {!!}} {x = idₚ {Δₚ = Γₚ}})))) {!!}) (cong (M FFOL.▹ₜ) (≡sym (e▹ₚ {con Γₜ Γₚ}))) -- substP (λ X → FFOL._▹ₚ_ M X (mFor {Γ = ?} (A [ wkₜσₜ idₜ ]f)) ≡ (FFOL._▹ₜ M (mCon (con Γₜ (Γₚ ▹p⁰ A))))) (≡sym (e▹ₜ {Γ = con Γₜ Γₚ})) ? - - - {- - - m⊢ {Γ}{A}(var pvzero) = {!substP (λ X → FFOL._⊢_ M X (mFor A)) (≡sym e▹ₚ) ?!} m⊢ (var (pvnext pv)) = {!!} m⊢ (app pf pf') = FFOL.app M (m⊢ pf) (m⊢ pf') m⊢ (lam pf) = FFOL.lam M {!m⊢ pf!} m⊢ (p∀∀e pf) = {!FFOL.∀e M (m⊢ pf)!} m⊢ {Γ}{∀∀ A}(p∀∀i pf) = FFOL.∀i M (substP (λ X → FFOL._⊢_ M X (subst (FFOL.For M) (≡sym e▹ₜ) (mFor A))) e▹ₜ {!m⊢ pf!}) - + e[]f = {!!} + e▹ₚ = {!!} + + + {- + + + e∘ : {Γ Δ Ξ : Con}{δ : Sub Δ Ξ}{σ : Sub Γ Δ} → mSub (δ ∘ σ) ≡ FFOL._∘_ M (mSub δ) (mSub σ) @@ -779,7 +782,7 @@ module FFOLInitial where --mor : (M : FFOL) → Morphism ffol M --mor M = record {InitialMorphism M} - +\end{code} diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..7a4a79b --- /dev/null +++ b/Makefile @@ -0,0 +1,57 @@ +define extract + cat $(1) | grep -A5000 -m1 $(3) | grep -B5000 -m1 $(4) | head -n -1 | sed 's/\\>\[6\]/\\>\[0\]/g' > $(2) +endef + +all: report/build/M1Report.pdf + +latex/FFOL.tex: FFOL.lagda + agda --latex $< + cp latex/agda.sty report/agda.sty +latex/FFOLInitial.tex: FFOLInitial.lagda + agda --latex --allow-unsolved-metas $< + cp latex/agda.sty report/agda.sty + +report/build/M1Report.pdf: agda-tex-FFOL agda-tex-FIni + $(cd report/; latexmk -pdf -xelatex -silent -shell-escape -outdir=build/ -synctex=1 "M1Report") + +agda-tex-FIni: latex/FFOLInitial.tex + mkdir -p report/agda + @$(call extract,latex/FFOLInitial.tex,report/agda/ICont.tex,'Term\\ contexts\\ are\\ isomorphic\\ to\\ Nat','\\>\[0\]\\<') + @$(call extract,latex/FFOLInitial.tex,report/agda/ITm.tex,'A\\ term\\ variable\\ is\\ a\\ de-bruijn','\\>\[0\]\\<') + @$(call extract,latex/FFOLInitial.tex,report/agda/IFor.tex,'Now\\ we\\ can\\ define\\ formul','\\>\[0\]\\<') + @$(call extract,latex/FFOLInitial.tex,report/agda/ISubt.tex,'Then\\ we\\ define\\ term\\ substitutions','\\>\[0\]\\<') + @$(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}}','\\>\[0\]\\<') + @$(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','\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}') + @$(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") + +.PHONY: clean agda-tex agda-tex-FFOL +clean: + rm -fr *.agdai report/agda latex report/build diff --git a/report/M1Report.tex b/report/M1Report.tex index 3c1d493..3bb1c1f 100644 --- a/report/M1Report.tex +++ b/report/M1Report.tex @@ -1,4 +1,4 @@ -% !TeX spellcheck = fr_FR +% !TeX spellcheck = en_US \documentclass[10pt,a4paper]{article} \include{./header.tex} @@ -21,8 +21,17 @@ \newpage + \section{Introduction} + + In the first place, i was supposed to do this internship in Nottingham (UK) with Thorsten Altenkirsh. But, because of administrative issues, i was not able to go there, and Thorsten Altenkirsh contacted Ambrus Kaposi in Budapest, whose university agreed to accept me. Therefore, i went to Budapest and i did the internship under the physical supervision of Ambrus Kaposi, and the remote supervision of Thorsten Altenkirsch. + + The original subject of the internship was \enquote{Developping a simplified account of normalization by evaluation using the theory of categories with families}. But there was a lot to do, starting with learning how to use Agda. + \subsection{Introduction to the problem} + What i do call a \enquote{logic} is a set of definitions containing formulæ and a notion of provability of those formulæ, plus a set of operators/equalities to construct or reduce these rules. I have studied the most common logical frameworks, that is, Propositional Logic, First-order logic with infinitary predicates, and Predicate Logic. For each of those logics, one can define a notion of \emph{model}. A model of a certain kind of logic is something that implements all of the logic's definitions, operators and equalities. From all of those models, one can extract the \emph{initial model}, also called \emph{syntax}. It is the smallest of all models, which means that from any model of that logic, we have a morphism from the syntax to that model. + + Then, our goal is for each logic to prove the completeness of a specific class of models. Completeness can be stated as such: \enquote{For any formula that is \emph{true} in all models of the specified class, then the formula has a proof in the syntax}. By being true in the model, one can understand that the formula has a proof from the model. \subsection{Motivation} \subsection{Structure of this report} \section{A first account of Completeness and Normalization} @@ -31,11 +40,158 @@ \subsection{Merging the two proofs} \section{Predicate Logic} \subsection{SOGAT Presentation of FFOL} + + \begin{tcolorbox} + \[ + \begin{array}{lcl} + \Tm & : & \Set^+ \\ + \\ + \For & : & \Set \\ + - \implies - & : & \For \rightarrow \For \rightarrow \For\\ + \forall & : & (\Tm \rightarrow \For) \rightarrow \For \\ + \R & : & \Tm \rightarrow \Tm \rightarrow \For\\ + \\ + \Pf & : & \For \rightarrow \Prop^+ \\ + \lam & : & (\Pf A \rightarrow \Pf B) \rightarrow \Pf (A \implies B)\\ + \app & : & \Pf (A \implies B) \rightarrow (\Pf A \rightarrow \Pf B)\\ + \foralli & : & (t : \Tm \rightarrow^+ A\;t) \rightarrow \Pf (\forall A)\\ + \foralle & : & \Pf (\forall A) \rightarrow (t : \Tm) \rightarrow \Pf (A\;t)\\ + \end{array} + \] + \end{tcolorbox} + \subsection{Turning a SOGAT Presentation into a GAT} + \begin{tcolorbox} + \agda{agda/Con.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/Tm.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/Tm+.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/For.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/Pf.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/Pf+.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/R.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/Imp.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/Forall.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/LamApp.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ForallR.tex} + \end{tcolorbox} + \section{Implementing the Syntax} \subsection{Separated Contexts} + + \begin{tcolorbox} + \agda{agda/ICont.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IFor.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubt.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ITm.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubtT.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubTF.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IIdCompT.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IConp.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubtC.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IConpTp.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IPf.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IRen.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubp.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubtP.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubtS.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISubpP.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IIdCompP.tex} + \end{tcolorbox} + \begin{tcolorbox} + \agda{agda/ICon.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ISub.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/IIdComp.tex} + \end{tcolorbox} + + \begin{tcolorbox} + \agda{agda/ICExt.tex} + \end{tcolorbox} + \subsection{Transport Hell} - %\section{Completeness and Normalization for FFOL} \section{Summary} diff --git a/report/header.tex b/report/header.tex index 381017e..239dba8 100644 --- a/report/header.tex +++ b/report/header.tex @@ -1,6 +1,5 @@ -% Loading packages -\usepackage[T1]{fontenc} -\usepackage[utf8]{inputenc} +% Loading packages +\usepackage{autofe} \usepackage{hyperref} \hypersetup{ colorlinks=true, @@ -16,7 +15,6 @@ \usepackage{csquotes} \usepackage{listings} \usepackage{lstautogobble} -\usepackage{algorithm2e} \usepackage{svg} \usepackage{tikz} \usepackage{multirow} @@ -34,6 +32,7 @@ \usepackage{mathtools} \usepackage[page,header]{appendix} \usepackage{minitoc} +\usepackage{mathtools} \usepackage{geometry} @@ -59,9 +58,6 @@ \def\nDownarrow{\not\mspace{1mu}\Downarrow} \let\pprec\preccurlyeq -\DeclareUnicodeCharacter{03BB}{$\lambda$} -\DeclareUnicodeCharacter{03B1}{$\alpha$} -\DeclareUnicodeCharacter{03C0}{$\pi$} % Création des environnement globaux \newtheorem{theorem}{Théorème} @@ -95,7 +91,46 @@ % Macros caractères spécifiques au document +\newcommand\Tm{\operatorname{Tm}} +\newcommand\Set{\operatorname{Set}} +\newcommand\For{\operatorname{For}} +\newcommand\Prop{\operatorname{Prop}} +\newcommand\R{\operatorname{R}} +\newcommand\lam{\operatorname{lam}} +\newcommand\app{\operatorname{app}} +\newcommand\foralli{\operatorname{\operatorname{\forall i}}} +\newcommand\foralle{\operatorname{\operatorname{\forall e}}} +\newcommand\Pf{\operatorname{Pf}\;} +% Agda Config +\usepackage{agda} +\usepackage{newunicodechar} +\newunicodechar{∘}{\ensuremath{\mathnormal{\circ}}} +\newunicodechar{≡}{\ensuremath{\mathnormal{\equiv}}} +\newunicodechar{◇}{\ensuremath{\mathnormal{\diamond}}} +\newunicodechar{α}{\ensuremath{\mathnormal{\alpha}}} +\newunicodechar{β}{\ensuremath{\mathnormal{\beta}}} +\newunicodechar{γ}{\ensuremath{\mathnormal{\gamma}}} +\newunicodechar{δ}{\ensuremath{\mathnormal{\delta}}} +\newunicodechar{ε}{\ensuremath{\mathnormal{\varepsilon}}} +\newunicodechar{σ}{\ensuremath{\mathnormal{\sigma}}} +\newunicodechar{π}{\ensuremath{\mathnormal{\pi}}} +\newunicodechar{▹}{\ensuremath{\mathnormal{\triangleright}}} +\newunicodechar{⊢}{\ensuremath{\mathnormal{\vdash}}} +\newunicodechar{⇒}{\ensuremath{\mathnormal{\Rightarrow}}} +\newunicodechar{∀}{\ensuremath{\mathnormal{\forall}}} +\newunicodechar{≈}{\ensuremath{\mathnormal{\approx}}} +\newunicodechar{ₜ}{\ensuremath{{}_t}} +\newunicodechar{ₚ}{\ensuremath{{}_p}} +\newunicodechar{⁰}{\ensuremath{{}^0}} + + +\newcommand\agda[1]{ + \small + \begin{code} + \input{#1} + \end{code} +} % Création des environnements spécifiques au document