ebproof (3feb15)

git-svn-id: svn://tug.org/texlive/trunk@36202 c570f23f-e606-0410-a88d-b1316a301751

3 files changed, 509 insertions, 0 deletions

diff --git a/Master/texmf-dist/doc/latex/ebproof/README b/Master/texmf-dist/doc/latex/ebproof/README
new file mode 100644
index 00000000000..a64bac6f41f
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/ebproof/README
@@ -0,0 +1,16 @@
+The ebproofs package provides commands to typeset proof trees, in the style of
+sequent calculus and related systems. The commands allow for writing
+inferences with any number of premisses and alignment of successive formulas
+on an arbitrary point. Various options allow complete control over spacing,
+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
+
+The package requires pgfkeys (from TikZ/PGF) for the option system.
+
+This package is written by Emmanuel Beffara <manu@beffara.org>
+It is subject to the LaTeX Project Public License.
diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf
new file mode 100644
index 00000000000..e58d9616168
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf
diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.tex b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex
new file mode 100644
index 00000000000..acb05d56759
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex
@@ -0,0 +1,493 @@
+\documentclass{article}
+
+\DeclareRobustCommand\package[1]{\texttt{#1}}
+
+\title{The \package{ebproof} package}
+\author{Emmanuel Beffara \\ \url{manu@beffara.org}}
+\date{Version 1.0 \\ February 3, 2015}
+
+\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 desribed 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 centered on a line of its own; it is essentially
+  equivalent to wrapping the \env{prooftree} environment inside a \env{center}
+  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}
+      \Hypo{ \vdash A }
+      \Hypo{ \vdash B } \Infer1{ \vdash B, C }
+      \Infer2{ \vdash A\wedge B, C }
+    \end{prooftree}
+    \quad \rightsquigarrow \quad
+    \begin{prooftree}
+      \Hypo{ \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 describes 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.
+
+\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}
+
+\subsection{Additional statements}
+
+The following additional statements may be used to affect the format of the
+last proof tree on the stack:
+
+\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}
+
+\begin{csdoc}{\cs{Alter}\marg{code}}
+  Modify the proof with arbitrary commands, assuming that these commands do
+  not affect the size.
+  The \meta{code} is executed in an \cs{hbox} and is followed by the insertion
+  of the actual box with the current sub-proof.
+  It is mostly useful with \cs{color} commands:
+  \begin{example}{gobble=4}
+    \begin{prooftree}
+      \Hypo{ \Gamma, A &\vdash B }
+      \Infer1[abs]{ \Gamma &\vdash A\to B }
+      \Alter{\color{red}}
+      \Hypo{ \Gamma \vdash A }
+      \Infer2[app]{ \Gamma \vdash B }
+    \end{prooftree}
+  \end{example}
+\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, specfied using the key-value system of PGF/TikZ, provided by the
+\package{pgfkeys} package.
+All options are in the \lit{/ebproof/} path in the key tree of
+\package{pgfkeys}.
+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
+  afterwards.
+\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}
+
+The option \opt{rule code} is particularly useful in a ``styles'' in the sense of
+\package{pgfkeys} as it allows to define new rule styles.
+The allowed values for \opt{rule style} are actually defined this way.
+The above example could be turned into a new rule style \lit{zigzag} with the
+following command:
+\begin{example}{gobble=2}
+  \ebproofset{
+    rule style/zigzag/.style={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}
+
+\subsection{Format of conclusions}
+
+\begin{csdoc}{%
+    \opt{template=}\meta{macro} \\
+    \opt{left template=}\meta{macro} \\
+    \opt{right template=}\meta{macro}}
+  Defines how conclusions are formatted.
+  The macros are arbitrary \TeX\ code, composed in horizontal mode, with the
+  macro argument \verb|#1| standing for 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|$#1$|, 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{#1})]
+      \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.
+\end{csdoc}
+\begin{csdoc}{%
+    \opt{left label template=}\meta{macro} \\
+    \opt{right label template=}\meta{macro}}
+  These macros are used to typeset the text of labels on the left and right of
+  inference lines.
+  The default values are \verb|#1| 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}
+
+
+\end{document}