答案1
您可以吸收适当材料以表格形式输入并测量列宽。
\documentclass{article}
\usepackage{amsmath}
\usepackage{lipsum}
\ExplSyntaxOn
\NewDocumentEnvironment{formalproof}{b}
{
\begin{flushleft}
\linespread{1.2}\selectfont
\james_formalproof:n { #1 }
\end{flushleft}
}
{}
\seq_new:N \l__james_formalproof_body_seq
\seq_new:N \l__james_formalproof_tmp_seq
\dim_new:N \l__james_formalproof_left_dim
\dim_new:N \l__james_formalproof_right_dim
\dim_new:N \l__james_formalproof_step_dim
\int_new:N \l__james_formalproof_line_int
\cs_new_protected:Nn \james_formalproof:n
{
\seq_set_split:Nnn \l__james_formalproof_body_seq { \\ } { #1 }
% check for a trailing \\
\seq_pop_right:NN \l__james_formalproof_body_seq \l_tmpa_tl
\tl_if_blank:VF \l_tmpa_tl
{% the last item is not empty, restore it
\seq_put_right:NV \l__james_formalproof_body_seq \l_tmpa_tl
}
% now let's compute the item widths
\dim_zero:N \l__james_formalproof_left_dim
\dim_zero:N \l__james_formalproof_right_dim
\seq_map_inline:Nn \l__james_formalproof_body_seq
{
\seq_set_split:Nnn \l__james_formalproof_tmp_seq { & } { ##1 }
\hbox_set:Nn \l_tmpa_box { $\seq_item:Nn \l__james_formalproof_tmp_seq { 1 }$ }
\dim_set:Nn \l__james_formalproof_left_dim
{
\dim_max:nn { \l__james_formalproof_left_dim } { \box_wd:N \l_tmpa_box }
}
\hbox_set:Nn \l_tmpb_box { (\seq_item:Nn \l__james_formalproof_tmp_seq { 2 }) }
\dim_set:Nn \l__james_formalproof_right_dim
{
\dim_max:nn { \l__james_formalproof_right_dim } { \box_wd:N \l_tmpb_box }
}
}
\hbox_set:Nn \l_tmpa_box { \seq_count:N \l__james_formalproof_body_seq }
\dim_set:Nn \l__james_formalproof_step_dim { \box_wd:N \l_tmpa_box }
% now we can process the whole thing
\int_zero:N \l__james_formalproof_line_int
\seq_map_inline:Nn \l__james_formalproof_body_seq
{
\seq_set_split:Nnn \l__james_formalproof_tmp_seq { & } { ##1 }
\int_incr:N \l__james_formalproof_line_int
\par
\makebox[\l__james_formalproof_step_dim][r]
{ \int_to_arabic:n { \l__james_formalproof_line_int } }.\enspace
\makebox[\l__james_formalproof_left_dim][l]
{ $\seq_item:Nn \l__james_formalproof_tmp_seq { 1 }$ }
\hfill
\makebox[\l__james_formalproof_right_dim][l]
{ (\seq_item:Nn \l__james_formalproof_tmp_seq { 2 }) }
}
}
\ExplSyntaxOff
\begin{document}
\lipsum[2][1-4]
\begin{formalproof}
\exists x \overline{A(x)} & premise \\
\overline{A(a)} & existential instantiation \\
\forall x(C(x)\to\overline{D(x)}) & premise \\
C(a)\to\overline{D(a)} & universal instantiation \\
\overline{C(a)}\lor \overline{D(a)} & definition \\
\forall x(\overline{B(x)}\lor D(x)) & premise \\
\overline{B(a)}\lor D(a) & universal instantiation \\
\overline{C(a)}\lor\overline{B(a)} & resolution 5+7 \\
\forall x(A(x)\lor B(x)) & premise
\end{formalproof}
\lipsum[3][1-4]
\begin{formalproof}
\exists x \overline{A(x)} & premise \\
\overline{A(a)} & existential instantiation \\
\forall x(C(x)\to\overline{D(x)}) & premise \\
C(a)\to\overline{D(a)} & universal instantiation \\
\overline{C(a)}\lor \overline{D(a)} & definition \\
\forall x(\overline{B(x)}\lor D(x)) & premise \\
\overline{B(a)}\lor D(a) & universal instantiation \\
\overline{C(a)}\lor\overline{B(a)} & resolution 5+7 \\
\forall x(A(x)\lor B(x)) & premise \\
A+B+C & just one more line \\
\end{formalproof}
\lipsum[4][1-3]
\end{document}
在第二个例子中,您会看到两件事:为数字保留的宽度得到了照顾;此外,尾随\\
没有任何影响。
请注意,这允许在正式证明中分页。另一种方法是使用tabular*
:
\documentclass{article}
\usepackage{amsmath}
\usepackage{array}
\usepackage{lipsum}
\ExplSyntaxOn
\NewDocumentEnvironment{formalproof}{b}
{
\james_formalproof:n { #1 }
}
{}
\seq_new:N \l__james_formalproof_body_seq
\int_new:N \g__james_formalproof_line_int
\cs_new_protected:Nn \james_formalproof:n
{
\renewcommand{\arraystretch}{1.2}
\setlength{\tabcolsep}{0pt}
\seq_set_split:Nnn \l__james_formalproof_body_seq { \\ } { #1 }
% check for a trailing \\
\seq_pop_right:NN \l__james_formalproof_body_seq \l_tmpa_tl
\tl_if_blank:VF \l_tmpa_tl
{% the last item is not empty, restore it
\seq_put_right:NV \l__james_formalproof_body_seq \l_tmpa_tl
}
% process the material in a tabular*
\int_gzero:N \g__james_formalproof_line_int
\begin{tabular*}{\textwidth}
{
>{
\int_gincr:N \g__james_formalproof_line_int
\int_to_arabic:n { \g__james_formalproof_line_int }
.
}r
@{\hspace{0.5em}}
>{$}l<{$}
@{\extracolsep{\fill}}
>{(}l<{)}
@{}
}
\seq_map_function:NN \l__james_formalproof_body_seq \__james_formalproof_line:n
\end{tabular*}
}
\cs_new:Nn \__james_formalproof_line:n { & #1 \\ }
\ExplSyntaxOff
\begin{document}
\lipsum[2][1-4]
\begin{center}
\begin{formalproof}
\exists x \overline{A(x)} & premise \\
\overline{A(a)} & existential instantiation \\
\forall x(C(x)\to\overline{D(x)}) & premise \\
C(a)\to\overline{D(a)} & universal instantiation \\
\overline{C(a)}\lor \overline{D(a)} & definition \\
\forall x(\overline{B(x)}\lor D(x)) & premise \\
\overline{B(a)}\lor D(a) & universal instantiation \\
\overline{C(a)}\lor\overline{B(a)} & resolution 5+7 \\
\forall x(A(x)\lor B(x)) & premise
\end{formalproof}
\end{center}
\lipsum[3][1-4]
\begin{center}
\begin{formalproof}
\exists x \overline{A(x)} & premise \\
\overline{A(a)} & existential instantiation \\
\forall x(C(x)\to\overline{D(x)}) & premise \\
C(a)\to\overline{D(a)} & universal instantiation \\
\overline{C(a)}\lor \overline{D(a)} & definition \\
\forall x(\overline{B(x)}\lor D(x)) & premise \\
\overline{B(a)}\lor D(a) & universal instantiation \\
\overline{C(a)}\lor\overline{B(a)} & resolution 5+7 \\
\forall x(A(x)\lor B(x)) & premise \\
A+B+C & just one more line \\
\end{formalproof}
\end{center}
\lipsum[4][1-3]
\end{document}
输出基本与以前相同。