使用森林排版的逻辑证明树中跨节点的良好对齐

Question

在这个答案，用户 cfr 提供了以下代码，其输出如下图所示：

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    for tree={math content},
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.\quad ##1\quad ##3} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=15, close
  ]]]]]]]]]
\end{forest}
\end{document}

我想知道是否有人知道如何修改代码以产生如下图所示的输出：

我能想到的一种方法是存储每个分支上最宽的行号、公式和对齐方式的宽度，然后将分支上每个节点的内容包装在一个三列表格中，其中列宽固定为这些最大宽度。然后，节点锚点的位置将设置在公式列的北边，以便分支之间的线被绘制到公式的中心。

一种不太优雅但更简单的方法是使用多行表格来包含分支上的所有公式（即一个表格包含编号为 1、2、3 的公式；另一个包含 4；另一个包含 5、8、11；等等）。但我想避免使用这种方法，因为它需要对树本身而不是其样式进行重大更改。

不幸的是，我目前确实不具备技术专长，甚至不知道从哪里开始实际实施更优雅的解决方案，因此，我将不胜感激所提供的任何帮助。

更新

这是部分答案，涉及将内容处理成具有三列的单行表格，一列用于行号，一列用于 wff，另一列用于理由：

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\usepackage{array}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{\begin{tabular}{>{\raggedleft}p{1em}cp{1em}}##2. & \ensuremath{##1} & \ensuremath{##3}\\\end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=1500, close
  ]]]]]]]]]
\end{forest}
\end{document}

上述操作使得公式的中心水平对齐。因此我们得到

代替

与原始代码一样。这已经提高了可读性和美观性。

难题中缺失的一块是组织事物，以便将 17. 和 19. 处的公式列的宽度设置为 15. 处的公式列的宽度，以便行号和对齐方式也水平对齐。（整个树都是类似的做法。）

我觉得cfr 的这个答案提示了计算每个公式宽度的方法。但我不知道如何存储宽度，然后为每组公式选择最合适的宽度。

另一个更新

我创建了一个fwidth传递给公式列宽度的 tok。现在一切都很好地对齐了，但代价是用户需要为树上的每个节点设置此键。找出应该设置为什么的最佳方法是将分支的最宽公式插入代码中

\newlength{\myl}
\settowidth{\myl}{formula goes here}
\the\myl

然后将fwidth分支中的每个公式设置为该长度。请参阅下面的示例代码：

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\usepackage{array}
\forestset{
  declare toks={from}{},
  declare toks={fwidth}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  Ow4 {content}{tempcounta}{from}{}{}{(##1)}{fwidth}{\begin{tabular}{p{1em}>{\centering\arraybackslash}p{##4}p{1em}}##2. & \ensuremath{##1} & \ensuremath{##3}\\\end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r))), fwidth=158.8pt    
    [ (p\lor (q\land r)) , from=1, fwidth=158.8pt
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1, fwidth=158.8pt
        [ p , from=2, fwidth=5.1pt
          [ \lnot (p\lor q) , from=3, fwidth=35.5pt
            [ \lnot p , from=6, fwidth=35.5pt
              [ \lnot q , from=6, close, fwidth=35.5pt
          ]]]
          [ \lnot (p\lor r) , from=3, fwidth=35.5pt
            [1 \lnot p , from=7, fwidth=35.5pt
            [1 \lnot r , from=7, close, fwidth=35.5pt
        ]]]]
        [ (q\land r) , from=2, fwidth=28.6pt
          [1 q , from=5, fwidth=28.6pt
            [1 r , from=5, fwidth=28.6pt
              [1 \lnot (p\lor q) , from=3, fwidth=40.5pt
                [1 \lnot p , from=14, fwidth=40.5pt
                  [1 \lnot q , from=14, close, fwidth=40.5pt
              ]]]
              [1 \lnot (p\lor r) , from=3, fwidth=40.5pt
                [1 \lnot p , from=15, fwidth=40.5pt
                  [1 \lnot r , from=1500, close, fwidth=40.5pt
  ]]]]]]]]]
\end{forest}
\end{document}

现在看起来确实很不错，但如果可以自动计算和设置，那就方便多了fwidth。（如果能隐藏将行号和对齐列设置为较小的固定宽度而产生的过满警告，那就太好了。）我期待有更深入了解 TikZ 的人能指点迷津forest。

Answer 1

这是tabular/ alignidea 的一个变体，它可以自动确定中心列的宽度（对于 wff）。

% ref.: https://tex.stackexchange.com/q/570449/

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb,array}
\newcolumntype{C}[1]{>{\centering $}p{#1}<{$}}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  declare boolean={align me}{0},
  declare dimen={my width}{0pt},
  declare dimen register={lmeas},
  lmeas/.pgfmath=width("99."),
  declare dimen register={rmeas},
  rmeas/.pgfmath=width("(99)"),
  claim=,
  ll proof/.style={
    for tree={
      math content,
    },
    for root=align me,
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip},}{},
    for root={align me},
    where n children>=2{
      for children={align me}}{},
    before packing={
      tempcountb'=0,
      where align me={%
        tempcountb'+=1,
        tempdima/.max={>{OOw2+d}{max x}{min x}{##1-##2}}{%
          walk and save={temptoksa}{current,
             until={> O_=!{n children}{1}}{first,typeset node}}%
        },
        for nodewalk={load=temptoksa}{my width/.register=tempdima, typeset node}, 
      }{},
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        align=p{\foresteregister{lmeas}}C{\foresteoption{my width}}p{\foresteregister{rmeas}},
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.\quad & ##1\quad & ##3} },
        typeset node,
      }
    },
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=15, close
  ]]]]]]]]]
\end{forest}
\end{document}

无论如何，Sašo 都可以让这个变得更快，但我缺乏练习，所以其他人可能也能做得更好。花哨的列说明符似乎与forest的解析器纠缠在一起。因此方法有点笨拙。就像我说的，其他人无疑会让它表现得更有礼貌。