diff options
Diffstat (limited to 'Master/texmf-dist/doc')
-rw-r--r-- | Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf | bin | 273555 -> 278480 bytes | |||
-rw-r--r-- | Master/texmf-dist/doc/latex/prftree/prftreedoc.tex | 210 |
2 files changed, 157 insertions, 53 deletions
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf Binary files differindex 87e9d490d6a..f92aee2c858 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 b28e254b1d5..9db4c1f9e90 100644 --- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex +++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex @@ -1,4 +1,6 @@ \documentclass{amsart} +\usepackage{color} +\usepackage{graphics} \usepackage[ND,SEQ]{prftree} \usepackage{url} @@ -284,9 +286,10 @@ sub-proof basis, as will be done in most examples.\vspace{2ex} There are various \TeX{} dimensions that influence how proofs are constructed: \begin{itemize} -\item\ \verb|\prflinepad| (default 0.3ex): the space between the - bottom line of assumptions and the proof line, and also the space - between the proof line and the top of the conclusion; +\item\ \verb|\prflinepadbefore| (default 0.3ex): the space between the + bottom line of assumptions and the proof line +\item\ \verb|\prflinepadafter| (default 0.3ex): the space between the + proof line and the top of the conclusion; \item\ \verb|\prflineextra| (default 0.3em): the length which extends on the left and on the right the proof line so that it is slightly longer than the largest between the conclusion and the list of @@ -309,7 +312,7 @@ constructed: For example, \begin{displaymath} - \prflinepad=.7ex + \prflinepadafter=.7ex \prftree[r]{$\supset$I} {\prftree[r]{$\supset$I} {\prftree[r]{$\supset$E} @@ -321,7 +324,7 @@ For example, \end{displaymath} is typeset by \begin{verbatim} - \prflinepad=.7ex + \prflinepadafter=.7ex \prftree[r]{$\supset$I} {\prftree[r]{$\supset$I} {\prftree[r]{$\supset$E} @@ -496,6 +499,25 @@ sub-proof whose conclusion is $C$, one obtains the more pleasant \rightarrow (A \rightarrow C))} \end{displaymath}\vspace{.2ex} +The \verb|Strut| option of the package controls a subtle point about +spacing around a proof line: assumptions and conclusion are usually +typeset so that the height and the depth of their box is at least the +one of \verb|\mathstrut|. In this way, adjacent proofs will have their +proof lines aligned (well, whenever they don't have huge +conclusions). But, as signalled by Dominic Hughes, sometimes one wants +the height and the depth to be the ``real'' ones, especially when +there are no characters/symbols with a positive depth: this forces the +perceived space above and below the proof line to be exactly the +values of \verb|\prflinepadbefore| and \verb|\prflinepadafter|. This +behaviour can be achieved by calling the package with the \verb|STRUT| +option. Alternatively, one may use the \verb|\prfSTRUToptionfalse| +command to locally force this behaviour, and +\verb|\prfSTRUToptiontrue| to return to the standard one. Similarly, +the \verb|STRUTlabel| package option, together with the pair of +commands \verb|\prfSTRUTlabeloptiontrue| and +\verb|\prfSTRUTlabeloptionfalse|, operate on rule names and rule +labels.\vspace{2ex} + The rendering of bounded assumptions is modified by \verb|\prfboundedstyle|. When $\verb|\prfboundedstyle| = 0$, the format of the assumption is $[\mbox{formula}]$, which is the default @@ -574,12 +596,15 @@ command. This can be modified at will. The package defines it as The assumptions, conclusions, labels, and rule names are drawn using the following commands, which may be redefined: \begin{verbatim} - \def\prfConclusionBox#1{\hbox% - {$\displaystyle\begingroup#1\endgroup\mathstrut$}} - \def\prfAssumptionBox#1{\hbox% - {$\displaystyle\begingroup#1\endgroup\mathstrut$}} - \def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}} - \def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}} +\def\prfConclusionBox#1{% + \hbox{$\displaystyle\begingroup#1\endgroup% +\def\prfAssumptionBox#1{% + \hbox{$\displaystyle\begingroup#1\endgroup% + \ifprfSTRUToption\mathstrut\fi$}} +\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup% + \ifprfSTRUTlabeloption\strut\fi}} +\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup% + \ifprfSTRUTlabeloption\strut\fi}} \end{verbatim} It is not advisable to change these commands in a radical way, unless one understands how the graphical engine works. @@ -597,7 +622,7 @@ value aside the labelled point of the proof. For example, \begin{displaymath} - \begin{prooftree} + \begin{prfenv} \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$} {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$} {\prftree[r]{$\supset$E} @@ -606,11 +631,11 @@ For example, {\bot}} {\neg\neg A}} {A \supset \neg\neg A} - \end{prooftree} + \end{prfenv} \end{displaymath} is generated by the following code \begin{verbatim} - \begin{prooftree} + \begin{prfenv} \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$} {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$} {\prftree[r]{$\supset$E} @@ -619,17 +644,17 @@ is generated by the following code {\bot}} {\neg\neg A}} {A \supset \neg\neg A} - \end{prooftree} + \end{prfenv} \end{verbatim} The labels are \verb|assum:A| and \verb|assum:not_A|, the reference values are $1$ and $2$, respectively, and the anchors are these values on the discharged assumptions on the top of the proof. The references to these labels are the values in the rule names.\vspace{2ex} -The \verb|prooftree| environment delimits the scope of labels: the -\verb|\end{prooftree}| declaration makes the labels still available +The \verb|prfenv| environment delimits the scope of labels: the +\verb|\end{prfenv}| declaration makes the labels still available for reference, but numbering of new labels will restart from -$1$. Enclosing a proof tree in a \verb|prooftree| environment is not +$1$. Enclosing a proof tree in a \verb|prfenv| environment is not mandatory: in such case, labels will be global to the document.\vspace{2ex} @@ -687,7 +712,7 @@ For example, the disjunction elimination rule is a perfect way to illustrate the reason behind the \textbf{label} option, i.e., the need to discharge a pair of assumptions: \begin{displaymath} - \begin{prooftree} + \begin{prfenv} \prfinterspace=1.2em \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$} {\prfsummary{\Gamma}{A \vee B}} @@ -695,7 +720,7 @@ to discharge a pair of assumptions: \prfboundedassumption<assum:orE>{A}}{C}} {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orE>{B}}{C}}{C} - \end{prooftree} + \end{prfenv} \end{displaymath} \begin{verbatim} \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$} @@ -713,7 +738,7 @@ may indicate that a label is reused when it should not. The same example can be used to show how the other options work: \begin{displaymath} \begin{array}{@{}ccc@{}} - \begin{prooftree} + \begin{prfenv} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$} {\prfsummary{\Gamma}{A \vee B}} @@ -722,8 +747,8 @@ The same example can be used to show how the other options work: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orEn>{B}}{C}} {C} - \end{prooftree} & - \begin{prooftree} + \end{prfenv} & + \begin{prfenv} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$} {\prfsummary{\Gamma}{A \vee B}} @@ -732,8 +757,8 @@ The same example can be used to show how the other options work: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orEr>{B}}{C}} {C} - \end{prooftree} & - \begin{prooftree} + \end{prfenv} & + \begin{prfenv} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$} {\prfsummary{\Gamma}{A \vee B}} @@ -742,8 +767,8 @@ The same example can be used to show how the other options work: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orER>{B}}{C}} {C} - \end{prooftree} \\ - \begin{prooftree} + \end{prfenv} \\ + \begin{prfenv} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$} {\prfsummary{\Gamma}{A \vee B}} @@ -752,8 +777,8 @@ The same example can be used to show how the other options work: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orEa>{B}}{C}} {C} - \end{prooftree} & - \begin{prooftree} + \end{prfenv} & + \begin{prfenv} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$} {\prfsummary{\Gamma}{A \vee B}} @@ -762,8 +787,8 @@ The same example can be used to show how the other options work: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orEA>{B}}{C}} {C} - \end{prooftree} & - \begin{prooftree} + \end{prfenv} & + \begin{prfenv} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$} {\prfsummary{\Gamma}{A \vee B}} @@ -772,7 +797,7 @@ The same example can be used to show how the other options work: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orEf>{B}}{C}} {C} - \end{prooftree} + \end{prfenv} \end{array} \end{displaymath} @@ -780,7 +805,7 @@ Also, as the \verb|\prfboundedstyle| varies, the resulting proof trees are: \begin{displaymath} \begin{array}{ccc} - \begin{prooftree} + \begin{prfenv} \prfboundedstyle=0 \prfsummarystyle=4 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$} @@ -790,8 +815,8 @@ are: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:AorE>{B}}{C}} {C} - \end{prooftree} & - \begin{prooftree} + \end{prfenv} & + \begin{prfenv} \prfboundedstyle=1 \prfsummarystyle=4 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$} @@ -801,8 +826,8 @@ are: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:BorE>{B}}{C}} {C} - \end{prooftree} & - \begin{prooftree} + \end{prfenv} & + \begin{prfenv} \prfboundedstyle=2 \prfsummarystyle=4 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$} @@ -812,7 +837,7 @@ are: {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:CorE>{B}}{C}} {C} - \end{prooftree} + \end{prfenv} \end{array} \end{displaymath} @@ -821,7 +846,7 @@ generate the assumption values. It contains the last used value, and initially, it is set to $0$. By modifying its value, e.g., to \verb|\setcounter{prfassumptioncounter}{1}|, \begin{displaymath} - \begin{prooftree} + \begin{prfenv} \setcounter{prfassumptioncounter}{1} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEff>}$} @@ -831,7 +856,7 @@ initially, it is set to $0$. By modifying its value, e.g., to {\prfsummary{\Gamma, \prfboundedassumption<[l]assum:orEff>{B}}{C}} {C} - \end{prooftree} + \end{prfenv} \end{displaymath} A labelled assumption box is graphically constructed by the package @@ -974,7 +999,7 @@ elimination or disjunction introduction. For example, the proof \begin{displaymath} - \begin{prooftree} + \begin{prfenv} \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}} {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}} {\NDIMPIL{simp:notnotA} @@ -982,7 +1007,7 @@ For example, the proof {\NDDL{simp:notA}{\neg A}}{\bot}}{A}} {\neg\neg A \supset A}} {\neg\neg A \supset A} - \end{prooftree} + \end{prfenv} \end{displaymath} is typeset in abbreviated form by the following code \begin{verbatim} @@ -996,7 +1021,7 @@ is typeset in abbreviated form by the following code \end{verbatim}\vspace{2ex} Similarly, by loading the package as -\verb|\usepackage[SEQ]{prooftree.sty}|, the following abbreviations +\verb|\usepackage[SEQ]{prftree.sty}|, the following abbreviations are available, which roughly correspond to the inference rule of sequent calculi: \begin{itemize} @@ -1044,7 +1069,7 @@ best.\vspace{2ex} Consider the proof: \begin{displaymath} - \begin{prooftree} + \begin{prfenv} \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} {\NDIMPI{\NDDL{a:notA}{A}}{\neg\neg A \supset A}} {\NDIMPIL{a:notnotA} @@ -1052,7 +1077,7 @@ Consider the proof: {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} {\neg\neg A \supset A}} {\neg\neg A \supset A} - \end{prooftree} + \end{prfenv} \end{displaymath} the space between the axiom and the sub-proof of the positive case is visually much less than the space between the positive and the @@ -1065,7 +1090,7 @@ negative case closer to the positive one. The first strategy yields: \begin{displaymath} - \begin{prooftree} + \begin{prfenv} \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.8em}} {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} {\NDIMPIL{a:notnotA} @@ -1073,7 +1098,7 @@ The first strategy yields: {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} {\neg\neg A \supset A}} {\neg\neg A \supset A} - \end{prooftree} + \end{prfenv} \end{displaymath} and this effect is given by adding an appropriate \verb|\hspace| after the axiom, as in @@ -1091,7 +1116,7 @@ Adding the same space in front of the positive case is equivalent. The second strategy yields: \begin{displaymath} - \begin{prooftree} + \begin{prfenv} \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} {\hspace{-.4em}\NDIMPIL{a:notnotA} @@ -1099,7 +1124,7 @@ The second strategy yields: {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} {\neg\neg A \supset A}} {\neg\neg A \supset A} - \end{prooftree} + \end{prfenv} \end{displaymath} Again, this is obtained by adding a negative \verb|hspace| after the positive case, or, equivalently, before the negative one: @@ -1132,7 +1157,7 @@ align proof trees, as in \begin{center} \fbox{\prfsummarystyle=1 \prfsummary{f}{g}{f \wedge g}}\qquad - \fbox{$\begin{prooftree} + \fbox{$\begin{prfenv} \NDOREL{a:notA}{\NDLEM{A \vee \neg A}} {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}} {\hspace{-.4em}\NDIMPIL{a:notnotA} @@ -1140,7 +1165,7 @@ align proof trees, as in {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} {\neg\neg A \supset A}} {\neg\neg A \supset A} - \end{prooftree}$} + \end{prfenv}$} \end{center} since this is the natural way to put proofs side by side: \begin{verbatim} @@ -1533,6 +1558,85 @@ 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: +\begin{displaymath} + \begin{prfenv} + \color{green}\NDIMPIL{ex6:1} + {\NDANDI + {\color{red}\NDNOTIL{ex6:2} + {\NDNOTE + {\NDDL{ex6:1}{\neg (A \vee B)}} + {\NDORIL + {\NDDL{ex6:2}{A}} + {A \vee B}} + {\bot}} + {\neg A}} + {\color{blue}\NDNOTIL{ex6:3} + {\NDNOTE + {\NDDL{[l]ex6:1}{\neg (A \vee B)}} + {\NDORIR + {\NDDL{ex6:3}{B}} + {A \vee B}} + {\bot}} + {\neg B}} + {\neg A \wedge \neg B}} + {\neg (A \vee B) \supset \neg A \wedge \neg B} + \end{prfenv} +\end{displaymath}\vspace{.2ex} + +Also. all the standard box manipulation commands can be freely applied. +The following examples are not significant for doing mathematics, but +the mechanics behind can be occasionally useful, for example, to +shrink a large proof to fit the page length: +\begin{displaymath} + \rotatebox{15}{\begin{prfenv} + \NDIMPIL{ex5:1} + {\NDANDI + {\NDNOTIL{ex5:2} + {\NDNOTE + {\NDDL{ex5:1}{\neg (A \vee B)}} + {\NDORIL + {\NDDL{ex5:2}{A}} + {A \vee B}} + {\bot}} + {\neg A}} + {\NDNOTIL{ex5:3} + {\NDNOTE + {\NDDL{[l]ex5:1}{\neg (A \vee B)}} + {\NDORIR + {\NDDL{ex5:3}{B}} + {A \vee B}} + {\bot}} + {\neg B}} + {\neg A \wedge \neg B}} + {\neg (A \vee B) \supset \neg A \wedge \neg B} + \end{prfenv}} +\end{displaymath} +\begin{displaymath} + \begin{prfenv} + \NDIMPIL{ex7:1} + {\NDANDI + {\reflectbox{\NDNOTIL{ex7:2} + {\NDNOTE + {\NDDL{ex7:1}{\neg (A \vee B)}} + {\NDORIL + {\NDDL{ex7:2}{A}} + {A \vee B}} + {\bot}} + {\neg A}}} + {\resizebox{20em}{!}{\NDNOTIL{ex7:3} + {\NDNOTE + {\NDDL{[l]ex7:1}{\neg (A \vee B)}} + {\scalebox{.7}[1]{\NDORIR + {\NDDL{ex7:3}{B}} + {A \vee B}}} + {\bot}} + {\neg B}}} + {\neg A \wedge \neg B}} + {\neg (A \vee B) \supset \neg A \wedge \neg B} + \end{prfenv} +\end{displaymath} + % ------------------------------------- \clearpage \section{Internals}\label{sec:internals} @@ -1645,7 +1749,8 @@ occurrence of a reference, which can be resolved. Most difficulties in the implementation of references lie in the way to construct the boxes to be used in the proof tree. But, the tricky part is the interaction with the \LaTeX{} and \TeX{} kernel for error -reporting. +reporting. A small hack has been introduced to force recompilation +when the references in a proof change. % ------------------------------------- \clearpage @@ -1673,7 +1778,6 @@ 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. - \vfill \end{document} |