From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Mon, 2 Sep 2019 13:46:59 +0900 Subject: Initial commit --- macros/latex/contrib/ebproof/README.md | 42 ++ macros/latex/contrib/ebproof/ebproof.pdf | Bin 0 -> 227686 bytes macros/latex/contrib/ebproof/ebproof.sty | 767 +++++++++++++++++++++++++++++++ macros/latex/contrib/ebproof/ebproof.tex | 638 +++++++++++++++++++++++++ 4 files changed, 1447 insertions(+) create mode 100644 macros/latex/contrib/ebproof/README.md create mode 100644 macros/latex/contrib/ebproof/ebproof.pdf create mode 100644 macros/latex/contrib/ebproof/ebproof.sty create 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 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 + +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 + +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 Binary files /dev/null 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 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 + +% 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 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 +% +% 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