Luna Flow
简体中文

prover 设计

prover 包把一个定理脚本变为三种结果之一：内核定理、结构化失败，或未完成证明。本页解释该结果模型、分支块如何在策略层之上被调度，以及该包为何采用失败即关闭 (fail closed)：没有任何路径能在没有所述目标的内核定理时报告成功。

设计目标

  • 端到端运行定理脚本：解析、安装前奏、降级目标、执行步骤、调度分支块。
  • 准确告诉用户证明在何处停止：定理、步骤编号、分支路径、源文本、当前目标和局部假设。
  • 绝不把内核 Thm 之外的任何东西呈现为证明。不受支持的输入、失败的步骤和 hole 都如实报告。
  • 通过发布测试所运行、手册所引用的脚本语料 (corpus)，保持文档诚实。

数学背景

作为和类型的结果

对于目标为 Γ⊢c\Gamma \vdash c 的脚本，结果为

run(script)∈ThmΓ⊢c⏟Proved  +  Failure⏟Failed  +  Goal×Position⏟Unfinished\mathsf{run}(\mathit{script}) \in \underbrace{\mathsf{Thm}_{\Gamma \vdash c}}_{\texttt{Proved}} \;+\; \underbrace{\mathsf{Failure}}_{\texttt{Failed}} \;+\; \underbrace{\mathsf{Goal} \times \mathsf{Position}}_{\texttt{Unfinished}}

这三种情形互不相交，且只有第一种携带定理。特别地，未完成证明不是带有额外假设的定理：它是一份报告，包含 hole 所代表的目标 Γ′⊢c′\Gamma' \vdash c'。把 hole 变成假设会得到定理 Γ∪{c′}⊢c\Gamma \cup \{c'\} \vdash c，那与用户所要求的是不同的命题。

作为嵌套证明的分支块

后面跟着分支块的步骤，例如 split { s₁ } { s₂ }，会在当前目标 GG 上运行该步骤，产生子目标 G1,G2G_1, G_2。每个块 sis_i 随后是 GiG_i 的一个独立证明：

s1 proves G1s2 proves G2split {s1} {s2} proves G\frac{s_1 \text{ proves } G_1 \qquad s_2 \text{ proves } G_2}{\texttt{split}\,\{s_1\}\,\{s_2\} \text{ proves } G}

证明器在以 GiG_i 为根的全新证明状态中运行 sis_i（ps_isolate_pending_at），从该状态中得到 GiG_i 的定理 tit_i，并在父状态中用 tit_i 关闭 GiG_i。由于父状态中 split 的论证 (justification) 有效，这些定理组合成 GG 的定理；这就是策略设计中所述的论证的 LCF 组合，只是上升了一层。

设计决策

三路结果，而非 Result

问题。 Result[Thm, Error] 会迫使未完成证明要么是定理（这是错的），要么是错误（这会丢掉“错误”与“尚未完成”的区别）。

选择。 ProverRunResult 有三个构造子。prove_theorem_script 仍为只想要定理的调用者返回 Result，但其错误一侧 ProverScriptError 把失败与未完成证明区分开来。

原因。 编辑器和命令行工具对这些情形的处理不同：错误会让用户停下，而未完成证明是带有待处理目标的警告。规范要求 hole 绝不产生定理权限；类型使得这一点不可能被弄错。

诊断携带位置与上下文

每个失败和未完成报告都记录定理名称、步骤索引、分支路径、该步骤的跨度和源文本，以及当时的目标和局部变量，全部以原始输入为准。cmd 包直接打印这些字段。代价是记录较宽；好处是任何使用者都无需重新运行任何东西即可解释结果。

分支块的隔离框架

问题。 在父状态内运行分支体，会让一个分支中的失败干扰其兄弟分支的簿记，并使所报告的分支路径依赖于调度细节。

选择。 每个分支体在其自己的、由一个待处理目标构建的证明状态中运行，不带父状态的重放上下文。当分支体结束时，ps_close_frame 必须返回该目标的定理；父状态用它关闭目标。留有未关闭目标的分支体在该分支步骤处失败。

原因。 这样每个块都是其子目标的独立证明，正如块语法所暗示的那样；并且无论嵌套如何，步骤索引和分支路径都按阅读顺序分配。

坏定理之后文件继续

问题。 含多个定理的文件应报告所有问题，而不只是第一个。

选择。 prove_theorem_file_results_detailed 运行每个定理，并各返回一项。只有无法解析的文件或前奏安装失败才会使整个文件失败。已证明的定理不会加入状态：后面的定理不能按名称引用前面的定理。

原因。 报告每个定理正是 CLI 用户所期望的。不把定理加入状态，使可引用名称的目录保持固定，正如用户手册所述；定理环境不属于已发布子集。

前奏由选项安装

当 auto_install_prelude 开启（默认如此）时，证明器在运行前安装命题前奏。脚本便可使用 T、F 和目录定理而无需准备状态。需要特定状态的测试会将其关闭并自行安装常量。

语料即代码

手册和本页所引用的脚本是 corpus.mbt 中的值：包括正例、反例、未完成和量词用例，每个用例都带有标识符及其所展示的能力或失败，另有从用例到文档锚点的映射矩阵。测试运行每个用例并检查映射，因此已发布的示例不会偏离代码的实际行为。符合性指南 (conformance guide) 把这条规定为公开示例的规则。

正确性与不变量

  • 失败即关闭 (fail closed)。 Proved 只在一处构造，来自 ps_qed 的结果，而 ps_qed 仅在策略层对照根目标检查之后才返回定理。其他每条路径都返回 Failed 或 Unfinished。
  • 无权限。 该包调用解析器、策略层和内核状态函数；它自身不构建定理。
  • hole 不会泄漏。 hole 会在 ps_qed 之前终止脚本；没有任何代码路径能把未完成状态变成定理。
  • 位置是原始的。 报告中的偏移和跨度通过解析器的偏移映射，指向所给定的输入字符串。
  • 顺序。 文件报告中的各项按源码顺序排列，步骤索引在分支块之间按阅读顺序计数。

被否决的替代方案

  • 用异常表示失败。 Result 让每种结果都体现在类型中，并使 CLI 能统一渲染所有结果。
  • 把 hole 当作假设。 被拒绝，因为如上所示，所得定理陈述的将不是目标。
  • 分支体共享一个状态。 实现更简单，但会耦合兄弟分支，并使归咎依赖于调度。
  • 跨文件的定理环境。 让后面的定理引用前面的定理，需要规范尚未定义的命名与重放规程；在此之前，目录是名称的唯一来源。

边界

  • 证明器不增加步骤；步骤集合就是 tactics 的步骤加上 hole。
  • 它不读取文件也不打印；这由 cmd 包完成。
  • 它不搜索证明、不重写也不化简。research_rewrite 中的研究原型并未接入。
  • 它不存储已证明的定理，也不让脚本相互引用。