diff options
author | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
commit | e0c6872cf40896c7be36b11dcc744620f10adf1d (patch) | |
tree | 60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/prftree/prftreedoc.tex |
Initial commit
Diffstat (limited to 'macros/latex/contrib/prftree/prftreedoc.tex')
-rw-r--r-- | macros/latex/contrib/prftree/prftreedoc.tex | 2425 |
1 files changed, 2425 insertions, 0 deletions
diff --git a/macros/latex/contrib/prftree/prftreedoc.tex b/macros/latex/contrib/prftree/prftreedoc.tex new file mode 100644 index 0000000000..19477fa856 --- /dev/null +++ b/macros/latex/contrib/prftree/prftreedoc.tex @@ -0,0 +1,2425 @@ +\documentclass{amsart} +\usepackage{color} +\usepackage{graphics} +\usepackage[ND,SEQ,EQ,ML]{prftree} +\usepackage{url} +\usepackage{microtype} + +\setlength{\fboxsep}{0pt} + +\begin{document} +\title{Proof Trees in \LaTeX} +\date{} +\author{Marco Benini} +\address{Dipartimento di Scienza e Alta Tecnologia\\ + Universit\`a degli Studi dell'Insubria\\ + via Valleggio 11, I-22100 Como, Italy} +\email{marco.benini@uninsubria.it} +\urladdr{http://marcobenini.wordpress.com} +\maketitle + +% -------------------------- + +\section{Introduction}\label{sec:introduction} +Writing proofs in natural deduction or in similar, tree-like calculi, +is always a challenge: from the typographical point of view, these +proofs are complex objects that cannot be simply typeset using the +standard \LaTeX{} commands. Thus, many packages have been developed: +Sam Buss's \texttt{bussproofs.sty}, +\url{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}; Makoto +Tatsuta's \texttt{proof.sty}, +\url{http://research.nii.ac.jp/~tatsuta/proof-sty.html}; and +\texttt{prooftree.sty} by Paul Taylor, +\url{http://mirror.ctan.org/macros/generic/proofs/taylor}. + +All these packages have their merits and weaknesses. For example, +Buss's package is extremely flexible but inference rules with more +than five assumptions cannot be directly typeset. On the other hand, +Tatsuta's package provides a very simple set of commands doing a +fine job, but customisation is very limited. Taylor's package provides +a natural syntax for writing proofs, but customisation is limited, and +the package has an expire date. + +The package presented in the following provides most of the features +which are already present in Buss's package, coupled with some new +ones. This package uses a syntax which is closer to Tatsuta's one, but +almost all the typesetting process is parametric, so that each bit of +a proof can be customised at will. + +The graphical appearance of a proof is similar to the one obtained +using Taylor's package, but the additional features allow to set up +the graphical output to follow the style of some of the standard +textbooks, e.g., A.S.~Troelstra and H.~Schwichtenberg, \textit{Basic + Proof Theory}, Cambridge University Press (2000). + +% -------------------------- +\clearpage +\section{Basic Commands}\label{sec:basic_commands} +The package is invoked by putting \verb|\usepackage{prftree.sty}| in +the preamble of the document, and installation reduces to put the file +\texttt{prftree.sty} somewhere in the \LaTeX{} search +path.\vspace{2ex} + +A proof tree constructs a box with the following internal structure: +\begin{center} + {\setlength{\unitlength}{1em} + \begin{picture}(31,6) + \put(7,4){\framebox(17,2){$\mbox{assumption}_1 \cdots + \mbox{assumption}_n$}} + \put(6,3){\line(1,0){19}} + \put(26,2){\framebox(5,2){rule name}} + \put(0,2){\framebox(5,2){label}} + \put(10,0){\framebox(11,2){conclusion}} + \end{picture}} +\end{center} +In turn, each assumption is typeset as a box which has usually the +shape of another proof tree, while the rule name and the label are +typeset in a text box, and the conclusion in a math box. The aspect of +the proof line is controlled by suitable options, as is the presence +of the rule name and of the label. Options cover other aspects of the +graphical rendering of a proof tree, as it will be explained +later. The basic command to build a proof tree is \verb|\prftree|. + +For example, the proof of $A \supset \neg\neg A$ in natural deduction +is: +\begin{displaymath} + \prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{E}$} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{displaymath} +This proof is generated by the following \LaTeX{} code: +\begin{verbatim} + \begin{displaymath} + \prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{E}$} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} + \end{displaymath} +\end{verbatim} + +In general, the syntax of the \verb|\prftree| command is: +\begin{displaymath} + \verb|\prftree|[\mbox{options}] \cdots + [\mbox{options}]\{\mbox{assumption}_1\} \cdots + \{\mbox{assumption}_n\}\{\mbox{conclusion}\} +\end{displaymath} +Assumptions are optional and there may be any number of them. Each +assumption may contain a proof tree, which is typeset independently: +the order allows to use indentation to help reading the source. The +conclusion is mandatory, and it is supposed to be a +formula. + +Assumptions and the conclusion are typeset in a display style math +environment. Options control the way the proof is generated: in the +example, the \verb|r| option has been used to signal that the first +argument of \verb|\prftree| is the name of the inference rule. + +The available options are: +\begin{itemize} +\item\ [\textbf{r}], [\textbf{rule}], [\textbf{by rule}], + [\textbf{by}], [\textbf{right}]: the first argument after the + options is the rule name, which is typeset in text mode; +\item\ [\textbf{l}], [\textbf{left}], [\textbf{label}]: the first + argument after the options is the label of the rule, which is + typeset in text mode. If a rule name is present, the first argument + is the rule name, and the second one is the label; +\item\ [\textbf{straight}], [\textbf{straight line}], + [\textbf{straightline}]: makes the proof line solid; +\item\ [\textbf{dotted}], [\textbf{dotted line}], + [\textbf{dottedline}]: makes the proof line dotted; +\item\ [\textbf{dashed}], [\textbf{dashed line}], + [\textbf{dashedline}]: makes the proof line dashed; +\item\ [\textbf{f}], [\textbf{fancy}], [\textbf{fancy line}], + [\textbf{fancyline}]: the proof line will be fancy; +\item\ [\textbf{s}], [\textbf{single}], [\textbf{single line}], + [\textbf{singleline}]: makes the proof line single; +\item\ [\textbf{d}], [\textbf{double}], [\textbf{double line}], + [\textbf{doubleline}]: makes the proof line double; +\item\ [\textbf{noline}]: suppresses the proof line (prevails over all + other line options); +\item\ [\textbf{summary}]: renders the proof line as the summary + symbol (prevails over all other line options except \textbf{noline}). +\end{itemize} +By default the proof line is straight and single. Options may be +written in sequence, as in \verb|[r,f,d]|, which means that the proof +tree will have a rule name, and the proof line will be fancy and +double, or separately, as in \verb|[r][f][d]|, or even as a +combination, like \verb|[r][f,d]|. Options are evaluated +left-to-right, so \verb|[d,s]| is the same as \verb|[s]|, while +\verb|[noline,straight,d]| is the same as \verb|[noline]|. + +The conjunction introduction rule illustrates the various line +options: +\begin{displaymath} + \begin{array}{lcc@{\qquad}l} + \mbox{default (single straight)} & + \prftree{A}{B}{A \wedge B} & + \prftree[r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[straight]} \\ + \mbox{double straight} & + \prftree[d]{A}{B}{A \wedge B} & + \prftree[d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[double,straight]} \\ + \mbox{single dotted} & + \prftree[dotted]{A}{B}{A \wedge B} & + \prftree[dotted,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[dotted]} \\ + \mbox{double dotted} & + \prftree[dotted,d]{A}{B}{A \wedge B} & + \prftree[dotted,d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[double,dotted]} \\ + \mbox{single dashed} & + \prftree[dashed]{A}{B}{A \wedge B} & + \prftree[dashed,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[dashed]} \\ + \mbox{double dashed} & + \prftree[dashed,d]{A}{B}{A \wedge B} & + \prftree[dashed,d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[double,dashed]} \\ + \mbox{single fancy} & + \prftree[f]{A}{B}{A \wedge B} & + \prftree[f,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[fancy]} \\ + \mbox{double fancy} & + \prftree[f,d]{A}{B}{A \wedge B} & + \prftree[f,d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[double,fancy]} \\ + \mbox{noline} & + \prftree[noline]{A}{B}{A \wedge B} & + \prftree[noline,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & + \texttt{[noline]} + \end{array} +\end{displaymath} +These examples are implemented in an array whose cells have the form +\begin{center} + \verb|\prftree[|\emph{option}\verb|]{A}{B}{A \wedge B} &| + \verb|\prftree[|\emph{option}\verb|,r]{$\scriptstyle\wedge\mathrm{I}$}| +\end{center} +in which the option part is the one on the right of the +picture.\vspace{1ex} + +An assumption is a special proof tree, built by the command: +\begin{displaymath} + \verb|\prfassumption|\{\text{formula}\} +\end{displaymath} +Similarly, a bounded assumption is produced by the command: +\begin{displaymath} + \verb|\prfboundedassumption|\{\text{formula}\} +\end{displaymath} +as in the previous example. + +Although it is possible to type assumptions directly as argument of +\verb|\prftree|, it is better to use the commands above: as explained +later, since a proof tree is a box with an internal structure, the +assumption commands take care of building this structure +appropriately, while the direct typing does not, which may produce +unexpected results.\vspace{2ex} + +Similarly, axioms are produced by the commands +\begin{displaymath} + \verb|\prfaxiom|\{\mbox{axiom}\} +\end{displaymath} +and +\begin{displaymath} + \verb|\prfbyaxiom|\{\mbox{name}\}\{\mbox{axiom}\} +\end{displaymath} +For example, the axiom stating that equality is reflexive, is +\begin{displaymath} + \begin{array}{cc} + \prfaxiom{\forall x\, x = x} & + \prfbyaxiom{refl}{\forall x\, x = x} + \end{array} +\end{displaymath} +and they are generated by the \LaTeX{} code +\begin{displaymath} + \begin{array}{l} + \verb|\prfaxiom{\forall x\, x = x}|\\ + \verb|\prfbyaxiom{refl}{\forall x\, x = x}| + \end{array} +\end{displaymath}\vspace{-.2ex} + +Finally, a proof summary is used to summarise a proof. The +corresponding command is: +\begin{displaymath} + \verb|\prfsummary|[\mbox{name}]\{\mbox{assumption}_1\} \cdots + \{\mbox{assumption}_n\}\{\mbox{conclusion}\} +\end{displaymath} +The name of the proof is optional, while the assumptions and the +conclusion are treated as in \verb|\prftree|. When present, the proof +name is typeset in text mode. + +For example, \verb|\prfsummary{\forall x\, x = x}| produces +\begin{displaymath} + \prfsummary{\forall x\, x = x} +\end{displaymath} +while +\verb|\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}| +gives +\begin{displaymath} + \prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)} +\end{displaymath}\vspace{-.2ex} + +In general, a proof tree is a \TeX{} box containing all the pieces of +the tree, with strict bounds: for example, +\begin{displaymath} + \fbox{\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}} +\end{displaymath} + +% -------------------------- +\clearpage +\section{Parameters}\label{sec:parameters} +A number of parameters may be used to control the typesetting of proof +trees. They may be changed globally or locally, following the usual +scoping rules of \TeX{}. In this respect, remember that each +assumption is typeset independently, so parameters may be changed on a +sub-proof basis, as will be done in most examples.\vspace{2ex} + +There are various \TeX{} dimensions that influence how proofs are +constructed: +\begin{itemize} +\item\ \verb|\prflinepadbefore| (default 0.3ex): the space between the + bottom line of assumptions and the proof line +\item\ \verb|\prflinepadafter| (default 0.3ex): the space between the + proof line and the top of the conclusion; +\item\ \verb|\prflineextra| (default 0.3em): the length which extends + on the left and on the right the proof line so that it is slightly + longer than the largest between the conclusion and the list of + (direct) assumptions; +\item\ \verb|\prflinethickness| (default 0.12ex): the thickness of the + proof line; +\item\ \verb|\prfemptylinethickness| (default 4 times the line + thickness): in the rare case when the line is empty, but there are + assumptions, this is the distance between the assumptions and the + conclusion; +\item\ \verb|\prfrulenameskip| (default 0.2em): the space between the + proof line and the rule name; +\item\ \verb|\prflabelskip| (default 0.2em): the space between the + proof label and the proof line; +\item\ \verb|\prfinterspace| (default .8em): the space between two + subsequent assumptions in the assumption list; +\item\ \verb|\prfdoublelineinterspace| (default 0.06ex): the space + between the two lines of a double line. +\end{itemize} + +For example, +\begin{displaymath} + \prflinepadafter=0ex + \prftree[r]{$\supset$I} + {\prftree[r]{$\supset$I} + {\prftree[r]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{displaymath} +is typeset by +\begin{verbatim} + \prflinepadafter=0ex + \prftree[r]{$\supset$I} + {\prftree[r]{$\supset$I} + {\prftree[r]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{verbatim} + +Similarly, \verb|\prflineextra=-.4em| and \verb|\prfrulenameskip=.8em| +produce: +\begin{displaymath} + {\prflineextra=-.4em + \prfrulenameskip=.8em + \prftree[r]{$\supset$I} + {\prftree[r]{$\supset$I} + {\prftree[r]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A}} +\end{displaymath} + +Also, \verb|\prflinethickness=3pt| and +\verb|\prfdoublelineinterspace=2pt| in the upper sub-proof generate: +\begin{displaymath} + \prftree[r]{$\supset$I} + {\prftree[r]{$\supset$I} + {\prflinethickness=3pt + \prfdoublelineinterspace=2pt + \prftree[r,d]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{displaymath} +The corresponding code is +\begin{verbatim} + \prftree[r]{$\supset$I} + {\prftree[r]{$\supset$I} + {\prflinethickness=3pt + \prfdoublelineinterspace=2pt + \prftree[r,d]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{verbatim} + +Line thickness does not affect dashed, dotted, and fancy lines, but +interline space does: in the example, +\verb|\prfdoublelineinterspace=4pt| on a fancy line produces +\begin{displaymath} + \prftree[r]{$\supset$I} + {\prftree[r]{$\supset$I} + {\prfdoublelineinterspace=4pt + \prftree[r,d,f]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{displaymath}\vspace{.2ex} + +Fancy lines are drawn by the \verb|\prffancyline| command. This can be +redefined: as a guideline, the package defines it as +\begin{verbatim} + \def\prffancyline{\cleaders\hbox to .63em% + {\hss\raisebox{-.5ex}[.2ex][0pt]{$\sim$}\hss}\hfill} +\end{verbatim}\vspace{2ex} + +Label spacing works exactly as rule name spacing. Actually, it is +possible to have a proof with both a label and a rule name: +\begin{displaymath} + \prftree[r]{$\supset$I} + {\prflabelskip=.7em + \prftree[r,l]{$\supset$I} + {[\textsl{$\bot\mathrm{E}$ will not work here!}]} + {\prftree[r]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{displaymath} +which has been typeset by +\begin{verbatim} + \prftree[r]{$\supset$I} + {\prflabelskip=.7em + \prftree[r,l]{$\supset$I} + {[\textsl{$\bot\mathrm{E}$ will not work here!}]} + {\prftree[r]{$\supset$E} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} +\end{verbatim}\vspace{2ex} + +The \verb|\prfinterspace| controls the distance between +assumptions. Specifically, this is the space between the \emph{boxes} +containing two assumptions. + +Consider the following example +\begin{displaymath} + \prftree + {\prftree + {\prftree + {\prftree + {\prftree + {\prfboundedassumption{A \rightarrow (B \rightarrow C)}} + {\prfboundedassumption{A}} + {B \rightarrow C}} + {\prftree + {\prfboundedassumption{A \rightarrow B}} + {\prfboundedassumption{A}} + {B}} + {C}} + {A \rightarrow C}} + {(A \rightarrow B) \rightarrow (A \rightarrow C)}} + {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) + \rightarrow (A \rightarrow C))} +\end{displaymath} +Although the assumptions in the top line are well spaced, the two +sub-proofs on the top are too close. This can be corrected in two +different ways: by putting an explicit space, via \verb|\hspace|, in +front of the second sub-proof, or after the first +sub-proof---remember, they are just boxes +\begin{displaymath} + \prftree + {\prftree + {\prftree + {\prftree + {\prftree + {\prfboundedassumption{A \rightarrow (B \rightarrow C)}} + {\prfboundedassumption{A}} + {B \rightarrow C}\hspace{1.5em}} + {\prftree + {\prfboundedassumption{A \rightarrow B}} + {\prfboundedassumption{A}} + {B}} + {C}} + {A \rightarrow C}} + {(A \rightarrow B) \rightarrow (A \rightarrow C)}} + {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) + \rightarrow (A \rightarrow C))} +\end{displaymath} +otherwise, putting $\verb|\prfinterspace|=1.5\mathrm{em}$ before the +sub-proof whose conclusion is $C$, one obtains the more pleasant +\begin{displaymath} + \prftree + {\prftree + {\prftree + {\prfinterspace=1.5em + \prftree + {\prftree + {\prfboundedassumption{A \rightarrow (B \rightarrow C)}} + {\prfboundedassumption{A}} + {B \rightarrow C}} + {\prftree + {\prfboundedassumption{A \rightarrow B}} + {\prfboundedassumption{A}} + {B}} + {C}} + {A \rightarrow C}} + {(A \rightarrow B) \rightarrow (A \rightarrow C)}} + {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) + \rightarrow (A \rightarrow C))} +\end{displaymath}\vspace{.2ex} + +The \verb|Strut| option of the package controls a subtle point about +spacing around a proof line: assumptions and conclusion are usually +typeset so that the height and the depth of their box is at least the +one of \verb|\mathstrut|. In this way, adjacent proofs will have their +proof lines aligned (well, whenever they don't have huge +conclusions). But, as signalled by Dominic Hughes, sometimes one wants +the height and the depth to be the ``real'' ones, especially when +there are no characters/symbols with a positive depth: this forces the +perceived space above and below the proof line to be exactly the +values of \verb|\prflinepadbefore| and \verb|\prflinepadafter|. This +behaviour can be achieved by calling the package with the \verb|STRUT| +option. Alternatively, one may use the \verb|\prfSTRUToptionfalse| +command to locally force this behaviour, and +\verb|\prfSTRUToptiontrue| to return to the standard one. Similarly, +the \verb|STRUTlabel| package option, together with the pair of +commands \verb|\prfSTRUTlabeloptiontrue| and +\verb|\prfSTRUTlabeloptionfalse|, operate on rule names and rule +labels.\vspace{2ex} + +The rendering of bounded assumptions is modified by +\verb|\prfboundedstyle|. When $\verb|\prfboundedstyle| = 0$, the +format of the assumption is $[\mbox{formula}]$, which is the default +behaviour; with $\verb|\prfboundedstyle| = 1$, the formula is +cancelled by a horizontal line; with $\verb|\prfboundedstyle| > 1$, +the custom \verb|\prfdiscargedassumption| command is invoked: +\begin{displaymath} + \begin{array}{c@{\qquad}c@{\qquad}c} + \prfboundedassumption{A(x)} & + {\prfboundedstyle=1\prfboundedassumption{A(x)}} & + {\prfboundedstyle=2\prfboundedassumption{A(x)}} + \end{array} +\end{displaymath} + +The \verb|\prfdiscargedassumption| can be freely redefined. The +package provides a reference implementation: +\begin{verbatim} + \def\prfdiscargedassumption#1{\left\langle{#1}\right\rangle} +\end{verbatim}\vspace{2ex} + +Proof summaries are drawn according to \verb|\prfsummarystyle|. The +default value is $0$, which produces a vertical dotted line. Setting +$\verb|\prfsummarystyle| = 1$ produces a huge $\Pi$, while +$\verb|\prfsummarystyle| = 2$ produces a $\prod$. The value $3$ uses a +$\mathcal{D}$ as the derivation symbol. Values greater than $3$ force +the summary to be rendered by the \verb|\prffancysummarybox| command. +\begin{displaymath} + \begin{array}{@{}c@{\quad}c@{\qquad}c@{\qquad}c@{}} + \verb|\prfsummarystyle| = 0 & + {\prfsummary{\forall x.\, x = x}} & + {\prfsummary{B(x)}{A(x)}} & + {\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}} \\[2ex] + \verb|\prfsummarystyle| = 1 & + {\prfsummarystyle1\prfsummary{\forall x.\, x = x}} & + {\prfsummarystyle1\prfsummary{B(x)}{A(x)}} & + {\prfsummarystyle1\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge + C(x)}} \\[1ex] + \verb|\prfsummarystyle| = 2 & + {\prfsummarystyle2\prfsummary{\forall x.\, x = x}} & + {\prfsummarystyle2\prfsummary{B(x)}{A(x)}} & + {\prfsummarystyle2\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge + C(x)}} \\[1ex] + \verb|\prfsummarystyle| = 3 & + {\prfsummarystyle3\prfsummary{\forall x.\, x = x}} & + {\prfsummarystyle3\prfsummary{B(x)}{A(x)}} & + {\prfsummarystyle3\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}} + \\[1ex] + \verb|\prfsummarystyle| = 4 & + {\prfsummarystyle4\prfsummary{\forall x.\, x = x}} & + {\prfsummarystyle4\prfsummary{B(x)}{A(x)}} & + {\prfsummarystyle4\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}} + \end{array} +\end{displaymath} + +The fancy summary box is composed by the \verb|\prffancysummarybox| +command. This can be modified at will. The package defines it as +\begin{verbatim} + \newbox\prf@@fancysummarybox\newdimen\prf@@fancysymmarylen + \def\prffancysummarybox{% + \sbox{\prf@@fancysummarybox}{\Huge$\bigtriangledown$}% + \prf@@fancysymmarylen\ht\prf@@fancysummarybox% + \advance\prf@@fancysymmarylen\dp\prf@@fancysummarybox% + \sbox{\prf@@fancysummarybox}{% + \raisebox{.25\prf@@fancysymmarylen}[.8\prf@@fancysymmarylen]% + [0pt]{\usebox{\prf@@fancysummarybox}}}% + \prf@@fancysymmarylen\wd\prf@summary@label% + \ifdim\prf@@fancysymmarylen>\z@\relax% + \prf@@fancysymmarylen\wd\prf@@fancysummarybox% + \wd\prf@summary@label.4em% + \hbox to\prf@@fancysymmarylen{% + \usebox\prf@@fancysummarybox}\kern-.4em% + \box\prf@summary@label% + \else\usebox\prf@@fancysummarybox\fi} +\end{verbatim}\vspace{2ex} + +The assumptions, conclusions, labels, and rule names are drawn using +the following commands, which may be redefined: +\begin{verbatim} +\def\prfConclusionBox#1{% + \hbox{$\displaystyle\begingroup#1\endgroup% +\def\prfAssumptionBox#1{% + \hbox{$\displaystyle\begingroup#1\endgroup% + \ifprfSTRUToption\mathstrut\fi$}} +\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup% + \ifprfSTRUTlabeloption\strut\fi}} +\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup% + \ifprfSTRUTlabeloption\strut\fi}} +\end{verbatim} +It is not advisable to change these commands in a radical way, unless +one understands how the graphical engine works. + +% ------------------------------------- +\clearpage +\section{Labels and References}\label{sec:references} +As discharged assumptions are often hard to track in a proof, the +package provides a mechanism to label them and to reference them +inside a proof tree. A reference is made up of three pieces: the +\emph{label}, which is the name to denote the reference inside the +text, the \emph{reference value}, which is the value denoted by the +label, and the \emph{anchor}, which is the graphical rendering of the +value aside the labelled point of the proof. + +For example, +\begin{displaymath} + \begin{prfenv} + \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$} + {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$} + {\prftree[r]{$\supset$E} + {\prfboundedassumption<assum:A>{A}} + {\prfboundedassumption<assum:not_A>{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} + \end{prfenv} +\end{displaymath} +is generated by the following code +\begin{verbatim} + \begin{prfenv} + \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$} + {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$} + {\prftree[r]{$\supset$E} + {\prfboundedassumption<assum:A>{A}} + {\prfboundedassumption<assum:not_A>{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} + \end{prfenv} +\end{verbatim} +The labels are \verb|assum:A| and \verb|assum:not_A|, the reference +values are $1$ and $2$, respectively, and the anchors are these values +on the discharged assumptions on the top of the proof. The references +to these labels are the values in the rule names.\vspace{2ex} + +The \verb|prfenv| environment delimits the scope of labels: the +\verb|\end{prfenv}| declaration makes the labels still available +for reference, but numbering of new labels will restart from +$1$. Enclosing a proof tree in a \verb|prfenv| environment is not +mandatory: in such case, labels will be global to the +document.\vspace{2ex} + +Sometimes, labels require two compilation steps to be correctly +generated: in fact, as \LaTeX{} labels, forward references may be +undefined in the first compilation step. The package issues a warning +in this case, and display a \verb|??| for the invalid reference. Also, +notice how the assumption reference mechanism is analogous to \LaTeX{} +labels, but it is independent from it.\vspace{2ex} + +A reference to a label is made by the +$\verb|\prfref|\langle\mathrm{label}\rangle$ command: its argument is +a label, i.e., a string of text following the same rules as the +argument of the \LaTeX{} \verb|\label| command. As in the \verb|\ref| +command, the resulting value has no formatting.\vspace{2ex} + +A labelled assumption is generated by the following commands: +\begin{displaymath} + \begin{array}{l} + \verb|\prfassumption|\langle[\mathrm{option}]\mathrm{label}\rangle + \{\mathrm{assumption}\} + \\ + \verb|\prfboundedassumption|\langle[\mathrm{option}] + \mathrm{label}\rangle\{\mathrm{assumption}\} + \end{array} +\end{displaymath} +The first one acts as \verb|\prfassumption| but also declares the +assumption label and decorates the assumption text with the +anchor. The second one does the same on bounded assumptions. + +The generation of labels is controlled by the option value: +\begin{itemize} +\item \textbf{n}, \textbf{number}, \textbf{arabic}: generates a number + (default); +\item \textbf{r}, \textbf{roman}: generates a lowercase roman number; +\item \textbf{R}, \textbf{Roman}: generates an uppercase + roman number; +\item \textbf{a}, \textbf{alph}, \textbf{alpha}, \textbf{alphabetic}: + produces a lowercase letter; +\item \textbf{A}, \textbf{Alph}, \textbf{Alpha}, \textbf{Alphabetic}: + produces an uppercase letter; +\item \textbf{f}, \textbf{s}, \textbf{function}, \textbf{symbol}, + \textbf{function symbol}: produces a footnote symbol, as in + Section~C.8.4 of Lamport's, \textit{\LaTeX: A document preparation + system}; +\item \textbf{l}, \textbf{label}: tells that the label has not to be + defined. This is used to generate a labelled assumption sharing the + label with another one, which declares the value and the format. +\end{itemize} + +Except for \textbf{l} and \textbf{label}, all the options are used to +format the anchor following the standard \LaTeX{} way available for +counters. No multiple options are allowed. + +For example, the disjunction elimination rule is a perfect way to +illustrate the reason behind the \textbf{label} option, i.e., the need +to discharge a pair of assumptions: +\begin{displaymath} + \begin{prfenv} + \prfinterspace=1.2em + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<assum:orE>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orE>{B}}{C}}{C} + \end{prfenv} +\end{displaymath} +\begin{verbatim} + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<assum:orE>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orE>{B}}{C}}{C} +\end{verbatim} + +If a label is declared more than once, a warning is issued when the +\textbf{label} option is not used: although this is not a mistake, it +may indicate that a label is reused when it should not. + +The same example can be used to show how the other options work: +\begin{displaymath} + \renewcommand{\arraystretch}{6} + \begin{array}{@{}ccc@{}} + \begin{prfenv} + \prfinterspace=.6em + \prfsummarystyle=2 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<[n]assum:orEn>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orEn>{B}}{C}} + {C} + \end{prfenv} & + \begin{prfenv} + \prfinterspace=.6em + \prfsummarystyle=2 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<[r]assum:orEr>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orEr>{B}}{C}} + {C} + \end{prfenv} & + \begin{prfenv} + \prfinterspace=.6em + \prfsummarystyle=2 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<[R]assum:orER>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orER>{B}}{C}} + {C} + \end{prfenv} \\ + \begin{prfenv} + \prfinterspace=.6em + \prfsummarystyle=2 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<[a]assum:orEa>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orEa>{B}}{C}} + {C} + \end{prfenv} & + \begin{prfenv} + \prfinterspace=.6em + \prfsummarystyle=2 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<[A]assum:orEA>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orEA>{B}}{C}} + {C} + \end{prfenv} & + \begin{prfenv} + \prfinterspace=.6em + \prfsummarystyle=2 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<[f]assum:orEf>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orEf>{B}}{C}} + {C} + \end{prfenv} + \end{array} +\end{displaymath} + +Also, as the \verb|\prfboundedstyle| varies, the resulting proof trees +are: +\begin{displaymath} + \begin{array}{ccc} + \begin{prfenv} + \prfinterspace=.6em + \prfboundedstyle=0 + \prfsummarystyle=4 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<assum:AorE>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:AorE>{B}}{C}} + {C} + \end{prfenv} & + \begin{prfenv} + \prfinterspace=.6em + \prfboundedstyle=1 + \prfsummarystyle=4 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<assum:BorE>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:BorE>{B}}{C}} + {C} + \end{prfenv} & + \begin{prfenv} + \prfinterspace=.6em + \prfboundedstyle=2 + \prfsummarystyle=4 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<assum:CorE>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:CorE>{B}}{C}} + {C} + \end{prfenv} + \end{array} +\end{displaymath} + +The \verb|prfassumptioncounter| is the \LaTeX{} counter used to +generate the assumption values. It contains the last used value, and +initially, it is set to $0$. By modifying its value, e.g., to +\verb|\setcounter{prfassumptioncounter}{1}|, +\begin{displaymath} + \begin{prfenv} + \setcounter{prfassumptioncounter}{1} + \prfsummarystyle=2 + \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEff>}$} + {\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, + \prfboundedassumption<[f]assum:orEff>{A}}{C}} + {\prfsummary{\Gamma, + \prfboundedassumption<[l]assum:orEff>{B}}{C}} + {C} + \end{prfenv} +\end{displaymath} + +A labelled assumption box is graphically constructed by the package +command \verb|\prflabelledassumptionbox| which can be redefined if +needed. It takes two arguments: the assumption and the anchor. Its +standard definition is +\begin{verbatim} + \def\prflabelledassumptionbox#1#2{% + \setbox\prf@fancybox\hbox{${#1}$}% + \prf@tmp\wd\prf@fancybox% + \setbox\prf@fancybox\hbox{$\box\prf@fancybox^{#2}$}% + \wd\prf@fancybox\prf@tmp% + \prf@assumption{\box\prf@fancybox}} +\end{verbatim} + +Moreover, also a labelled and bounded assumption is graphically +rendered by the same command. There is just one exception: when +$\verb|\prfboundedstyle| > 1$. In fact, since that style is +controlled by a command that can be redefined, the same must hold for +references in that style. The command which is called in this case is +\verb|\prflabelleddiscargedassumption| which can be redefined if +needed; its standard definition in the package is +\begin{verbatim} + \def\prflabelleddiscargedassumption#1#2{% + \prflabelledassumptionbox{\left\langle{#1}\right\rangle}{#2}} +\end{verbatim}\vspace{2ex} + +Also proof summaries can be labelled and referenced. The syntax +extends the \verb|\prfsummary| command: +\begin{displaymath} + \verb|\prfsummary|\langle[\mathrm{option}]\mathrm{label}\rangle + [\mathrm{name}]\{\mathrm{assumption}1\} \cdots + \{\mathrm{assumption}_n\}\{\mathrm{conclusion}\} +\end{displaymath} +The reference argument works in the same way as the corresponding one +for assumptions, and the options are the same. + +\begin{displaymath} + \setcounter{prfsummarycounter}{0} + \begin{array}{c@{\qquad}c@{\qquad}c@{\qquad}c@{\qquad}c} + {\prfsummarystyle=0 + \prfsummary<proof:a0>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<proof:a1>{A}{B}{A \wedge B}} & + {\prfsummarystyle=2 + \prfsummary<proof:a2>{A}{B}{A \wedge B}} & + {\prfsummarystyle=3 + \prfsummary<proof:a3>{A}{B}{A \wedge B}} & + {\prfsummarystyle=4 + \prfsummary<proof:a4>{A}{B}{A \wedge B}} + \end{array} +\end{displaymath} + +These examples have been generated by the following code snippet: +\begin{verbatim} + {\prfsummarystyle=X + \prfsummary<proof:aX>{A}{B}{A \wedge B}} +\end{verbatim} + +The \verb|[option]| part of the label specification is optional, and +it works exactly as the option field of labelled assumptions. This is +best illustrated by an example: +\begin{displaymath} + \setcounter{prfsummarycounter}{0} + \begin{array}{cccc} + {\prfsummarystyle=1 + \prfsummary<[r]proof:b1>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[R]proof:b2>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[f]proof:b3>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[a]proof:b4>{A}{B}{A \wedge B}} \\ & + {\prfsummarystyle=1 + \prfsummary<[A]proof:b5>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} & + \end{array} +\end{displaymath} + +These examples have been generated by the following code snippet: +\begin{verbatim} + {\prfsummarystyle=1 + \prfsummary<[r]proof:bX>{A}{B}{A \wedge B}} +\end{verbatim} +and the last line uses the \verb|label| option.\vspace{2ex} + +The value of the summary labelling is controlled by the +\verb|prfsummarycounter| counter, which is initially $0$ and contains +the last used value. + +% ------------------------------------- +\clearpage +\section{Simplified Commands}\label{sec:simplified_commands} +The basic commands illustrated so far allow to control proof trees in +all aspects, but they tend to be verbose in practise. Thus, a number +of abbreviations are provided to make handier the writing of proofs. +Since they may collide with other packages, these macros are activated +by suitable options. Multiple options can be used at the same time. + +\subsection{Natural deduction} +By loading the package with the \verb|ND| option, the following +abbreviations are available, which correspond to the inference rules +of natural deduction calculi: +\begin{itemize} +\item \verb|\NDA|: assumption; +\item \verb|\NDAL|: labelled assumption; +\item \verb|\NDD|: discharged assumption; +\item \verb|\NDDL|: labelled discharged assumption; +\item \verb|\NDP|: generic proof tree; +\item \verb|\NDAX|: a generic axiom rule; + \begin{displaymath} + \vcenter{\NDAX{x = x}}\enspace; + \end{displaymath} +\item \verb|\NDANDI|: conjunction introduction + \begin{displaymath} + \vcenter{\NDANDI{\NDA{A}}{\NDA{B}}{A \wedge B}}\enspace; + \end{displaymath} +\item \verb|\NDANDER|, \verb|\NDANDEL|, \verb|\NDANDE|: conjunction + elimination right, left, and unspecified, respectively + \begin{displaymath} + \vcenter{\NDANDEL{\NDA{A \wedge B}}{\NDA{A}}} \quad + \vcenter{\NDANDER{\NDA{A \wedge B}}{\NDA{B}}}\enspace; + \end{displaymath} +\item \verb|\NDORIR|, \verb|\NDORIL|, \verb|\NDORI|: disjunction + introduction right, left, and unspecified, respectively + \begin{displaymath} + \vcenter{\NDORIL{\NDA{A}}{\NDA{A \vee B}}} \quad + \vcenter{\NDORIR{\NDA{B}}{\NDA{A \vee B}}}\enspace; + \end{displaymath} +\item \verb|\NDOREL|, \verb|\NDORE|: disjunction elimination, possibly + labelled + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDOREL{ndorel:1}{\NDA{A \vee B}} + {\prfsummary{\NDDL{ndorel:1}{A}}{C}} + {\prfsummary{\NDDL{[l]ndorel:1}{B}}{C}}{C}} \quad + \vcenter{\NDORE{\NDA{A \vee B}}{\prfsummary{\NDA{A}}{C}} + {\prfsummary{\NDA{B}}{C}}{C}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDIMPIL|, \verb|\NDIMPI|: implication introduction, + possibly labelled + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDIMPIL{ndimpil:1} + {\prfsummary{\NDDL{ndimpil:1}{A}}{B}} + {A \rightarrow B}} \quad + \vcenter{\NDIMPI{\prfsummary{\NDA{A}}{B}}{A \rightarrow B}} + \enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDIMPE|: implication elimination + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDIMPE{\NDA{A \rightarrow B}}{\NDA{A}}{B}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDNOTIL|, \verb|\NDNOTI|: negation introduction, possibly + labelled + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDNOTIL{ndnotil:1} + {\prfsummary{\NDDL{ndnotil:1}{A}}{\bot}}{\neg A}}\quad + \vcenter{\NDNOTI{\prfsummary{\NDA{A}}{\bot}}{\neg A}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDNOTE|: negation elimination + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDNOTE{\NDA{\neg A}}{\NDA{A}}{\bot}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDALLI|: universal quantifier introduction + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDALLI{\NDA{A}}{\forall x.\, A}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDALLE|: universal quantifier elimination + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDALLE{\NDA{\forall x.\, A}}{A[t/x]}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDEXI|: existential quantifier introduction + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDEXI{\NDA{A[t/x]}}{\exists x.\, A}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDEXEL|, \verb|\NDEXE|: existential quantifier + elimination, possibly labelled + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDEXEL{ndexel:1}{\NDA{\exists x.\, A}} + {\prfsummary{\NDDL{ndexel:1}{A}}{B}}{B}}\quad + \vcenter{\NDEXE{\NDA{\exists x.\, A}} + {\prfsummary{\NDA{A}}{B}}{B}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDTI|: truth introduction + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDTI{\top}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDFE|: falsity elimination + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDFE{\NDA{\bot}}{A}}\enspace; + \end{prfenv} + \end{displaymath} +\item \verb|\NDLEM|: law of Excluded Middle + \begin{displaymath} + \begin{prfenv} + \vcenter{\NDLEM{A \vee \neg A}}\enspace. + \end{prfenv} + \end{displaymath} +\end{itemize} + +The labels, when present, are the first argument, the rest being the +assumptions and, finally, the conclusion. The rules do not have a +fixed format, so extensions are allowed, e.g., on conjunction +elimination or disjunction introduction. + +For example, the proof +\begin{displaymath} + \begin{prfenv} + \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}} + {\NDIMPIL{simp:notnotA} + {\NDFE{\NDIMPE{\NDDL{simp:notnotA}{\neg\neg A}} + {\NDDL{simp:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} + \end{prfenv} +\end{displaymath} +is typeset in abbreviated form by the following code +\begin{verbatim} + \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}} + {\NDIMPIL{simp:notnotA} + {\NDFE{\NDIMPE{\NDDL{simp:notnotA}{\neg\neg A}} + {\NDDL{simp:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} +\end{verbatim}\vspace{2ex} + +\subsection{Sequents} +Similarly, by loading the package with the \verb|SEQ| option, the +following abbreviations are available, which roughly correspond to the +inference rule of sequent calculi: +\begin{itemize} +\item \verb|\SEQA|: assumption; +\item \verb|\SEQD|: bounded assumption (not normally used, but handy + to have in case of fancy calculi); +\item \verb|\SEQP|: generic proof; +\item \verb|\SEQAX|: axiom rule + \begin{displaymath} + \vcenter{\SEQAX{A \Rightarrow A}}\enspace; + \end{displaymath} +\item \verb|\SEQLF|: left falsity + \begin{displaymath} + \vcenter{\SEQLF{\bot \Rightarrow {}}}\enspace; + \end{displaymath} +\item \verb|\SEQLW|, \verb|\SEQRW|: left and right weakening + \begin{displaymath} + \vcenter{\SEQLW{\Gamma \Rightarrow \Delta}{A, \Gamma \Rightarrow + \Delta}}\quad + \vcenter{\SEQLW{\Gamma \Rightarrow \Delta}{\Gamma \Rightarrow + \Delta, A}}\enspace; + \end{displaymath} +\item \verb|\SEQLC|, \verb|\SEQRC|: left and right contraction + \begin{displaymath} + \vcenter{\SEQLC{A, A, \Gamma \Rightarrow \Delta}{A, \Gamma + \Rightarrow \Delta}}\quad + \vcenter{\SEQRC{\Gamma \Rightarrow \Delta, A, A}{\Gamma + \Rightarrow \Delta, A}}\enspace; + \end{displaymath} +\item \verb|\SEQLAND|, \verb|\SEQLANDL|, \verb|\SEQLANDR|: left + conjunction; the \verb|L| and \verb|R| variants specify which side + of the conjunction is introduced + \begin{displaymath} + \vcenter{\SEQLANDL{A, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma + \Rightarrow \Delta}}\quad + \vcenter{\SEQLANDR{B, \Gamma \Rightarrow \Delta}{A \wedge B, \Gamma + \Rightarrow \Delta}}\enspace; + \end{displaymath} +\item \verb|\SEQRAND|: right conjunction + \begin{displaymath} + \vcenter{\SEQRAND{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow + \Delta, B}{\Gamma \Rightarrow \Delta, A \wedge B}}\enspace; + \end{displaymath} +\item \verb|\SEQLOR|: left disjunction + \begin{displaymath} + \vcenter{\SEQLOR{A, \Gamma \Rightarrow \Delta}{B, \Gamma + \Rightarrow \Delta}{A \vee B, \Gamma \Rightarrow + \Delta}}\enspace; + \end{displaymath} +\item \verb|\SEQROR|, \verb|\SEQRORL|, \verb|\SEQRORR|: right + disjunction; the \verb|R| and \verb|L| variants specify which side + of the disjunction is introduced + \begin{displaymath} + \vcenter{\SEQRORL{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow + \Delta, A \vee B}}\quad + \vcenter{\SEQRORR{\Gamma \Rightarrow \Delta, B}{\Gamma \Rightarrow + \Delta, A \vee B}}\enspace; + \end{displaymath} +\item \verb|\SEQLIMP|: left implication + \begin{displaymath} + \vcenter{\SEQLIMP{\Gamma \Rightarrow \Delta, A}{B, \Gamma + \Rightarrow \Delta}{A \rightarrow B, \Gamma \Rightarrow + \Delta}}\enspace; + \end{displaymath} +\item \verb|\SEQRIMP|: right implication + \begin{displaymath} + \vcenter{\SEQRIMP{A, \Gamma \Rightarrow \Delta, B}{\Gamma + \Rightarrow, \Delta, A \rightarrow B}}\enspace; + \end{displaymath} +\item \verb|\SEQLALL|: left universal quantification + \begin{displaymath} + \vcenter{\SEQLALL{A[t/x], \Gamma \Rightarrow \Delta}{\forall x.\, + A, \Gamma \Rightarrow \Delta}}\enspace; + \end{displaymath} +\item \verb|\SEQRALL|: right universal quantification + \begin{displaymath} + \vcenter{\SEQRALL{\Gamma \Rightarrow \Delta, A}{\Gamma \Rightarrow + \Delta, \forall x.\, A}}\enspace; + \end{displaymath} +\item \verb|\SEQLEX|: left existential quantification + \begin{displaymath} + \vcenter{\SEQLEX{A, \Gamma \Rightarrow \Delta}{\exists x.\, A, + \Gamma \Rightarrow \Delta}}\enspace; + \end{displaymath} +\item \verb|\SEQREX|: right existential quantification + \begin{displaymath} + \vcenter{\SEQREX{\Gamma \Rightarrow \Delta, A[t/x]}{\Gamma + \Rightarrow \Delta, \exists x.\, A}}\enspace; + \end{displaymath} +\item \verb|\SEQCUT|: cut rule + \begin{displaymath} + \vcenter{\SEQCUT{\Gamma \Rightarrow \Delta, A}{A, \Gamma' + \Rightarrow \Delta'}{\Gamma \Gamma' \Rightarrow \Delta + \Delta'}}\enspace. + \end{displaymath} +\end{itemize} + +\subsection{Equality} +Invoking the \verb|EQ| option defines the following inference rules: +\begin{itemize} +\item \verb|\EQREFL|: reflexivity + \begin{displaymath} + \vcenter{\EQREFL{t = t}}\enspace; + \end{displaymath} +\item \verb|\EQSYM|: symmetry + \begin{displaymath} + \vcenter{\EQSYM{t = s}{s = t}}\enspace; + \end{displaymath} +\item \verb|\EQTRANS|: transitivity + \begin{displaymath} + \vcenter{\EQTRANS{t = s}{s = r}{t = r}}\enspace; + \end{displaymath} +\item \verb|\EQSUBST|: the substitution rule + \begin{displaymath} + \vcenter{\EQSUBST{t = s}{A[t/x]}{A[s/x]}}\enspace. + \end{displaymath} +\end{itemize} + +\subsection{Implication} +Since the implication symbol is usually represented either as +$\rightarrow$ or as $\supset$, the package allows to choose which +representation to use. By default, implication is $\rightarrow$, but +loading the package with the \verb|[IMP]| option switches to +$\supset$. The same effect is obtained by the commands +\verb|\prfIMPOptiontrue| (implication is $\supset$) and +\verb|prfIMPOptionfalse| (implication is $\rightarrow$). + +\subsection{Martin-L{\"o}f Type Theory and Homotopy Type Theory} +Invoking the package with the \verb|ML| option enables the support for +these type theories. This part is derived from Roberta Bonacina's PhD +dissertation, which used this package in an essential way to develop +proof trees in Homotopy Type Theory. + +Enabling the option \verb|ML| defines a number of symbols which are +useful to have. However, since they may conflict with other packages, +they can be disabled invoking the option \verb|MLnodef|. These +operators are +\begin{itemize} +\item \verb|\type|: the symbol $\type$ correctly spaced as a + mathematical binary operation; +\item \verb|\universe|: the symbol for universes; +\item \verb|\judgementaldef| and \verb|\propositionaldef|: the symbols + $\judgementaldef$ and $\propositionaldef$ spaced as mathematical + binary operations; +\item \verb|\emptytype| ($\emptytype$), \verb|\unittype| + ($\unittype$), \verb|\booleantype| ($\booleantype$): these symbols + are ordinary operators typeset in mathematical boldface font; +\item \verb|\context| ($\context$), \verb|\identitytype| + ($\identitytype$), \verb|\refl| ($\refl$), \verb|\axiomofchoice| + ($\axiomofchoice$), \verb|\accessibility| ($\accessibility$), + \verb|\ap| ($\ap$), \verb|\apd| ($\apd$), \verb|\basepoint| + ($\basepoint$), \verb|\biinv| ($\biinv$), \verb|\cardtype| + ($\cardtype$), \verb|\cocone| ($\cocone$), \verb|\cons| ($\cons$), + \verb|\contr| ($\contr$), \verb|\equivtype| ($\equivtype$), + \verb|\ext| ($\ext$), \verb|\fiber| ($\fiber$), \verb|\funext| + ($\funext$), \verb|\glue| ($\glue$), \verb|\happly| ($\happly$), + \verb|\hom| ($\hom$), \verb|\id| ($\id$), \verb|\idtoeqv| + ($\idtoeqv$), \verb|\im| ($\im$), \verb|\idtoiso| ($\idtoiso$), + \verb|\ind| ($\ind$), \verb|\inj| ($\inj$), \verb|\inl| ($\inl$), + \verb|\inr| ($\inr$), \verb|\iscontr| ($\iscontr$), \verb|\isequiv| + ($\isequiv$), \verb|\ishae| ($\ishae$), \verb|\isotoid| + ($\isotoid$), \verb|\isprop| ($\isprop$), \verb|\isset| ($\isset$), + \verb|\ker| ($\ker$), \verb|\LEM| ($\LEM$), \verb|\linv| ($\linv$), + \verb|\listtype| ($\listtype$), \verb|\loopcons| ($\loopcons$), + \verb|\Map| ($\Map$), \verb|\merid| ($\merid$), \verb|\nil| + ($\nil$), \verb|\ordtype| ($\ordtype$), \verb|\pair| ($\pair$), + \verb|\pred| ($\pred$), \verb|\pr| ($\pr$), \verb|\Prop| ($\Prop$), + \verb|\qinv| ($\qinv$), \verb|\rec| ($\rec$), \verb|\rinv| + ($\rinv$), \verb|\seg| ($\seg$), \verb|\Set| ($\Set$), \verb|\Succ| + ($\Succ$), \verb|\sup| ($\sup$), \verb|\total| ($\total$), + \verb|\transport| ($\transport$), \verb|\ua| ($\ua$), \verb|\Wtype| + ($\Wtype$), \verb|\transportconst| ($\transportconst$): these + symbols are ordinary operators, typeset in the mathematical + sans-serif font; their graphical appearance is in brackets. +\end{itemize} + +The large number of inference rules is listed below: they cover the +structural part of the theories, plus most of the usual inductive +types, comprehending also some higher-order inductive types. To each +rule is associated a rule name, which is available as a command: the +convention is that the rule name is obtained appending \verb|rule| to +the name of the inference rule. In general, the command to typeset a +rule conforms to the standard name in the book \emph{Homotopy Type + Theory}. The name as typeset, is shown in brackets: +\begin{itemize} +\item \verb|\MLctxEMP| $(\scriptstyle\MLctxEMPrule)$,\\ \verb|\MLctxEXT| + $(\scriptstyle\MLctxEXTrule)$: context manipulation; +\item \verb|\MLVble| $(\scriptstyle\MLVblerule)$: variable + introduction; +\item \verb|\MLSubst| $(\scriptstyle\MLSubstrule)$, + \verb|\MLWkg| + $(\scriptstyle\MLWkgrule)$: substitution and weakening; +\item \verb|\MLEQrefl| $(\scriptstyle\MLEQreflrule)$, + \verb|\MLEQsym| $(\scriptstyle\MLEQsymrule)$, + \verb|\MLEQtrans| $(\scriptstyle\MLEQtransrule)$, \\ + \verb|\MLEQsubst| $(\scriptstyle\MLEQsubstrule)$, + \verb|\MLEQsubsteq| $(\scriptstyle\MLEQsubsteqrule)$: structural + rules about judgemental equality; +\item \verb|\MLUintro| $(\scriptstyle\MLUintrorule)$, + \verb|\MLUcumul| $(\scriptstyle\MLUcumulrule)$, + \verb|\MLUcumuleq| $(\scriptstyle\MLUcumuleqrule)$: type universe; +\item \verb|\MLpiform| $(\scriptstyle\MLpiformrule)$, + \verb|\MLpiformeq| $(\scriptstyle\MLpiformeqrule)$, \\ + \verb|\MLpiintro| $(\scriptstyle\MLpiintrorule)$, + \verb|\MLpiintroeq| $(\scriptstyle\MLpiintroeqrule)$, \\ + \verb|\MLpielim| $(\scriptstyle\MLpielimrule)$, + \verb|\MLpielimeq| $(\scriptstyle\MLpielimeqrule)$, \\ + \verb|\MLpicomp| $(\scriptstyle\MLpicomprule)$, + \verb|\MLpiuniq| $(\scriptstyle\MLpiuniqrule)$: dependent function + types; +\item \verb|\MLKintro| $(\scriptstyle\MLKintrorule)$: generic rule for + constant introduction; +\item \verb|\MLsigmaform| $(\scriptstyle\MLsigmaformrule)$, + \verb|\MLsigmaintro| $(\scriptstyle\MLsigmaintrorule)$, + \verb|\MLsigmaelim| $(\scriptstyle\MLsigmaelimrule)$, \\ + \verb|\MLsigmacomp| $(\scriptstyle\MLsigmacomprule)$, + \verb|\MLsigmauniq| $(\scriptstyle\MLsigmauniqrule)$: dependent pair + types; +\item \verb|\MLplusform| $(\scriptstyle\MLplusformrule)$, + \verb|\MLplusintrol| $(\scriptstyle\MLplusintrolrule)$, + \verb|\MLplusintror| $(\scriptstyle\MLplusintrorrule)$, \\ + \verb|\MLpluselim| $(\scriptstyle\MLpluselimrule)$, + \verb|\MLpluscompl| $(\scriptstyle\MLpluscomplrule)$, + \verb|\MLpluscompr| $(\scriptstyle\MLpluscomprrule)$, \\ + \verb|\MLplusuniq| $(\scriptstyle\MLplusuniqrule)$: coproduct types; +\item \verb|\MLzeroform| $(\scriptstyle\MLzeroformrule)$, + \verb|\MLzeroelim| $(\scriptstyle\MLzeroelimrule)$, + \verb|\MLzerouniq| $(\scriptstyle\MLzerouniqrule)$: the empty type; +\item \verb|\MLunitform| $(\scriptstyle\MLunitformrule)$, + \verb|\MLunitintro| $(\scriptstyle\MLunitintrorule)$, + \verb|\MLunitelim| $(\scriptstyle\MLunitelimrule)$, \\ + \verb|\MLunitcomp| $(\scriptstyle\MLunitcomprule)$, + \verb|\MLunituniq| $(\scriptstyle\MLunituniqrule)$: the unit type; +\item \verb|\MLnatform| $(\scriptstyle\MLnatformrule)$, + \verb|\MLnatintrozero| $(\scriptstyle\MLnatintrozerorule)$, \\ + \verb|\MLnatintrosucc| $(\scriptstyle\MLnatintrosuccrule)$, + \verb|\MLnatelim| $(\scriptstyle\MLnatelimrule)$, \\ + \verb|\MLnatcompzero| $(\scriptstyle\MLnatcompzerorule)$, + \verb|\MLnatcompsucc| $(\scriptstyle\MLnatcompsuccrule)$, \\ + \verb|\MLnatuniq| $(\scriptstyle\MLnatuniqrule)$: the natural number + type; +\item \verb|\MLidform| $(\scriptstyle\MLidformrule)$, + \verb|\MLidintro| $(\scriptstyle\MLidintrorule)$, + \verb|\MLidelim| $(\scriptstyle\MLidelimrule)$, \\ + \verb|\MLidcomp| $(\scriptstyle\MLidcomprule)$, + \verb|\MLiduniq| $(\scriptstyle\MLiduniqrule)$: identity types; +\item \verb|\MLwform| $(\scriptstyle\MLwformrule)$, + \verb|\MLwintro| $(\scriptstyle\MLwintrorule)$, + \verb|\MLwelim| $(\scriptstyle\MLwelimrule)$, \\ + \verb|\MLwcomp| $(\scriptstyle\MLwcomprule)$, + \verb|\MLwuniq| $(\scriptstyle\MLwuniqrule)$: $\mathsf{W}$ types; +\item \verb|\MLListform| $(\scriptstyle\MLListformrule)$, + \verb|\MLListintron| $(\scriptstyle\MLListintronrule)$,\\ + \verb|\MLListintroc| $(\scriptstyle\MLListintrocrule)$, + \verb|\MLListelim| $(\scriptstyle\MLListelimrule)$,\\ + \verb|\MLListcompn| $(\scriptstyle\MLListcompnrule)$, + \verb|\MLListcompc| $(\scriptstyle\MLListcompcrule)$,\\ + \verb|\MLListuniq| $(\scriptstyle\MLListuniqrule)$: + $\mathsf{List}$ types; +\item \verb|\MLfunext| $(\scriptstyle\MLfunextrule)$: function extensionality; +\item \verb|\MLuniv| $(\scriptstyle\MLunivrule)$: univalence; +\item \verb|\MLSform| $(\scriptstyle\MLSformrule)$, + \verb|\MLSintro| $(\scriptstyle\MLSintrorule)$, + \verb|\MLSelim| $(\scriptstyle\MLSelimrule)$,\\ + \verb|\MLScomp| $(\scriptstyle\MLScomprule)$, + \verb|\MLSuniq| $(\scriptstyle\MLSuniqrule)$, + \verb|\MLSpeqintro| $(\scriptstyle\MLSpeqintrorule)$,\\ + \verb|\MLSpeqcomp| $(\scriptstyle\MLSpeqcomprule)$: the + $\mathbb{S}^1$ circle type; +\item \verb|\MLIform| $(\scriptstyle\MLIformrule)$, + \verb|\MLIintroa| $(\scriptstyle\MLIintroarule)$, + \verb|\MLIintrob| $(\scriptstyle\MLIintrobrule)$, \\ + \verb|\MLIelim| $(\scriptstyle\MLIelimrule)$, + \verb|\MLIcompa| $(\scriptstyle\MLIcomparule)$, + \verb|\MLIcompb| $(\scriptstyle\MLIcompbrule)$, \\ + \verb|\MLIuniq| $(\scriptstyle\MLIuniqrule)$, + \verb|\MLIpeqintro| $(\scriptstyle\MLIpeqintrorule)$, + \verb|\MLIpeqcomp| $(\scriptstyle\MLIpeqcomprule)$: the interval + type; +\item \verb|\MLsigmaintroa| $(\scriptstyle\MLsigmaintroarule)$, + \verb|\MLsigmaintrob| $(\scriptstyle\MLsigmaintrobrule)$, \\ + \verb|\MLsigmacompa| $(\scriptstyle\MLsigmacomparule)$, + \verb|\MLsigmacompb| $(\scriptstyle\MLsigmacompbrule)$, \\ + \verb|\MLsigmapeqintro| $(\scriptstyle\MLsigmapeqintrorule)$, + \verb|\MLsigmapeqcomp| $(\scriptstyle\MLsigmapeqcomprule)$: + suspensions; +\item \verb|\MLPOform| $(\scriptstyle\MLPOformrule)$, + \verb|\MLPOintroa| $(\scriptstyle\MLPOintroarule)$, + \verb|\MLPOintrob| $(\scriptstyle\MLPOintrobrule)$, \\ + \verb|\MLPOelim| $(\scriptstyle\MLPOelimrule)$, + \verb|\MLPOcompa| $(\scriptstyle\MLPOcomparule)$, + \verb|\MLPOcompb| $(\scriptstyle\MLPOcompbrule)$, \\ + \verb|\MLPOuniq| $(\scriptstyle\MLPOuniqrule)$, + \verb|\MLPOpeqintro| $(\scriptstyle\MLPOpeqintrorule)$, + \verb|\MLPOpeqcomp| $(\scriptstyle\MLPOpeqcomprule)$: pushouts; +\item \verb|\MLTform| $(\scriptstyle\MLTformrule)$, + \verb|\MLTintro| $(\scriptstyle\MLTintrorule)$, + \verb|\MLTelim| $(\scriptstyle\MLTelimrule)$, \\ + \verb|\MLTcomp| $(\scriptstyle\MLTcomprule)$, + \verb|\MLTuniq| $(\scriptstyle\MLTuniqrule)$, + \verb|\MLTpeqintro| $(\scriptstyle\MLTpeqintrorule)$, \\ + \verb|\MLTpeqcomp| $(\scriptstyle\MLTpeqcomprule)$: truncations; +\item \verb|\MLtorusform| $(\scriptstyle\MLtorusformrule)$, + \verb|\MLtorusintro| $(\scriptstyle\MLtorusintrorule)$, + \verb|\MLtoruselim| $(\scriptstyle\MLtoruselimrule)$,\\ + \verb|\MLtoruscomp| $(\scriptstyle\MLtoruscomprule)$, + \verb|\MLtoruspeqintroa| $(\scriptstyle\MLtoruspeqintroarule)$, \\ + \verb|\MLtoruspeqintrob| $(\scriptstyle\MLtoruspeqintrobrule)$, + \verb|\MLtoruspeqintroc| $(\scriptstyle\MLtoruspeqintrocrule)$, \\ + \verb|\MLtoruspeqcompa| $(\scriptstyle\MLtoruspeqcomparule)$, + \verb|\MLtoruspeqcompb| $(\scriptstyle\MLtoruspeqcompbrule)$, \\ + \verb|\MLtoruspeqcompc| $(\scriptstyle\MLtoruspeqcompcrule)$: + the torus type. +\end{itemize} + +\subsection{Defining new inference rules} +Of course, the reader is encouraged to develop her own abbreviations +starting from the provided ones. To this aim two commands are +provided. They share the same syntax: \verb|\prfMakeInferenceRule| and +\verb|\prfMakeInferenceRuleRef| take two arguments, the first one is +the name of the command associated to the inference rule, and the +second one is used to write the rule name. For example, +\begin{center} + \verb|\prfMakeInferenceRule{NDANDI}{\mathord{\wedge}\textup{I}}| +\end{center} +is how the conjunction introduction rule is defined, and +\begin{center} + \verb| \prfMakeInferenceRuleRef{NDOREL}{\mathord{\vee}\textup{E}}| +\end{center} +is how the disjunction elimination rule is defined. The rules +generated by the \verb|Ref| variant use their first argument as the +reference to the assumption(s) they discharge. + +\subsection{Stacking proofs and assumptions} +Sometimes, a proof is too large to fit into the text width. Although +some strategies could be implemented to compress it, see the next +section, they fail in extreme cases. For example, the elimination rule +for the circle in Homotopy type theories is: +\begin{displaymath} + \MLScomp + {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i} + {\Gamma \vdash b \type C[\basepoint/x]} + {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b} + {\Gamma \vdash p \type \mathbb{S}^1} + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{displaymath} +typeset by +\begin{verbatim} + \MLScomp + {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i} + {\Gamma \vdash b \type C[\basepoint/x]} + {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b} + {\Gamma \vdash p \type \mathbb{S}^1} + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{verbatim} +It is clear that on an A5 paper, there is not enough space to write it +down. In these cases, the package provides a way to \emph{stack} the +premises of a rule, obtaining +\begin{displaymath} + \MLScomp + {\prfStackPremises + {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i} + {\Gamma \vdash b \type C[\basepoint/x]} } + {\prfStackPremises + {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b} + {\Gamma \vdash p \type \mathbb{S}^1} } + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{displaymath} +The corresponding \LaTeX{} code is +\begin{verbatim} + \MLScomp + {\prfStackPremises + {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i} + {\Gamma \vdash b \type C[\basepoint/x]} + } + {\prfStackPremises + {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b} + {\Gamma \vdash p \type \mathbb{S}^1} + } + {\Gamma \vdash + \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) \type C[p/x]} +\end{verbatim} +The command +\verb|\prfStackPremises{|$a_1$\verb|}{|$\ldots$\verb|}{|$a_n$\verb|}| +takes the arguments $a_1, \ldots, a_n$ and typeset them as a proof +tree with no lines with $a_1$ on the top. + +Actually, stacking proofs is possible: +\begin{displaymath} + \MLScomp + {\prfStackPremises + {\prfsummary{\Gamma\;\context} + {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type + \universe_i}} + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \basepoint \type \mathbb{S}^1}} } + {\prfStackPremises + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \ell \type \basepoint = \basepoint}} + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash p \type \mathbb{S}^1}} } + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{displaymath} +has been typeset by +\begin{verbatim} + \MLScomp + {\prfStackPremises + {\prfsummary{\Gamma\;\context} + {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type + \universe_i}} + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \basepoint \type \mathbb{S}^1}} + } + {\prfStackPremises + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \ell \type \basepoint = \basepoint}} + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash p \type \mathbb{S}^1}} + } + {\Gamma \vdash + \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) \type C[p/x]} +\end{verbatim} + +Since a stack is a proof tree, the parameters could be locally changed +to control its appearance. For example +\begin{displaymath} + \MLScomp + {\prfemptylinethickness20\prflinethickness + \prfStackPremises + {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i} + {\Gamma \vdash b \type C[\basepoint/x]} } + {\prfStackPremises + {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b} + {\Gamma \vdash p \type \mathbb{S}^1} } + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{displaymath} +makes the lines in the left stack far apart. +\begin{verbatim} + \MLScomp + {\prfemptylinethickness20\prflinethickness + \prfStackPremises + {\Gamma, x \type \mathbb{S}^1 \vdash C \type \universe_i} + {\Gamma \vdash b \type C[\basepoint/x]} } + {\prfStackPremises + {\Gamma \vdash \ell \type b =_{\loopcons}^{C} b} + {\Gamma \vdash p \type \mathbb{S}^1} } + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{verbatim} + +Spacing in stacks of proofs is normally difficult to control: if +really sophisticated formatting is needed, it is better to consider +the following option: +\begin{displaymath} + \MLScomp + {\prfassumption{ + \begin{array}{@{}c@{\quad}c@{}} + {\prfsummary{\Gamma\;\context} + {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type + \universe_i}} & + {\Gamma \vdash \ell \type \basepoint = \basepoint} \\ + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \basepoint \type \mathbb{S}^1}} & + {\Gamma \vdash p \type \mathbb{S}^1} + \end{array}}} + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{displaymath} +which uses the \verb|array| environment +\begin{verbatim} + \MLScomp + {\prfassumption{ + \begin{array}{@{}c@{\quad}c@{}} + {\prfsummary{\Gamma\;\context} + {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type + \universe_i}} & + {\Gamma \vdash \ell \type \basepoint = \basepoint} \\ + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \basepoint \type \mathbb{S}^1}} & + {\Gamma \vdash p \type \mathbb{S}^1} + \end{array}}} + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{verbatim} +or similar ones, using the multitude of packages to format tables. By +the way, the obvious solution using stacks is +\begin{displaymath} + \MLScomp + {\prfStackPremises + {\prfsummary{\Gamma\;\context} + {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type + \universe_i}} + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \basepoint \type \mathbb{S}^1}} } + {\prfStackPremises + {\prfassumption + {\Gamma \vdash \ell \type \basepoint = \basepoint}} + {\prfassumption + {\Gamma \vdash p \type \mathbb{S}^1}} } + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{displaymath} +\begin{verbatim} + \MLScomp + {\prfStackPremises{\prfsummary{\Gamma\;\context} + {\Gamma, x \type \mathbb{S}^1 \vdash \mathbb{S}^1 \type + \universe_i}} + {\prfsummary{\Gamma\;\context} + {\Gamma \vdash \basepoint \type \mathbb{S}^1}} } + {\prfStackPremises{\prfassumption + {\Gamma \vdash \ell \type \basepoint = \basepoint}} + {\prfassumption + {\Gamma \vdash p \type \mathbb{S}^1}} } + {\Gamma \vdash \ind_{\mathbb{S}^1}(x.\, C, b, \ell, \basepoint) + \type C[p/x]} +\end{verbatim} + +%------------------------------------- +\clearpage +\section{Hints and Tricks}\label{sec:hints_and_tricks} +This section shows a few hints and tricks to use the package at its +best.\vspace{2ex} + +Consider the proof: +\begin{displaymath} + \begin{prfenv} + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{a:notA}{A}}{\neg\neg A \supset A}} + {\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} + \end{prfenv} +\end{displaymath} +the space between the axiom and the sub-proof of the positive case is +visually much less than the space between the positive and the +negative cases. Looking at boxes, the space is exactly the same, but +the perception is that spacing is wrong. + +We can correct this perception in two distinct ways: by adding space +between the axiom and the positive case; or, conversely, by moving the +negative case closer to the positive one. + +The first strategy yields: +\begin{displaymath} + \begin{prfenv} + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.8em}} + {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} + {\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} + \end{prfenv} +\end{displaymath} +and this effect is given by adding an appropriate \verb|\hspace| after +the axiom, as in +\begin{verbatim} + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.4em}} + {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} + {\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} +\end{verbatim} + +Adding the same space in front of the positive case is equivalent. + +The second strategy yields: +\begin{displaymath} + \begin{prfenv} + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} + {\hspace{-.4em}\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} + \end{prfenv} +\end{displaymath} +Again, this is obtained by adding a negative \verb|hspace| after the +positive case, or, equivalently, before the negative one: +\begin{verbatim} + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} + {\hspace{-.8em}\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} +\end{verbatim} + +In general, to make a wide proof \emph{compact}, one can appropriately +add negative spaces in front of sub-proofs so to make them closer and +letting them to overlap as boxes, but not visually, thus \emph{tiling} +the space.\vspace{2ex} + +Since proof trees are boxes, it is easy to align them on need. For +example the following proof tree, with the bounding box put in +evidence +\begin{displaymath} + \fbox{\prfsummarystyle=1 + \prfsummary{A}{B}{A \wedge B}} +\end{displaymath} +can be used wherever a box may appear. In the flow of text, it will +look like \fbox{\prfsummarystyle=1\prfsummary{A}{B}{A \wedge B}}, so +that the conclusion is aligned with the baseline. This makes easier to +align proof trees, as in +\begin{center} + \fbox{\prfsummarystyle=1 + \prfsummary{f}{g}{f \wedge g}}\qquad + \fbox{$\begin{prfenv} + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} + {\hspace{-.4em}\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} + \end{prfenv}$} +\end{center} +since this is the natural way to put proofs side by side: +\begin{verbatim} + \fbox{\prfsummarystyle=1 + \prfsummary{f}{g}{f \wedge g}}\qquad + \fbox{$ + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} + {\hspace{-.4em}\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A}$} +\end{verbatim} + +But, if really one has to include a proof tree in the flow of text, it +is slightly better to vertically centre the box, as in +\fbox{$\vcenter{\prfsummary{A}{B}{A \wedge B}}$}. This is obtained by +\begin{verbatim} + $\vcenter{\prfsummary{A}{B}{A \wedge B}}$ +\end{verbatim} + +Of course, the result is not pleasant, because rows are far apart, +which is unavoidable because of the height of the proof tree. + +The same principle applies also to arrays of proof trees: +\begin{displaymath} + \begin{array}{lcccc} + \text{some text} & + \setcounter{prfsummarycounter}{0} + \setcounter{prfassumptioncounter}{0} + {\prfsummarystyle=1 + \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}} + \end{array} +\end{displaymath} +which has been typeset by +\begin{verbatim} + \begin{array}{lcccc} + \text{some text} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} & + {\prfsummarystyle=1 + \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}} + \end{array} +\end{verbatim} +vertically aligns the cells to their baselines. + +On the contrary +\begin{displaymath} + \begin{array}{lcccc} + \text{some text} & + \setcounter{prfsummarycounter}{0} + \setcounter{prfassumptioncounter}{0} + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} & + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} & + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} & + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}} + \end{array} +\end{displaymath} +is much better, and it is obtained by +\begin{verbatim} + \begin{array}{lcccc} + \text{some text} & + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} & + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} & + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} & + \vcenter{\prfsummarystyle=1 + \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}} + \end{array} +\end{verbatim}\vspace{2ex} + +The labelling of proof summaries is useful when a proof is very large +and there is the need to split it. The strategy is to select some +sub-proofs and to show them as summaries: instead of writing +\begin{displaymath} + \setcounter{prfsummarycounter}{0} + \setcounter{prfassumptioncounter}{0} + \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} + {\NDIMPIL{a:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}} + {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} +\end{displaymath} +we may consider to define +\begin{displaymath} + \setcounter{prfsummarycounter}{0} + \setcounter{prfassumptioncounter}{0} + \mbox{Let } + \left(\vcenter{\prfsummary<[f]s:abbrev> + {\NDDL{s:notnotA}{\neg\neg A}} + {\NDAL{s:notA}{\neg A}} + {\neg\neg A \supset A}}\right) + \equiv + \left(\vcenter{\NDIMPIL{s:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}} + {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}}\right) +\end{displaymath} +allowing to abbreviate the whole proof as +\begin{displaymath} + \NDOREL{s:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}} + {\hspace{-1em}\prfsummary<s:abbrev> + {\NDDL{[l]s:notnotA}{\neg\neg A}} + {\NDDL{[l]s:notA}{\neg A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} +\end{displaymath} + +The corresponding \LaTeX{} code is +\begin{verbatim} + \setcounter{prfsummarycounter}{0} + \setcounter{prfassumptioncounter}{0} + \mbox{Let } + \left(\vcenter{\prfsummary<[f]s:abbrev> + {\NDDL{s:notnotA}{\neg\neg A}} + {\NDAL{s:notA}{\neg A}} + {\neg\neg A \supset A}}\right) + \equiv + \left(\vcenter{\NDIMPIL{s:notnotA} + {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}} + {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}} + {\neg\neg A \supset A}}\right) +\end{verbatim} +for the definition of the proof summary, and +\begin{verbatim} + \NDOREL{s:notA}{\NDLEM{A \vee \neg A}} + {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}} + {\hspace{-1em}\prfsummary<s:abbrev> + {\NDDL{[l]s:notnotA}{\neg\neg A}} + {\NDDL{[l]s:notA}{\neg A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} +\end{verbatim} +for its use. + +% ------------------------------------- +\clearpage +\section{More Examples}\label{sec:examples} +This section shows a number of examples illustrating the package. See +the previous sections for the description of the features.\vspace{2ex} + +The disjunction elimination rule, with various line options: +\begin{displaymath} + \renewcommand{\arraystretch}{3.7} + \begin{array}{@{}ccc@{}} + {\prfsummarystyle=1 + \prftree{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[r]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[l]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} \\ + {\prfsummarystyle=1 + \prftree[d]{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[r][d]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[l][d]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} \\ + {\prfsummarystyle=1 + \prftree[dotted]{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[r,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[l,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} \\ + {\prfsummarystyle=1 + \prftree[d,dotted]{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[r,d,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[l,d,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} \\ + {\prfsummarystyle=1 + \prftree[dashed]{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[r,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[l,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} \\ + {\prfsummarystyle=1 + \prftree[d,dashed]{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[d,r,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[d,l,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} \\ + {\prfsummarystyle=1 + \prftree[f]{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[r,f]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[l,f]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} \\ + {\prfsummarystyle=1 + \prftree[noline]{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[noline][r]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} & + {\prfsummarystyle=1 + \prftree[noline][l]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}} + {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}} + {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}} + {C}} + \end{array} +\end{displaymath} + +Proof that the Law of Excluded middle implies $\neg\neg A \supset A$: +\begin{displaymath} + \prfIMPOptiontrue + \NDORE + {\NDLEM + {A \vee \neg A}\hspace{.4em}} + {\NDIMPI + {\NDD{A}} + {\neg\neg A \supset A}} + {\NDIMPI + {\NDFE + {\NDIMPE + {\NDD{\neg\neg A}} + {\NDD{\neg A}} + {\bot}} + {A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} + \prfIMPOptionfalse +\end{displaymath} + +Proof that the Law of Excluded middle implies $\neg\neg A \supset A$ +with labels instead of rule names, except on axioms: +\begin{displaymath} + \prftree[l]{$\scriptstyle\vee\mathrm{E}$} + {\NDLEM + {A \vee \neg A}\hspace{.6em}} + {\prftree[l]{$\scriptstyle\supset\mathrm{I}$} + {\NDD{A}} + {\neg\neg A \supset A}} + {\prftree[l]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[l]{$\scriptstyle\bot\mathrm{E}$} + {\prftree[l]{$\scriptstyle\supset\mathrm{E}$} + {\NDD{\neg\neg A}} + {\NDD{\neg A}} + {\bot}} + {A}} + {\neg\neg A \supset A}} + {\neg\neg A \supset A} +\end{displaymath} + +Another simple proof in natural deduction: +\begin{displaymath} + \prftree + {\prftree + {\prftree + {\prftree + {\prftree + {\prfboundedassumption{A \rightarrow (B \rightarrow C)}} + {\prfboundedassumption{A}} + {B \rightarrow C}\hspace{2em}} + {\prftree + {\prfboundedassumption{A \rightarrow B}} + {\prfboundedassumption{A}} + {B}} + {C}} + {A \rightarrow C}} + {(A \rightarrow B) \rightarrow (A \rightarrow C)}} + {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) + \rightarrow (A \rightarrow C))} +\end{displaymath} + +The same proof, under the proposition-as-types interpretation: +\begin{displaymath} + \prftree + {\prftree + {\prftree + {\prftree + {\prftree + {\prfassumption{u\colon A \rightarrow (B \rightarrow C)}} + {\prfassumption{w\colon A}} + {u w\colon B \rightarrow C}\hspace{2em}} + {\prftree + {\prfassumption{v\colon A \rightarrow B}} + {\prfassumption{w\colon A}} + {v w\colon B}} + {u w(v w)\colon C}} + {\lambda w.\, u w(v w)\colon A \rightarrow C}} + {\lambda v w.\, u w(v w)\colon (A \rightarrow B) \rightarrow (A + \rightarrow C)}} + {\lambda u v w.\, u w(v w)\colon (A \rightarrow (B \rightarrow C)) + \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))} +\end{displaymath} + +A deduction in a sequent calculus: +\begin{displaymath} + \prfinterspace=1.2em + \prftree + {\prftree + {\prftree + {\prftree + {\prfassumption{A \Rightarrow A}} + {\prftree + {\prfassumption{A \Rightarrow A}} + {\prftree + {B \Rightarrow B} + {C \Rightarrow C} + {B, B \rightarrow C \Rightarrow C}} + {A, A \rightarrow B, B \rightarrow C \Rightarrow C}} + {A, A \rightarrow B, A \rightarrow (B \rightarrow C) + \Rightarrow C}} + {A \rightarrow B, A \rightarrow (B \rightarrow C) \Rightarrow A + \rightarrow C}} + {A \rightarrow (B \rightarrow C) \Rightarrow (A \rightarrow B) + \rightarrow (A \rightarrow C)}} + {\Rightarrow (A \rightarrow (B \rightarrow C)) \rightarrow ((A + \rightarrow B) \rightarrow (A \rightarrow C))} +\end{displaymath} + +Proof trees can be coloured, as kindly pointed out by Dominic Hughes: +\begin{displaymath} + \begin{prfenv} + \color{green}\NDIMPIL{ex6:1} + {\NDANDI + {\color{red}\NDNOTIL{ex6:2} + {\NDNOTE + {\NDDL{ex6:1}{\neg (A \vee B)}} + {\NDORIL + {\NDDL{ex6:2}{A}} + {A \vee B}} + {\bot}} + {\neg A}} + {\color{blue}\NDNOTIL{ex6:3} + {\NDNOTE + {\NDDL{[l]ex6:1}{\neg (A \vee B)}} + {\NDORIR + {\NDDL{ex6:3}{B}} + {A \vee B}} + {\bot}} + {\neg B}} + {\neg A \wedge \neg B}} + {\neg (A \vee B) \supset \neg A \wedge \neg B} + \end{prfenv} +\end{displaymath}\vspace{.2ex} + +Also. all the standard box manipulation commands can be freely applied. +The following examples are not significant for doing mathematics, but +the mechanics behind can be occasionally useful, for example, to +shrink a large proof to fit the page length: +\begin{displaymath} + \rotatebox{15}{\begin{prfenv} + \NDIMPIL{ex5:1} + {\NDANDI + {\NDNOTIL{ex5:2} + {\NDNOTE + {\NDDL{ex5:1}{\neg (A \vee B)}} + {\NDORIL + {\NDDL{ex5:2}{A}} + {A \vee B}} + {\bot}} + {\neg A}} + {\NDNOTIL{ex5:3} + {\NDNOTE + {\NDDL{[l]ex5:1}{\neg (A \vee B)}} + {\NDORIR + {\NDDL{ex5:3}{B}} + {A \vee B}} + {\bot}} + {\neg B}} + {\neg A \wedge \neg B}} + {\neg (A \vee B) \supset \neg A \wedge \neg B} + \end{prfenv}} +\end{displaymath} +\begin{displaymath} + \begin{prfenv} + \NDIMPIL{ex7:1} + {\NDANDI + {\reflectbox{\NDNOTIL{ex7:2} + {\NDNOTE + {\NDDL{ex7:1}{\neg (A \vee B)}} + {\NDORIL + {\NDDL{ex7:2}{A}} + {A \vee B}} + {\bot}} + {\neg A}}} + {\resizebox{20em}{!}{\NDNOTIL{ex7:3} + {\NDNOTE + {\NDDL{[l]ex7:1}{\neg (A \vee B)}} + {\scalebox{.7}[1]{\NDORIR + {\NDDL{ex7:3}{B}} + {A \vee B}}} + {\bot}} + {\neg B}}} + {\neg A \wedge \neg B}} + {\neg (A \vee B) \supset \neg A \wedge \neg B} + \end{prfenv} +\end{displaymath} + +% ------------------------------------- +\clearpage +\section{Fonts}\label{sec:fonts} +The package works with any font. It uses the current math fonts for +typesetting proofs, while it uses the current text font to typeset +labels and rule names. + +Care has been taken to ensure that the various dimensions and +parameters in Section~\ref{sec:parameters} are relative to the current +font, that is, technically, they are expressed with units \texttt{ex} +for vertical lengths, and \texttt{em} for horizontal lengths. Dashes +are \TeX\ rules with thickness \verb|\prflinethickness|. + +For unknown reasons, the \texttt{fontenc} package modifies slightly +the values for \texttt{ex} and \texttt{em}, thus the graphical +appearance of proof trees may vary when comparing the results obtained +by compiling with and without this package. + +In most cases, the graphical appearance of proofs is acceptable, even +changing font and size. But using fonts whose body is particularly +heavy, may result in proof lines which are too thin. In this case, the +user of the package should increment the value of +\verb|\prflinethickness|. + +The package, up to version 1.5, was designed to work with the Computer +Modern family of fonts. It worked also with other fonts, without any +major problem, but, as kindly signalled by D{\'e}mi Nollet at ENS Lyon +and universit{\'e} Paris-Diderot, dashed and dotted lines do not +behave correctly, as dashes overlap. Please, update to the latest +version of the package if you plan to use fonts different from +Computer Modern. + +% ------------------------------------- +\clearpage +\section{Internals}\label{sec:internals} +A proof tree is typeset as a \TeX{} box in horizontal mode. This means +that wherever a character can stay, so does a proof: in principle, +there is no need to put the proof in a math environment. Also, the +width of a proof is exactly the width of the box; the height of the +proof is the height of the conclusion plus the total height of all the +matter above it; the depth of the proof is the depth of the +conclusion. The proof is aligned so that the current baseline is the +baseline of the conclusion. + +For example, the proof of $g \supset \neg\neg g$ in natural deduction +is: +\begin{displaymath} + \mbox{proof} \equiv + \fbox{\prftree[r]{$\supset$I} + {\prftree[r]{$\supset$I} + {\prftree[r]{$\supset$E} + {\prfboundedassumption{g}} + {\prfboundedassumption{\neg g}} + {\bot}} + {\neg\neg g}} + {g \supset \neg\neg g}} +\end{displaymath} +The proof has been surrounded by a framebox to make evident its +bounds. Also, since the letter $g$ has a depth, the example shows how +depth in the conclusion influences the alignment of the proof with +respect to the preceding text.\vspace{2ex} + +Actually, the fundamental command in the package is \verb|\prftree|: +the commands to construct assumptions (\verb|\prfassumption| and +\verb|\prfboundedassumption|), those to generate axioms +(\verb|\prfaxiom| and \verb|\prfbyaxiom|), and \verb|\prfsummary| are +just appropriate instances.\vspace{2ex} + +The \verb|\prftree| command is composed by a parser, which takes care +of reading the various options and parameters, and by a graphical +engine, \verb|\prf@draw|, which calculates and draw the box containing +the proof tree. + +It may be useful to understand how the graphical engine works. In the +first place, each proof tree is a box with a structure: +\begin{center} + {\setlength{\unitlength}{1em} + \begin{picture}(27,6) + \put(0.8,0){\framebox(26.2,6){}} + \put(5,4){\framebox(18,1.8){$\cdots$}} + \put(5.2,4.2){\framebox(6,1.4){$\mbox{assumption}_1$}} + \put(16.8,4.2){\framebox(6,1.4){$\mbox{assumption}_n$}} + \put(7,3){\line(1,0){14}} + \put(22,2.3){\framebox(4.8,1.4){rule name}} + \put(1,2.3){\framebox(4.8,1.4){label}} + \put(8.5,0.2){\framebox(11,1.8){conclusion}} + \end{picture}} +\end{center} + +The conclusion, the proof line, and the \emph{assumption line} are +centred. The assumption line is the line whose first element is the +conclusion of the first assumption, and whose last element is the +conclusion of the last assumption, properly spaced so that all the +assumptions fit in between. The width of the proof line is calculated +as the maximum of the width of the assumption line and the conclusion, +with the rule name and the label, if present, hanging on the right and +the left, respectively. + +To calculate the assumption line, the engine keeps track of the +position of the conclusion within a proof tree, which reduces to +remember how far is the conclusion from the left margin +(\verb|Lassum|), and how far it is from the right margin +(\verb|Rassum|). So, the assumption line starts from the value of +\verb|Lassum| of the first assumption, and finishes at \verb|Rassum| +of the last assumption. + +Thus, with these values it is not difficult to figure out the +mathematics to place the various boxes around, so to combine them into +a proof tree. This is exactly what the graphical engine does. + +Unfortunately, when one writes assumptions as simple formulae, without +the \verb|\prfassumption| command, the corresponding \verb|Lassum| and +\verb|Rassum| are not set to $0$, which is the right value. In fact, +the recursive expansion of the \verb|\prf@draw| macro follows the +\emph{natural} order in the construction of the proof box, which is +extremely useful because it allows to locally modify parameters in +sub-proofs; but this order conflicts with proper rendering of +assumptions which are not proof trees. + +Also, the hints on how to put space between assumptions, see +Section~\ref{sec:hints_and_tricks}, may have strange effects: if space +is added in front of the first assumption or behind the last one, this +space makes invalid the values of \verb|Lassum| and \verb|Rassum|, +respectively, yielding hard to predict results. + +It is worth remarking that the mathematics of the graphical engine is +sound, which means that zero or negative values for the various +dimensions specified as parameters, or using \emph{bizarre} boxes in +the fancy commands, yields the expected results, as far as boxes do +not have parts which extends beyond the bounds.\vspace{2ex} + +The implementation of references mimics the implementation of +\verb|\label| and \verb|\ref| in \LaTeX. Whenever a reference is +defined, through a command with the $\langle \mathrm{label}\rangle$ as +the first argument, the reference value is created according to the +options, and it gets stored in the \texttt{.aux} file, by writing +$\verb|\prfauxvalue|\{\mathrm{label}\}\{\mathrm{value}\}$ in the +file. Then, when the source code will be recompiled, and the +\texttt{.aux} file read, this command will be executed before any +occurrence of a reference, which can be resolved. + +Most difficulties in the implementation of references lie in the way +to construct the boxes to be used in the proof tree. But, the tricky +part is the interaction with the \LaTeX{} and \TeX{} kernel for error +reporting. A small hack has been introduced to force recompilation +when the references in a proof change. + +% ------------------------------------- +\clearpage +\section{Future Features and Bugs}\label{sec:future_features} +Essentially, all the features of Buss's package have been implemented +but one: alignment of proofs according to the $\vdash$ (or equivalent) +sign. While this feature is occasionally useful in the writing of +sequent proofs, it requires some trickery in the graphical engine, so +it has been postponed for the moment.\vspace{2ex} + +Moreover, automatic compact proofs have been analysed, but not +implemented. A compact proof minimises the amount of space between +subsequent assumptions, eventually making the upper trees to overlap +as boxes, but not as typed text. + +The algorithm to obtain this result is not immediate: one should keep +track of the left and right \emph{skylines} of a proof. Comparing the +left skyline of an assumption with the right skyline of the next one, +one can calculate what is the distance between the boxes so that the +distance between the closest points in the skylines is exactly +\verb|\prfinterspace|. + +It is not simple to code such an algorithm in \TeX{}, but the real +difficulty is how to represent skylines and how to store them, since +\TeX{} provides no abstract data structures. Hence, the implementation +of this feature has been postponed to a remote future, or to the will +of a real \TeX{} magician.\vspace{2ex} + +The abbreviated commands reflect their use by the author. It is quite +possible that you want to define your own commands for inference rules +of your interest. If you think they could be of general interest, send +them by email to the author (see below) who will include them in a +future release of the package, acknowledging your contribution. +\vfill + +Although the package has been tested for a long time by now, it is +possible that a few bugs are still present. To signal a bug, please, +write an email to the author (see below), possibly attaching a sample +document which exhibit the misbehaviour, to help tracking and fixing. +\vfill +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: |