diff options
Diffstat (limited to 'Master')
| -rw-r--r-- | Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf | bin | 280556 -> 346581 bytes | |||
| -rw-r--r-- | Master/texmf-dist/doc/latex/prftree/prftreedoc.tex | 781 | ||||
| -rw-r--r-- | Master/texmf-dist/tex/latex/prftree/prftree.sty | 532 |
3 files changed, 1123 insertions, 190 deletions
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf Binary files differindex 3e4ed547069..5f3b0a615e6 100644 --- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf +++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf 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: diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty index 8f77541c058..10d6fbce6c2 100644 --- a/Master/texmf-dist/tex/latex/prftree/prftree.sty +++ b/Master/texmf-dist/tex/latex/prftree/prftree.sty @@ -1,7 +1,7 @@ % % prftree.sty -% by Marco Benini - 3rd September 2016 -% v1.5 +% by Marco Benini - 19th June 2019 +% v1.6 % % A package to typeset natural deduction proofs, or sequent proofs, or % tableau proofs @@ -10,18 +10,25 @@ % \NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{prftree}[2016/09/03 Natural Deduction Proofs] +\ProvidesPackage{prftree}[2019/06/19 Natural Deduction Proofs] % Package options: deactivated by default \newif\ifprf@NDOption\prf@NDOptionfalse \newif\ifprf@SEQOption\prf@SEQOptionfalse \newif\ifprfIMPOption\prfIMPOptionfalse +\newif\ifprf@EQOption\prf@EQOptionfalse +\newif\ifprf@MLOption\prf@MLOptionfalse +\newif\ifprf@MLnodefOption\prf@MLnodefOptionfalse +% but the STRUT and STRUTlabel are on by default \newif\ifprfSTRUToption\prfSTRUToptiontrue \newif\ifprfSTRUTlabeloption\prfSTRUTlabeloptiontrue \DeclareOption{ND}{\prf@NDOptiontrue} \DeclareOption{SEQ}{\prf@SEQOptiontrue} \DeclareOption{IMP}{\prfIMPOptiontrue} +\DeclareOption{EQ}{\prf@EQOptiontrue} +\DeclareOption{ML}{\prf@MLOptiontrue} +\DeclareOption{MLnodef}{\prf@MLnodefOptiontrue} \DeclareOption{Strut}{\prfSTRUToptionfalse} \DeclareOption{StrutLabel}{\prfSTRUTlabeloptionfalse} \ProcessOptions\relax @@ -977,14 +984,42 @@ \hbox{$\box\prf@rulenamebox$}} % ------------------------------------------------------------------- -% The following macros are used to simplify the writing of proofs in -% natural deduction, and they roughly follow the format of proofs as -% in Troelstra, Schwichtenberg "Basic Proof Theory". -% -% Since they may conflict with other packages, they are controlled by -% options in the package. +% Support macros to define new inference rules +% +% \prfMakeInferenceRule#1#2 +% \prfMakeInferenceRuleRef#1#2 +% #1: name of the command associated to the inference rule +% #2: rule name +% The plain version generates a command for typesetting a proof with +% the inference rule; the Ref version uses the first parameter of the +% rule as a reference that is appended to the rule name % ------------------------------------------------------------------- +\def\prfMakeInferenceRule#1#2{% + \expandafter\def\csname #1\endcsname% + {\prftree[by]{$\scriptstyle{#2}$}}} +\def\prfMakeInferenceRuleRef#1#2{% + \expandafter\def\csname #1\endcsname##1% + {\prftree[by]{$\scriptstyle{#2}^{\prfref<##1>}$}}} + +% ------------------------------------------------------------------- +% Macros to stack the premises of an inference rule +% +% \prfStackPremises{a_1}...{a_n} generates a vertical list containing +% a_1 on the top and a_n on the bottom. +% ------------------------------------------------------------------- + +\def\prfStackPremises{\prf@StackPremises{}} +\def\prf@StackPremises#1{\@ifnextchar\bgroup% + {\prf@@StackPremises{\prfassumption{#1}}}% + {\prfassumption{#1}}} +\def\prf@@StackPremises#1#2{\@ifnextchar\bgroup% + {\prf@@@StackPremises{\prftree[noline]{#1}{#2}}}% + {\prftree[noline]{#1}{#2}}} +\def\prf@@@StackPremises#1#2{\@ifnextchar\bgroup% + {\prf@@@StackPremises{\prftree[noline]{#1}{#2}}} + {\prftree[noline]{#1}{#2}}} + % ------------------------------------------------------------------- % Natural deduction systems % @@ -997,62 +1032,36 @@ \def\NDAL#1{\prfassumption<#1>} \def\NDDL#1{\prfboundedassumption<#1>} \def\NDP{\prftree} - \def\NDANDI{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \textup{I}$}} - \def\NDANDEL{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \textup{E}_1$}} - \def\NDANDER{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \textup{E}_2$}} - \def\NDANDE{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \textup{E}$}} - \def\NDORIL{\prftree[by]{$\scriptstyle\mathord{\vee}% - \textup{I}_1$}} - \def\NDORIR{\prftree[by]{$\scriptstyle\mathord{\vee}% - \textup{I}_2$}} - \def\NDORI{\prftree[by]{$\scriptstyle\mathord{\vee}% - \textup{I}$}} - \def\NDORE{\prftree[by]{$\scriptstyle\mathord{\vee}% - \textup{E}$}} - \def\NDOREL#1{\prftree[by]{$\scriptstyle{\vee}% - {\textup{E}}^{\prfref<#1>}$}} + \prfMakeInferenceRule{NDANDI}{\mathord{\wedge}\textup{I}} + \prfMakeInferenceRule{NDANDEL}{\mathord{\wedge}\textup{E}_1} + \prfMakeInferenceRule{NDANDER}{\mathord{\wedge}\textup{E}_2} + \prfMakeInferenceRule{NDANDE}{\mathord{\wedge}\textup{E}} + \prfMakeInferenceRule{NDORIL}{\mathord{\vee}\textup{I}_1} + \prfMakeInferenceRule{NDORIR}{\mathord{\vee}\textup{I}_2} + \prfMakeInferenceRule{NDORI}{\mathord{\vee}\textup{I}} + \prfMakeInferenceRule{NDORE}{\mathord{\vee}\textup{E}} + \prfMakeInferenceRuleRef{NDOREL}{\mathord{\vee}\textup{E}} \ifprfIMPOption - \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\supset}% - \textup{I}$}} - \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\supset}% - \textup{E}$}} - \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\mathord{\supset}% - \textup{I}^{\prfref<#1>}$}} + \prfMakeInferenceRule{NDIMPI}{\mathord{\supset}\textup{I}} + \prfMakeInferenceRule{NDIMPE}{\mathord{\supset}\textup{E}} + \prfMakeInferenceRuleRef{NDIMPIL}{\mathord{\supset}\textup{I}} \else - \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\rightarrow}% - \textup{I}$}} - \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\rightarrow}% - \textup{E}$}} - \def\NDIMPIL#1{% - \prftree[by]{$\scriptstyle\mathord{\rightarrow}% - \textup{I}^{\prfref<#1>}$}}\fi - \def\NDNOTI{\prftree[by]{$\scriptstyle\mathord{\neg}% - \textup{I}$}} - \def\NDNOTIL#1{\prftree[by]{$\scriptstyle{\neg}% - \textup{I}^{\prfref<#1>}$}} - \def\NDNOTE{\prftree[by]{$\scriptstyle\mathord{\neg}% - \textup{E}$}} - \def\NDALLI{\prftree[by]{$\scriptstyle\mathord{\forall}% - \textup{I}$}} - \def\NDALLE{\prftree[by]{$\scriptstyle\mathord{\forall}% - \textup{E}$}} - \def\NDEXI{\prftree[by]{$\scriptstyle\mathord{\exists}% - \textup{I}$}} - \def\NDEXE{\prftree[by]{$\scriptstyle\mathord{\exists}% - \textup{E}$}} - \def\NDEXEL#1{% - \prftree[by]{$\scriptstyle\mathord{\exists}% - \textup{E}^{\prfref<#1>}$}} - \def\NDTI{\prftree[by]{$\scriptstyle\mathord{\top}% - \textup{I}$}} - \def\NDFE{\prftree[by]{$\scriptstyle\mathord{\bot}% - \textup{E}$}} - \def\NDLEM{\prftree[by]{$\scriptstyle\textup{lem}$}} - \def\NDAX{\prftree[by]{$\scriptstyle\textup{ax}$}} + \prfMakeInferenceRule{NDIMPI}{\mathord{\rightarrow}\textup{I}} + \prfMakeInferenceRule{NDIMPE}{\mathord{\rightarrow}\textup{E}} + \prfMakeInferenceRuleRef{NDIMPIL}{\mathord{\rightarrow}\textup{I}} + \fi + \prfMakeInferenceRule{NDNOTI}{\mathord{\neg}\textup{I}} + \prfMakeInferenceRuleRef{NDNOTIL}{\mathord{\neg}\textup{I}} + \prfMakeInferenceRule{NDNOTE}{\mathord{\neg}\textup{E}} + \prfMakeInferenceRule{NDALLI}{\mathord{\forall}\textup{I}} + \prfMakeInferenceRule{NDALLE}{\mathord{\forall}\textup{E}} + \prfMakeInferenceRule{NDEXI}{\mathord{\exists}\textup{I}} + \prfMakeInferenceRule{NDEXE}{\mathord{\exists}\textup{E}} + \prfMakeInferenceRuleRef{NDEXEL}{\mathord{\exists}\textup{E}} + \prfMakeInferenceRule{NDTI}{\mathord{\top}\textup{I}} + \prfMakeInferenceRule{NDFE}{\mathord{\bot}\textup{E}} + \prfMakeInferenceRule{NDLEM}{\textup{lem}} + \prfMakeInferenceRule{NDAX}{\textup{ax}} \fi % ------------------------------------------------------------------- @@ -1064,41 +1073,374 @@ \ifprf@SEQOption% \def\SEQA{\prfassumption} \def\SEQD{\prfboundedassumption} - \def\SEQP{\prftree} - \def\SEQAX{\prftree[by]{$\scriptstyle\textup{Ax}$}} - \def\SEQLF{\prftree[by]{$\scriptstyle\textup{L}\bot$}} - \def\SEQLW{\prftree[by]{$\scriptstyle\textup{LW}$}} - \def\SEQRW{\prftree[by]{$\scriptstyle\textup{RW}$}} - \def\SEQLC{\prftree[by]{$\scriptstyle\textup{LC}$}} - \def\SEQRC{\prftree[by]{$\scriptstyle\textup{RC}$}} - \def\SEQLAND{\prftree[by]{$\scriptstyle\textup{L}% - \mathord{\wedge}$}} - \def\SEQRAND{\prftree[by]{$\scriptstyle\textup{R}% - \mathord{\wedge}$}} - \def\SEQLOR{\prftree[by]{$\scriptstyle\textup{L}% - \mathord{\vee}$}} - \def\SEQROR{\prftree[by]{$\scriptstyle\textup{R}% - \mathord{\vee}$}} + \def\SEQP{\prftree} + \prfMakeInferenceRule{SEQAX}{\textup{Ax}} + \prfMakeInferenceRule{SEQLF}{\textup{L}\mathord{\bot}} + \prfMakeInferenceRule{SEQLW}{\textup{LW}} + \prfMakeInferenceRule{SEQRW}{\textup{RW}} + \prfMakeInferenceRule{SEQLC}{\textup{LC}} + \prfMakeInferenceRule{SEQRC}{\textup{RC}} + \prfMakeInferenceRule{SEQLAND}{\textup{L}\mathord{\wedge}} + \prfMakeInferenceRule{SEQLANDL}{\textup{L}\mathord{\wedge}_1} + \prfMakeInferenceRule{SEQLANDR}{\textup{L}\mathord{\wedge}_2} + \prfMakeInferenceRule{SEQRAND}{\textup{R}\mathord{\wedge}} + \prfMakeInferenceRule{SEQLOR}{\textup{L}\mathord{\vee}} + \prfMakeInferenceRule{SEQROR}{\textup{R}\mathord{\vee}} + \prfMakeInferenceRule{SEQRORL}{\textup{R}\mathord{\vee}_1} + \prfMakeInferenceRule{SEQRORR}{\textup{R}\mathord{\vee}_2} \ifprfIMPOption - \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}% - \mathord{\supset}$}} - \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}% - \mathord{\supset}$}} + \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\supset}} + \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\supset}} \else - \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}% - \mathord{\rightarrow}$}} - \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}% - \mathord{\rightarrow}$}} + \prfMakeInferenceRule{SEQLIMP}{\textup{L}\mathord{\rightarrow}} + \prfMakeInferenceRule{SEQRIMP}{\textup{R}\mathord{\rightarrow}} \fi - \def\SEQLALL{\prftree[by]{$\scriptstyle\textup{L}% - \mathord{\forall}$}} - \def\SEQRALL{\prftree[by]{$\scriptstyle\textup{R}% - \mathord{\forall}$}} - \def\SEQLEX{\prftree[by]{$\scriptstyle\textup{L}% - \mathord{\exists}$}} - \def\SEQREX{\prftree[by]{$\scriptstyle\textup{R}% - \mathord{\exists}$}} - \def\SEQCUT{\prftree[by]{$\scriptstyle\textup{Cut}$}} + \prfMakeInferenceRule{SEQLALL}{\textup{L}\mathord{\forall}} + \prfMakeInferenceRule{SEQRALL}{\textup{R}\mathord{\forall}} + \prfMakeInferenceRule{SEQLEX}{\textup{L}\mathord{\exists}} + \prfMakeInferenceRule{SEQREX}{\textup{R}\mathord{\exists}} + \prfMakeInferenceRule{SEQCUT}{\textup{Cut}} \fi % ------------------------------------------------------------------- +% Equality rules +% +% Package option [EQ] +% ------------------------------------------------------------------- + +\ifprf@EQOption% + \prfMakeInferenceRule{EQREFL}{\textup{refl}} + \prfMakeInferenceRule{EQSYM}{\textup{sym}} + \prfMakeInferenceRule{EQTRANS}{\textup{trans}} + \prfMakeInferenceRule{EQSUBST}{\textup{subst}} +\fi + +% ------------------------------------------------------------------- +% Martin-Lof and Homotopy Type Theory +% +% Package option [ML] +% ------------------------------------------------------------------- + +\ifprf@MLOption + \ifprf@MLnodefOption\relax\else + \def\type{\mathbin{:}} + \def\universe{\mathcal{U}} + \def\context{\mathsf{ctx}} + \def\judgementaldef{\mathbin{:\equiv}} + \def\propositionaldef{\mathbin{:=}} + \def\identitytype{\mathsf{Id}} + \def\refl{\mathsf{refl}} + \def\emptytype{\mathbf{0}} + \def\unittype{\mathbf{1}} + \def\booleantype{\mathbf{2}} + \def\axiomofchoice{\mathsf{AC}} + \def\accessibility{\mathsf{acc}} + \def\ap{\mathsf{ap}} + \def\apd{\mathsf{apd}} + \def\basepoint{\mathsf{base}} + \def\biinv{\mathsf{biinv}} + \def\cardtype{\mathsf{Card}} + \def\cocone{\mathsf{cocone}} + \def\cons{\mathsf{cons}} + \def\contr{\mathsf{contr}} + \def\equivtype{\mathsf{Equiv}} + \def\ext{\mathsf{ext}} + \def\fiber{\mathsf{fib}} + \def\funext{\mathsf{funext}} + \def\glue{\mathsf{glue}} + \def\happly{\mathsf{happly}} + \def\hom{\mathsf{hom}} + \def\id{\mathsf{id}} + \def\idtoeqv{\mathsf{idtoeqv}} + \def\idtoiso{\mathsf{idtoiso}} + \def\im{\mathsf{im}} + \def\ind{\mathsf{ind}} + \def\inj{\mathsf{inj}} + \def\inl{\mathsf{inl}} + \def\inr{\mathsf{inr}} + \def\iscontr{\mathsf{isContr}} + \def\isequiv{\mathsf{isequiv}} + \def\ishae{\mathsf{ishae}} + \def\isotoid{\mathsf{istoid}} + \def\isntype#1{\mathsf{is-}{#1}\mathsf{-type}} + \def\isprop{\mathsf{isProp}} + \def\isset{\mathsf{isSet}} + \def\ker{\mathsf{ker}} + \def\LEM{\mathsf{LEM}} + \def\linv{\mathsf{linv}} + \def\listtype{\mathsf{List}} + \def\loopcons{\mathsf{loop}} + \def\Map{\mathsf{Map}} + \def\merid{\mathsf{merid}} + \def\nil{\mathsf{nil}} + \def\ordtype{\mathsf{Ord}} + \def\pair{\mathsf{pair}} + \def\pred{\mathsf{pred}} + \def\pr{\mathsf{pr}} + \def\Prop{\mathsf{Prop}} + \def\qinv{\mathsf{qinv}} + \def\rec{\mathsf{rec}} + \def\rinv{\mathsf{rinv}} + \def\seg{\mathsf{seg}} + \def\Set{\mathsf{Set}} + \def\Succ{\mathsf{succ}} + \def\sup{\mathsf{sup}} + \def\total{\mathsf{total}} + \def\transport{\mathsf{transport}} + \def\transportconst{\mathsf{transportconst}} + \def\ua{\mathsf{ua}} + \def\Wtype{\mathsf{W}} + \fi + + \def\MLctxEMPrule{\ensuremath{\mathsf{ctx}\mathsf{-EMP}}} + \def\MLctxEXTrule{\ensuremath{\mathsf{ctx}\mathsf{-EXT}}} + \def\MLVblerule{\ensuremath{\mathsf{Vble}}} + \def\MLSubstrule{\ensuremath{\mathsf{Subst}}} + \def\MLWkgrule{\ensuremath{\mathsf{Wkg}}} + \def\MLEQreflrule{\ensuremath{\mathord{\equiv}\mathsf{-refl}}} + \def\MLEQsymrule{\ensuremath{\mathord{\equiv}\mathsf{-sym}}} + \def\MLEQtransrule{\ensuremath{\mathord{\equiv}\mathsf{-trans}}} + \def\MLEQsubstrule{\ensuremath{\mathord{\equiv}\mathsf{-subst}}} + \def\MLEQsubsteqrule{\ensuremath{\mathord{\equiv}% + \mathsf{-subst}\mathsf{-eq}}} + \def\MLUintrorule{\ensuremath{\universe\mathsf{-intro}}} + \def\MLUcumulrule{\ensuremath{\universe\mathsf{-cumul}}} + \def\MLUcumuleqrule{\ensuremath{\universe% + \mathsf{-cumul}\mathsf{-eq}}} + \def\MLpiformrule{\ensuremath{\Pi\mathsf{-form}}} + \def\MLpiformeqrule{\ensuremath{\Pi\mathsf{-form}\mathsf{-eq}}} + \def\MLpiintrorule{\ensuremath{\Pi\mathsf{-intro}}} + \def\MLpiintroeqrule{\ensuremath{\Pi\mathsf{-intro}\mathsf{-eq}}} + \def\MLpielimrule{\ensuremath{\Pi\mathsf{-elim}}} + \def\MLpielimeqrule{\ensuremath{\Pi\mathsf{-elim}\mathsf{-eq}}} + \def\MLpicomprule{\ensuremath{\Pi\mathsf{-comp}}} + \def\MLpiuniqrule{\ensuremath{\Pi\mathsf{-uniq}}} + \def\MLKintrorule{\ensuremath{k\mathsf{-intro}}} + \def\MLsigmaformrule{\ensuremath{\Sigma\mathsf{-form}}} + \def\MLsigmaintrorule{\ensuremath{\Sigma\mathsf{-intro}}} + \def\MLsigmaelimrule{\ensuremath{\Sigma\mathsf{-elim}}} + \def\MLsigmacomprule{\ensuremath{\Sigma\mathsf{-comp}}} + \def\MLsigmauniqrule{\ensuremath{\Sigma\mathsf{-uniq}}} + \def\MLplusformrule{\ensuremath{\mathord{+}\mathsf{-form}}} + \def\MLplusintrolrule{\ensuremath{\mathord{+}\mathsf{-intro}_1}} + \def\MLplusintrorrule{\ensuremath{\mathord{+}\mathsf{-intro}_2}} + \def\MLpluselimrule{\ensuremath{\mathord{+}\mathsf{-elim}}} + \def\MLpluscomplrule{\ensuremath{\mathord{+}\mathsf{-comp}_1}} + \def\MLpluscomprrule{\ensuremath{\mathord{+}\mathsf{-comp}_2}} + \def\MLplusuniqrule{\ensuremath{\mathord{+}\mathsf{-uniq}}} + \def\MLzeroformrule{\ensuremath{\mathbf{0}\mathsf{-form}}} + \def\MLzeroelimrule{\ensuremath{\mathbf{0}\mathsf{-elim}}} + \def\MLzerouniqrule{\ensuremath{\mathbf{0}\mathsf{-uniq}}} + \def\MLunitformrule{\ensuremath{\mathbf{1}\mathsf{-form}}} + \def\MLunitintrorule{\ensuremath{\mathbf{1}\mathsf{-intro}}} + \def\MLunitelimrule{\ensuremath{\mathbf{1}\mathsf{-elim}}} + \def\MLunitcomprule{\ensuremath{\mathbf{1}\mathsf{-comp}}} + \def\MLunituniqrule{\ensuremath{\mathbf{1}\mathsf{-uniq}}} + \def\MLnatformrule{\ensuremath{\mathbb{N}\mathsf{-form}}} + \def\MLnatintrozerorule{\ensuremath{\mathbb{N}\mathsf{-intro}_1}} + \def\MLnatintrosuccrule{\ensuremath{\mathbb{N}\mathsf{-intro}_2}} + \def\MLnatelimrule{\ensuremath{\mathbb{N}\mathsf{-elim}}} + \def\MLnatcompzerorule{\ensuremath{\mathbb{N}\mathsf{-comp}_1}} + \def\MLnatcompsuccrule{\ensuremath{\mathbb{N}\mathsf{-comp}_2}} + \def\MLnatuniqrule{\ensuremath{\mathbb{N}\mathsf{-uniq}}} + \def\MLidformrule{\ensuremath{\mathord{=}\mathsf{-form}}} + \def\MLidintrorule{\ensuremath{\mathord{=}\mathsf{-intro}}} + \def\MLidelimrule{\ensuremath{\mathord{=}\mathsf{-elim}}} + \def\MLidcomprule{\ensuremath{\mathord{=}\mathsf{-comp}}} + \def\MLiduniqrule{\ensuremath{\mathord{=}\mathsf{-uniq}}} + \def\MLwformrule{\ensuremath{\mathsf{W}\mathsf{-form}}} + \def\MLwintrorule{\ensuremath{\mathsf{W}\mathsf{-intro}}} + \def\MLwelimrule{\ensuremath{\mathsf{W}\mathsf{-elim}}} + \def\MLwcomprule{\ensuremath{\mathsf{W}\mathsf{-comp}}} + \def\MLwuniqrule{\ensuremath{\mathsf{W}\mathsf{-uniq}}} + \def\MLListformrule{\ensuremath{\mathsf{List}\mathsf{-form}}} + \def\MLListintronrule{\ensuremath{\mathsf{List}\mathsf{-intro_1}}} + \def\MLListintrocrule{\ensuremath{\mathsf{List}\mathsf{-intro_2}}} + \def\MLListelimrule{\ensuremath{\mathsf{List}\mathsf{-elim}}} + \def\MLListcompnrule{\ensuremath{\mathsf{List}\mathsf{-comp_1}}} + \def\MLListcompcrule{\ensuremath{\mathsf{List}\mathsf{-comp_2}}} + \def\MLListuniqrule{\ensuremath{\mathsf{List}\mathsf{-uniq}}} + \def\MLfunextrule{\ensuremath{\Pi\mathsf{-ext}}} + \def\MLunivrule{\ensuremath{\universe_i\mathsf{-univ}}} + \def\MLSformrule{\ensuremath{\mathbb{S}^1\mathsf{-form}}} + \def\MLSintrorule{\ensuremath{\mathbb{S}^1\mathsf{-intro}}} + \def\MLSelimrule{\ensuremath{\mathbb{S}^1\mathsf{-elim}}} + \def\MLScomprule{\ensuremath{\mathbb{S}^1\mathsf{-comp}}} + \def\MLSuniqrule{\ensuremath{\mathbb{S}^1\mathsf{-uniq}}} + \def\MLSpeqintrorule{\ensuremath{\mathbb{S}^1\mathsf{-intro}% + \mathsf{-}\mathsf{=}}} + \def\MLSpeqcomprule{\ensuremath{\mathbb{S}^1\mathsf{-comp}% + \mathsf{-}\mathsf{=}}} + \def\MLIformrule{\ensuremath{I\mathsf{-form}}} + \def\MLIintroarule{\ensuremath{I\mathsf{-intro}_1}} + \def\MLIintrobrule{\ensuremath{I\mathsf{-intro}_2}} + \def\MLIelimrule{\ensuremath{I\mathsf{-elim}}} + \def\MLIcomparule{\ensuremath{I\mathsf{-comp}_1}} + \def\MLIcompbrule{\ensuremath{I\mathsf{-comp}_2}} + \def\MLIuniqrule{\ensuremath{I\mathsf{-uniq}}} + \def\MLIpeqintrorule{\ensuremath{I\mathsf{-intro}% + \mathsf{-}\mathsf{=}}} + \def\MLIpeqcomprule{\ensuremath{I\mathsf{-comp}{-}\mathsf{=}}} + \def\MLsigmaintroarule{\ensuremath{\Sigma\mathsf{-intro}_1}} + \def\MLsigmaintrobrule{\ensuremath{\Sigma\mathsf{-intro}_2}} + \def\MLsigmacomparule{\ensuremath{\Sigma\mathsf{-comp}_1}} + \def\MLsigmacompbrule{\ensuremath{\Sigma\mathsf{-comp}_2}} + \def\MLsigmapeqintrorule{\ensuremath{\Sigma\mathsf{-intro}% + \mathsf{-}\mathsf{=}}} + \def\MLsigmapeqcomprule{\ensuremath{\Sigma\mathsf{-comp}% + \mathsf{-}\mathsf{=}}} + \def\MLPOformrule{\ensuremath{\sqcup\mathsf{-form}}} + \def\MLPOintroarule{\ensuremath{\sqcup\mathsf{-intro}_1}} + \def\MLPOintrobrule{\ensuremath{\sqcup\mathsf{-intro}_2}} + \def\MLPOelimrule{\ensuremath{\sqcup\mathsf{-elim}}} + \def\MLPOcomparule{\ensuremath{\sqcup\mathsf{-comp}_1}} + \def\MLPOcompbrule{\ensuremath{\sqcup\mathsf{-comp}_2}} + \def\MLPOuniqrule{\ensuremath{\sqcup\mathsf{-uniq}}} + \def\MLPOpeqintrorule{\ensuremath{\sqcup\mathsf{-intro}% + \mathsf{-}\mathsf{=}}} + \def\MLPOpeqcomprule{\ensuremath{\sqcup% + \mathsf{-comp}\mathsf{-}\mathsf{=}}} + \def\MLTformrule{\ensuremath{||\cdot||\mathsf{-form}}} + \def\MLTintrorule{\ensuremath{||\cdot||\mathsf{-intro}}} + \def\MLTelimrule{\ensuremath{||\cdot||\mathsf{-elim}}} + \def\MLTcomprule{\ensuremath{||\cdot||\mathsf{-comp}}} + \def\MLTuniqrule{\ensuremath{||\cdot||\mathsf{-uniq}}} + \def\MLTpeqintrorule{\ensuremath{||\cdot||\mathsf{-intro}% + \mathsf{-}\mathsf{=}}} + \def\MLTpeqcomprule{\ensuremath{||\cdot||\mathsf{-comp}% + \mathsf{-}\mathsf{=}}} + \def\MLtorusformrule{\ensuremath{T^2\mathsf{-form}}} + \def\MLtorusintrorule{\ensuremath{T^2\mathsf{-intro}}} + \def\MLtoruselimrule{\ensuremath{T^2\mathsf{-elim}}} + \def\MLtoruscomprule{\ensuremath{T^2\mathsf{-comp}}} + \def\MLtoruspeqintroarule{\ensuremath{T^2\mathsf{-intro}% + \mathsf{-}\mathsf{=_p}}} + \def\MLtoruspeqintrobrule{\ensuremath{T^2\mathsf{-intro}% + \mathsf{-}\mathsf{=_q}}} + \def\MLtoruspeqintrocrule{\ensuremath{T^2\mathsf{-intro}% + \mathsf{-}\mathsf{=_t}}} + \def\MLtoruspeqcomparule{\ensuremath{T^2\mathsf{-comp}% + \mathsf{-}\mathsf{=_p}}} + \def\MLtoruspeqcompbrule{\ensuremath{T^2\mathsf{-comp}% + \mathsf{-}\mathsf{=_q}}} + \def\MLtoruspeqcompcrule{\ensuremath{T^2\mathsf{-comp}% + \mathsf{-}\mathsf{=_t}}} + + \prfMakeInferenceRule{MLctxEMP}{\MLctxEMPrule} + \prfMakeInferenceRule{MLctxEXT}{\MLctxEXTrule} + \prfMakeInferenceRule{MLSubst}{\MLSubstrule} + \prfMakeInferenceRule{MLWkg}{\MLWkgrule} + \prfMakeInferenceRule{MLVble}{\MLVblerule} + \prfMakeInferenceRule{MLEQrefl}{\MLEQreflrule} + \prfMakeInferenceRule{MLEQsym}{\MLEQsymrule} + \prfMakeInferenceRule{MLEQtrans}{\MLEQtransrule} + \prfMakeInferenceRule{MLEQsubst}{\MLEQsubstrule} + \prfMakeInferenceRule{MLEQsubsteq}{\MLEQsubsteqrule} + \prfMakeInferenceRule{MLUintro}{\MLUintrorule} + \prfMakeInferenceRule{MLUcumul}{\MLUcumulrule} + \prfMakeInferenceRule{MLUcumuleq}{\MLUcumuleqrule} + \prfMakeInferenceRule{MLpiform}{\MLpiformrule} + \prfMakeInferenceRule{MLpiformeq}{\MLpiformeqrule} + \prfMakeInferenceRule{MLpiintro}{\MLpiintrorule} + \prfMakeInferenceRule{MLpiintroeq}{\MLpiintroeqrule} + \prfMakeInferenceRule{MLpielim}{\MLpielimrule} + \prfMakeInferenceRule{MLpielimeq}{\MLpielimeqrule} + \prfMakeInferenceRule{MLpicomp}{\MLpicomprule} + \prfMakeInferenceRule{MLpiuniq}{\MLpiuniqrule} + \prfMakeInferenceRule{MLKintro}{\MLKintrorule} + \prfMakeInferenceRule{MLsigmaform}{\MLsigmaformrule} + \prfMakeInferenceRule{MLsigmaintro}{\MLsigmaintrorule} + \prfMakeInferenceRule{MLsigmaelim}{\MLsigmaelimrule} + \prfMakeInferenceRule{MLsigmacomp}{\MLsigmacomprule} + \prfMakeInferenceRule{MLsigmauniq}{\MLsigmauniqrule} + \prfMakeInferenceRule{MLplusform}{\MLplusformrule} + \prfMakeInferenceRule{MLplusintrol}{\MLplusintrolrule} + \prfMakeInferenceRule{MLplusintror}{\MLplusintrorrule} + \prfMakeInferenceRule{MLpluselim}{\MLpluselimrule} + \prfMakeInferenceRule{MLpluscompl}{\MLpluscomplrule} + \prfMakeInferenceRule{MLpluscompr}{\MLpluscomprrule} + \prfMakeInferenceRule{MLplusuniq}{\MLplusuniqrule} + \prfMakeInferenceRule{MLzeroform}{\MLzeroformrule} + \prfMakeInferenceRule{MLzeroelim}{\MLzeroelimrule} + \prfMakeInferenceRule{MLzerouniq}{\MLzerouniqrule} + \prfMakeInferenceRule{MLunitform}{\MLunitformrule} + \prfMakeInferenceRule{MLunitintro}{\MLunitintrorule} + \prfMakeInferenceRule{MLunitelim}{\MLunitelimrule} + \prfMakeInferenceRule{MLunitcomp}{\MLunitcomprule} + \prfMakeInferenceRule{MLunituniq}{\MLunituniqrule} + \prfMakeInferenceRule{MLnatform}{\MLnatformrule} + \prfMakeInferenceRule{MLnatintrozero}{\MLnatintrozerorule} + \prfMakeInferenceRule{MLnatintrosucc}{\MLnatintrosuccrule} + \prfMakeInferenceRule{MLnatelim}{\MLnatelimrule} + \prfMakeInferenceRule{MLnatcompzero}{\MLnatcompzerorule} + \prfMakeInferenceRule{MLnatcompsucc}{\MLnatcompsuccrule} + \prfMakeInferenceRule{MLnatuniq}{\MLnatuniqrule} + \prfMakeInferenceRule{MLidform}{\MLidformrule} + \prfMakeInferenceRule{MLidintro}{\MLidintrorule} + \prfMakeInferenceRule{MLidelim}{\MLidelimrule} + \prfMakeInferenceRule{MLidcomp}{\MLidcomprule} + \prfMakeInferenceRule{MLiduniq}{\MLiduniqrule} + \prfMakeInferenceRule{MLwform}{\MLwformrule} + \prfMakeInferenceRule{MLwintro}{\MLwintrorule} + \prfMakeInferenceRule{MLwelim}{\MLwelimrule} + \prfMakeInferenceRule{MLwcomp}{\MLwcomprule} + \prfMakeInferenceRule{MLwuniq}{\MLwuniqrule} + \prfMakeInferenceRule{MLListform}{\MLListformrule} + \prfMakeInferenceRule{MLListintron}{\MLListintronrule} + \prfMakeInferenceRule{MLListintroc}{\MLListintrocrule} + \prfMakeInferenceRule{MLListelim}{\MLListelimrule} + \prfMakeInferenceRule{MLListcompn}{\MLListcompnrule} + \prfMakeInferenceRule{MLListcompc}{\MLListcompcrule} + \prfMakeInferenceRule{MLListuniq}{\MLListuniqrule} + \prfMakeInferenceRule{MLfunext}{\MLfunextrule} + \prfMakeInferenceRule{MLuniv}{\MLunivrule} + \prfMakeInferenceRule{MLSform}{\MLSformrule} + \prfMakeInferenceRule{MLSintro}{\MLSintrorule} + \prfMakeInferenceRule{MLSelim}{\MLSelimrule} + \prfMakeInferenceRule{MLScomp}{\MLScomprule} + \prfMakeInferenceRule{MLSuniq}{\MLSuniqrule} + \prfMakeInferenceRule{MLSpeqintro}{\MLSpeqintrorule} + \prfMakeInferenceRule{MLSpeqcomp}{\MLSpeqcomprule} + \prfMakeInferenceRule{MLIform}{\MLIformrule} + \prfMakeInferenceRule{MLIintroa}{\MLIintroarule} + \prfMakeInferenceRule{MLIintrob}{\MLIintrobrule} + \prfMakeInferenceRule{MLIelim}{\MLIelimrule} + \prfMakeInferenceRule{MLIcompa}{\MLIcomparule} + \prfMakeInferenceRule{MLIcompb}{\MLIcompbrule} + \prfMakeInferenceRule{MLIuniq}{\MLIuniqrule} + \prfMakeInferenceRule{MLIpeqintro}{\MLIpeqintrorule} + \prfMakeInferenceRule{MLIpeqcomp}{\MLIpeqcomprule} + \prfMakeInferenceRule{MLsigmaintroa}{\MLsigmaintroarule} + \prfMakeInferenceRule{MLsigmaintrob}{\MLsigmaintrobrule} + \prfMakeInferenceRule{MLsigmacompa}{\MLsigmacomparule} + \prfMakeInferenceRule{MLsigmacompb}{\MLsigmacompbrule} + \prfMakeInferenceRule{MLsigmapeqintro}{\MLsigmapeqintrorule} + \prfMakeInferenceRule{MLsigmapeqcomp}{\MLsigmapeqcomprule} + \prfMakeInferenceRule{MLPOform}{\MLPOformrule} + \prfMakeInferenceRule{MLPOintroa}{\MLPOintroarule} + \prfMakeInferenceRule{MLPOintrob}{\MLPOintrobrule} + \prfMakeInferenceRule{MLPOelim}{\MLPOelimrule} + \prfMakeInferenceRule{MLPOcompa}{\MLPOcomparule} + \prfMakeInferenceRule{MLPOcompb}{\MLPOcompbrule} + \prfMakeInferenceRule{MLPOuniq}{\MLPOuniqrule} + \prfMakeInferenceRule{MLPOpeqintro}{\MLPOpeqintrorule} + \prfMakeInferenceRule{MLPOpeqcomp}{\MLPOpeqcomprule} + \prfMakeInferenceRule{MLTform}{\MLTformrule} + \prfMakeInferenceRule{MLTintro}{\MLTintrorule} + \prfMakeInferenceRule{MLTelim}{\MLTelimrule} + \prfMakeInferenceRule{MLTcomp}{\MLTcomprule} + \prfMakeInferenceRule{MLTuniq}{\MLTuniqrule} + \prfMakeInferenceRule{MLTpeqintro}{\MLTpeqintrorule} + \prfMakeInferenceRule{MLTpeqcomp}{\MLTpeqcomprule} + \prfMakeInferenceRule{MLtorusform}{\MLtorusformrule} + \prfMakeInferenceRule{MLtorusintro}{\MLtorusintrorule} + \prfMakeInferenceRule{MLtoruselim}{\MLtoruselimrule} + \prfMakeInferenceRule{MLtoruscomp}{\MLtoruscomprule} + \prfMakeInferenceRule{MLtoruspeqintroa}{\MLtoruspeqintroarule} + \prfMakeInferenceRule{MLtoruspeqintrob}{\MLtoruspeqintrobrule} + \prfMakeInferenceRule{MLtoruspeqintroc}{\MLtoruspeqintrocrule} + \prfMakeInferenceRule{MLtoruspeqcompa}{\MLtoruspeqcomparule} + \prfMakeInferenceRule{MLtoruspeqcompb}{\MLtoruspeqcompbrule} + \prfMakeInferenceRule{MLtoruspeqcompc}{\MLtoruspeqcompcrule} +\fi +% ------------------------------------------------------------------- |