Luna Flow
简体中文

cmd 教程

本教程使用命令行工具 qed-cmd 检查定理脚本文件。你将运行 examples/ 中自带的示例，读懂成功、错误和未完成证明的输出，并在脚本中使用退出状态。无需编写 MoonBit 代码。

快速开始

在仓库根目录下，已安装 MoonBit 工具链：

moon run src/cmd examples/truth_file.qed
ok truth_file

该文件包含一个定理：

theorem truth_file : ⊢ T := by exact truth

moon run src/cmd 构建并运行该工具。工具自身的参数写在 -- 之后，例如 moon run src/cmd -- -d <file>；构建为独立可执行文件后，等价调用为 qed-cmd -d <file>。

日常任务

检查多个定理

用只含 qed 的一行分隔定理。examples/multi_theorems.qed：

theorem truth_demo : ⊢ T := by exact truth
qed

theorem id_bool_demo (x : bool) : ⊢ x -> x := by
  intro h
  exact h
qed

theorem dup_bool_demo (x : bool) : ⊢ x -> x ∧ x := by
  intro h
  split { exact h } { exact h }
qed
moon run src/cmd examples/multi_theorems.qed
ok truth_demo
ok id_bool_demo
ok dup_bool_demo

退出状态为 0。

查看证明了什么

-d 以内核的结构化记法打印每个定理的结论：

moon run src/cmd -- -d examples/truth_file.qed
ok truth_file: Const(T#1 : bool)

对于较大的目标，结论会很长，因为联结词是按其定义打印的。

读懂错误

examples/bad_branch.qed 试图用 truth 证明 x ∨ x 的左分支 x：

theorem bad_branch (x : bool) : ⊢ x -> x ∨ x := by
  intro h
  left { exact truth }
moon run src/cmd examples/bad_branch.qed
error[tactic] examples/bad_branch.qed (bad_branch): GoalShapeMismatch(exact witness does not directly close current goal)
step: 3
branch: 1
goal: [Var(x : bool)] |- Var(x : bool)
locals: h: Var(x : bool)

第 3 步是 exact truth；此处的目标是假设 x 下的 x，带有局部变量 h。将 exact truth 换成 exact h 即可证明该定理。退出状态为 1。

留下 hole 并继续

hole 标记一处缺口。工具将其报告为警告，并继续检查其余定理。examples/multi_with_hole.qed：

moon run src/cmd examples/multi_with_hole.qed
ok before_hole
warning[unfinished] examples/multi_with_hole.qed (unfinished_demo): proof contains an unfinished hole
theorem: unfinished_demo
step: 4
branch: 1.1
goal: [Var(x : bool)] |- Var(x : bool)
locals: h: Var(x : bool)
hole: h1
message: proof contains an unfinished hole
ok after_hole

状态为 1，因为含有 hole 的文件尚未完成。开发期间可以允许警告：

moon run src/cmd -- --no-warn examples/multi_with_hole.qed
echo $?
0

输出相同，只有状态不同。

进一步使用

在 CI 中使用。 对每个证明文件运行该工具并依赖其状态：0 表示每个定理都已证明。CI 中不要加 --no-warn，这样 hole 会使构建失败。

构建独立二进制。 moon build 为默认目标生成该工具；在 native 目标上，可执行文件可直接以 qed-cmd -d --no-warn <file> 调用，无需 --。

超越该子集。 工具接受证明器 (prover) 所接受的内容：语法指南中列出的步骤和定理名称，以及用户手册的支持矩阵。若要以编程方式使用，请在 MoonBit 中调用 prover。

常见陷阱

  • moon run 时忘记 --。 moon run src/cmd -d file 会把 -d 传给 moon，而不是该工具。
  • 缺少 qed 分隔符。 在含多个定理的文件中，缺少 qed 会导致文件解析失败（error[parse] <file>: offset …: missing qed before next theorem），且不会检查任何内容。
  • 自由名称。 目标只能提到头部绑定子，如 (x : bool)、T 和 F；其他名称是未知常量，定理会失败并给出 error[sig] <file> (<name>): UnknownConst。
  • 以为 --no-warn 会隐藏警告。 它只改变状态。
  • 引用前面的定理。 文件中的定理相互独立；exact before_hole 并不指向上面的定理。

后续步骤