From e2dfc4cc8dc03d323073de46903005e3a9d12255 Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Thu, 20 Aug 2020 03:01:54 +0000 Subject: CTAN sync 202008200301 --- macros/latex/contrib/ebproof/README.md | 10 +- macros/latex/contrib/ebproof/ebproof.dtx | 1629 ++++++++++++++++++++++++++++++ macros/latex/contrib/ebproof/ebproof.ins | 15 + macros/latex/contrib/ebproof/ebproof.pdf | Bin 227686 -> 496470 bytes macros/latex/contrib/ebproof/ebproof.sty | 767 -------------- macros/latex/contrib/ebproof/ebproof.tex | 638 ------------ 6 files changed, 1649 insertions(+), 1410 deletions(-) create mode 100644 macros/latex/contrib/ebproof/ebproof.dtx create mode 100644 macros/latex/contrib/ebproof/ebproof.ins delete mode 100644 macros/latex/contrib/ebproof/ebproof.sty delete mode 100644 macros/latex/contrib/ebproof/ebproof.tex (limited to 'macros/latex/contrib/ebproof') diff --git a/macros/latex/contrib/ebproof/README.md b/macros/latex/contrib/ebproof/README.md index 0f8b35038c..e794db1fee 100644 --- a/macros/latex/contrib/ebproof/README.md +++ b/macros/latex/contrib/ebproof/README.md @@ -14,9 +14,9 @@ styles of inference rules, placement of labels, etc. The distribution includes the following files: -- `ebproof.sty` : the package -- `ebproof.pdf` : the documentation -- `ebproof.tex` : the LaTeX source for the documentation +- `ebproof.dtx` : the doctrip source for the package and documentation +- `ebproof.pdf` : the compiled documentation +- `ebproof.sty` : the generated package The package requires `expl3` (the LaTeX3 programming environment) which provides many useful programming tools. @@ -25,7 +25,7 @@ provides many useful programming tools. License ------- -Copyright 2015 Emmanuel Beffara +Copyright 2015-2020 Emmanuel Beffara This work may be distributed and/or modified under the conditions of the LaTeX Project Public License, either version 1.3 @@ -39,4 +39,4 @@ This work has the LPPL maintenance status “maintained”. The Current Maintainer of this work is Emmanuel Beffara. -This work consists of the files `ebproof.sty` and `ebproof.tex`. +This work consists of the file `ebproof.dtx`. diff --git a/macros/latex/contrib/ebproof/ebproof.dtx b/macros/latex/contrib/ebproof/ebproof.dtx new file mode 100644 index 0000000000..71735ffc00 --- /dev/null +++ b/macros/latex/contrib/ebproof/ebproof.dtx @@ -0,0 +1,1629 @@ +% \iffalse meta-comment +% +% Copyright (C) 2015-2020 by Emmanuel Beffara +% +% This file may be distributed and/or modified under the conditions of the +% LaTeX Project Public License, either version 1.3 of this license or (at +% your option) any later version. The latest version of this license is in: +% +% http://www.latex-project.org/lppl.txt +% +% and version 1.3 or later is part of all distributions of LaTeX version +% 2005/12/01 or later. +% +%<*driver> +\documentclass[full]{l3doc} +\usepackage{ebproof} +\usepackage{multicol} +\usepackage{tikz} +\usetikzlibrary{decorations.pathmorphing} +\EnableCrossrefs +\newenvironment{example}{% + \VerbatimEnvironment + \begin{VerbatimOut}{example.tex}}{% + \end{VerbatimOut} + \begin{center} + \begin{minipage}{.4\textwidth} + \input{example.tex} + \end{minipage}% + \begin{minipage}{.6\textwidth} + \small\VerbatimInput[gobble=0]{example.tex} + \end{minipage}% + \end{center} +} +\begin{document} + \DocInput{\jobname.dtx} +\end{document} +% +% \fi +% +% \title{^^A +% The \pkg{ebproof} package \\ +% Formal proofs in the style of sequent calculus^^A +% } +% +% \author{^^A +% Emmanuel Beffara\thanks +% {^^A +% E-mail: \href{mailto:manu@beffara.org}{manu@beffara.org}^^A +% }^^A +% } +% +% \date{Version 2.1 -- Released 2020-08-19} +% +% \maketitle +% +% \setcounter{tocdepth}{2} +% \begin{multicols}{2} +% \tableofcontents +% \end{multicols} +% +% \begin{documentation} +% +% \section{Introduction} +% +% The \pkg{ebproof} package provides commands to typeset proof trees, in the +% style of sequent calculus and related systems: +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% The structure is very much inspired by the +% \href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\pkg{bussproofs}} +% package, in particular for the postfix notation. +% I actually wrote \pkg{ebproof} because there were some limitations in +% \pkg{bussproofs} that I did not know how to lift, and also because I did +% not like some choices in that package (and also because it was fun to write). +% +% Any feedback is welcome, in the form of bug reports, feature requests or +% suggestions, through the web page of the project at \url{https://framagit.org/manu/ebproof}. +% +% \section{Environments} +% +% \begin{function}{prooftree,prooftree*} +% \begin{syntax} +% \verb|\begin{prooftree}|\oarg{options} +% ~ \meta{statements} +% \verb|\end{prooftree}| +% \end{syntax} +% The package provides the \env{prooftree} environment, in standard and +% starred variants. +% This typesets the proof tree described by the \meta{statements}, as +% described in section~\ref{sec:statements}. +% The \meta{options} provide default formatting options for the proof tree, +% available options are described in section~\ref{sec:options}. +% +% Following the conventions of \pkg{amsmath} for alignment environments, the +% non-starred version produces a proof tree at the current position in the +% text flow (it can be used in math mode or text mode) while the starred +% version typesets the proof on a line of its own, like a displayed formula. +% \end{function} +% +% \begin{example} +% \[ +% \begin{prooftree} +% \infer0{ \vdash A } +% \hypo{ \vdash B } \infer1{ \vdash B, C } +% \infer2{ \vdash A\wedge B, C } +% \end{prooftree} +% \quad \rightsquigarrow \quad +% \begin{prooftree} +% \infer0{ \vdash A } \hypo{ \vdash B } +% \infer2{ \vdash A\wedge B } +% \infer1{ \vdash A\wedge B, C } +% \end{prooftree} +% \] +% \end{example} +% +% \section{Statements} +% \label{sec:statements} +% +% Statements describe proofs in postfix notation: when typesetting a proof tree +% whose last rule has, say, two premisses, you will first write statements for +% the subtree of the first premiss, then statements for the subtree of the +% second premiss, then a statement like \cs{infer2}\{\meta{conclusion}\} to +% build an inference with these two subtrees as premisses and the given text as +% conclusion. +% +% Hence statements operate on a stack of proof trees. +% At the beginning of a \env{prooftree} environment, the stack is empty. +% At the end, it must contain exactly one tree, which is the one that will be +% printed. +% +% Note that the commands defined in this section only exist right inside +% \env{prooftree} environments. +% If you have a macro with the same name as one of the statements, for instance +% \cs{hypo}, then this macro will keep its meaning outside \env{prooftree} +% environments as well as inside the arguments of a statement. +% If you really need to access the statements in another context, you can can +% always call them by prefixing their names with \texttt{ebproof}, for instance as +% \cs{ebproofhypo}. +% +% \subsection{Basic statements} +% +% The basic statements for building proofs are the following, where +% \meta{options} stands for arbitrary options as described in +% section~\ref{sec:options}. +% +% \begin{function}{\hypo} +% \begin{syntax} +% \cs{hypo}\oarg{options}\marg{text} +% \end{syntax} +% The statement \cs{hypo} pushes a new proof tree consisting only in one +% conclusion line, with no premiss and no line above, in other words a tree +% with only a leaf (\cs{hypo} stands for \emph{hypothesis}). +% \end{function} +% +% \begin{function}{\infer} +% \begin{syntax} +% \cs{infer}\oarg{options}\meta{arity}\oarg{label}\marg{text} +% \end{syntax} +% The statement \cs{infer} builds an inference step by taking some proof +% trees from the top of the stack, assembling them with a rule joining their +% conclusions and putting a new conclusion below. +% The \meta{arity} is the number of sub-proofs, it may be any number +% including 0 (in this case there will be a line above the conclusion but no +% sub-proof). +% If \meta{label} is present, it is used as the label on the right of the +% inference line; it is equivalent to using the \cmd{right label} option. +% \end{function} +% +% \medskip +% +% The \meta{text} in these statements is the contents of the conclusion at the +% root of the tree that the statements create. +% It is typeset in math mode by default but any kind of formatting can be used +% instead, using the \cmd{template} option. +% The \meta{label} text is formatted in horizontal text mode by default. +% +% Each proof tree has a vertical axis, used for alignment of successive steps. +% The position of the axis is deduced from the text of the conclusion at the +% root of the tree: if \meta{text} contains the alignment character \verb|&| +% then the axis is set at that position, otherwise the axis is set at the center +% of the conclusion text. +% The \cs{infer} statement makes sure that the axis of the premiss is at the +% same position as the axis of the conclusion. +% If there are several premisses, it places the axis at the center between the +% left of the leftmost conclusion and the right of the rightmost conclusion: +% +% \begin{example} +% \begin{prooftree} +% \hypo{ &\vdash A, B, C } +% \infer1{ A &\vdash B, C } +% \infer1{ A, B &\vdash C } +% \hypo{ D &\vdash E } +% \infer2{ A, B, D &\vdash C, E } +% \infer1{ A, B &\vdash C, D, E } +% \infer1{ A &\vdash B, C, D, E } +% \end{prooftree} +% \end{example} +% +% \begin{function}{\ellipsis} +% \begin{syntax} +% \cs{ellipsis}\marg{label}\marg{text} +% \end{syntax} +% The statement \cs{ellipsis} typesets vertical dots, with a label on the right, +% and a new conclusion. No inference lines are inserted. +% \end{function} +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma &\vdash A } +% \ellipsis{foo}{ \Gamma &\vdash A, B } +% \end{prooftree} +% \end{example} +% +% +% \subsection{Modifying proof trees} +% +% The following additional statements may be used to affect the format of the +% last proof tree on the stack. +% +% \begin{function}{\rewrite} +% \begin{syntax} +% \cs{rewrite}\marg{code} +% \end{syntax} +% The statement \cs{rewrite} is used to modify the proof of the stack while +% preserving its size and alignment. +% The \meta{code} is typeset in horizontal mode, with the following control +% sequences defined: +% \begin{itemize} +% \item \cs{treebox} is a box register that contains the original material, +% \item \cs{treemark}\marg{name} expands as the position of a given mark with +% respect to the left of the box. +% \end{itemize} +% \end{function} +% +% A simple use of this statement is to change the color of a proof tree: +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \rewrite{\color{red}\box\treebox} +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% Note the absence of spaces inside the call to \cs{rewrite}, because spaces +% would affect the position of the tree box. +% Note also that explicit use of \cs{treebox} is required to actually draw the +% subtree. +% Not using it will effectively not render the subtree, while still reserving +% its space in the enclosing tree: +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \rewrite{} +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% This kind of manipulation is useful for instance in conjunction with the +% \pkg{beamer} package to allow revealing subtrees of a proof tree +% progressively in successive slides of a given frame. +% +% \begin{function}{\delims} +% \begin{syntax} +% \cs{delims}\marg{left}\marg{right} +% \end{syntax} +% The statement \cs{delims} puts left and right delimiters around the whole +% sub-proof, without changing the alignment (the spacing is affected by the +% delimiters, however). +% The \meta{left} text must contain an opening occurrence of \cs{left} and +% the \meta{right} text must contain a matching occurrence of \cs{right}. +% For instance, \verb|\delims{\left(}{\right)}| will put the sub-proof +% between parentheses. +% \end{function} +% +% \begin{example} +% \begin{prooftree} +% \hypo{ A_1 \vee \cdots \vee A_n } +% \hypo{ [A_i] } +% \ellipsis{}{ B } +% \delims{ \left( }{ \right)_{1\leq i\leq n} } +% \infer2{ B } +% \end{prooftree} +% \end{example} +% +% \begin{function}{\overlay} +% \begin{syntax} +% \cs{overlay} +% \end{syntax} +% The statement \cs{overlay} combines the last two proofs on the stack into +% a single one, so that their conclusions are placed at the same point. +% \end{function} +% +% \begin{example} +% \begin{prooftree} +% \hypo{Z} +% \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D} +% \rewrite{\color{blue}\box\treebox} +% \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I} +% \rewrite{\color{red}\box\treebox} +% \overlay \hypo{J} \infer3{K} +% \end{prooftree} +% \end{example} +% +% The primary use of this feature is for building animated presentations where +% a subtree in a proof has to be modified without affecting the general +% alignment of the surrounding proof. For instance, the example above could be +% used in Beamer to build successive slides in a given frame with two +% different subtrees: +% +% \begin{verbatim} +% \begin{prooftree} +% \hypo{Z} +% \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D} +% \only<2>{\rewrite{}} % erases this version on slide 2 +% \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I} +% \only<1>{\rewrite{}} % erases this version on slide 1 +% \overlay \hypo{J} \infer3{K} +% \end{prooftree} +% \end{verbatim} +% +% \section{Options} +% \label{sec:options} +% +% The formatting of trees, conclusion texts and inference rules is affected by +% options, specified using the \LaTeX3 key-value system. +% All options are in the \texttt{ebproof} module in the key tree. +% They can be set locally for a proof tree or for a single statement using +% optional arguments in the associated commands. +% +% \begin{function}{\ebproofset,\set} +% \begin{syntax} +% \cs{ebproofset}\marg{options} +% \end{syntax} +% The statement \cs{ebproofset} is used to set some options. When used +% inside a \env{prooftree} environment, it can written \cs{set}. +% The options will apply in the current scope; using this in preamble will +% effectively set options globally. +% Specific options may also be specified for each proof tree and for each +% statement in a proof tree, using optional arguments. +% \end{function} +% +% \subsection{General shape} +% +% The options in this section only make sense at the global level and at the +% proof level. +% Changing the proof style inside a \env{proof} environment has undefined +% behaviour. +% +% \begin{variable}{proof style} +% The option \cmd{proof style} sets the general shape for representing proofs. +% The following styles are provided: +% \begin{description} +% \item[upwards] +% This is the default style. +% Proof trees grow upwards, with conclusions below and premisses above. +% \item[downwards] +% Proof trees grow downwards, with conclusions above and premisses below. +% \fvset{gobble=6} +% \begin{example} +% \begin{prooftree}[proof style=downwards] +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% \end{description} +% \end{variable} +% +% In the optional argument of \env{prooftree} environments, proof styles can +% be specified directly, without prefixing the name by ``\texttt{proof style=}''. +% For instance, the first line of the example above could be written +% \verb|\begin{prooftree}| equivalently. +% +% \begin{variable}{center} +% The option \cmd{center} toggles vertical centering of typeset proofs. +% If set to \texttt{true}, the tree produced by the \env{prooftree} +% environment will be vertically centered around the text line. +% If set to \texttt{false}, the base line of the tree will be the base line +% of the conclusion. +% The default value is \texttt{true}. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[center=false] +% \infer0{ A \vdash A } +% \end{prooftree} +% \qquad +% \begin{prooftree}[center=false] +% \hypo{ \Gamma, A \vdash B } +% \infer1{ \Gamma \vdash A \to B } +% \end{prooftree} +% \end{example} +% +% \subsection{Spacing} +% +% \begin{variable}{separation} +% Horizontal separation between sub-proofs in an inference is defined by the +% option \cmd{separation}. +% The default value is \texttt{1.5em}. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[separation=0.5em] +% \hypo{ A } \hypo{ B } \infer2{ C } +% \hypo{ D } \hypo{ E } \hypo{ F } \infer3{ G } +% \hypo{ H } \infer[separation=3em]3{ K } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{rule margin} +% The spacing above and below inference lines is defined by the option +% \cmd{rule margin}. +% The default value is \texttt{0.7ex}. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[rule margin=2ex] +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% \subsection{Shape of inference lines} +% +% \begin{variable}{rule style} +% The shape of inference lines is set by the option \cmd{rule style}. +% The following values are provided: +% \begin{center} +% \begin{tabular}{@{}l@{\qquad}l@{}} +% \toprule +% \cmd{simple} & a simple line (this is the default style) \\ +% \cmd{no rule} & no rule, only a single space of length \texttt{rule margin} \\ +% \cmd{double} & a double line \\ +% \cmd{dashed} & a single dashed line \\ +% \bottomrule +% \end{tabular} +% \end{center} +% \end{variable} +% +% The precise rendering is influenced by parameters specified below. +% Arbitrary new shapes can defined using the \cs{ebproofnewrulestyle} command +% described in section~\ref{sec:styles}, using \texttt{rule code} option +% described below. +% +% In the optional argument of the \cs{infer} statement, rule styles can be +% specified directly, without prefixing the style name by ``\texttt{rule style=}''. +% For instance, \verb|\infer[dashed]| is equivalent to +% \verb|\infer[rule style=dashed]|. +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma &\vdash A \to B } +% \infer[no rule]1{ \Gamma &\vdash {!A} \multimap B } +% \hypo{ \Delta &\vdash A } +% \infer[rule thickness=2pt]1{ \Delta &\vdash {!A} } +% \infer0{ B \vdash B } +% \infer[dashed]2{ \Delta, {!A}\multimap B \vdash B } +% \infer2{ \Gamma, \Delta &\vdash B } +% \infer[double]1{ \Gamma \cup \Delta &\vdash B } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{rule thickness,rule separation} +% The thickness of inference lines is defined by option \cmd{rule +% thickness}, it is \texttt{0.4pt} by default. +% The distance between the two lines in the \texttt{double} rule style is +% defined by the \cmd{rule separation} option. +% It is \texttt{2pt} by default. +% \end{variable} +% \begin{variable}{rule dash length,rule dash space} +% For dashed rules, the length of dashes is defined by the option +% \cmd{rule dash length} and the space between dashes is defined by the +% option \cmd{rule dash space}. +% The default values are \texttt{0.2em} and \texttt{0.3em} respectively. +% \end{variable} +% +% \begin{variable}{rule code} +% Arbitrary rule shapes can be optained using the \cmd{rule code} option. +% The argument is code is used to render the rule, it is executed in +% vertical mode in a \cs{vbox} whose \cs{hsize} is set to the width of the +% rule. +% Margins above and below are inserted automatically (they can be removed by +% setting \texttt{rule margin} to \texttt{0pt}). +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[rule code={\hbox{\tikz +% \draw[decorate,decoration={snake,amplitude=.3ex}] +% (0,0) -- (\hsize,0);}}] +% \hypo{ \Gamma &\vdash A } +% \infer1{ \Gamma &\vdash A, \ldots, A } +% \hypo{ \Delta, A, \ldots, A \vdash \Theta } +% \infer2{ \Gamma, \Delta \vdash \Theta } +% \end{prooftree} +% \end{example} +% Note that this example requires the \pkg{tikz} package, with the +% \pkg{decorations.pathmorphing} library for the \texttt{snake} decoration. +% +% \subsection{Format of conclusions and labels} +% +% \begin{variable}{template,left template,right template} +% The format of text in inferences is defined by templates. +% The option \cmd{template} is used for text with no alignment mark, the +% options \cmd{left template} and \cmd{right template} are used for the left +% and right side of the alignment mark when it is present. +% The value of these options is arbitrary \TeX\ code, composed in horizontal mode. +% The macro \cs{inserttext} is used to insert the actual text passed to the +% \cs{hypo} and \cs{infer} statements. +% The default value for \cmd{template} is simply \verb|$\inserttext$|, so +% that conclusions are set in math mode. +% The default values for \cmd{left template} and \cmd{right template} are +% similar, with spacing assuming that a relation symbol is put near the +% alignment mark, so that \verb|\infer1{A &\vdash B}| is spaced correctly. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[template=(\textbf\inserttext)] +% \hypo{ foo } +% \hypo{ bar } +% \infer1{ baz } +% \infer2{ quux } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{left label,right label} +% The text to use as the labels of the rules, on the left and on the right +% of the inference line, is defined by the options \cmd{left label} and +% \cmd{right label}. +% Using the second optional argument in \cs{infer} is equivalent to setting +% the \env{right label} option with the value of that argument. +% \end{variable} +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer[left label=$\lambda$]1[abs] +% { \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer[left label=@]2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{left label template,right label template} +% Similarly to conclusions, labels are formatted according to templates. +% The code is arbitrary \TeX\ code, composed in horizontal mode, where the +% macro \cs{inserttext} can be used to insert the actual label text. +% The default values are simply \cs{inserttext} so that labels are set in +% plain text mode. +% \end{variable} +% \begin{variable}{label separation} +% The spacing between an inference line and its labels is defined by the +% option \cmd{label separation}, the default value is \texttt{0.5em}. +% The height of the horizontal axis used for aligning the labels with the +% rules is defined by the option \cmd{label axis}, the default value is +% \texttt{0.5ex}. +% \end{variable} +% +% +% \subsection{Style macros} +% \label{sec:styles} +% +% The following commands allow for the definition of custom styles using the +% basic style options, in a way similar to PGF's ``styles'' and \LaTeX3's +% ``meta-keys''. +% This allows setting a bunch of options with the same values in many proofs +% using a single definition. +% +% \begin{function}{\ebproofnewstyle} +% \begin{syntax} +% \cs{ebproofnewstyle}\marg{name}\marg{options} +% \end{syntax} +% The statement \cs{ebproofnewstyle} defines a new style option with some +% \meta{name} that sets a given set of \meta{options}. +% \end{function} +% For instance, the following code defines a new option \cmd{small} that sets +% various parameters so that proofs are rendered smaller. +% \begin{example} +% \ebproofnewstyle{small}{ +% separation = 1em, rule margin = .5ex, +% template = \footnotesize$\inserttext$ } +% \begin{prooftree}[small] +% \hypo{ \Gamma, A \vdash B } +% \infer1{ \Gamma \vdash A\to B } +% \hypo{ \Gamma \vdash A } \infer2{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% \begin{function}{\ebproofnewrulestyle} +% \begin{syntax} +% \cs{ebproofnewrulestyle}\marg{name}\marg{options} +% \end{syntax} +% The statement \cs{ebproofnewrulestyle} does the same for rule styles. +% The \meta{options} part includes options used to set how to draw rules in +% the new style. +% \end{function} +% +% The option \cmd{rule code} is useful in this command as it allows to +% define arbitrary rule styles. +% For instance, the squiggly rule example above could be turned into a new +% rule style \texttt{zigzag} with the following code: +% \begin{example} +% \ebproofnewrulestyle{zigzag}{ +% rule code = {\hbox{\tikz +% \draw[decorate,decoration={snake,amplitude=.3ex}] +% (0,0) -- (\hsize,0);}}} +% \begin{prooftree} +% \hypo{ \Gamma &\vdash A } +% \infer1{ \Gamma &\vdash A, \ldots, A } +% \hypo{ \Delta, A, \ldots, A \vdash \Theta } +% \infer[zigzag]2{ \Gamma, \Delta \vdash \Theta } +% \end{prooftree} +% \end{example} +% +% +% \section{License} +% +% This work may be distributed and/or modified under the +% conditions of the \LaTeX\ Project Public License, either version 1.3 +% of this license or (at your option) any later version. +% The latest version of this license is in +% \begin{center} +% \url{http://www.latex-project.org/lppl.txt} +% \end{center} +% and version 1.3 or later is part of all distributions of \LaTeX\ +% version 2005/12/01 or later. +% +% This work has the LPPL maintenance status `maintained'. +% +% The Current Maintainer of this work is Emmanuel Beffara. +% +% This work consists of the files \texttt{ebproof.sty} and \texttt{ebproof.tex}. +% +% \section{History} +% +% This section lists the principal evolutions of the package, in reverse +% chronological order. +% \begin{description} +% \item[Version 2.1 (2020-08-19)] +% Mostly a bugfix release. +% \begin{itemize} +% \item Makes the \env{prooftree} environment robust to use in tabular +% contexts. +% \item Adds the \cs{overlay} statement. +% \item Fixes a compatibility issue with \LaTeX\ release 2020-10-01. +% \end{itemize} +% \item[Version 2.0 (2017-05-17)] +% A complete rewrite of the code using the \LaTeX3 programming environment. +% The incompatible changes from the user's point of view are the following: +% \begin{itemize} +% \item Proof statements are now writtten in lowercase ({i.e.} \cs{Infer} is +% now written \cs{infer} etc.) but the syntax is otherwise unchanged. +% The old uppercase commands still work but produce a deprecation warning, +% they will be removed in a future version. +% \item New styles are now defined using \cs{ebproofnewstyle} and +% \cs{ebproofnewrulestyle}. The previous method using PGF styles does not +% work anymore (because PGF is not used anymore). +% \end{itemize} +% The new commands and options are the following: +% \begin{itemize} +% \item The statement \cs{rewrite} generalizes \cs{Alter}, +% \item The option \cmd{label axis} controls vertical alignment of labels. +% \end{itemize} +% \item[Version 1.1 (2015-03-13)] +% A bugfix release. +% In \cmd{template} options, one now uses \cs{inserttext} instead of \verb|#1| +% for the text arguments, which improves robustness. +% \item[Version 1.0 (2015-02-04)] +% The first public release. +% \end{description} +% +% \end{documentation} +% +% \clearpage \appendix +% +% \begin{implementation} +% +% \section{Implementation} +% +% \begin{macrocode} +%<*package> +\NeedsTeXFormat{LaTeX2e} +\RequirePackage{expl3} +\RequirePackage{xparse} +\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees} +%<@@=ebproof> +% \end{macrocode} +% +% \subsection{Parameters} +% +% We first declare all options. For the meaning of options, see +% section~\ref{sec:options}. +% +% \begin{macrocode} +\keys_define:nn { ebproof } { +center .bool_set:N = \l_@@_center_bool, +proof~style .choice: , +proof~style / upwards .code:n = \bool_set_false:N \l_@@_updown_bool, +proof~style / downwards .code:n = \bool_set_true:N \l_@@_updown_bool, +separation .dim_set:N = \l_@@_separation_dim, +rule~margin .dim_set:N = \l_@@_rule_margin_dim, +rule~thickness .dim_set:N = \l_@@_rule_thickness_dim, +rule~separation .dim_set:N = \l_@@_rule_separation_dim, +rule~dash~length .dim_set:N = \l_@@_rule_dash_length_dim, +rule~dash~space .dim_set:N = \l_@@_rule_dash_space_dim, +rule~code .tl_set:N = \l_@@_rule_code_tl, +rule~style .choice:, +template .tl_set:N = \l_@@_template_tl, +left~template .tl_set:N = \l_@@_left_template_tl, +right~template .tl_set:N = \l_@@_right_template_tl, +left~label .tl_set:N = \l_@@_left_label_tl, +right~label .tl_set:N = \l_@@_right_label_tl, +left~label~template .tl_set:N = \l_@@_left_label_template_tl, +right~label~template .tl_set:N = \l_@@_right_label_template_tl, +label~separation .dim_set:N = \l_@@_label_separation_dim, +label~axis .dim_set:N = \l_@@_label_axis_dim, +} +% \end{macrocode} +% +% \begin{macro}{\ebproofnewrulestyle} +% We then define the document-level macro \cs{ebproofnewrulestyle} and use +% it to define the default styles. This simply consists in defining a +% meta-key. +% \begin{macrocode} +\NewDocumentCommand \ebproofnewrulestyle { mm } { + \keys_define:nn { ebproof } { + rule~style / #1 .meta:nn = { ebproof } { #2 } + } +} +% \end{macrocode} +% \end{macro} +% +% The styles |simple|, |no rule| and |double| are defined in a straightforward +% way. +% +% \begin{macrocode} +\ebproofnewrulestyle { simple } { + rule~code = { \tex_hrule:D height \l_@@_rule_thickness_dim } +} +\ebproofnewrulestyle { no~rule } { + rule~code = +} +\ebproofnewrulestyle { double } { + rule~code = { + \tex_hrule:D height \l_@@_rule_thickness_dim + \skip_vertical:N \l_@@_rule_separation_dim + \tex_hrule:D height \l_@@_rule_thickness_dim + } +} +% \end{macrocode} +% +% The |dashed| style uses leaders and filling for repeating a single dash. We +% use \TeX\ primitives that have no \LaTeX3 counterpart for this. +% +% \begin{macrocode} +\ebproofnewrulestyle { dashed } { + rule~code = { + \hbox_to_wd:nn { \tex_hsize:D } { + \dim_set:Nn \l_tmpa_dim { \l_@@_rule_dash_space_dim / 2 } + \skip_horizontal:n { -\l_tmpa_dim } + \tex_cleaders:D \hbox:n { + \skip_horizontal:N \l_tmpa_dim + \tex_vrule:D + height \l_@@_rule_thickness_dim + width \l_@@_rule_dash_length_dim + \skip_horizontal:N \l_tmpa_dim + } \tex_hfill:D + \skip_horizontal:n { -\l_tmpa_dim } + } + } +} +% \end{macrocode} +% +% Now we can define the default values, including the default rule style. +% +% \begin{macrocode} +\keys_set:nn { ebproof } { + center = true, + proof~style = upwards, + separation = 1.5em, + rule~margin = .7ex, + rule~thickness = .4pt, + rule~separation = 2pt, + rule~dash~length = .2em, + rule~dash~space = .3em, + rule~style = simple, + template = $\inserttext$, + left~template = $\inserttext\mathrel{}$, + right~template = $\mathrel{}\inserttext$, + left~label = , + right~label = , + left~label~template = \inserttext, + right~label~template = \inserttext, + label~separation = 0.5em, + label~axis = 0.5ex +} +% \end{macrocode} +% +% \begin{macro}{\ebproofnewstyle} +% Defining a style simply means defining a meta-key. +% \begin{macrocode} +\NewDocumentCommand \ebproofnewstyle { mm } { + \keys_define:nn { ebproof } { #1 .meta:n = { #2 } } +} +% \end{macrocode} +% \end{macro} +% +% +% \subsection{Proof boxes} +% +% \TeX\ does not actually provide data structures, so we have to encode things. +% We provide an allocator for ``registers'' holding boxes with attributes. Such +% a register consists in a box register and a property list for marks, which +% maps mark names to values as explicit dimensions with units. +% +% \begin{macro}{\@@_new:N} +% Using only public interfaces forces a convoluted approach to allocation: +% we use a global counter \cs{g_ebproof_register_int} to number registers, +% then each allocation creates registers named \cs{g_ebproof_K_N} where K is +% the kind of component (box or marks) and N is the identifier of the +% register. The proof box register itself only contains the identifier used +% for indirection. +% \begin{macrocode} +\int_new:N \g_@@_register_int +\cs_new:Nn \@@_box:N { g__ebproof_box_ \tl_use:N #1 } +\cs_new:Nn \@@_marks:N { g__ebproof_marks_ \tl_use:N #1 } +\cs_new:Nn \@@_new:N { + \tl_new:N #1 + \int_gincr:N \g_@@_register_int + \tl_gset:Nx #1 { \int_to_arabic:n { \g_@@_register_int } } + \box_new:c { \@@_box:N #1 } + \prop_new:c { \@@_marks:N #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_clear:N} +% The box is cleared by setting it to an empty hbox. +% Using \cs{box_clear:N} instead would not work because trying to push this +% box on the stack would not actually append any box. +% \begin{macrocode} +\cs_new:Nn \@@_clear:N { + \hbox_set:cn { \@@_box:N #1 } {} + \prop_clear:c { \@@_marks:N #1 } + \@@_set_mark:Nnn #1 { left } { 0pt } + \@@_set_mark:Nnn #1 { right } { 0pt } + \@@_set_mark:Nnn #1 { axis } { 0pt } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Mark operations} +% +% \begin{macro}{\@@_set_mark:Nnn} +% Setting the value of a mark uses a temporary register to evaluate the +% dimension expression because values are stored textually in a property +% list. +% \begin{macrocode} +\dim_new:N \l_@@_transit_dim +\cs_new:Nn \@@_set_mark:Nnn { + \dim_set:Nn \l_@@_transit_dim { #3 } + \prop_put:cnV { \@@_marks:N #1 } { #2 } + \l_@@_transit_dim +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_mark:Nn} +% Getting the value of a mark simply consists in getting an item in a +% property list. +% \begin{macrocode} +\cs_new:Nn \@@_mark:Nn { + \prop_item:cn { \@@_marks:N #1 } { #2 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_shift_x:Nn} +% This function shifts the marks by a specified amount, without modifying +% the box. +% \begin{macrocode} +\cs_new:Nn \@@_shift_x:Nn { + \prop_map_inline:cn { \@@_marks:N #1 } { + \@@_set_mark:Nnn #1 { ##1 } { ##2 + #2 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_enlarge_conclusion:NN} +% This function moves the left and right marks of the first tree so that +% they are at least as far from the axis as they are in the second tree. +% For instance we get the following: +% \begin{center} +% \begin{tikzpicture}[y=-3ex] +% \node (L1) at (1,0) {L}; \node (A1) at (2,0) {A}; \node (R1) at (4,0) {R}; +% \node (L2) at (0,1) {L}; \node (A2) at (2,1) {A}; \node (R2) at (3,1) {R}; +% \node (L3) at (0,2) {L}; \node (A3) at (2,2) {A}; \node (R3) at (4,2) {R}; +% \draw (L1) -- (A1) -- (R1); +% \draw (L2) -- (A2) -- (R2); +% \draw (L3) -- (A3) -- (R3); +% \node[anchor=west] at (5,0) {box 1 before}; +% \node[anchor=west] at (5,1) {box 2 before}; +% \node[anchor=west] at (5,2) {box 1 after}; +% \end{tikzpicture} +% \end{center} +% The contents of the trees are unchanged. +% \begin{macrocode} +\cs_new:Nn \@@_enlarge_conclusion:NN { + \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis} + + \@@_mark:Nn #2 {left} - \@@_mark:Nn #2 {axis} } + \dim_compare:nNnT { \l_tmpa_dim } < { \@@_mark:Nn #1 {left} } { + \@@_set_mark:Nnn #1 {left} { \l_tmpa_dim } } + \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis} + + \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {axis} } + \dim_compare:nNnT { \l_tmpa_dim } > { \@@_mark:Nn #1 {right} } { + \@@_set_mark:Nnn #1 {right} { \l_tmpa_dim } } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Building blocks} +% +% \begin{macro}{\@@_make_simple:Nn} +% Make a tree with explicit material in horizontal mode. Set the left and +% right marks to extremal positions and set the axis in the middle. +% \begin{macrocode} +\cs_new:Nn \@@_make_simple:Nn { + \hbox_set:cn { \@@_box:N #1 } { #2 } + \@@_set_mark:Nnn #1 { left } { 0pt } + \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } / 2 } + \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_make_split:Nnn} +% Make a tree with explicit material in horizontal mode, split in two parts. +% Set the left and right marks to extremal positions and set the axis +% between the two parts. +% \begin{macrocode} +\cs_new:Nn \@@_make_split:Nnn { + \@@_set_mark:Nnn #1 { left } { 0pt } + \hbox_set:cn { \@@_box:N #1 } { #2 } + \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } } + \hbox_set:cn { \@@_box:N #1 } { \hbox_unpack:c { \@@_box:N #1 } #3 } + \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_make_vertical:Nnnn} +% Make a tree with explicit material in vertical mode, using an explicit +% width and axis. +% \begin{macrocode} +\cs_new:Nn \@@_make_vertical:Nnnn { + \@@_set_mark:Nnn #1 { left } { 0pt } + \@@_set_mark:Nnn #1 { axis } { #2 } + \@@_set_mark:Nnn #1 { right } { #3 } + \vbox_set:cn { \@@_box:N #1 } { + \dim_set:Nn \tex_hsize:D { \@@_mark:Nn #1 {right} } + #4 + } + \box_set_wd:cn { \@@_box:N #1 } { \@@_mark:Nn #1 {right} } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Assembling boxes} +% +% \begin{macro}{\@@_extend:Nnnnn} +% Extend a tree box. The marks are shifted so that alignment is preserved. +% The arguments are dimensions for the left, top, right and bottom sides +% respectively. +% \begin{macrocode} +\cs_new:Nn \@@_extend:Nnnnn { + \dim_compare:nNnF { #2 } = { 0pt } { + \hbox_set:cn { \@@_box:N #1 } { + \skip_horizontal:n { #2 } + \box_use:c { \@@_box:N #1 } + } + \@@_shift_x:Nn #1 { #2 } + } + \box_set_ht:Nn #1 { \box_ht:c { \@@_box:N #1 } + #3 } + \box_set_wd:Nn #1 { \box_wd:c { \@@_box:N #1 } + #4 } + \box_set_dp:Nn #1 { \box_dp:c { \@@_box:N #1 } + #5 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_right:NnN} +% Append the contents of the second tree to the first one on the right, with +% matching baselines. The marks of both trees are preserved. The middle +% argument specifies the space to insert between boxes. +% \begin{macrocode} +\cs_new:Nn \@@_append_right:NnN { + \hbox_set:cn { \@@_box:N #1 } { + \box_use:c { \@@_box:N #1 } + \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } + \box_use:c { \@@_box:N #3 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_left:NnN} +% Append the contents of the second tree to the first one on the left, with +% matching baselines. The marks of the first tree are shifted accordingly. +% The middle argument specifies the space to insert between boxes. +% \begin{macrocode} +\cs_new:Nn \@@_append_left:NnN { + \@@_shift_x:Nn #1 { \box_wd:c { \@@_box:N #3 } + #2 } + \hbox_set:cn { \@@_box:N #1 } { + \box_use:c { \@@_box:N #3 } + \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } + \box_use:c { \@@_box:N #1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_align:NN} +% Shift one of two trees to the right so that their axes match. The marks of +% the one that is shifted are updated accordingly. +% \begin{macrocode} +\cs_new:Nn \@@_align:NN { + \dim_set:Nn \l_tmpa_dim + { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #1 {axis} } + \dim_compare:nNnTF \l_tmpa_dim < { 0pt } { + \@@_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt } + } { + \@@_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_above:NN} +% Append the contents of the second tree above the first one, with matching +% axes. The marks of the first tree are preserved. +% \begin{macrocode} +\cs_new:Nn \@@_append_above:NN { + \@@_align:NN #1 #2 + \vbox_set:cn { \@@_box:N #1 } { + \box_use:c { \@@_box:N #2 } + \tex_prevdepth:D -1000pt + \box_use:c { \@@_box:N #1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_below:NN} +% Append the contents of the second tree below the first one, with matching +% axes. The marks of the first tree are preserved. +% \begin{macrocode} +\cs_new:Nn \@@_append_below:NN { + \@@_align:NN #1 #2 + \vbox_set_top:Nn #1 { + \box_use:c { \@@_box:N #1 } + \tex_prevdepth:D -1000pt + \box_use:c { \@@_box:N #2 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_overlay:NN} +% Append the second tree as an overlay over the first one, so that the +% baselines and axes match. The bounding box of the result adjusts to +% contain both trees. +% \begin{macrocode} +\cs_new:Nn \@@_overlay:NN { + \@@_align:NN #1 #2 + \hbox_set:cn { \@@_box:N #1 } { + \hbox_overlap_right:n { \box_use:c { \@@_box:N #1 } } + \box_use:c { \@@_box:N #2 } + \dim_compare:nNnT + { \box_wd:c { \@@_box:N #2 } } < { \box_wd:c { \@@_box:N #1 } } + { \skip_horizontal:n + { \box_wd:c { \@@_box:N #1 } - \box_wd:c { \@@_box:N #2 } } } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_vcenter:N} +% Shift the material in a tree vertically so that the height and depth are +% equal (like \TeX's \cs{vcenter} but around the baseline). +% \begin{macrocode} +\cs_new:Nn \@@_vcenter:N { + \dim_set:Nn \l_tmpa_dim + { ( \box_ht:c { \@@_box:N #1 } - \box_dp:c { \@@_box:N #1 } ) / 2 } + \box_set_eq:Nc \l_tmpa_box { \@@_box:N #1 } + \hbox_set:cn { \@@_box:N #1 } + { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } } +} +% \end{macrocode} +% \end{macro} +% +% \subsection{Making inferences} +% +% The following commands use the parameters defined at the beginning of the +% package for actually building proof trees using the commands defined above. +% +% \begin{macro}{\@@_append_vertical:NN} +% Append the contents of the second tree above or below the first one, +% depending on current settings. Axes are aligned and the marks of the first +% tree are preserved. +% \begin{macrocode} +\cs_new:Nn \@@_append_vertical:NN { + \bool_if:NTF \l_@@_updown_bool + { \@@_append_below:NN #1 #2 } + { \@@_append_above:NN #1 #2 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_make_rule_for:NNN} +% Make a box containing an inference rule with labels, using the current +% settings. The width and axis position are taken as those of the conclusion +% of another tree box. The third argument is used as a temporary register +% for building labels. +% \begin{macrocode} +\cs_new:Nn \@@_make_rule_for:NNN { +% \end{macrocode} +% Build the rule. +% \begin{macrocode} + \@@_make_vertical:Nnnn #1 + { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #2 {left} } + { \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {left} } + { + \skip_vertical:N \l_@@_rule_margin_dim + \tl_if_empty:NF { \l_@@_rule_code_tl } { + \tl_use:N \l_@@_rule_code_tl + \skip_vertical:N \l_@@_rule_margin_dim + } + } + \@@_vcenter:N #1 +% \end{macrocode} +% Append the left label. +% \begin{macrocode} + \tl_if_blank:VF \l_@@_left_label_tl { + \@@_make_simple:Nn #3 { + \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n { + \cs_set_eq:NN \inserttext \l_@@_left_label_tl + \tl_use:N \l_@@_left_label_template_tl + } } + } + \box_set_ht:cn { \@@_box:N #3 } { 0pt } + \box_set_dp:cn { \@@_box:N #3 } { 0pt } + \@@_append_left:NnN + \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box + } +% \end{macrocode} +% Append the right label. +% \begin{macrocode} + \tl_if_blank:VF \l_@@_right_label_tl { + \@@_make_simple:Nn #3 { + \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n { + \cs_set_eq:NN \inserttext \l_@@_right_label_tl + \tl_use:N \l_@@_right_label_template_tl + } } + } + \box_set_ht:cn { \@@_box:N #3 } { 0pt } + \box_set_dp:cn { \@@_box:N #3 } { 0pt } + \@@_append_right:NnN + \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box + } +} +% \end{macrocode} +% \end{macro} +% +% \subsection{Stack-based interface} +% +% \subsubsection{The stack} +% +% Logically, box structures are stored on a stack. However, \TeX\ does not +% provide data structures for that and the grouping mechanism is not flexible +% enough, so we encode them using what we actually have. A stack for boxes is +% implemented using a global hbox \cs{g_@@_stack_box} that contains all the +% boxes successively. A sequence \cs{g_@@_stack_seq} is used to store the +% dimensions property lists textually. We maintain a counter +% \cs{g_@@_level_int} with the number of elements on the stack, for +% consistency checks. +% \begin{macrocode} +\int_new:N \g_@@_level_int +\box_new:N \g_@@_stack_box +\seq_new:N \g_@@_stack_seq +% \end{macrocode} +% +% \begin{macro}{\@@_clear_stack:} +% Clear the stack. +% \begin{macrocode} +\cs_new:Nn \@@_clear_stack: { + \int_gset:Nn \g_@@_level_int { 0 } + \hbox_gset:Nn \g_@@_stack_box { } + \seq_gclear:N \g_@@_stack_seq +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_push:N} +% Push the contents of a register on the stack. +% \begin{macrocode} +\cs_new:Nn \@@_push:N { + \int_gincr:N \g_@@_level_int + \hbox_gset:Nn \g_@@_stack_box + { \hbox_unpack:N \g_@@_stack_box \box_use:c { \@@_box:N #1 } } + \seq_gput_left:Nv \g_@@_stack_seq + { \@@_marks:N #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_pop:N} +% Pop the value from the top of the stack into a register. +% \begin{macrocode} +\cs_new:Nn \@@_pop:N { + \int_compare:nNnTF { \g_@@_level_int } > { 0 } { + \int_gdecr:N \g_@@_level_int + \hbox_gset:Nn \g_@@_stack_box { + \hbox_unpack:N \g_@@_stack_box + \box_gset_to_last:N \g_tmpa_box + } + \box_set_eq_clear:cN { \@@_box:N #1 } \g_tmpa_box + \seq_gpop_left:NN \g_@@_stack_seq \l_tmpa_tl + \tl_set_eq:cN { \@@_marks:N #1 } \l_tmpa_tl + } { + \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{} + \@@_clear:N #1 + } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Assembling trees} +% +% \begin{macrocode} +\@@_new:N \l_@@_a_box +\@@_new:N \l_@@_b_box +\@@_new:N \l_@@_c_box +\@@_new:N \l_@@_d_box +% \end{macrocode} +% +% \begin{macro}{\@@_join_horizontal:n} +% Join horizontally a number of elements at the top of the stack. If several +% trees are joined, use the left mark of the left tree, the right mark of +% the right tree and set the axis in the middle of these marks. +% \begin{macrocode} +\cs_new:Nn \@@_join_horizontal:n { + \int_case:nnF { #1 } { + { 0 } { + \group_begin: + \@@_clear:N \l_@@_a_box + \@@_push:N \l_@@_a_box + \group_end: + } + { 1 } { } + } { + \group_begin: + \@@_pop:N \l_@@_a_box + \prg_replicate:nn { #1 - 1 } { + \@@_pop:N \l_@@_b_box + \@@_append_left:NnN + \l_@@_a_box \l_@@_separation_dim \l_@@_b_box + } + \@@_set_mark:Nnn \l_@@_a_box { left } + { \@@_mark:Nn \l_@@_b_box { left } } + \@@_set_mark:Nnn \l_@@_a_box { axis } + { ( \@@_mark:Nn \l_@@_a_box { left } + + \@@_mark:Nn \l_@@_a_box { right } ) / 2 } + \@@_push:N \l_@@_a_box + \group_end: + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_join_vertical:} +% Join vertically the two elements at the top of the stack, with a +% horizontal rule of the appropriate size. +% \begin{macrocode} +\cs_new:Nn \@@_join_vertical: { + \group_begin: + \@@_pop:N \l_@@_a_box + \@@_pop:N \l_@@_b_box + \@@_enlarge_conclusion:NN \l_@@_b_box \l_@@_a_box + \@@_make_rule_for:NNN \l_@@_c_box \l_@@_b_box + \l_@@_d_box + \@@_append_vertical:NN \l_@@_a_box \l_@@_c_box + \@@_append_vertical:NN \l_@@_a_box \l_@@_b_box + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{High-level commands} +% +% \begin{macro}{\@@_statement_parse:w} +% An auxiliary function for parsing the argument in +% \cs{@@_push_statement:n}. +% \begin{macrocode} +\cs_new:Npn \@@_statement_parse:w #1 & #2 & #3 \q_stop { + \tl_if_empty:nTF { #3 } { + \@@_make_simple:Nn \l_@@_a_box + { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_template_tl } + } { + \@@_make_split:Nnn \l_@@_a_box + { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_left_template_tl } + { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_@@_right_template_tl } + } + \@@_push:N \l_@@_a_box +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_push_statement:n} +% Push a box with default formatting, using explicit alignment if the code +% contains a |&| character +% \begin{macrocode} +\cs_new:Nn \@@_push_statement:n { + \@@_statement_parse:w #1 & & \q_stop +} +% \end{macrocode} +% \end{macro} +% +% \subsection{Document interface} +% +% \subsubsection{Functions to define statements} +% +% The \cs{g_@@_statements_seq} variable contains the list of all defined +% statements. For each statement |X|, there is a document command \cs{ebproofX} +% and the alias \cs{X} is defined when entering a |prooftree| environment. +% \begin{macrocode} +\seq_new:N \g_@@_statements_seq +% \end{macrocode} +% +% \begin{macro}{\@@_setup_statements:} +% Install the aliases for statements, saving the original value of the control +% sequences. +% \begin{macrocode} +\cs_new:Nn \@@_setup_statements: { + \seq_map_inline:Nn \g_@@_statements_seq { + \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 } + \cs_set_eq:cc { ##1 } { ebproof ##1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_restore_statements:} +% Restore the saved meanings of the control sequences. This is useful when +% interpreting user-provided code in statement arguments. The meanings are +% automatically restored when leaving a |prooftree| environment because of +% grouping. +% \begin{macrocode} +\cs_new:Nn \@@_restore_statements: { + \seq_map_inline:Nn \g_@@_statements_seq { + \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_new_statement:nnn} +% Define a new statement. The first argument is the name, the second one is +% an argument specifier as used by |xparse| and the third one is the body of +% the command. +% \begin{macrocode} +\cs_new:Nn \@@_new_statement:nnn { + \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 } + \seq_put_right:Nn \g_@@_statements_seq { #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_new_deprecated_statement:nnnn} +% Define a deprecated statement. The syntax is the same as above except that +% an extra argument in third position indicates what should be used instead. +% The effect is the same except that a warning message is issued the first +% time the statement is used. +% \begin{macrocode} +\cs_new:Nn \@@_new_deprecated_statement:nnnn { + \cs_new:cpn { ebproof_#1_warning: } { + \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 } + \cs_gset:cn { ebproof_#1_warning: } { } + } + \@@_new_statement:nnn { #1 } { #2 } + { \use:c { ebproof_#1_warning: } #4 } +} +% \end{macrocode} +% \end{macro} +% +% +% \subsubsection{Basic commands} +% +% \begin{macro}{\ebproofset,\set} +% This is a simple wrapper around \cs{keys_set:nn}. +% \begin{macrocode} +\@@_new_statement:nnn { set } { m } { + \keys_set:nn { ebproof } { #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\hypo} +% This is mostly a wrapper around \cs{ebproof_push_statement:n}, with +% material to handle options and the statements macros. +% \begin{macrocode} +\@@_new_statement:nnn { hypo } { O{} m } { + \group_begin: + \@@_restore_statements: + \keys_set:nn { ebproof } { #1 } + \@@_push_statement:n { #2 } + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\infer} +% This is a bit more involved than \cs{hypo} because we have to handle rule +% style options and joining. +% \begin{macrocode} +\@@_new_statement:nnn { infer } { O{} m O{} m } { + \group_begin: + \@@_restore_statements: + \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl + \keys_set:nV { ebproof } \l_tmpa_tl + \tl_set:Nn \l_@@_right_label_tl { #3 } + \@@_join_horizontal:n { #2 } + \@@_push_statement:n { #4 } + \@@_join_vertical: + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\ellipsis} +% An ellipsis is made by hand using vertical leaders to render the dots +% after rendering the label. +% \begin{macrocode} +\@@_new_statement:nnn { ellipsis } { m m } { + \group_begin: + \@@_restore_statements: + \tl_clear:N \l_@@_rule_code_tl + \@@_make_split:Nnn \l_@@_a_box { } { + \vbox_set:Nn \l_tmpa_box { + \skip_vertical:n { 1.2ex } + \hbox:n { \tex_ignorespaces:D #1 } + \skip_vertical:n { 1.2ex } + } + \vbox_to_ht:nn { \box_ht:N \l_tmpa_box } { + \tex_xleaders:D \vbox_to_ht:nn { .8ex } + { \tex_vss:D \hbox:n { . } \tex_vss:D } + \tex_vfill:D + } + \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box } + } + \@@_push:N \l_@@_a_box + \@@_join_vertical: + \@@_push_statement:n {#2} + \@@_join_vertical: + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Modifying trees} +% +% \begin{macro}{\rewrite} +% Rewrite the box at the top of the stack while preserving its dimensions an +% marks. The code is typeset in horizontal mode, with control sequences to +% access the original box and its marks. +% \begin{macrocode} +\@@_new_statement:nnn { rewrite } { m } { + \group_begin: + \@@_restore_statements: + \@@_pop:N \l_@@_a_box + \box_set_eq:Nc \l_tmpa_box { \@@_box:N \l_@@_a_box } + \hbox_set:Nn \l_tmpb_box { + \cs_set_eq:NN \treebox \l_tmpa_box + \cs_set:Npn \treemark { \@@_mark:Nn \l_@@_a_box } + { #1 } + } + \box_set_wd:Nn \l_tmpb_box { \box_wd:c { \@@_box:N \l_@@_a_box } } + \box_set_ht:Nn \l_tmpb_box { \box_ht:c { \@@_box:N \l_@@_a_box } } + \box_set_dp:Nn \l_tmpb_box { \box_dp:c { \@@_box:N \l_@@_a_box } } + \box_set_eq:cN { \@@_box:N \l_@@_a_box } \l_tmpb_box + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\delims} +% Insert \cs{left} and \cs{right} delimiters without changing the alignment. +% \begin{macrocode} +\@@_new_statement:nnn { delims } { m m } { + \group_begin: + \@@_restore_statements: + \@@_pop:N \l_@@_a_box + \hbox_set:Nn \l_tmpa_box + { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ } + \dim_set:Nn \l_tmpa_dim + { \box_ht:N \l_tmpa_box - \box_ht:c { \@@_box:N \l_@@_a_box } } + \hbox_set:cn { \@@_box:N \l_@@_a_box } { + $ #1 \tex_vrule:D + height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt + \tex_right:D . $ + } + \@@_shift_x:Nn \l_@@_a_box + { \box_wd:c { \@@_box:N \l_@@_a_box } } + \hbox_set:cn { \@@_box:N \l_@@_a_box } { + \hbox_unpack:c { \@@_box:N \l_@@_a_box } + $ \tex_left:D . \box_use:N \l_tmpa_box #2 $ + } + \hbox_set:cn { \@@_box:N \l_@@_a_box } + { \box_move_down:nn { \l_tmpa_dim } + { \box_use:c { \@@_box:N \l_@@_a_box } } } + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\overlay} +% Pop two trees and append the second tree as an overlay over the first one, +% so that the baselines and axes match. The bounding box of the result +% adjusts to contain both trees. +% \begin{macrocode} +\@@_new_statement:nnn { overlay } { } { + \group_begin: + \@@_pop:N \l_@@_a_box + \@@_pop:N \l_@@_b_box + \@@_overlay:NN \l_@@_a_box \l_@@_b_box + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Deprecated statements} +% +% These statements were defined in versions 1.x of the package, they are +% preserved for temporary upwards compatibility and will be removed in a +% future version. +% \begin{macrocode} +\@@_new_deprecated_statement:nnnn { Alter } { m } + { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } } +\@@_new_deprecated_statement:nnnn { Delims } { } + { use~\token_to_str:c{delims}~instead } { \ebproofdelims } +\@@_new_deprecated_statement:nnnn { Ellipsis } { } + { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis } +\@@_new_deprecated_statement:nnnn { Hypo } { } + { use~\token_to_str:c{hypo}~instead } { \ebproofhypo } +\@@_new_deprecated_statement:nnnn { Infer } { } + { use~\token_to_str:c{infer}~instead } { \ebproofinfer } +% \end{macrocode} +% +% +% \subsubsection{Environment interface} +% +% The stack is initialised globally. The \env{prooftree} environment does not +% clear the stack, instead it saves the initial level in order to check that +% statements are properly balanced. This allows for nested uses of the +% environment, if it ever happens to be useful. +% +% \begin{macrocode} +\@@_clear_stack: +\tl_new:N \l_@@_start_level_tl +% \end{macrocode} +% +% \begin{macro}{prooftree,prooftree*} +% The \env{prooftree} environment. +% \begin{macrocode} +\NewDocumentEnvironment { prooftree } { s O{} } { + \group_align_safe_begin: + \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl + \keys_set:nV { ebproof } \l_tmpa_tl + \tl_set:Nx \l_@@_start_level_tl { \int_use:N \g_@@_level_int } + \vbox_set:Nw \l_tmpa_box + \@@_setup_statements: +} { + \vbox_set_end: + \@@_pop:N \l_@@_a_box + \int_compare:nNnF { \g_@@_level_int } = { \tl_use:N \l_@@_start_level_tl } { + \PackageError{ebproof}{Malformed~proof~tree}{ + Some~hypotheses~were~declared~but~not~used~in~this~tree.} + } + \IfBooleanTF { #1 } { + \[ \box_use:c { \@@_box:N \l_@@_a_box } \] + \ignorespacesafterend + } { + \hbox_unpack:N \c_empty_box + \bool_if:NTF \l_@@_center_bool { + \hbox:n { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ } + } { + \box_use:c { \@@_box:N \l_@@_a_box } + } + } + \group_align_safe_end: +} +% \end{macrocode} +% A trick for the starred version: +% \begin{macrocode} +\cs_new:cpn { prooftree* } { \prooftree* } +\cs_new:cpn { endprooftree* } { \endprooftree } +% \end{macrocode} +% \end{macro} +% +% \begin{macrocode} +% +% \end{macrocode} +% +% \end{implementation} diff --git a/macros/latex/contrib/ebproof/ebproof.ins b/macros/latex/contrib/ebproof/ebproof.ins new file mode 100644 index 0000000000..25bcc73496 --- /dev/null +++ b/macros/latex/contrib/ebproof/ebproof.ins @@ -0,0 +1,15 @@ +%% Copyright (C) 2015-2018 by Emmanuel Beffara +%% +%% This file may be distributed and/or modified under the conditions of the +%% LaTeX Project Public License, either version 1.3 of this license or (at +%% your option) any later version. The latest version of this license is in: +%% +%% http://www.latex-project.org/lppl.txt +%% +%% and version 1.3 or later is part of all distributions of LaTeX version +%% 2005/12/01 or later. + +\input l3docstrip.tex +\keepsilent \askforoverwritefalse +\generate{\file{ebproof.sty}{\from{ebproof.dtx}{package}}} +\endbatchfile diff --git a/macros/latex/contrib/ebproof/ebproof.pdf b/macros/latex/contrib/ebproof/ebproof.pdf index e4c8d03b25..60d433b9fd 100644 Binary files a/macros/latex/contrib/ebproof/ebproof.pdf and b/macros/latex/contrib/ebproof/ebproof.pdf differ diff --git a/macros/latex/contrib/ebproof/ebproof.sty b/macros/latex/contrib/ebproof/ebproof.sty deleted file mode 100644 index 7601f8e9e8..0000000000 --- a/macros/latex/contrib/ebproof/ebproof.sty +++ /dev/null @@ -1,767 +0,0 @@ -% The ebproof package - Formal proofs in the style of sequent calculus - -%% ebproof.sty -%% Copyright 2017 Emmanuel Beffara - -% This work may be distributed and/or modified under the -% conditions of the LaTeX Project Public License, either version 1.3 -% of this license or (at your option) any later version. -% The latest version of this license is in -% http://www.latex-project.org/lppl.txt -% and version 1.3 or later is part of all distributions of LaTeX -% version 2005/12/01 or later. - -% This work has the LPPL maintenance status `maintained'. - -% The Current Maintainer of this work is Emmanuel Beffara. - -% This work consists of the files ebproof.sty and ebproof.tex. - -\NeedsTeXFormat{LaTeX2e} -\RequirePackage{expl3} -\RequirePackage{xparse} -\ProvidesExplPackage{ebproof}{2017/05/17}{2.0}{EB's proof trees} - - -%% Parameters - -%%% Declaration of the parameters - -\keys_define:nn { ebproof } { - -% general shape - -center .bool_set:N = \l_ebproof_center_bool, - -proof~style .choice: , -proof~style / upwards .code:n = \bool_set_false:N \l_ebproof_updown_bool, -proof~style / downwards .code:n = \bool_set_true:N \l_ebproof_updown_bool, - -% spacing - -separation .dim_set:N = \l_ebproof_separation_dim, -rule~margin .dim_set:N = \l_ebproof_rule_margin_dim, - -% shape of inference lines - -rule~thickness .dim_set:N = \l_ebproof_rule_thickness_dim, -rule~separation .dim_set:N = \l_ebproof_rule_separation_dim, -rule~dash~length .dim_set:N = \l_ebproof_rule_dash_length_dim, -rule~dash~space .dim_set:N = \l_ebproof_rule_dash_space_dim, -rule~code .tl_set:N = \l_ebproof_rule_code_tl, - -rule~style .choice:, - -% templates - -template .tl_set:N = \l_ebproof_template_tl, -left~template .tl_set:N = \l_ebproof_left_template_tl, -right~template .tl_set:N = \l_ebproof_right_template_tl, - -% labels - -left~label .tl_set:N = \l_ebproof_left_label_tl, -right~label .tl_set:N = \l_ebproof_right_label_tl, -left~label~template .tl_set:N = \l_ebproof_left_label_template_tl, -right~label~template .tl_set:N = \l_ebproof_right_label_template_tl, -label~separation .dim_set:N = \l_ebproof_label_separation_dim, -label~axis .dim_set:N = \l_ebproof_label_axis_dim, - -} - -%%% Rule styles - -\NewDocumentCommand \ebproofnewrulestyle { mm } { - \keys_define:nn { ebproof } { - rule~style / #1 .meta:nn = { ebproof } { #2 } - } -} - -\ebproofnewrulestyle { simple } { - rule~code = { \tex_hrule:D height \l_ebproof_rule_thickness_dim } -} - -\ebproofnewrulestyle { no~rule } { - rule~code = -} - -\ebproofnewrulestyle { double } { - rule~code = { - \tex_hrule:D height \l_ebproof_rule_thickness_dim - \skip_vertical:N \l_ebproof_rule_separation_dim - \tex_hrule:D height \l_ebproof_rule_thickness_dim - } -} - -\ebproofnewrulestyle { dashed } { - rule~code = { - \hbox_to_wd:nn { \tex_hsize:D } { - \dim_set:Nn \l_tmpa_dim { \l_ebproof_rule_dash_space_dim / 2 } - \skip_horizontal:n { -\l_tmpa_dim } - \tex_cleaders:D \hbox:n { - \skip_horizontal:N \l_tmpa_dim - \tex_vrule:D - height \l_ebproof_rule_thickness_dim - width \l_ebproof_rule_dash_length_dim - \skip_horizontal:N \l_tmpa_dim - }\tex_hfill:D - \skip_horizontal:n { -\l_tmpa_dim } - } - } -} - -%%% Default values - -\keys_set:nn { ebproof } { - center = true, - proof~style = upwards, - separation = 1.5em, - rule~margin = .7ex, - rule~thickness = .4pt, - rule~separation = 2pt, - rule~dash~length = .2em, - rule~dash~space = .3em, - rule~style = simple, - template = $\inserttext$, - left~template = $\inserttext\mathrel{}$, - right~template = $\mathrel{}\inserttext$, - left~label = , - right~label = , - left~label~template = \inserttext, - right~label~template = \inserttext, - label~separation = 0.5em, - label~axis = 0.5ex -} - -%%% Defining style macros - -\NewDocumentCommand \ebproofnewstyle { mm } { - \keys_define:nn { ebproof } { #1 .meta:n = { #2 } } -} - - -%% Proof trees - -% Proof trees are represented as a data structure that consists of a box and a -% set of marks, which are vertical positions in the box (as distances from the -% left edge). Arbitrary marks can be defined, the folowing are used for -% alignment: -% - left : the left of the conclusion -% - right : the right of the conclusion -% - axis : the vertical axis of the conclusion - - -%%% Registers - -% TeX does not actually provide data structures, so we have to encode things. -% We provide an allocator for "registers" holding boxes with attributes. Such -% a register consists in a box register and a property list for marks, which -% maps mark names to values as explicit dimensions with units. - -% Create a new register. - -\cs_new:Nn \ebproof_new:N { - \box_new:N #1 - \prop_new:c { l_ebproof_marks_ \__int_value:w #1 _prop } -} - -% Clear a register. - -\cs_new:Nn \ebproof_clear:N { - \hbox_set:Nn #1 {} - % Using \box_clear:N instead would not work because trying to push this box - % on the stack would not actually append any box. - \prop_clear:c { l_ebproof_marks_ \__int_value:w #1 _prop } - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \ebproof_set_mark:Nnn #1 { right } { 0pt } - \ebproof_set_mark:Nnn #1 { axis } { 0pt } -} - - -%%% Mark operations - -% Set the value of a mark. The third argument is a dimension expression. - -\dim_new:N \l_ebproof_transit_dim - -\cs_new:Nn \ebproof_set_mark:Nnn { - \dim_set:Nn \l_ebproof_transit_dim { #3 } - \prop_put:cnV { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 } - \l_ebproof_transit_dim -} - -% Get the value of a mark. This is expandable and can be used in expressions. - -\cs_new:Nn \ebproof_mark:Nn { - \prop_item:cn { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 } -} - -% Shift the marks by a specified amount, without modifying the box. - -\cs_new:Nn \ebproof_shift_x:Nn { - \prop_map_inline:cn { l_ebproof_marks_ \__int_value:w #1 _prop } { - \ebproof_set_mark:Nnn #1 { ##1 } { ##2 + #2 } - } -} - -% Move the left and right marks of the first tree so that they are at least as -% far from the axis as they are in the second tree. For instance if the marks -% are set as -% 1: L---A-------R -% 2: L-------A---R -% then the marks of the first tree are then set as -% 1: L-------A-------R -% The contents of the tree are unchanged. - -\cs_new:Nn \ebproof_enlarge_conclusion:NN { - \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis} - + \ebproof_mark:Nn #2 {left} - \ebproof_mark:Nn #2 {axis} } - \dim_compare:nNnT { \l_tmpa_dim } < { \ebproof_mark:Nn #1 {left} } { - \ebproof_set_mark:Nnn #1 {left} { \l_tmpa_dim } } - \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis} - + \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {axis} } - \dim_compare:nNnT { \l_tmpa_dim } > { \ebproof_mark:Nn #1 {right} } { - \ebproof_set_mark:Nnn #1 {right} { \l_tmpa_dim } } -} - - -%%% Building blocks - -% Make a tree with explicit material in horizontal mode. Set the left and -% right marks to extremal positions and set the axis in the middle. - -\cs_new:Nn \ebproof_make_simple:Nn { - \hbox_set:Nn #1 { #2 } - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 / 2 } - \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 } -} - -% Make a tree with explicit material in horizontal mode, split in two parts. -% Set the left and right marks to extremal positions and set the axis between -% the two parts. - -\cs_new:Nn \ebproof_make_split:Nnn { - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \hbox_set:Nn #1 { #2 } - \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 } - \hbox_set:Nn #1 { \hbox_unpack:N #1 #3 } - \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 } -} - -% Make a tree with explicit material in vertical mode, using an explicit width -% and axis. - -\cs_new:Nn \ebproof_make_vertical:Nnnn { - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \ebproof_set_mark:Nnn #1 { axis } { #2 } - \ebproof_set_mark:Nnn #1 { right } { #3 } - \vbox_set:Nn #1 { - \dim_set:Nn \tex_hsize:D { \ebproof_mark:Nn #1 {right} } - #4 - } - \box_set_wd:Nn #1 { \ebproof_mark:Nn #1 {right} } -} - -%%% Assembling boxes - -% Extend a tree box. The marks are shifted so that alignment is preserved. The -% arguments are dimensions for the left, top, right and bottom sides -% respectively. - -\cs_new:Nn \ebproof_extend:Nnnnn { - \dim_compare:nNnF { #2 } = { 0pt } { - \hbox_set:Nn #1 { - \skip_horizontal:n { #2 } - \box_use:N #1 - } - \ebproof_shift_x:Nn #1 { #2 } - } - \box_set_ht:Nn #1 { \box_ht:N #1 + #3 } - \box_set_wd:Nn #1 { \box_wd:N #1 + #4 } - \box_set_dp:Nn #1 { \box_dp:N #1 + #5 } -} - -% Append the contents of the second tree to the first one on the right, with -% matching baselines. The marks of both trees are preserved. The middle -% argument specifies the space to insert between boxes. - -\cs_new:Nn \ebproof_append_right:NnN { - \hbox_set:Nn #1 { - \box_use:N #1 - \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } - \box_use:N #3 - } -} - -% Append the contents of the second tree to the first one on the left, with -% matching baselines. The marks of the first tree are shifted accordingly. The -% middle argument specifies the space to insert between boxes. - -\cs_new:Nn \ebproof_append_left:NnN { - \ebproof_shift_x:Nn #1 { \box_wd:N #3 + #2 } - \hbox_set:Nn #1 { - \box_use:N #3 - \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } - \box_use:N #1 - } -} - -% Shift of two trees to the right so that the axes match. The marks of the one -% that is shifted are updated accordingly. - -\cs_new:Nn \ebproof_align:NN { - \dim_set:Nn \l_tmpa_dim - { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #1 {axis} } - \dim_compare:nNnTF \l_tmpa_dim < { 0pt } { - \ebproof_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt } - } { - \ebproof_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt } - } -} - -% Append the contents of the second tree above the first one, with matching -% axes. The marks of the first tree are preserved. - -\cs_new:Nn \ebproof_append_above:NN { - \ebproof_align:NN #1 #2 - \vbox_set:Nn #1 { - \box_use:N #2 - \tex_prevdepth:D -1000pt - \box_use:N #1 - } -} - -% Append the contents of the second tree below the first one, with matching -% axes. The marks of the first tree are preserved. - -\cs_new:Nn \ebproof_append_below:NN { - \ebproof_align:NN #1 #2 - \vbox_set_top:Nn #1 { - \box_use:N #1 - \tex_prevdepth:D -1000pt - \box_use:N #2 - } -} - -% Shift the material in a tree vertically so that the height and depth are -% equal (like TeX's \vcenter but around the baseline). - -\cs_new:Nn \ebproof_vcenter:N { - \dim_set:Nn \l_tmpa_dim { ( \box_ht:N #1 - \box_dp:N #1 ) / 2 } - \box_set_eq:NN \l_tmpa_box #1 - \hbox_set:Nn #1 - { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } } -} - - -%% Making inferences -% -% The following commands use the parameters defined at the beginning of the -% package for actually building proof trees using the commands defined above. - -% Append the contents of the second tree above or below the first one, -% depending on current settings. Axes are aligned and the marks of the first -% tree are preserved. - -\cs_new:Nn \ebproof_append_vertical:NN { - \bool_if:NTF \l_ebproof_updown_bool - { \ebproof_append_below:NN #1 #2 } - { \ebproof_append_above:NN #1 #2 } -} - -% Make a box containing an inference rule with labels, using the current -% settings. The width and axis position are taken as those of the conclusion -% of another tree box. The third argument is used as a temporary register for -% building labels. - -\cs_new:Nn \ebproof_make_rule_for:NNN { - - % Build the rule. - - \ebproof_make_vertical:Nnnn #1 - { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #2 {left} } - { \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {left} } - { - \skip_vertical:N \l_ebproof_rule_margin_dim - \tl_if_empty:NF { \l_ebproof_rule_code_tl } { - \tl_use:N \l_ebproof_rule_code_tl - \skip_vertical:N \l_ebproof_rule_margin_dim - } - } - \ebproof_vcenter:N #1 - - % Append the left label - - \tl_if_blank:VF \l_ebproof_left_label_tl { - \ebproof_make_simple:Nn #3 { - \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n { - \cs_set_eq:NN \inserttext \l_ebproof_left_label_tl - \tl_use:N \l_ebproof_left_label_template_tl - } } - } - \box_set_ht:Nn #3 { 0pt } - \box_set_dp:Nn #3 { 0pt } - \ebproof_append_left:NnN - \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box - } - - % Append the right label - - \tl_if_blank:VF \l_ebproof_right_label_tl { - \ebproof_make_simple:Nn #3 { - \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n { - \cs_set_eq:NN \inserttext \l_ebproof_right_label_tl - \tl_use:N \l_ebproof_right_label_template_tl - } } - } - \box_set_ht:Nn #3 { 0pt } - \box_set_dp:Nn #3 { 0pt } - \ebproof_append_right:NnN - \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box - } - -} - - -%% Stack-based interface - -%%% The stack - -% Logically, box structures are stored on a stack. However, TeX does not -% provide data structures for that and the grouping mechanism is not flexible -% enough, so we encode them using what we actually have. A stack for boxes is -% implemented using a global hbox |\g_ebproof_stack_box| that contains all the -% boxes successively. A sequence |\g_ebproof_stack_seq| is used to store the -% dimensions property lists textually. We maintain a counter -% |\g_ebproof_level_int| with the number of elements on the stack, for -% consistency checks. - -\int_new:N \g_ebproof_level_int -\box_new:N \g_ebproof_stack_box -\seq_new:N \g_ebproof_stack_seq - -% Clear the stack. - -\cs_new:Nn \ebproof_clear_stack: { - \int_gset:Nn \g_ebproof_level_int { 0 } - \hbox_gset:Nn \g_ebproof_stack_box { } - \seq_gclear:N \g_ebproof_stack_seq -} - -% Push the contents of a register on the stack. - -\cs_new:Nn \ebproof_push:N { - \int_gincr:N \g_ebproof_level_int - \hbox_gset:Nn \g_ebproof_stack_box - { \hbox_unpack:N \g_ebproof_stack_box \box_use:N #1 } - \seq_gput_left:Nv \g_ebproof_stack_seq - { l_ebproof_marks_ \__int_value:w #1 _prop } -} - -% Pop the value from the top of the stack into a register. - -\cs_new:Nn \ebproof_pop:N { - \int_compare:nNnTF { \g_ebproof_level_int } > { 0 } { - \int_gdecr:N \g_ebproof_level_int - \hbox_gset:Nn \g_ebproof_stack_box { - \hbox_unpack:N \g_ebproof_stack_box - \box_gset_to_last:N \g_tmpa_box - } - \box_set_eq_clear:NN #1 \g_tmpa_box - \seq_gpop_left:NN \g_ebproof_stack_seq \l_tmpa_tl - \tl_set_eq:cN { l_ebproof_marks_ \__int_value:w #1 _prop } \l_tmpa_tl - } { - \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{} - \ebproof_clear:N #1 - } -} - -%%% Assembling trees - -\ebproof_new:N \l_ebproof_a_box -\ebproof_new:N \l_ebproof_b_box -\ebproof_new:N \l_ebproof_c_box -\ebproof_new:N \l_ebproof_d_box - -% Join horizontally a number of elements at the top of the stack. If several -% trees are joined, use the left mark of the left tree, the right mark of the -% right tree and set the axis in the middle of these marks. - -\cs_new:Nn \ebproof_join_horizontal:n { - \int_case:nnF { #1 } { - { 0 } { - \group_begin: - \ebproof_clear:N \l_ebproof_a_box - \ebproof_push:N \l_ebproof_a_box - \group_end: - } - { 1 } { } - } { - \group_begin: - \ebproof_pop:N \l_ebproof_a_box - \prg_replicate:nn { #1 - 1 } { - \ebproof_pop:N \l_ebproof_b_box - \ebproof_append_left:NnN - \l_ebproof_a_box \l_ebproof_separation_dim \l_ebproof_b_box - } - \ebproof_set_mark:Nnn \l_ebproof_a_box { left } - { \ebproof_mark:Nn \l_ebproof_b_box { left } } - \ebproof_set_mark:Nnn \l_ebproof_a_box { axis } - { ( \ebproof_mark:Nn \l_ebproof_a_box { left } - + \ebproof_mark:Nn \l_ebproof_a_box { right } ) / 2 } - \ebproof_push:N \l_ebproof_a_box - \group_end: - } -} - -% Join vertically the two elements at the top of the stack, with a horizontal -% rule of the appropriate size. - -\cs_new:Nn \ebproof_join_vertical: { - \group_begin: - \ebproof_pop:N \l_ebproof_a_box - \ebproof_pop:N \l_ebproof_b_box - \ebproof_enlarge_conclusion:NN \l_ebproof_b_box \l_ebproof_a_box - \ebproof_make_rule_for:NNN \l_ebproof_c_box \l_ebproof_b_box - \l_ebproof_d_box - \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_c_box - \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_b_box - \ebproof_push:N \l_ebproof_a_box - \group_end: -} - -%%% High-level commands - -% Push a box with default formatting, using explicit alignment if the code -% contains a |&| character - -\cs_new:Npn \ebproof_statement_parse:w #1\ebproof_statement_stop: { - \tl_if_empty:nTF { #3 } { - \ebproof_make_simple:Nn \l_ebproof_a_box - { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_template_tl } - } { - \ebproof_make_split:Nnn \l_ebproof_a_box - { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_left_template_tl } - { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_ebproof_right_template_tl } - } - \ebproof_push:N \l_ebproof_a_box -} - -\cs_new:Nn \ebproof_push_statement:n { - \ebproof_statement_parse:w #1&& \ebproof_statement_stop: -} - - -%% Document interface - -%%% Functions to define statements - -% The |\g_ebproof_stack_seq| variable contains the list of all defined -% statements. For each statement |X|, there is a document command |\ebproofX| -% and the alias |\X| is defined when entering a |prooftree| environment. - -\seq_new:N \g_ebproof_statements_seq - -% Install the aliases for statements, saving the original value of the control -% sequences. - -\cs_new:Nn \ebproof_setup_statements: { - \seq_map_inline:Nn \g_ebproof_statements_seq { - \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 } - \cs_set_eq:cc { ##1 } { ebproof ##1 } - } -} - -% Restore the saved meanings of the control sequences. This is useful when -% interpreting user-provided code in statement arguments. The meanings are -% automatically restored when leaving a |prooftree| environment because of -% grouping. - -\cs_new:Nn \ebproof_restore_statements: { - \seq_map_inline:Nn \g_ebproof_statements_seq { - \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 } - } -} - -% Define a new statement. The first argument is the name, the second one is an -% argument specifier as used by |xparse| and the third one is the body of the -% command. - -\cs_new:Nn \ebproof_new_statement:nnn { - \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 } - \seq_put_right:Nn \g_ebproof_statements_seq { #1 } -} - -% Define a deprecated statement. The syntax is the same as above except that -% an extra argument in third position indicates what should be used instead. -% The effect is the same except that a warning message is issued the first -% time the statement is used. - -\cs_new:Nn \ebproof_new_deprecated_statement:nnnn { - \cs_new:cpn { ebproof_#1_warning: } { - \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 } - \cs_gset:cn { ebproof_#1_warning: } { } - } - \ebproof_new_statement:nnn { #1 } { #2 } - { \use:c { ebproof_#1_warning: } #4 } -} - - -%%% Basic commands - -\ebproof_new_statement:nnn { set } { m } { - \keys_set:nn { ebproof } { #1 } -} - -\ebproof_new_statement:nnn { hypo } { O{} m } { - \group_begin: - \ebproof_restore_statements: - \keys_set:nn { ebproof } { #1 } - \ebproof_push_statement:n { #2 } - \group_end: -} - -\ebproof_new_statement:nnn { infer } { O{} m O{} m } { - \group_begin: - \ebproof_restore_statements: - \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl - \keys_set:nV { ebproof } \l_tmpa_tl - \tl_set:Nn \l_ebproof_right_label_tl { #3 } - \ebproof_join_horizontal:n { #2 } - \ebproof_push_statement:n { #4 } - \ebproof_join_vertical: - \group_end: -} - -\ebproof_new_statement:nnn { ellipsis } { m m } { - \group_begin: - \ebproof_restore_statements: - \tl_clear:N \l_ebproof_rule_code_tl - \ebproof_make_split:Nnn \l_ebproof_a_box { } { - \vbox_set:Nn \l_tmpa_box { - \skip_vertical:n { 1.2ex } - \hbox:n { \tex_ignorespaces:D #1 } - \skip_vertical:n { 1.2ex } - } - \vbox_to_ht:nn { \box_ht:N \l_tmpa_box } { - \tex_xleaders:D \vbox_to_ht:nn { .8ex } - { \tex_vss:D \hbox:n { . } \tex_vss:D } - \tex_vfill:D - } - \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box } - } - \ebproof_push:N \l_ebproof_a_box - \ebproof_join_vertical: - \ebproof_push_statement:n {#2} - \ebproof_join_vertical: - \group_end: -} - - -%%% Modifying trees - -% Rewrite the box at the top of the stack while preserving its dimensions an -% marks. The code is typeset in horizontal mode, with control sequences to -% access the original box and its marks: -% - \treebox is a box register with the original material -% - \treemark{NAME} provides the value of a given mark - -\ebproof_new_statement:nnn { rewrite } { m } { - \group_begin: - \ebproof_restore_statements: - \ebproof_pop:N \l_ebproof_a_box - \box_set_eq:NN \l_tmpa_box \l_ebproof_a_box - \hbox_set:Nn \l_tmpb_box { - \cs_set_eq:NN \treebox \l_tmpa_box - \cs_set:Npn \treemark { \ebproof_mark:Nn \l_ebproof_a_box } - { #1 } - } - \box_set_wd:Nn \l_tmpb_box { \box_wd:N \l_ebproof_a_box } - \box_set_ht:Nn \l_tmpb_box { \box_ht:N \l_ebproof_a_box } - \box_set_dp:Nn \l_tmpb_box { \box_dp:N \l_ebproof_a_box } - \box_set_eq:NN \l_ebproof_a_box \l_tmpb_box - \ebproof_push:N \l_ebproof_a_box - \group_end: -} - -% Insert |\left| and |\right| delimiters without changing the alignment - -\ebproof_new_statement:nnn { delims } { m m } { - \group_begin: - \ebproof_restore_statements: - \ebproof_pop:N \l_ebproof_a_box - \hbox_set:Nn \l_tmpa_box - { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ } - \dim_set:Nn \l_tmpa_dim - { \box_ht:N \l_tmpa_box - \box_ht:N \l_ebproof_a_box } - \hbox_set:Nn \l_ebproof_a_box { - $ #1 \tex_vrule:D - height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt - \tex_right:D . $ - } - \ebproof_shift_x:Nn \l_ebproof_a_box { \box_wd:N \l_ebproof_a_box } - \hbox_set:Nn \l_ebproof_a_box { - \hbox_unpack:N \l_ebproof_a_box - $ \tex_left:D . \box_use:N \l_tmpa_box #2 $ - } - \hbox_set:Nn \l_ebproof_a_box - { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_ebproof_a_box } } - \ebproof_push:N \l_ebproof_a_box - \group_end: -} - - -%%% Deprecated statements - -% These statements were defined in versions 1.x of the package, they are -% preserved for temporary upwards compatibility and will be removed in a -% future version. - -\ebproof_new_deprecated_statement:nnnn { Alter } { m } - { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } } -\ebproof_new_deprecated_statement:nnnn { Delims } { } - { use~\token_to_str:c{delims}~instead } { \ebproofdelims } -\ebproof_new_deprecated_statement:nnnn { Ellipsis } { } - { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis } -\ebproof_new_deprecated_statement:nnnn { Hypo } { } - { use~\token_to_str:c{hypo}~instead } { \ebproofhypo } -\ebproof_new_deprecated_statement:nnnn { Infer } { } - { use~\token_to_str:c{infer}~instead } { \ebproofinfer } - - -%%% Environment interface - -\ebproof_clear_stack: - -\tl_new:N \l_ebproof_start_level_tl - -\NewDocumentEnvironment { prooftree } { s O{} } { - \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl - \keys_set:nV { ebproof } \l_tmpa_tl - \tl_set:Nx \l_ebproof_start_level_tl { \int_use:N \g_ebproof_level_int } - \vbox_set:Nw \l_tmpa_box - \ebproof_setup_statements: -} { - \vbox_set_end: - \ebproof_pop:N \l_ebproof_a_box - \int_compare:nNnF { \g_ebproof_level_int } = { \tl_use:N \l_ebproof_start_level_tl } { - \PackageError{ebproof}{Malformed~proof~tree}{ - Some~hypotheses~were~declared~but~not~used~in~this~tree.} - } - \IfBooleanTF { #1 } { - \[ \box_use:N \l_ebproof_a_box \] - \ignorespacesafterend - } { - \hbox_unpack:N \c_empty_box - \bool_if:NTF \l_ebproof_center_bool { - \hbox:n { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ } - } { - \box_use:N \l_ebproof_a_box - } - } -} - -% A trick for the starred version: -\cs_new:cpn { prooftree* } { \prooftree* } -\cs_new:cpn { endprooftree* } { \endprooftree } diff --git a/macros/latex/contrib/ebproof/ebproof.tex b/macros/latex/contrib/ebproof/ebproof.tex deleted file mode 100644 index eeb93e5cdf..0000000000 --- a/macros/latex/contrib/ebproof/ebproof.tex +++ /dev/null @@ -1,638 +0,0 @@ -%% ebproof.sty -%% Copyright 2017 Emmanuel Beffara -% -% This work may be distributed and/or modified under the -% conditions of the LaTeX Project Public License, either version 1.3 -% of this license or (at your option) any later version. -% The latest version of this license is in -% http://www.latex-project.org/lppl.txt -% and version 1.3 or later is part of all distributions of LaTeX -% version 2005/12/01 or later. -% -% This work has the LPPL maintenance status `maintained'. -% -% The Current Maintainer of this work is Emmanuel Beffara. -% -% This work consists of the files ebproof.sty and ebproof.tex. - -\documentclass{article} - -\DeclareRobustCommand\package[1]{\texttt{#1}} - -\title{The \package{ebproof} package} -\author{Emmanuel Beffara \\ \url{manu@beffara.org}} -\date{Version 2.0 \\ March 17, 2017} - -\usepackage{amssymb} -\usepackage{color} -\usepackage{fancyvrb} -\usepackage[a4paper]{geometry} -\usepackage[colorlinks=true,urlcolor=blue]{hyperref} -\usepackage{multicol} - -\usepackage{tikz} -\usetikzlibrary{decorations.pathmorphing} - -\usepackage{ebproof} - -\newcommand\lit[1]{\texttt{#1}} -\newcommand\cs[1]{\lit{\char`\\#1}} -\newcommand\env[1]{\lit{#1}} -\newcommand\opt[1]{\lit{#1}} -\newcommand\meta[1]{$\langle$\textit{#1}$\rangle$} -\newcommand\oarg[1]{\lit[\meta{#1}\lit]} -\newcommand\marg[1]{\lit{\{}\meta{#1}\lit{\}}} - -\newenvironment{csdoc}[1]{% - \smallbreak\noindent{#1}% - \begin{list}{}{% - \topsep=1ex% - }% - \item -}{% - \end{list}% -} - -\newenvironment{example}[1]{% - \def\exampleoptions{#1}% - \VerbatimOut{example.tex}}{% - \endVerbatimOut - \begin{center} - \begin{minipage}{.4\textwidth} - \input{example.tex} - \end{minipage}% - \begin{minipage}{.6\textwidth} - \small - \expandafter\VerbatimInput\expandafter[\exampleoptions]{example.tex} - \end{minipage}% - \end{center} -} - -\setcounter{tocdepth}{2} - -\begin{document} -\maketitle - -\begin{multicols}{2} - \tableofcontents -\end{multicols} - -\section{Introduction} - -The \env{ebproof} package provides commands to typeset proof trees, in the -style of sequent calculus and related systems: - -\begin{example}{gobble=2} - \begin{prooftree} - \hypo{ \Gamma, A &\vdash B } - \infer1[abs]{ \Gamma &\vdash A\to B } - \hypo{ \Gamma \vdash A } - \infer2[app]{ \Gamma \vdash B } - \end{prooftree} -\end{example} - -The structure is very much inspired by the -\href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\package{bussproofs}} -package, in particular for the postfix notation. -I actually wrote \package{ebproof} because there were some limitations in -\package{bussproofs} that I did not know how to lift, and also because I did -not like some choices in that package (and also because it was fun to write). - -\section{Environments} - -The package provides the \env{prooftree} environment, in a standard and -starred variants. - -\begin{csdoc}{ - \cs{begin}\lit{\{prooftree\}}\oarg{options} - \meta{statements} - \cs{end}\lit{\{prooftree\}}} - Typeset the proof tree described by the \meta{statements}, as described in - section~\ref{sec:statements}. - The \meta{options} provide default formatting options for the proof tree. - This environment can be used either in math mode or in text mode. - It produces a proof tree at the current position in the text flow. -\end{csdoc} - -\begin{csdoc}{ - \cs{begin}\lit{\{prooftree*\}}\oarg{options} - \meta{statements} - \cs{end}\lit{\{prooftree*\}}} - Typeset the proof on a line of its own; it is essentially equivalent to - wrapping the \env{prooftree} environment inside a displayed math - environment. -\end{csdoc} - -\noindent -The starred version is used in situations when a single proof will be -displayed. -The non-starred version is useful in order to integrate the proof into some -larger structure, like two parts of a formula: - -\begin{example}{gobble=2} - \[ - \begin{prooftree} - \infer0{ \vdash A } - \hypo{ \vdash B } \infer1{ \vdash B, C } - \infer2{ \vdash A\wedge B, C } - \end{prooftree} - \quad \rightsquigarrow \quad - \begin{prooftree} - \infer0{ \vdash A } \hypo{ \vdash B } - \infer2{ \vdash A\wedge B } - \infer1{ \vdash A\wedge B, C } - \end{prooftree} - \] -\end{example} - -\section{Statements} -\label{sec:statements} - -Statements describe proofs in postfix notation: when typesetting a proof tree -whose last rule has, say, two premisses, you will first write statements for -the subtree of the first premiss, then statements for the subtree of the -second premiss, then a statement like \cs{infer2}\{\meta{conclusion}\} to -build an inference with these two subtrees as premisses and the given text as -conclusion. - -Hence statements operate on a stack of proof trees. -At the beginning of a \lit{prooftree} environment, the stack is empty. -At the end, it must contain exactly one tree, which is the one that will be -printed. - -Note that the commands defined in this section only exist right inside -\env{prooftree} environments. -If you have a macro with the same name as one of the statements, for instance -\cs{hypo}, then this macro will keep its meaning outside \env{prooftree} -environments as well as inside the arguments of a statement. -If you really need to access the statements in another context, you can can -always call them by prefixing their names with \lit{ebproof}, for instance as -\cs{ebproofhypo}. - -\subsection{Basic statements} - -The basic statements for building proofs are the following, where -\meta{options} stands for arbitrary options as described in -section~\ref{sec:options}. -\begin{csdoc}{\cs{hypo}\oarg{options}\marg{text}} - Push a new proof tree consisting only in one conclusion line, with no - premiss and no line above, in other words a tree with only a leaf - (\cs{hypo} stands for \emph{hypothesis}). -\end{csdoc} -\begin{csdoc}{\cs{infer}\oarg{options}\marg{arity}\oarg{label}\marg{text}} - Build an inference step by taking some proof trees from the top of the - stack, assembling them with a rule joining their conclusions and putting a - new conclusion below. - The \meta{arity} is the number of sub-proofs, it may be any number - including 0 (in this case there will be a line above the conclusion but no - sub-proof). - If \meta{label} is present, it is used as the label on the right of the - inference line; it is equivalent to using the \opt{right label} option. -\end{csdoc} - -The \meta{text} in these statements is the contents of the conclusion at the -root of the tree that the statements create. -It is typeset in math mode by default but any kind of formatting can be used -instead, using the \opt{template} option. -The \meta{label} text is formatted in horizontal text mode by default. - -Each proof tree has a vertical axis, used for alignment of successive steps. -The position of the axis is deduced from the text of the conclusion at the -root of the tree: if \meta{text} contains the alignment character \verb|&| -then the axis is set at that position, otherwise the axis is set at the center -of the conclusion text. -The \cs{infer} statement makes sure that the axis of the premiss is at the -same position as the axis of the conclusion. -If there are several premisses, it places the axis at the center between the -left of the leftmost conclusion and the right of the rightmost conclusion: - -\begin{example}{gobble=2} - \begin{prooftree} - \hypo{ &\vdash A, B, C } - \infer1{ A &\vdash B, C } - \infer1{ A, B &\vdash C } - \hypo{ D &\vdash E } - \infer2{ A, B, D &\vdash C, E } - \infer1{ A, B &\vdash C, D, E } - \infer1{ A &\vdash B, C, D, E } - \end{prooftree} -\end{example} - -\begin{csdoc}{\cs{ellipsis}\marg{label}\marg{text}} - Typeset vertical dots, with a label on the right, and a new conclusion. - No inference lines are inserted. - \begin{example}{gobble=4} - \begin{prooftree} - \hypo{ \Gamma &\vdash A } - \ellipsis{foo}{ \Gamma &\vdash A, B } - \end{prooftree} - \end{example} -\end{csdoc} - - -\subsection{Modifying proof trees} - -The following additional statements may be used to affect the format of the -last proof tree on the stack: - -\begin{csdoc}{\cs{rewrite}\marg{code}} - Rewrite the proof while preserving its size and alignment. The \meta{code} - is typeset in horizontal mode, with the following control sequences defined: - \begin{itemize} - \item \cs{treebox} is a box register that contains the original material, - \item \cs{treemark}\marg{name} expands as the position of a given mark with - respect to the left of the box. - \end{itemize} - A simple use of this statement is to change the color of a proof tree: - \begin{example}{gobble=4} - \begin{prooftree} - \hypo{ \Gamma, A &\vdash B } - \infer1[abs]{ \Gamma &\vdash A\to B } - \rewrite{\color{red}\box\treebox} - \hypo{ \Gamma \vdash A } - \infer2[app]{ \Gamma \vdash B } - \end{prooftree} - \end{example} - Note the absence of spaces inside the call to \cs{rewrite}, because spaces - would affect the position of the tree box. - Note also that explicit use of \cs{treebox} is required to actually draw the - subtree. - Not using it will effectively not render the subtree, while still reserving - its space in the enclosing tree: - \begin{example}{gobble=4} - \begin{prooftree} - \hypo{ \Gamma, A &\vdash B } - \infer1[abs]{ \Gamma &\vdash A\to B } - \rewrite{} - \hypo{ \Gamma \vdash A } - \infer2[app]{ \Gamma \vdash B } - \end{prooftree} - \end{example} - This kind of manipulation is useful for instance in conjunction with the - \package{beamer} package to allow revealing subtrees of a proof tree - progressively in successive slides of a given frame. -\end{csdoc} - -\begin{csdoc}{\cs{delims}\marg{left}\marg{right}} - Put left and right delimiters around the whole sub-proof, without changing - the alignment (the spacing is affected by the delimiters, however). - The \meta{left} text must contain an opening occurrence of \cs{left} and the - \meta{right} text must contain a matching occurrence of \cs{right}. - For instance, \verb|\delims{\left(}{\right)}| will put the - sub-proof between parentheses. - \begin{example}{gobble=4} - \begin{prooftree} - \hypo{ A_1 \vee \cdots \vee A_n } - \hypo{ [A_i] } - \ellipsis{}{ B } - \delims{ \left( }{ \right)_{1\leq i\leq n} } - \infer2{ B } - \end{prooftree} - \end{example} -\end{csdoc} - -\section{Options} -\label{sec:options} - -The formatting of trees, conclusion texts and inference rules is affected by -options, specified using the \LaTeX3 key-value system. -All options are in the \lit{ebproof} module in the key tree. -They can be set locally for a proof tree or for a single statement using -optional arguments in the associated commands. - -\begin{csdoc}{\cs{ebproofset}\marg{options}} - Set some options. - The options will apply in the current scope; using this in preamble will - effectively set options globally. - Specific options may also be specified for each proof tree and for each - statement in a proof tree, using optional arguments. -\end{csdoc} - -\subsection{General shape} - -The options in this section only make sense at the global level and at the -proof level. -Changing the proof style inside a \lit{proof} environment has undefined -behaviour. - -\begin{csdoc}{\opt{proof style=}\meta{name}} - Set the general shape for representing proofs. - The following styles are provided: - \begin{csdoc}{\lit{upwards}} - This is the default style. - Proof trees grow upwards, with conclusions below and premisses above. - \end{csdoc} - \begin{csdoc}{\lit{downwards}} - Proof trees grow downwards, with conclusions above and premisses below. - \begin{example}{gobble=4} - \begin{prooftree}[proof style=downwards] - \hypo{ \Gamma, A &\vdash B } - \infer1[abs]{ \Gamma &\vdash A\to B } - \hypo{ \Gamma \vdash A } - \infer2[app]{ \Gamma \vdash B } - \end{prooftree} - \end{example} - \end{csdoc} -\end{csdoc} - -In the optional argument of \lit{prooftree} environments, proof styles can -be specified directly, without prefixing the name by ``\lit{proof style=}''. -For instance, the first line of the example above could be written -\cs{begin}\lit{\{prooftree\}[downwards]} equivalently. - -\begin{csdoc}{\opt{center=}\meta{boolean}} - If set to \lit{true}, the tree produced by the \env{prooftree} environment - will be vertically centered around the text line. - If set to \lit{false}, the base line of the tree will be the base line of - the conclusion. - The default value is \lit{true}. - \begin{example}{gobble=4} - \begin{prooftree}[center=false] - \infer0{ A \vdash A } - \end{prooftree} - \qquad - \begin{prooftree}[center=false] - \hypo{ \Gamma, A \vdash B } - \infer1{ \Gamma \vdash A \to B } - \end{prooftree} - \end{example} -\end{csdoc} - -\subsection{Spacing} - -\begin{csdoc}{\opt{separation=}\meta{dimension}} - The horizontal separation between sub-proofs in an inference. - The default value is \lit{1.5em}. - \begin{example}{gobble=4} - \begin{prooftree}[separation=0.5em] - \hypo{ A } \hypo{ B } \infer2{ C } - \hypo{ D } \hypo{ E } \hypo{ F } \infer3{ G } - \hypo{ H } \infer[separation=3em]3{ K } - \end{prooftree} - \end{example} -\end{csdoc} - -\begin{csdoc}{\opt{rule margin=}\meta{dimension}} - The spacing above and below inference lines. - The default value is \lit{0.7ex}. - \begin{example}{gobble=4} - \begin{prooftree}[rule margin=2ex] - \hypo{ \Gamma, A &\vdash B } - \infer1[abs]{ \Gamma &\vdash A\to B } - \hypo{ \Gamma \vdash A } - \infer2[app]{ \Gamma \vdash B } - \end{prooftree} - \end{example} -\end{csdoc} - -\subsection{Shape of inference lines} - -\begin{csdoc}{\opt{rule style=}\meta{name}} - Set the shape of inference lines. - The following values are provided: - \begin{csdoc}{\opt{simple}} - A simple horizontal rule is drawn. - This is the default style. - \end{csdoc} - \begin{csdoc}{\opt{no rule}} - No inference line is drawn. - A single space of the length of \lit{rule margin} is inserted. - \end{csdoc} - \begin{csdoc}{\opt{double}} - A double line is drawn. - \end{csdoc} - \begin{csdoc}{\opt{dashed}} - A single dashed line is drawn. - \end{csdoc} - The precise rendering is influenced by parameters specified below. - Arbitrary new shapes can defined using the \lit{rule code} option described - below and the \cs{ebproofnewrulestyle} command described in - section~\ref{sec:styles}. -\end{csdoc} - -In the optional argument of the \cs{infer} statement, rule styles can be -specified directly, without prefixing the style name by ``\lit{rule style=}''. -For instance, \cs{infer}\lit{[dashed]} is equivalent to -\cs{infer}\lit{[rule style=dashed]}. - -\begin{example}{gobble=2} - \begin{prooftree} - \hypo{ \Gamma &\vdash A \to B } - \infer[no rule]1{ \Gamma &\vdash {!A} \multimap B } - \hypo{ \Delta &\vdash A } - \infer[rule thickness=2pt]1{ \Delta &\vdash {!A} } - \infer0{ B \vdash B } - \infer[dashed]2{ \Delta, {!A}\multimap B \vdash B } - \infer2{ \Gamma, \Delta &\vdash B } - \infer[double]1{ \Gamma \cup \Delta &\vdash B } - \end{prooftree} -\end{example} - -\begin{csdoc}{\opt{rule thickness=}\meta{dimension}} - The thickness of inference lines. - It is \lit{0.4pt} by default. -\end{csdoc} -\begin{csdoc}{\opt{rule separation=}\meta{dimension}} - The distance between the two lines in the \lit{double} rule style. - It is \lit{2pt} by default. -\end{csdoc} -\begin{csdoc}{\opt{rule dash length=}\meta{dimension}} - The length of dashes in the \lit{dashed} rule style. - It is \lit{0.2em} by default. -\end{csdoc} -\begin{csdoc}{\opt{rule dash space=}\meta{dimension}} - The space between dashes in the \lit{dashed} rule style. - It is \lit{0.3em} by default. -\end{csdoc} - -\begin{csdoc}{\opt{rule code=}\meta{code}} - This option is used to define an arbitrary shape for rules. - The \meta{code} is used to render the rule, it is executed in vertical mode - in a \cs{vbox} whose \cs{hsize} is set to the width of the rule. - Margins above and below are inserted automatically (they can be removed by - setting \lit{rule margin} to \lit{0pt}). - - \begin{example}{gobble=4} - \begin{prooftree}[rule code={\hbox{\tikz - \draw[decorate,decoration={snake,amplitude=.3ex}] - (0,0) -- (\hsize,0);}}] - \hypo{ \Gamma &\vdash A } - \infer1{ \Gamma &\vdash A, \ldots, A } - \hypo{ \Delta, A, \ldots, A \vdash \Theta } - \infer2{ \Gamma, \Delta \vdash \Theta } - \end{prooftree} - \end{example} - Note that this example requires the \package{tikz} package, with the - \package{decorations.pathmorphing} library for the \lit{snake} decoration. -\end{csdoc} - -\subsection{Format of conclusions} - -\begin{csdoc}{% - \opt{template=}\meta{code} \\ - \opt{left template=}\meta{code} \\ - \opt{right template=}\meta{code}} - Defines how conclusions are formatted. - The code is arbitrary \TeX\ code, composed in horizontal mode. - The macro \cs{inserttext} is used to insert the actual text passed to the - \cs{hypo} and \cs{infer} statements. - The \opt{template} value is used for conclusions with no alignment mark. - The \opt{left template} and \opt{right template} values are used on the left - and right side of the alignment mark when it is present. - The default value for \opt{template} is simply \verb|$\inserttext$|, so that - conclusions are set in math mode. - The default values for \opt{left template} and \opt{right template} are - similar, with spacing assuming that a relation symbol is put near the - alignment mark, so that \verb|\infer1{A &\vdash B}| is spaced correctly. - - \begin{example}{gobble=4} - \begin{prooftree}[template=(\textbf\inserttext)] - \hypo{ foo } - \hypo{ bar } - \infer1{ baz } - \infer2{ quux } - \end{prooftree} - \end{example} -\end{csdoc} - -\subsection{Format of labels} - -\begin{csdoc}{% - \opt{left label=}\meta{text} \\ - \opt{right label=}\meta{text}} - The text to use as the labels of the rules, on the left and on the right - of the inference line. - Using the second optional argument in \cs{infer} is equivalent to setting - the \env{right label} option with the value of that argument. - - \begin{example}{gobble=4} - \begin{prooftree} - \hypo{ \Gamma, A &\vdash B } - \infer[left label=$\lambda$]1[abs] - { \Gamma &\vdash A\to B } - \hypo{ \Gamma \vdash A } - \infer[left label=@]2[app]{ \Gamma \vdash B } - \end{prooftree} - \end{example} -\end{csdoc} -\begin{csdoc}{% - \opt{left label template=}\meta{code} \\ - \opt{right label template=}\meta{code}} - Defines how rule labels are formatted. - The code is arbitrary \TeX\ code, composed in horizontal mode. - The macro \cs{inserttext} can be used to insert the actual label text, as - defined by the options above. - The default values are simply \cs{inserttext} so that labels are set in - plain text mode. -\end{csdoc} - -\begin{csdoc}{\opt{label separation=}\meta{dimension}} - The spacing between an inference lines and its labels. - The default value is \lit{0.5em}. -\end{csdoc} -\begin{csdoc}{\opt{label axis=}\meta{dimension}} - The height of the horizontal axis used for aligning the labels with the - rules. The default value is \lit{0.5ex}. -\end{csdoc} - - -\subsection{Style macros} -\label{sec:styles} - -The following commands allow for the definition of custom styles using the -basic style options, in a way similar to PGF's ``styles'' and \LaTeX3's -``meta-keys''. -This allows setting a bunch of options with the same values in many proofs -using a single definition. - -\begin{csdoc}{\cs{ebproofnewstyle}\marg{name}\marg{options}} - Define a new style option \meta{name} that sets the given \meta{options}. - - For instance, the following code defines a new option \opt{small} that sets - various parameters so that proofs are rendered smaller. - \begin{example}{gobble=4} - \ebproofnewstyle{small}{ - separation = 1em, rule margin = .5ex, - template = \footnotesize$\inserttext$ } - \begin{prooftree}[small] - \hypo{ \Gamma, A \vdash B } - \infer1{ \Gamma \vdash A\to B } - \hypo{ \Gamma \vdash A } \infer2{ \Gamma \vdash B } - \end{prooftree} - \end{example} -\end{csdoc} - -\begin{csdoc}{\cs{ebproofnewrulestyle}\marg{name}\marg{options}} - Define a new rule style. - The \meta{options} part includes options used to set how to draw rules in - the new style. - - The option \opt{rule code} is useful in this command as it allows to - define arbitrary rule styles. - For instance, the squiggly rule example above could be turned into a new - rule style \lit{zigzag} with the following code: - \begin{example}{gobble=4} - \ebproofnewrulestyle{zigzag}{ - rule code = {\hbox{\tikz - \draw[decorate,decoration={snake,amplitude=.3ex}] - (0,0) -- (\hsize,0);}}} - \begin{prooftree} - \hypo{ \Gamma &\vdash A } - \infer1{ \Gamma &\vdash A, \ldots, A } - \hypo{ \Delta, A, \ldots, A \vdash \Theta } - \infer[zigzag]2{ \Gamma, \Delta \vdash \Theta } - \end{prooftree} - \end{example} -\end{csdoc} - - -\section{License} - -This work may be distributed and/or modified under the -conditions of the \LaTeX\ Project Public License, either version 1.3 -of this license or (at your option) any later version. -The latest version of this license is in -\begin{center} - \url{http://www.latex-project.org/lppl.txt} -\end{center} -and version 1.3 or later is part of all distributions of \LaTeX\ -version 2005/12/01 or later. - -This work has the LPPL maintenance status `maintained'. - -The Current Maintainer of this work is Emmanuel Beffara. - -This work consists of the files \texttt{ebproof.sty} and \texttt{ebproof.tex}. - - -\section{History} - -This section lists the principal evolutions of the package, in reverse -chronological order. -\begin{description} -\item[Version 2.0] - A complete rewrite of the code using the \LaTeX3 programming environment. - The incompatible changes from the user's point of view are the following: - \begin{itemize} - \item Proof statements are now writtten in lowercase ({i.e.} \cs{Infer} is - now written \cs{infer} etc.) but the syntax is otherwise unchanged. - The old uppercase commands still work but produce a deprecation warning, - they will be removed in a future version. - \item New styles are now defined using \cs{ebproofnewstyle} and - \cs{ebproofnewrulestyle}. The previous method using PGF styles does not - work anymore (because PGF is not used anymore). - \end{itemize} - The new commands and options are the following: - \begin{itemize} - \item The statement \cs{rewrite} generalizes \cs{Alter}, - \item The option \opt{label axis} controls vertical alignment of labels. - \end{itemize} -\item[Version 1.1] - A bugfix release. - In \opt{template} options, one now uses \cs{inserttext} instead of \lit{\#1} - for the text arguments, which improves robustness. -\item[Version 1.0] - The first public release. -\end{description} - -\end{document} -- cgit v1.2.3