summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/prftree
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2019-06-19 20:35:11 +0000
committerKarl Berry <karl@freefriends.org>2019-06-19 20:35:11 +0000
commita1eb6c9ee4af7077c2880c37f051b564b8e05ca7 (patch)
tree5c34083fb183cb91bcdb5d92bc88bb1bc1d45c1c /Master/texmf-dist/doc/latex/prftree
parent41be7740176343cd88808bef0d403a044b4c5895 (diff)
prftree (19jun19)
git-svn-id: svn://tug.org/texlive/trunk@51404 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex/prftree')
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.pdfbin280556 -> 346581 bytes
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.tex781
2 files changed, 686 insertions, 95 deletions
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
index 3e4ed547069..5f3b0a615e6 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
index 1fe8d227c6c..19477fa856f 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
@@ -1,8 +1,9 @@
\documentclass{amsart}
\usepackage{color}
\usepackage{graphics}
-\usepackage[ND,SEQ]{prftree}
+\usepackage[ND,SEQ,EQ,ML]{prftree}
\usepackage{url}
+\usepackage{microtype}
\setlength{\fboxsep}{0pt}
@@ -54,7 +55,7 @@ textbooks, e.g., A.S.~Troelstra and H.~Schwichtenberg, \textit{Basic
% --------------------------
\clearpage
\section{Basic Commands}\label{sec:basic_commands}
-The package is invoked by putting \verb|\usepackage{prfree.sty}| in
+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}
@@ -157,8 +158,7 @@ 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\footnote{The reader is invited to look at the source code of
- the documentation to see how these examples have been implemented.}:
+options:
\begin{displaymath}
\begin{array}{lcc@{\qquad}l}
\mbox{default (single straight)} &
@@ -207,7 +207,14 @@ options\footnote{The reader is invited to look at the source code of
{A}{B}{A \wedge B} &
\texttt{[noline]}
\end{array}
-\end{displaymath}\vspace{1ex}
+\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}
@@ -967,42 +974,128 @@ the last used value.
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. By loading the package as
-\verb|\usepackage[ND]{prftree.sty}|, the following abbreviations are
-available, which correspond to the inference rule of natural deduction
-calculi:
+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|: bounded assumption;
-\item \verb|\NDDL|: labelled bounded assumption;
+\item \verb|\NDD|: discharged assumption;
+\item \verb|\NDDL|: labelled discharged assumption;
\item \verb|\NDP|: generic proof tree;
-\item \verb|\NDANDI|: conjunction introduction;
-\item \verb|\NDANDER|: conjunction elimination, right;
-\item \verb|\NDANDEL|: conjunction elimination, left;
-\item \verb|\NDANDE|: conjunction elimination, unspecified;
-\item \verb|\NDORIR|: disjunction introduction, right;
-\item \verb|\NDORIL|: disjunction introduction, left;
-\item \verb|\NDORI|: disjunction introduction, unspecified;
-\item \verb|\NDORE|: disjunction elimination;
-\item \verb|\NDOREL|: labelled disjunction elimination;
-\item \verb|\NDIMPI|: implication introduction;
-\item \verb|\NDIMPIL|: labelled implication introduction;
-\item \verb|\NDIMPE|: implication elimination;
-\item \verb|\NDNOTI|: negation introduction;
-\item \verb|\NDNOTIL|: labelled negation introduction;
-\item \verb|\NDNOTE|: negation elimination;
-\item \verb|\NDALLI|: universal quantifier introduction;
-\item \verb|\NDALLE|: universal quantifier elimination;
-\item \verb|\NDEXI|: existential quantifier introduction;
-\item \verb|\NDEXE|: existential quantifier elimination;
-\item \verb|\NDEXE|: labelled existential quantifier elimination;
-\item \verb|\NDTI|: truth introduction;
-\item \verb|\NDFE|: falsity elimination;
-\item \verb|\NDLEM|: law of Excluded Middle;
-\item \verb|\NDAX|: a generic axiom rule.
+\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
@@ -1033,36 +1126,127 @@ is typeset in abbreviated form by the following code
{\neg\neg A \supset A}
\end{verbatim}\vspace{2ex}
-Similarly, by loading the package as
-\verb|\usepackage[SEQ]{prftree.sty}|, the following abbreviations
-are available, which roughly correspond to the inference rule of
-sequent calculi:
+\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;
+\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;
-\item \verb|\SEQLF|: left falsity;
-\item \verb|\SEQLW|: left weakening;
-\item \verb|\SEQRW|: right weakening;
-\item \verb|\SEQLC|: left contraction;
-\item \verb|\SEQRC|: right contraction;
-\item \verb|\SEQLAND|: left conjunction;
-\item \verb|\SEQRAND|: right conjunction;
-\item \verb|\SEQLOR|: left disjunction;
-\item \verb|\SEQROR|: right disjunction;
-\item \verb|\SEQLIMP|: left implication;
-\item \verb|\SEQRIMP|: right implication;
-\item \verb|\SEQLALL|: left universal quantification;
-\item \verb|\SEQRALL|: right universal quantification;
-\item \verb|\SEQLEX|: left existential quantification;
-\item \verb|\SEQREX|: right existential quantification;
-\item \verb|\SEQCUT|: cut rule.
+\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}
-One can load the package with both options at the same
-time.\vspace{2ex}
+\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
@@ -1071,10 +1255,402 @@ $\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.
+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
@@ -1202,8 +1778,9 @@ is slightly better to vertically centre the box, as in
\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:
+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} &
@@ -1219,6 +1796,7 @@ same principle applies also to arrays of proof trees:
\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} &
@@ -1284,21 +1862,21 @@ we may consider to define
\setcounter{prfsummarycounter}{0}
\setcounter{prfassumptioncounter}{0}
\mbox{Let }
- \vcenter{\prfsummary<[f]s:abbrev>
+ \left(\vcenter{\prfsummary<[f]s:abbrev>
{\NDDL{s:notnotA}{\neg\neg A}}
{\NDAL{s:notA}{\neg A}}
- {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}}\right)
\equiv
- \vcenter{\NDIMPIL{s:notnotA}
+ \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}}
+ {\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}}
- {\prfsummary<s:abbrev>
+ {\hspace{-1em}\prfsummary<s:abbrev>
{\NDDL{[l]s:notnotA}{\neg\neg A}}
{\NDDL{[l]s:notA}{\neg A}}
{\neg\neg A \supset A}}
@@ -1310,21 +1888,21 @@ The corresponding \LaTeX{} code is
\setcounter{prfsummarycounter}{0}
\setcounter{prfassumptioncounter}{0}
\mbox{Let }
- \vcenter{\prfsummary<[f]s:abbrev>
+ \left(\vcenter{\prfsummary<[f]s:abbrev>
{\NDDL{s:notnotA}{\neg\neg A}}
{\NDAL{s:notA}{\neg A}}
- {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}}\right)
\equiv
- \vcenter{\NDIMPIL{s:notnotA}
+ \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}}
+ {\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}}
- {\prfsummary<[l]s:abbrev>
+ {\hspace{-1em}\prfsummary<s:abbrev>
{\NDDL{[l]s:notnotA}{\neg\neg A}}
{\NDDL{[l]s:notA}{\neg A}}
{\neg\neg A \supset A}}
@@ -1467,37 +2045,39 @@ The disjunction elimination rule, with various line options:
Proof that the Law of Excluded middle implies $\neg\neg A \supset A$:
\begin{displaymath}
- \prftree[r]{$\vee$E}
- {\prfbyaxiom{LEM}
+ \prfIMPOptiontrue
+ \NDORE
+ {\NDLEM
{A \vee \neg A}\hspace{.4em}}
- {\prftree[r]{$\supset$I}
- {\prfboundedassumption{A}}
+ {\NDIMPI
+ {\NDD{A}}
{\neg\neg A \supset A}}
- {\prftree[r]{$\supset$I}
- {\prftree[r]{$\bot$E}
- {\prftree[r]{$\supset$E}
- {\prfboundedassumption{\neg\neg A}}
- {\prfboundedassumption{\neg 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]{$\vee$E}
- {\prfbyaxiom{LEM}
+ \prftree[l]{$\scriptstyle\vee\mathrm{E}$}
+ {\NDLEM
{A \vee \neg A}\hspace{.6em}}
- {\prftree[l]{$\supset$I}
- {\prfboundedassumption{A}}
+ {\prftree[l]{$\scriptstyle\supset\mathrm{I}$}
+ {\NDD{A}}
{\neg\neg A \supset A}}
- {\prftree[l]{$\supset$I}
- {\prftree[l]{$\bot$E}
- {\prftree[l]{$\supset$E}
- {\prfboundedassumption{\neg\neg A}}
- {\prfboundedassumption{\neg 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}}
@@ -1572,7 +2152,7 @@ A deduction in a sequent calculus:
\rightarrow B) \rightarrow (A \rightarrow C))}
\end{displaymath}
-Proof tree can be coloured, as kindly pointed out by Dominic Hughes:
+Proof trees can be coloured, as kindly pointed out by Dominic Hughes:
\begin{displaymath}
\begin{prfenv}
\color{green}\NDIMPIL{ex6:1}
@@ -1823,12 +2403,23 @@ 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.
+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
+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: