r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add "defined" status and distinguish Lean links.

finite-set-exercises
Joshua Potter 2023-05-10 20:19:18 -06:00
parent 9a879c90c1
commit 53a0bd1ebc
10 changed files with 45 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Bookshelf/Apostol/Chapter_1_11.tex
View File

@ -2,7 +2,7 @@
\input{../../preamble} \input{../../preamble}
\newcommand{\lean}[1]{\href \newcommand{\lean}[1]{\leanref
{./Chapter\_1\_11.html\#Apostol.Chapter\_1\_11.#1} {./Chapter\_1\_11.html\#Apostol.Chapter\_1\_11.#1}
{Apostol.Chapter\_1\_11.#1}} {Apostol.Chapter\_1\_11.#1}}

2
Bookshelf/Apostol/Chapter_I_03.tex
View File

@ -2,7 +2,7 @@
\input{../../preamble} \input{../../preamble}
\newcommand{\lean}[1]{\href \newcommand{\lean}[1]{\leanref
{./Chapter\_I\_03.html\#Apostol.Chapter\_I\_03.#1} {./Chapter\_I\_03.html\#Apostol.Chapter\_I\_03.#1}
{Apostol.Chapter\_I\_03.#1}} {Apostol.Chapter\_I\_03.#1}}

4
Bookshelf/Enderton/Chapter_0.tex
View File

@ -2,7 +2,7 @@
\input{../../preamble} \input{../../preamble}
\newcommand{\lean}[1]{\href \newcommand{\lean}[1]{\leanref
{./Chapter\_0.html\#Enderton.Chapter\_0.#1} {./Chapter\_0.html\#Enderton.Chapter\_0.#1}
{Enderton.Chapter\_0.#1}} {Enderton.Chapter\_0.#1}}
@ -10,7 +10,7 @@
\header{Useful Facts About Sets}{Herbert B. Enderton} \header{Useful Facts About Sets}{Herbert B. Enderton}
\section{\proceeding{Lemma 0A}}% \section*{\proceeding{Lemma 0A}}%
\hyperlabel{sec:lemma-0a}% \hyperlabel{sec:lemma-0a}%
Assume that $\langle x_1, \ldots, x_m \rangle = Assume that $\langle x_1, \ldots, x_m \rangle =

12
Common/Real/Geometry/Area.tex
View File

@ -2,7 +2,7 @@
\input{../../../preamble} \input{../../../preamble}
\newcommand{\lean}[2]{\href{./Area.html\##1}{#2}} \newcommand{\lean}[2]{\leanref{./Area.html\##1}{#2}}
\begin{document} \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 a set function $a$, whose domain is $\mathscr{M}$, with the following
properties: properties:
\section*{\verified{Nonnegative Property}}% \section*{\defined{Nonnegative Property}}%
\hyperlabel{sec:nonnegative-property}% \hyperlabel{sec:nonnegative-property}%
For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$. 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} \end{axiom}
\section*{\verified{Additive Property}}% \section*{\defined{Additive Property}}%
\hyperlabel{sec:additive-property}% \hyperlabel{sec:additive-property}%
If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in 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} \end{axiom}
\section*{\verified{Difference Property}}% \section*{\defined{Difference Property}}%
\hyperlabel{sec:difference-property}% \hyperlabel{sec:difference-property}%
If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in 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} \end{axiom}
\section*{\verified{Invariance Under Congruence}}% \section*{\defined{Invariance Under Congruence}}%
\hyperlabel{sec: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 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} \end{axiom}
\section*{\verified{Choice of Scale}}% \section*{\defined{Choice of Scale}}%
\label{sec:choice-scale} \label{sec:choice-scale}
Every rectangle $R$ is in $\mathscr{M}$. Every rectangle $R$ is in $\mathscr{M}$.

2
Common/Real/Sequence/Arithmetic.tex
View File

@ -2,7 +2,7 @@
\input{../../../preamble} \input{../../../preamble}
\newcommand{\lean}[1]{\href \newcommand{\lean}[1]{\leanref
{./Arithmetic.html\#Real.Arithmetic.#1} {./Arithmetic.html\#Real.Arithmetic.#1}
{Real.Arithmetic.#1}} {Real.Arithmetic.#1}}

2
Common/Real/Sequence/Geometric.tex
View File

@ -2,7 +2,7 @@
\input{../../../preamble} \input{../../../preamble}
\newcommand{\lean}[1]{\href \newcommand{\lean}[1]{\leanref
{./Geometric.html\#Real.Geometric.#1} {./Geometric.html\#Real.Geometric.#1}
{Real.Geometric.#1}} {Real.Geometric.#1}}

18
README.md
View File

@ -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 server behaves, refer to the `.env` file located in the root directory of this
project. 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 * Cyan statements indicate axioms and definitions. There must exist a
proof has been written in TeX and also formally verified in Lean. corresponding `axiom` or `def` in Lean.
* Magenta coloring indicates the corresponding proof is in progress. That is, a * Teal statements indicate those with complete proofs in both LaTeX *and* Lean.
proof in both TeX and Lean have not yet been finished, but is actively being * Magenta statements indicate those that have not been completely proven in
worked on. either LaTeX or Lean (or both). Progress is currently being made to correct
* Red coloring indicates the formal Lean proof has not yet been started. It may this though.
or may not also indicate the TeX proof has been written. * 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.

4
lake-manifest.json
View File

@ -16,9 +16,9 @@
{"git": {"git":
{"url": "https://github.com/jrpotter/bookshelf-docgen.git", {"url": "https://github.com/jrpotter/bookshelf-docgen.git",
"subDir?": null, "subDir?": null,
"rev": "87ecc512444afd073a2b201ef25caf3ef5fc74b1", "rev": "699f606df8f38c8abb287277df9e79669587c2b9",
"name": "doc-gen4", "name": "doc-gen4",
"inputRev?": "87ecc512444afd073a2b201ef25caf3ef5fc74b1"}}, "inputRev?": "699f606df8f38c8abb287277df9e79669587c2b9"}},
{"git": {"git":
{"url": "https://github.com/mhuisi/lean4-cli", {"url": "https://github.com/mhuisi/lean4-cli",
"subDir?": null, "subDir?": null,

2
lakefile.lean
View File

@ -12,7 +12,7 @@ require std4 from git
"6006307d2ceb8743fea7e00ba0036af8654d0347" "6006307d2ceb8743fea7e00ba0036af8654d0347"
require «doc-gen4» from git require «doc-gen4» from git
"https://github.com/jrpotter/bookshelf-docgen.git" @ "https://github.com/jrpotter/bookshelf-docgen.git" @
"87ecc512444afd073a2b201ef25caf3ef5fc74b1" "699f606df8f38c8abb287277df9e79669587c2b9"
@[default_target] @[default_target]
lean_lib «Bookshelf» { lean_lib «Bookshelf» {

26
preamble.tex
View File

@ -15,6 +15,7 @@
% ======================================== % ========================================
\hypersetup{colorlinks=true, urlcolor=blue} \hypersetup{colorlinks=true, urlcolor=blue}
\newcommand{\leanref}[2]{\color{blue}$\pmb{\exists}\;{-}\;$\href{#1}{#2}}
\newcommand{\hyperlabel}[1]{% \newcommand{\hyperlabel}[1]{%
\label{#1}% \label{#1}%
\hypertarget{#1}{}} \hypertarget{#1}{}}
@ -39,19 +40,32 @@
\begin{center} \begin{center}
\doublebox{ \doublebox{
\begin{minipage}{0.95\textwidth} \begin{minipage}{0.95\textwidth}
\vspace{2pt} \vspace{2pt}
\hl{Note:} #1 \hl{Note:} #1
\vspace{2pt} \vspace{2pt}
\end{minipage}} \end{minipage}}
\end{center}} \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 % Status
% progress, it's in a "proceeding" state. Otherwise it is unverified. % ========================================
% 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]{% \DeclareRobustCommand{\verified}[1]{%
\texorpdfstring{\color{teal}\faCheckCircle\ #1}{#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]{% \DeclareRobustCommand{\proceeding}[1]{%
\texorpdfstring{\color{magenta}\faDotCircle[regular]\ #1}{#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]{% \DeclareRobustCommand{\unverified}[1]{%
\texorpdfstring{\color{red}\faExclamationCircle\ #1}{#1}} \texorpdfstring{\color{red}\faExclamationCircle\ #1}{#1}}