格式化策略样式验证步骤

Question

我目前正在编写一个证明，其中需要在每个步骤中应用简单的机械过程。我目前有以下工作要做，但乳胶非常“粗糙”且易碎。

思考这个问题的最好方式是使用纸笔版的 Coq，右边是策略，左边是上下文。

我当前的代码看起来像

\usepackage{pfsteps}

\newcommand{\pf}[2]{\usepfcounter[#1]\ $#2$ &\hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaa}\\}
\newcommand{\pfstep}[3]{\midrule \usepfcounter[#2]\ $#3$ & \text{#1}\\}

...

\resetpfcounter
\begin{equation*}
    \begin{array}{p{0.6\textwidth}r}     
        \pf{1}{5(n + 1) = 15}
        \pfstep{By distributivity \pfref{1}}
            {2}{5n + 5 = 15}
        \pfstep{By subtraction of 5 \pfref{2}}
            {3}{5n = 10}
        \pfstep{By something wrong \pfref{3}}
            {4}{n = 10}
            \pf{5}{5 = 1}
    \end{array}
\end{equation*}

我的问题是是否有更好的方法来实现同样的目标。

具体来说，我希望每个证明步骤的内容更加灵活。目前，在策略描述或上下文中添加太多内容会破坏实施。

Answer 1

对于将来遇到这种情况的人来说。这是我的解决方案

\newcommand{\pf}[2]{\item $#2$ \pflabel{#1}}
\newcommand{\pfstep}[3]{\\\vspace{-0.3cm}\hrulefill\vspace{-0.1cm}\item $#3$ \pflabel{#2} \BY{#1}}
\begin{pfsteps*}
            \pf{1}{5(n + 1) = 15}
        \pfstep{distributivity \pfref{1}}
            {2}{5n + 5 = 15}
        \pfstep{subtraction~of~5~\pfref{2}}
            {3}{5n = 10}
        \pfstep{something~wrong~\pfref{3}}
            {4}{n = 10}
            \pf{5}{5 = 1}
\end{pfsteps*}