summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/ebproof
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/ebproof
Initial commit
Diffstat (limited to 'macros/latex/contrib/ebproof')
-rw-r--r--macros/latex/contrib/ebproof/README.md42
-rw-r--r--macros/latex/contrib/ebproof/ebproof.pdfbin0 -> 227686 bytes
-rw-r--r--macros/latex/contrib/ebproof/ebproof.sty767
-rw-r--r--macros/latex/contrib/ebproof/ebproof.tex638
4 files changed, 1447 insertions, 0 deletions
diff --git a/macros/latex/contrib/ebproof/README.md b/macros/latex/contrib/ebproof/README.md
new file mode 100644
index 0000000000..0f8b35038c
--- /dev/null
+++ b/macros/latex/contrib/ebproof/README.md
@@ -0,0 +1,42 @@
+The ebproof package
+===================
+
+A LaTeX package to typeset formal proofs in the style of sequent calculus.
+
+Presentation
+------------
+
+The `ebproof` 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 `expl3` (the LaTeX3 programming environment) which
+provides many useful programming tools.
+
+
+License
+-------
+
+Copyright 2015 Emmanuel Beffara <manu@beffara.org>
+
+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`.
diff --git a/macros/latex/contrib/ebproof/ebproof.pdf b/macros/latex/contrib/ebproof/ebproof.pdf
new file mode 100644
index 0000000000..e4c8d03b25
--- /dev/null
+++ b/macros/latex/contrib/ebproof/ebproof.pdf
Binary files differ
diff --git a/macros/latex/contrib/ebproof/ebproof.sty b/macros/latex/contrib/ebproof/ebproof.sty
new file mode 100644
index 0000000000..7601f8e9e8
--- /dev/null
+++ b/macros/latex/contrib/ebproof/ebproof.sty
@@ -0,0 +1,767 @@
+% The ebproof package - Formal proofs in the style of sequent calculus
+
+%% ebproof.sty
+%% Copyright 2017 Emmanuel Beffara <manu@beffara.org>
+
+% 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&#2&#3\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
new file mode 100644
index 0000000000..eeb93e5cdf
--- /dev/null
+++ b/macros/latex/contrib/ebproof/ebproof.tex
@@ -0,0 +1,638 @@
+%% ebproof.sty
+%% Copyright 2017 Emmanuel Beffara <manu@beffara.org>
+%
+% 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}