polishing the chapter

MevenBertrand · May 25, 2022 · b2be2fe · b2be2fe
1 parent 63a152f
commit b2be2fe
Show file tree

Hide file tree

Showing 4 changed files with 273 additions and 177 deletions.
diff --git a/Manuscript/biblio.bib b/Manuscript/biblio.bib
@@ -3861,6 +3861,24 @@ @Thesis{Altenkirch1993
   priority    = {prio3},
 }
 
+@InProceedings{Appel2022,
+  author    = {Appel, Andrew W.},
+  booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+  date      = {2022},
+  title     = {Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk)},
+  doi       = {10.1145/3497775.3503951},
+  isbn      = {9781450391825},
+  location  = {Philadelphia, PA, USA},
+  pages     = {2–11},
+  publisher = {Association for Computing Machinery},
+  series    = {CPP 2022},
+  abstract  = {Program verification in the large is not only a matter of mechanizing a program logic to handle the semantics of your programming language. You must reason in the mathematics of your application domain--and there are many application domains, each with their own community of domain experts. So you will need to import mechanized proof theories from many domains, and they must all interoperate. Such an ecosystem is not only a matter of mathematics, it is a matter of software process engineering and social engineering. Coq's ecosystem has been maturing nicely in these senses.},
+  address   = {New York, NY, USA},
+  keywords  = {None, nil},
+  numpages  = {10},
+  priority  = {prio3},
+}
+
 @Comment{jabref-meta: databaseType:biblatex;}
 
 @Comment{jabref-meta: grouping:

diff --git a/Manuscript/knowledge_declarations.tex b/Manuscript/knowledge_declarations.tex
@@ -448,6 +448,7 @@
   | mode
   | modes
   | subject
+  | subjects
   | inputs
   | input
   | outputs
@@ -500,6 +501,22 @@
   | principal types
   | principal@type
 
+% Chapter 6
+
+\knowledge{notion}
+  | Generic conversion
+  | generic conversion
+
+\knowledge{notion}
+  | Neutral comparison
+  | neutral comparison
+
+\knowledge{notion}
+  | Generic cumulativity
+  | generic cumulativity
+
+
+
 % MetaCoq
 
 % MetaCoq Tour

diff --git a/Manuscript/styles/macros.sty b/Manuscript/styles/macros.sty
@@ -406,40 +406,49 @@ set fill color=DarkBlue!10,
 
 % Bidirectional conversion
 
-\knowledgenewrobustcmd{\bconvop}{\mathrel{\cmdkl{\cong}}}
-\knowledgenewrobustcmd{\convhop}{\mathrel{\cmdkl{\cong_{\symup{h}}}}}
-\knowledgenewrobustcmd{\bcumop}{\mathrel{\cmdkl{\preceq}}}
-\knowledgenewrobustcmd{\cumhop}{\mathrel{\cmdkl{\preceq_{\symup{h}}}}}
-\knowledgenewrobustcmd{\nconvop}{\mathrel{\cmdkl{\approx}}}
+\newcommand{\typedcolor}[1]{\mathcolor{DarkBlue}{#1}}
+\newcommand{\tycol}[1]{\typedcolor{#1}}
+\newcommand{\untypedcolor}[1]{\mathcolor{Purple}{#1}}
+\newcommand{\ucol}[1]{\untypedcolor{#1}}
+
+\knowledgenewrobustcmd{\bconvop}{\typedcolor{\cmdkl{\cong}}}
+\knowledgenewrobustcmd{\convhop}{\typedcolor{\cmdkl{\cong_{\symup{h}}}}}
+\knowledgenewrobustcmd{\bcumop}{\typedcolor{\cmdkl{\preceq}}}
+\knowledgenewrobustcmd{\cumhop}{\typedcolor{\cmdkl{\preceq_{\symup{h}}}}}
+\knowledgenewrobustcmd{\nconvop}{\typedcolor{\cmdkl{\approx}}}
 % \knowledgenewrobustcmd{\nconvhop}{\mathrel{\cmdkl{\approx_{\symup{h}}}}}
 
+\newcommand{\tinferty}[3]{#1 \typedcolor{\vdash_{\symup{t}}} #2 \typedcolor{\ity} #3}
+\newcommand{\tpinferty}[4]{#2 \typedcolor{\vdash_{\symup{t}}} #3 \typedcolor{\pity{#1}} #4}
+\newcommand{\tcheckty}[3]{#1 \typedcolor{\vdash_{\symup{t}}} #2 \typedcolor{\cty} #3}
+
 \NewDocumentCommand{\bconv}{m m m o}
-	{#1 \vdash #2 \bconvop #3 \cty \IfValueT{#4}{#4}}
+	{#1 \typedcolor{\vdash} #2 \mathrel{\bconvop} #3 \typedcolor{\cty} \IfValueT{#4}{#4}}
 \NewDocumentCommand{\convh}{m m m o}
-  {#1 \vdash #2 \convhop #3 \cty \IfValueT{#4}{#4}}
+  {#1 \typedcolor{\vdash} #2 \mathrel{\convhop} #3 \typedcolor{\cty} \IfValueT{#4}{#4}}
 \NewDocumentCommand{\bcum}{m m m}
-	{#1 \vdash #2 \bcumop #3 \cty}
+	{#1 \typedcolor{\vdash} #2 \mathrel{\bcumop} #3 \typedcolor{\cty}}
 \NewDocumentCommand{\cumh}{m m m}
-  {#1 \vdash #2 \cumhop #3 \cty}
-\newcommand{\nconv}[4]{#1 \vdash #2 \nconvop #3 \ity #4}
-\newcommand{\pnconv}[5]{#2 \vdash #3 \nconvop #4 \pity{#1} #5}
-
-% \NewDocumentCommand{\buconv}{m m m}
-% 	{#1 \vdash #2 \bconvop #3}
-% \NewDocumentCommand{\uconvh}{m m m}
-%   {#1 \vdash #2 \convhop #3}
-% \NewDocumentCommand{\bucum}{m m m}
-% 	{#1 \vdash #2 \bcumop #3}
-% \NewDocumentCommand{\ucumh}{m m m}
-%   {#1 \vdash #2 \cumhop #3}
-% \newcommand{\nuconv}[3]{#1 \vdash #2 \nconvop #3}
+  {#1 \typedcolor{\vdash} #2 \mathrel{\cumhop} #3 \typedcolor{\cty}}
+\newcommand{\nconv}[4]{#1 \typedcolor{\vdash} #2 \mathrel{\nconvop} #3 \typedcolor{\ity} #4}
+\newcommand{\pnconv}[5]{#2 \typedcolor{\vdash} #3 \mathrel{\nconvop} #4 \typedcolor{\pity{#1}} #5}
+
+\newcommand{\uinferty}[3]{#1 \untypedcolor{\vdash_{\symup{u}}} #2 \untypedcolor{\ity} #3}
+\newcommand{\upinferty}[4]{#2 \untypedcolor{\vdash_{\symup{u}}} #3 \untypedcolor{\pity{#1}} #4}
+\newcommand{\ucheckty}[3]{#1 \untypedcolor{\vdash_{\symup{u}}} #2 \untypedcolor{\cty} #3}
+
+\knowledgenewrobustcmd{\buconvop}{\untypedcolor{\cmdkl{\cong}}}
+\knowledgenewrobustcmd{\uconvhop}{\untypedcolor{\cmdkl{\cong_{\symup{h}}}}}
+\knowledgenewrobustcmd{\bucumop}{\untypedcolor{\cmdkl{\preceq}}}
+\knowledgenewrobustcmd{\ucumhop}{\untypedcolor{\cmdkl{\preceq_{\symup{h}}}}}
+\knowledgenewrobustcmd{\nuconvop}{\untypedcolor{\cmdkl{\approx}}}
 
 \NewDocumentCommand{\buconv}{m m m}
-	{#2 \bconvop #3}
+	{#2 \mathrel{\buconvop} #3}
 \NewDocumentCommand{\uconvh}{m m m}
-  {#2 \convhop #3}
+  {#2 \mathrel{\uconvhop} #3}
 \NewDocumentCommand{\bucum}{m m m}
-	{#2 \bcumop #3}
+	{#2 \mathrel{\bucumop} #3}
 \NewDocumentCommand{\ucumh}{m m m}
-  {#2 \cumhop #3}
-\newcommand{\nuconv}[3]{#2 \nconvop #3}
+  {#2 \mathrel{\ucumhop} #3}
+\newcommand{\nuconv}[3]{#2 \mathrel{\nuconvop} #3}