![如何使用 ebproof 堆积假设](https://linux22.com/image/409019/%E5%A6%82%E4%BD%95%E4%BD%BF%E7%94%A8%20ebproof%20%E5%A0%86%E7%A7%AF%E5%81%87%E8%AE%BE.png)
使用ebproof.sty
包,可以编写推理规则如下
\begin{prooftree}
\hypo{A}
\hypo{B}
\hypo{C}
\infer3{D}
\end{prooftree}
获得以下内容:
A B C
___________________
D
在我的文档中,我的A
、B
和C
假设很长,所以我想把它们堆叠在推理规则之上,就像这样
A
B
C
_________
D
可以用 实现这样的排版吗ebproof
?
答案1
答案2
- 我已经扩展了 ebproof 包以包含以下扩展:ebproofx
您可以重新定义\infer
以接受逗号分隔的列表(可能是单例列表)以根据需要堆叠前提:
\documentclass{article}
\usepackage{ebproof}
\ExplSyntaxOn
\int_new:N \g__ebproof_sublevel_int
\box_new:N \g__ebproof_substack_box
\seq_new:N \g__ebproof_substack_seq
\cs_new:Nn \__ebproof_clear_substack:
{
\int_gset:Nn \g__ebproof_sublevel_int { 0 }
\hbox_gset:Nn \g__ebproof_substack_box { }
\seq_gclear:N \g__ebproof_substack_seq
}
\cs_new:Nn \__ebproof_subpush:N
{
\int_gincr:N \g__ebproof_sublevel_int
\hbox_gset:Nn \g__ebproof_substack_box
{ \hbox_unpack:N \g__ebproof_substack_box \box_use:c { \__ebproof_box:N #1 } }
\seq_gput_left:Nv \g__ebproof_substack_seq
{ \__ebproof_marks:N #1 }
}
\cs_new:Nn \__ebproof_subpop:N
{
\int_compare:nNnTF { \g__ebproof_sublevel_int } > { 0 }
{
\int_gdecr:N \g__ebproof_sublevel_int
\hbox_gset:Nn \g__ebproof_substack_box {
\hbox_unpack:N \g__ebproof_substack_box
\box_gset_to_last:N \g_tmpa_box
}
\box_set_eq_drop:cN { \__ebproof_box:N #1 } \g_tmpa_box
\seq_gpop_left:NN \g__ebproof_substack_seq \l_tmpa_tl
\tl_set_eq:cN { \__ebproof_marks:N #1 } \l_tmpa_tl
}
{ \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{} \__ebproof_clear:N #1 }
}
\cs_new:Nn \__ebproof_append_subvertical:NN
{
\bool_if:NTF \l__ebproof_updown_bool
{ \__ebproof_append_above:NN #1 #2 }
{ \__ebproof_append_below:NN #1 #2 }
}
\cs_new:Nn \__ebproof_join_subvertical:n
{
\group_begin:
\__ebproof_subpop:N \l__ebproof_a_box
\prg_replicate:nn { #1 - 1 }
{
\__ebproof_subpop:N \l__ebproof_b_box
\__ebproof_enlarge_conclusion:NN \l__ebproof_b_box \l__ebproof_a_box
\__ebproof_make_vertical:Nnnn \l__ebproof_c_box
{ \__ebproof_mark:Nn \l__ebproof_b_box {axis} - \__ebproof_mark:Nn \l__ebproof_b_box {left} }
{ \__ebproof_mark:Nn \l__ebproof_b_box {right} - \__ebproof_mark:Nn \l__ebproof_b_box {left} }
{ \skip_vertical:N \l__ebproof_rule_margin_dim }
\__ebproof_vcenter:N \l__ebproof_b_box
\__ebproof_append_subvertical:NN \l__ebproof_a_box \l__ebproof_c_box
\__ebproof_append_subvertical:NN \l__ebproof_a_box \l__ebproof_b_box
}
\__ebproof_push:N \l__ebproof_a_box
\group_end:
}
\cs_new:Nn \__ebproof_renew_statement:nnn
{
\exp_args:Nc \RenewDocumentCommand { ebproof#1 }{ #2 } { #3 }
\seq_gput_right:Nn \g__ebproof_statements_seq { #1 }
}
\cs_generate_variant:Nn \clist_map_inline:nn { xn }
\__ebproof_renew_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_clear_substack:
\clist_map_inline:xn { \clist_reverse:n { #2 } }
{
\__ebproof_join_horizontal:n { ##1 }
\__ebproof_pop:N \l__ebproof_a_box
\__ebproof_subpush:N \l__ebproof_a_box
}
\__ebproof_join_subvertical:n { \clist_count:n { #2 } }
\__ebproof_push_statement:n { #4 }
\__ebproof_join_vertical:
\group_end:
}
\ExplSyntaxOff
\begin{document}
\begin{prooftree*}
\hypo{\Gamma \vdash 1}
\hypo{\Gamma \vdash 2}
\hypo{\Gamma \vdash 3}
\hypo{\Gamma \vdash 4}
\infer{3,1}{a}
\hypo{\Gamma \vdash 5}
\hypo{\Gamma \vdash 6}
\hypo{\Gamma \vdash 7}
\hypo{\Gamma \vdash 8}
\hypo{\Gamma \vdash 9}
\infer{2,1,2}{b}
\hypo{\Gamma \vdash 10}
\infer3{c}
\end{prooftree*}
\end{document}
ebproof
使用全局堆栈来推送和弹出前提和结论。上面的代码定义了另一个堆栈来保存前提块,以垂直堆叠它们。其结构与ebproof
现有的几乎相同,并且据我所知与现有代码兼容。
警告:它使用私有的实现细节,因此将来可能会出现故障。