research_rewrite 设计

research_rewrite 包探索 QED 如何在不放弃内核优先原则的前提下提供重写与化简。它仅用于研究：已发布的包都不使用它，research/rewrite-simplify/ 中记录的评审决定在已审计基线上不将其升级。本页描述它所实现的模型，以及任何升级都必须满足的约束。

设计目标

重写用一个相等的子项替换子项。在 LCF 系统中，每次这样的替换都必须由一个等式定理来论证，所以重写器实际上是定理 $\vdash t = t'$ 的生产者。该原型检验：能否用一小组可审计的见证为 QED 的目标做到这一点，以及能否记录这些步骤以便后续阶段再次检查。

数学背景

转换与同余

转换 (conversion) 把项 $t$ 映射为定理 $\Gamma \vdash t = t'$ 。在较大项内部的某个位置重写需要同余：若 $\Gamma \vdash l = r$ ，则对每个上下文 $C[\cdot]$

\Gamma \vdash C[l] = C[r].

对于仅由应用构成的上下文，这可通过对通向空位的路径归纳得出，每步一次 MK_COMB：

\frac{\vdash f = f \quad \Gamma \vdash l = r}{\Gamma \vdash f\,l = f\,r}\;\textsf{MK\_COMB} \qquad \frac{\Gamma \vdash l = r \quad \vdash a = a}{\Gamma \vdash l\,a = r\,a}\;\textsf{MK\_COMB}

其中 REFL 提供不变的一侧。这就是 CombFun 和 CombArg 位置步骤构成的路径所产生的内容，每个位置步骤记录为一个 Congruence 步骤。在抽象之下，该步骤将是 ABS，它要求被绑定变量不在 $\Gamma$ 中自由出现；若以局部假设作为见证，这个侧条件可能失败，因此原型不支持 AbsBody 位置。

见证

焦点处的等式 $l = r$ 来自四种见证之一：

见证	定理	记录的步骤
`LocalEquality(h)`	$\{l = r\} \vdash l = r$ ，由 ASSUME 得到	`ResolveWitness`
`ExplicitTheorem(th)`	给定的定理	`ResolveWitness`
`CanonicalUnfold(k)`	联结词的定义应用于其参数并经 β 规范化	`Unfold`, `BetaNormalize`
`BetaNormalization`	REFL，随后是 BETA 和 TRANS 步骤	`BetaNormalize`

从右到左的重写会增加 Symmetry。用局部等式做重写会把该等式作为假设携带，因此它只在该等式是假设的目标中有效；不带该局部假设重放会失败，如教程所示。

在证明中使用重写

要把重写后的目标转回原目标的证明，需要 $\Gamma \vdash C[l] = C[r]$ 和 $C[r]$ 的证明；然后用对称等式做 EQ_MP 即可证明 $C[l]$ ：

\frac{\Gamma \vdash C[r] = C[l] \qquad \Delta \vdash C[r]}{\Gamma \cup \Delta \vdash C[l]}\;\textsf{EQ\_MP}

原型在内部构建该等式，但并不暴露它，也没有任何策略执行这最后一步。这是它不属于已发布路径的主要原因。

设计决策

记录义务，重建以检查

选择。 重写返回新结论和一个 ReplayObligation：请求、前后结论，以及所用内核步骤的种类。research_validate_replay_obligation 通过用内核规则从其请求重建每个片段并比较结果，来检查一个义务。

原因。 义务是可存储、可比较、可审查的普通数据，这是研究线的升级闸门所要求的。由于检查是重建而不是信任记录，伪造或过时的义务会被拒绝。

诚实失败

每个不受支持的情形都返回带原因的 HonestFailure：非布尔结论、AbsBody 位置、折叠定义、β 展开、未知局部变量、与焦点不匹配的见证，以及超出步数限制。除了表示没有规则适用的显式 NoChange 之外，没有任何情形会退化为悄无声息的空操作。

有界化简

research_simplify_term_concl 交替执行展开、β 规范化和用户的请求直至不动点，并在片段数将超过 step_limit 时以失败停止。该界使终止性成为配置的属性，而不是规则集的属性。

正确性与不变量

无权限。 该包构建的每个等式都来自内核和 logic 函数，没有任何定理离开该包。
可检查的记录。 当且仅当每个片段都能依据给定的状态、前奏和局部变量由其请求重建，并且这些片段从 before_concl 链接到 after_concl 时，义务才验证通过。
终止性。 化简最多执行 step_limit 个片段。

被否决的替代方案

直接返回定理。 这会使原型事实上成为一个策略，而没有研究流程所要求的评审。
带重命名的绑定子下重写。 它需要管理 ABS 侧条件，因此被排除在所评估的范围之外。

边界

仅供研究，未发布，不被任何其他包导入，也无法从定理脚本或命令行工具到达。
不在抽象之下重写，不折叠定义，不做 β 展开。
不证明原目标：该包返回项和义务，而不是定理。
这条研究线的权威状态见 research/README.md 以及 research/rewrite-simplify/ 中的文档，而不是本页。