From 53a0bd1ebc189cb6bd5e72ad100b9419a82bae6c Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 10 May 2023 20:19:18 -0600 Subject: [PATCH] Add "defined" status and distinguish Lean links. --- Bookshelf/Apostol/Chapter_1_11.tex | 2 +- Bookshelf/Apostol/Chapter_I_03.tex | 2 +- Bookshelf/Enderton/Chapter_0.tex | 4 ++-- Common/Real/Geometry/Area.tex | 12 ++++++------ Common/Real/Sequence/Arithmetic.tex | 2 +- Common/Real/Sequence/Geometric.tex | 2 +- README.md | 18 ++++++++++-------- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- preamble.tex | 26 ++++++++++++++++++++------ 10 files changed, 45 insertions(+), 29 deletions(-) diff --git a/Bookshelf/Apostol/Chapter_1_11.tex b/Bookshelf/Apostol/Chapter_1_11.tex index 09325f6..31f27e9 100644 --- a/Bookshelf/Apostol/Chapter_1_11.tex +++ b/Bookshelf/Apostol/Chapter_1_11.tex @@ -2,7 +2,7 @@ \input{../../preamble} -\newcommand{\lean}[1]{\href +\newcommand{\lean}[1]{\leanref {./Chapter\_1\_11.html\#Apostol.Chapter\_1\_11.#1} {Apostol.Chapter\_1\_11.#1}} diff --git a/Bookshelf/Apostol/Chapter_I_03.tex b/Bookshelf/Apostol/Chapter_I_03.tex index 695b893..20f2dc0 100644 --- a/Bookshelf/Apostol/Chapter_I_03.tex +++ b/Bookshelf/Apostol/Chapter_I_03.tex @@ -2,7 +2,7 @@ \input{../../preamble} -\newcommand{\lean}[1]{\href +\newcommand{\lean}[1]{\leanref {./Chapter\_I\_03.html\#Apostol.Chapter\_I\_03.#1} {Apostol.Chapter\_I\_03.#1}} diff --git a/Bookshelf/Enderton/Chapter_0.tex b/Bookshelf/Enderton/Chapter_0.tex index 4500a54..24f8a4e 100644 --- a/Bookshelf/Enderton/Chapter_0.tex +++ b/Bookshelf/Enderton/Chapter_0.tex @@ -2,7 +2,7 @@ \input{../../preamble} -\newcommand{\lean}[1]{\href +\newcommand{\lean}[1]{\leanref {./Chapter\_0.html\#Enderton.Chapter\_0.#1} {Enderton.Chapter\_0.#1}} @@ -10,7 +10,7 @@ \header{Useful Facts About Sets}{Herbert B. Enderton} -\section{\proceeding{Lemma 0A}}% +\section*{\proceeding{Lemma 0A}}% \hyperlabel{sec:lemma-0a}% Assume that $\langle x_1, \ldots, x_m \rangle = diff --git a/Common/Real/Geometry/Area.tex b/Common/Real/Geometry/Area.tex index b58d338..138324c 100644 --- a/Common/Real/Geometry/Area.tex +++ b/Common/Real/Geometry/Area.tex @@ -2,7 +2,7 @@ \input{../../../preamble} -\newcommand{\lean}[2]{\href{./Area.html\##1}{#2}} +\newcommand{\lean}[2]{\leanref{./Area.html\##1}{#2}} \begin{document} @@ -12,7 +12,7 @@ We assume there exists a class $\mathscr{M}$ of measurable sets in the plane and a set function $a$, whose domain is $\mathscr{M}$, with the following properties: -\section*{\verified{Nonnegative Property}}% +\section*{\defined{Nonnegative Property}}% \hyperlabel{sec:nonnegative-property}% For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$. @@ -23,7 +23,7 @@ For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$. \end{axiom} -\section*{\verified{Additive Property}}% +\section*{\defined{Additive Property}}% \hyperlabel{sec:additive-property}% If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in @@ -35,7 +35,7 @@ If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in \end{axiom} -\section*{\verified{Difference Property}}% +\section*{\defined{Difference Property}}% \hyperlabel{sec:difference-property}% If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in @@ -47,7 +47,7 @@ If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in \end{axiom} -\section*{\verified{Invariance Under Congruence}}% +\section*{\defined{Invariance Under Congruence}}% \hyperlabel{sec:invariance-under-congruence}% If a set $S$ is in $\mathscr{M}$ and if $T$ is congruent to $S$, then $T$ is @@ -59,7 +59,7 @@ If a set $S$ is in $\mathscr{M}$ and if $T$ is congruent to $S$, then $T$ is \end{axiom} -\section*{\verified{Choice of Scale}}% +\section*{\defined{Choice of Scale}}% \label{sec:choice-scale} Every rectangle $R$ is in $\mathscr{M}$. diff --git a/Common/Real/Sequence/Arithmetic.tex b/Common/Real/Sequence/Arithmetic.tex index 12389c6..6d00dca 100644 --- a/Common/Real/Sequence/Arithmetic.tex +++ b/Common/Real/Sequence/Arithmetic.tex @@ -2,7 +2,7 @@ \input{../../../preamble} -\newcommand{\lean}[1]{\href +\newcommand{\lean}[1]{\leanref {./Arithmetic.html\#Real.Arithmetic.#1} {Real.Arithmetic.#1}} diff --git a/Common/Real/Sequence/Geometric.tex b/Common/Real/Sequence/Geometric.tex index 0df893f..9a5611e 100644 --- a/Common/Real/Sequence/Geometric.tex +++ b/Common/Real/Sequence/Geometric.tex @@ -2,7 +2,7 @@ \input{../../../preamble} -\newcommand{\lean}[1]{\href +\newcommand{\lean}[1]{\leanref {./Geometric.html\#Real.Geometric.#1} {Real.Geometric.#1}} diff --git a/README.md b/README.md index be6ba94..9a6beb4 100644 --- a/README.md +++ b/README.md @@ -28,12 +28,14 @@ This assumes you have `python3` available in your `$PATH`. To change how the server behaves, refer to the `.env` file located in the root directory of this project. -A color/symbol code is used on generated PDF headers to indicate their status: +A color code is used on generated PDF headers to indicate their status: -* Teal coloring indicates the corresponding proof is complete. That is, the - proof has been written in TeX and also formally verified in Lean. -* Magenta coloring indicates the corresponding proof is in progress. That is, a - proof in both TeX and Lean have not yet been finished, but is actively being - worked on. -* Red coloring indicates the formal Lean proof has not yet been started. It may - or may not also indicate the TeX proof has been written. +* Cyan statements indicate axioms and definitions. There must exist a + corresponding `axiom` or `def` in Lean. +* Teal statements indicate those with complete proofs in both LaTeX *and* Lean. +* Magenta statements indicate those that have not been completely proven in + either LaTeX or Lean (or both). Progress is currently being made to correct + this though. +* Red coloring is a catch-all for all statements that don't fit the above + categorizations. Incomplete definitions, proofs only conducted in LaTeX, etc. + belong here. diff --git a/lake-manifest.json b/lake-manifest.json index 94d4ece..779a1a0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -16,9 +16,9 @@ {"git": {"url": "https://github.com/jrpotter/bookshelf-docgen.git", "subDir?": null, - "rev": "87ecc512444afd073a2b201ef25caf3ef5fc74b1", + "rev": "699f606df8f38c8abb287277df9e79669587c2b9", "name": "doc-gen4", - "inputRev?": "87ecc512444afd073a2b201ef25caf3ef5fc74b1"}}, + "inputRev?": "699f606df8f38c8abb287277df9e79669587c2b9"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 1ed3b44..96f0031 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,7 +12,7 @@ require std4 from git "6006307d2ceb8743fea7e00ba0036af8654d0347" require «doc-gen4» from git "https://github.com/jrpotter/bookshelf-docgen.git" @ - "87ecc512444afd073a2b201ef25caf3ef5fc74b1" + "699f606df8f38c8abb287277df9e79669587c2b9" @[default_target] lean_lib «Bookshelf» { diff --git a/preamble.tex b/preamble.tex index 502fc5b..cde5b39 100644 --- a/preamble.tex +++ b/preamble.tex @@ -15,6 +15,7 @@ % ======================================== \hypersetup{colorlinks=true, urlcolor=blue} +\newcommand{\leanref}[2]{\color{blue}$\pmb{\exists}\;{-}\;$\href{#1}{#2}} \newcommand{\hyperlabel}[1]{% \label{#1}% \hypertarget{#1}{}} @@ -39,19 +40,32 @@ \begin{center} \doublebox{ \begin{minipage}{0.95\textwidth} - \vspace{2pt} - \hl{Note:} #1 - \vspace{2pt} + \vspace{2pt} + \hl{Note:} #1 + \vspace{2pt} \end{minipage}} \end{center}} -% Status of a proof. A statement/theorem is verified if both a LaTeX proof -% and a corresponding Lean proof has been written. If a Lean proof is in -% progress, it's in a "proceeding" state. Otherwise it is unverified. +% ======================================== +% Status +% ======================================== + +% Indicates a statement corresponds to an axiom or definition. There must exist +% a corresponding `axiom` or `def` in Lean. +\DeclareRobustCommand{\defined}[1]{% + \texorpdfstring{\color{cyan}\faParagraph\ #1}{#1}} + +% Indicates a statement has a complete proof in both LaTeX *and* Lean. \DeclareRobustCommand{\verified}[1]{% \texorpdfstring{\color{teal}\faCheckCircle\ #1}{#1}} + +% Indicates a statement has not been completely proven in either LaTeX or +% Lean (or both). Progress is currently being made to correct this though. \DeclareRobustCommand{\proceeding}[1]{% \texorpdfstring{\color{magenta}\faDotCircle[regular]\ #1}{#1}} + +% A catch-all status for anything that doesn't fit the above categories. +% Incomplete definitions, proofs only conducted in LaTeX, etc. belong here. \DeclareRobustCommand{\unverified}[1]{% \texorpdfstring{\color{red}\faExclamationCircle\ #1}{#1}}