Luna Flow
简体中文

prover 教程

本教程在 MoonBit 中使用 prover 包运行定理脚本，并读取它的三种结果：已证明的定理、结构化失败和未完成证明。所有脚本都来自 examples/ 和回归语料，因此所示输出正是测试所检查的输出。

快速开始

在 moon.pkg 中导入内核和 prover：

import {
  "Luna-Flow/QED/kernel",
  "Luna-Flow/QED/tactics",
  "Luna-Flow/QED/prover",
}

运行最小的脚本 examples/truth_file.qed：

test "quick start" {
  let st = @kernel.empty_kernel_state()
  let src = "theorem truth_file : ⊢ T := by exact truth"
  match @prover.prove_theorem_script_detailed(st, src, @prover.default_prover_options()) {
    Proved(ok) => {
      inspect(ok.theorem_name, content="truth_file")
      inspect(@kernel.thm_hyp_count(ok.thm), content="0")
    }
    _ => fail("expected a proof")
  }
}

default_prover_options() 会安装命题序言，所以在空状态上 T 和目录定理 truth 都可用。结果的 thm 是内核定理。

日常任务

使用绑定子和分支块进行证明

头部绑定子声明目标的局部变量；split 之后的分支块分别证明各个部分。这是 examples/and_comm.qed：

test "and_comm" {
  let src =
    #|theorem and_comm (p : bool) (q : bool) : ⊢ p ∧ q -> q ∧ p := by
    #|  intro h
    #|  split { exact and_elim_r } { exact and_elim_l }
  let r = @prover.prove_theorem_script(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is Ok((_, th)) else { fail("expected a proof") }
  inspect(@kernel.thm_hyp_count(th), content="0")
}

对于只关心定理的调用者，prove_theorem_script 返回 Ok((state, thm)) 或一个错误。

定位失败

某一步失败时，结果会说明是哪一步、哪个分支、哪个目标以及哪些局部变量。这是 examples/bad_branch.qed：

test "failure" {
  let src =
    #|theorem bad_branch (x : bool) : ⊢ x -> x ∨ x := by
    #|  intro h
    #|  left { exact truth }
  let r = @prover.prove_theorem_script_detailed(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is Failed(f) else { fail("expected a failure") }
  inspect(f.kind is Tactic, content="true")
  inspect(f.detail, content="GoalShapeMismatch(exact witness does not directly close current goal)")
  assert_eq(f.step_index, Some(3))
  assert_eq(f.branch_path, [1])
  assert_eq(f.step_src, Some("exact truth"))
  assert_eq(f.local_hyps.map(h => h.name), ["h"])
}

第 3 步是 exact truth（在 intro h 和 left 之后），位于 left 块的分支 1 上。此时的目标是 x，而 truth 不能证明它。

报告未完成证明

hole 标记一处缺口。prover 在此停止，并报告该 hole 所代表的目标；不会产生定理。这是 examples/unfinished_branch.qed：

test "unfinished" {
  let src =
    #|theorem unfinished_branch (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by
    #|  intro h
    #|  right { right { hole h1 } }
  let r = @prover.prove_theorem_script_detailed(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is Unfinished(u) else { fail("expected an unfinished proof") }
  assert_eq(u.hole_name, Some("h1"))
  assert_eq(u.branch_path, [1, 1])
  inspect(u.detail, content="proof contains an unfinished hole")
  inspect(@tactics.goal_hyp_count(u.current_goal), content="1")
}

current_goal 是 x⊢xx \vdash x：用 exact h 填上 hole 即可完成证明。

检查整个文件

prove_theorem_file_results_detailed 检查文件中的每个定理，并在失败或遇到 hole 后继续。这是 examples/multi_with_hole.qed：

test "file" {
  let src =
    #|theorem before_hole : ⊢ T := by exact truth
    #|qed
    #|
    #|theorem unfinished_demo (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by
    #|  intro h
    #|  right { right { hole h1 } }
    #|qed
    #|
    #|theorem after_hole : ⊢ T := by exact truth
    #|qed
  let r = @prover.prove_theorem_file_results_detailed(@kernel.empty_kernel_state(), src, @prover.default_prover_options())
  guard r is FileChecked(report) else { fail("expected a report") }
  let names = report.items.map(item => match item {
    ProverItemProved(ok) => "ok " + ok.theorem_name
    ProverItemFailed(f) => "error " + f.detail
    ProverItemUnfinished(u) => "unfinished " + u.theorem_name
  })
  assert_eq(names, ["ok before_hole", "unfinished unfinished_demo", "ok after_hole"])
}

进一步使用

针对你自己的状态运行。 传入 @prover.prover_options(false) 以跳过序言，并针对你准备好的状态运行，例如通过内核声明了额外常量的状态。没有序言时，T 未知，运行会以 Sig 诊断失败：

test "no prelude" {
  let src = "theorem t : ⊢ T := by exact truth"
  let r = @prover.prove_theorem_script_detailed(@kernel.empty_kernel_state(), src, @prover.prover_options(false))
  guard r is Failed(f) else { fail("expected a failure") }
  inspect(f.kind is Sig, content="true")
  inspect(f.detail, content="UnknownConst")
}

使用语料。 positive_corpus_cases() 及其同类函数返回测试所运行的脚本及其预期结果。它们是现成的示例集，也是你在 prover 之上构建的任何东西的回归测试套件。

渲染结果。 cmd 包把这些结果转换为命令行工具的 ok、error[...] 和 warning[unfinished] 行；若需要相同的文本，请复用它的渲染器。

常见陷阱

  • 指望从 hole 得到定理。 Unfinished 结果没有定理，prove_theorem_script 会把它作为错误返回。
  • 引用先前的定理。 文件中先前证明的定理对后面的定理不可用；只有目录名称可用。
  • 定理之间忘记 qed。 在含多个定理的文件中，除最后一个外，每个后面都必须跟一行 qed，否则文件解析失败。
  • 目标中的自由名称。 目标中的名称必须是头部绑定子、状态中的常量，或序言中的 T/F。变量请使用 (x : bool) 这样的绑定子。
  • 项内部的裸 forall。 forall 只在目标开头被接受。

后续步骤