prover API 参考

prover 包（Luna-Flow/QED/prover）运行定理脚本。它解析一个脚本或一个脚本文件，按要求安装命题前奏，降级每个目标，用 tactics 包运行各步骤（自行调度 { ... } 分支块），并返回内核定理、结构化失败，或对含 hole 的脚本返回未完成证明报告。它还发布回归语料，把用户手册与测试联系起来。

该包负责编排与报告，不持有任何逻辑权威。prover 设计说明了结果模型，prover 教程演示如何从 MoonBit 运行脚本。

选项

`ProverOptions`、`default_prover_options` 与 `prover_options`

ProverOptions 只有一个开关：运行前是否把命题前奏安装到状态中。default_prover_options() 将其打开；prover_options(b) 显式设置。

pub struct ProverOptions {
  auto_install_prelude : Bool
}

pub fn default_prover_options() -> ProverOptions
pub fn prover_options(Bool) -> ProverOptions

没有前奏时，T、F 和目录中的定理不可用，除非状态已经定义了它们。

运行脚本

`prove_theorem_script_detailed`

prove_theorem_script_detailed(state, src, opts) 运行一个定理脚本，并返回三态结果。

pub fn prove_theorem_script_detailed(@kernel.KernelState, String, ProverOptions) -> ProverRunResult

头部绑定子 (x : A) 成为目标的局部量。步骤按顺序运行；后接分支块的步骤先运行，然后每个块在各自的框架中针对其子目标运行。第一个失败的步骤会终止脚本。hole 使脚本以未完成状态终止。如果所有步骤都成功但仍有剩余目标，结果是带 UnsolvedGoals 的失败。

`prove_theorem_script` 与 `prove_theorem_script_with_diagnostics`

这些函数运行一个脚本，返回定理和状态，或将失败或未完成报告作为错误返回。

pub fn prove_theorem_script(@kernel.KernelState, String, ProverOptions) -> Result[(@kernel.KernelState, @kernel.Thm), ProverScriptError]
pub fn prove_theorem_script_with_diagnostics(@kernel.KernelState, String, ProverOptions) -> Result[(@kernel.KernelState, @kernel.Thm), ProverScriptError]

这两个函数目前行为相同；两者都在 ProverScriptError 中携带完整诊断。返回的状态就是证明运行时所在的状态，在被要求时已安装前奏；证明出的定理不会加入其中。

`prove_theorem_file_results_detailed`

prove_theorem_file_results_detailed(state, src, opts) 运行文件中的每个定理（定理之间以 qed 行分隔），并为每个定理返回一个结果。

pub fn prove_theorem_file_results_detailed(@kernel.KernelState, String, ProverOptions) -> ProverFileRunResult

失败或未完成的定理不会终止整个文件：后面的定理仍会被检查。只有当文件无法解析或前奏无法安装时，整个文件才失败（FileFailed）。

`prove_theorem_file_detailed`

prove_theorem_file_detailed 运行一个文件，并将其汇总为一个结果：若有失败则取第一个失败，否则若有未完成定理则取第一个未完成的，否则取最后一个成功。

pub fn prove_theorem_file_detailed(@kernel.KernelState, String, ProverOptions) -> ProverRunResult

结果

`ProverRunResult`

ProverRunResult 是一个脚本的运行结果。

pub enum ProverRunResult {
  Proved(ProverSuccess)
  Failed(ProverFailure)
  Unfinished(ProverUnfinished)
}

`ProverSuccess`

ProverSuccess 携带定理、脚本名以及证明所在的状态。

pub struct ProverSuccess {
  state : @kernel.KernelState
  theorem_name : String
  thm : @kernel.Thm
}

`ProverFailure`

ProverFailure 描述脚本在何处、因何失败。

pub struct ProverFailure {
  theorem_name : String?
  kind : ProverDiagnosticKind
  detail : String
  raw_offset : Int?
  goal_src : String?
  goal_span : @parser.SourceSpan?
  step_index : Int?
  branch_path : Array[Int]
  step_span : @parser.SourceSpan?
  step_src : String?
  current_goal : @tactics.Goal?
  local_hyps : Array[ProverLocalHyp]
  error : ProverError
}

kind 和 error 说明哪一层失败；detail 渲染该错误。位置字段在源文本中定位失败：解析错误用 raw_offset，降级错误用目标区间，策略错误则用步骤索引、分支路径、步骤区间和步骤文本，并附带该处的目标和局部量。不适用的字段为 None 或空。

`ProverUnfinished`

ProverUnfinished 报告到达 hole 的脚本。

pub struct ProverUnfinished {
  theorem_name : String
  detail : String
  raw_offset : Int?
  goal_src : String?
  goal_span : @parser.SourceSpan?
  step_index : Int?
  branch_path : Array[Int]
  step_span : @parser.SourceSpan?
  step_src : String?
  current_goal : @tactics.Goal
  local_hyps : Array[ProverLocalHyp]
  hole_name : String?
}

它具有与失败相同的位置字段，还有该 hole 所代表的目标（总是存在）以及 hole 的名字（如果有）。它不是定理。

`ProverLocalHyp` 与 `prover_local_hyp`

ProverLocalHyp 是报告中具名的局部假设；prover_local_hyp 构造一个。

pub struct ProverLocalHyp {
  name : String
  term : @kernel.Term
}

pub fn prover_local_hyp(String, @kernel.Term) -> ProverLocalHyp

`prover_unfinished`

prover_unfinished 由各字段构造一个 Unfinished 结果，字段顺序为：定理名、目标源文本、目标区间、步骤索引、分支路径、步骤区间、步骤源文本、当前目标、局部量、hole 名、详情和原始偏移。

pub fn prover_unfinished(String, String?, @parser.SourceSpan?, Int?, Array[Int], @parser.SourceSpan?, String?, @tactics.Goal, Array[ProverLocalHyp], String?, String, Int?) -> ProverRunResult

它供需要固定未完成报告的测试和渲染器使用。

`ProverError` 与 `ProverDiagnosticKind`

ProverError 包装失败那一层的错误；ProverDiagnosticKind 给出该层的名称。

pub enum ProverError {
  Parse(@parser.ParseError)
  Bridge(@parser.ParseBridgeError)
  Tactic(@tactics.TacticExecError)
  Sig(@kernel.SigError)
  Logic(@kernel.LogicError)
}

pub enum ProverDiagnosticKind {
  Parse
  Bridge
  Tactic
  Sig
  Logic
}

`ProverScriptError`

ProverScriptError 是 prove_theorem_script 的错误一侧。

pub enum ProverScriptError {
  Failure(ProverFailure)
  Unfinished(ProverUnfinished)
}

`ProverFileRunResult`、`ProverFileReport` 与 `ProverFileItemResult`

文件运行要么整体失败，要么按顺序为每个定理产生一项。

pub enum ProverFileRunResult {
  FileChecked(ProverFileReport)
  FileFailed(ProverFailure)
}

pub struct ProverFileReport {
  state : @kernel.KernelState
  items : Array[ProverFileItemResult]
}

pub enum ProverFileItemResult {
  ProverItemProved(ProverSuccess)
  ProverItemFailed(ProverFailure)
  ProverItemUnfinished(ProverUnfinished)
}

test "run scripts" {
  let st = @kernel.empty_kernel_state()
  let opts = @prover.default_prover_options()
  let ok = @prover.prove_theorem_script_detailed(st, "theorem truth_file : ⊢ T := by exact truth", opts)
  inspect(ok is @prover.Proved({ theorem_name: "truth_file", .. }), content="true")
  // the manual's bad_branch example: a structured failure
  let bad = @prover.prove_theorem_script_detailed(
    st,
    "theorem bad_branch (x : bool) : ⊢ x -> x ∨ x := by\n  intro h\n  left { exact truth }",
    opts,
  )
  guard bad is @prover.Failed(f) else { fail("expected a failure") }
  inspect(f.detail, content="GoalShapeMismatch(exact witness does not directly close current goal)")
  assert_eq((f.step_index, f.branch_path, f.step_src), (Some(3), [1], Some("exact truth")))
  // a hole is reported, not proved
  let unf = @prover.prove_theorem_script_detailed(
    st,
    "theorem unfinished_branch (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by\n  intro h\n  right { right { hole h1 } }",
    opts,
  )
  guard unf is @prover.Unfinished(u) else { fail("expected an unfinished proof") }
  assert_eq((u.hole_name, u.step_index, u.branch_path), (Some("h1"), Some(4), [1, 1]))
}

test "run a 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 st = @kernel.empty_kernel_state()
  guard @prover.prove_theorem_file_results_detailed(st, src, @prover.default_prover_options())
    is @prover.FileChecked(report) else {
    fail("expected the file to parse")
  }
  let kinds = report.items.map(item => match item {
    @prover.ProverItemProved(_) => "ok"
    @prover.ProverItemFailed(_) => "error"
    @prover.ProverItemUnfinished(_) => "unfinished"
  })
  assert_eq(kinds, ["ok", "unfinished", "ok"])
}

该文件是 examples/multi_with_hole.qed。

回归语料

语料（corpus）是测试运行、文档可引用的脚本的唯一列表。每个用例有标识符、脚本、步骤布局，以及它所展示的能力或失败。

`positive_corpus_cases`、`negative_corpus_cases`、`unfinished_corpus_cases` 与 `quantifier_corpus_cases`

这些函数返回各类用例。

pub fn positive_corpus_cases() -> Array[PositiveCorpusCase]
pub fn negative_corpus_cases() -> Array[NegativeCorpusCase]
pub fn unfinished_corpus_cases() -> Array[UnfinishedCorpusCase]
pub fn quantifier_corpus_cases() -> Array[QuantifierCorpusCase]

`PositiveCorpusCase`

正例在声明布尔常量 const_names 之后，必须证明 expected_goal。

pub struct PositiveCorpusCase {
  case_id : String
  const_names : Array[String]
  expected_goal : String
  script : String
  layout : ScriptLayout
  catalog_class : PositiveCatalogClass
  capability : PositiveTacticCapability
}

`NegativeCorpusCase`

反例必须以错误形态 expected_error 失败。这些常量被声明为布尔值、一元或二元布尔函数。

pub struct NegativeCorpusCase {
  case_id : String
  bool_consts : Array[String]
  unary_bool_consts : Array[String]
  binary_bool_consts : Array[String]
  script : String
  layout : ScriptLayout
  failure_class : NegativeFailureClass
  expected_error : NegativeErrorShape
}

`UnfinishedCorpusCase`

未完成用例必须在给定的步骤、分支路径和 hole 处停止，并带有给定的详情。

pub struct UnfinishedCorpusCase {
  case_id : String
  const_names : Array[String]
  expected_goal : String
  script : String
  layout : ScriptLayout
  expected_step_index : Int
  expected_branch_path : Array[Int]
  expected_hole_name : String?
  expected_detail : String
}

`QuantifierCorpusCase` 与 `QuantifierSurfaceOutcome`

量词用例涵盖绑定子和原始 forall 的表层语法，结果可能是成功、失败或未完成。

pub struct QuantifierCorpusCase {
  case_id : String
  script : String
  layout : ScriptLayout
  kind : MappingCaseKind
  outcome : QuantifierSurfaceOutcome
  capability_label : String
  manual_anchor : String
  expected_step_index : Int?
  expected_branch_path : Array[Int]
  expected_hole_name : String?
  expected_detail : String?
}

pub enum QuantifierSurfaceOutcome {
  QuantifierSuccess
  QuantifierFailure
  QuantifierUnfinished
}

分类枚举

这些枚举对用例分类；下面的标签函数把它们渲染为测试和文档中使用的稳定字符串。

pub enum ScriptLayout {
  InlineSequential
  BlockSequential
  BranchStructured
}

pub enum PositiveCatalogClass {
  LocalFact
  DirectClose
  ImplicationBacked
  ContextDerived
  StructuralOnly
}

pub enum PositiveTacticCapability {
  IntroExact
  Assumption
  ExactNamedDirectClose
  ExactContextDerived
  ApplyLocalImp
  ApplyNamedImp
  Split
  Left
  Right
  Mixed
}

pub enum NegativeFailureClass {
  FailureUnknownName
  FailureWrongModeTheoremUsage
  FailureGoalShapeMismatch
  FailureNonBoolConnector
  FailureUnsupportedHonestFailure
  FailureShadowingOrScopeDrift
}

pub enum NegativeErrorShape {
  ErrorTacticUnknownName
  ErrorTacticApplyMismatch
  ErrorTacticGoalShapeMismatch
  ErrorTacticUnsolvedGoals
  ErrorLogicNotBoolTerm
}

`script_layout_label`、`catalog_label`、`capability_label`、`negative_failure_class_label`、`negative_error_shape_label` 与 `quantifier_surface_outcome_label`

这些函数返回分类值的稳定 snake-case 标签，例如 inline_sequential、local_fact 或 intro_exact。

pub fn script_layout_label(ScriptLayout) -> String
pub fn catalog_label(PositiveCatalogClass) -> String
pub fn capability_label(PositiveTacticCapability) -> String
pub fn negative_failure_class_label(NegativeFailureClass) -> String
pub fn negative_error_shape_label(NegativeErrorShape) -> String
pub fn quantifier_surface_outcome_label(QuantifierSurfaceOutcome) -> String

映射矩阵

映射矩阵把每个语料用例链接到它可出现的文档锚点，例如 manual:runnable_examples，并说明它是否为公开示例。

`MappingMatrixEntry` 和 `mapping_matrix_entries`

pub struct MappingMatrixEntry {
  case_id : String
  kind : MappingCaseKind
  script : String
  catalog_or_failure_label : String
  capability_or_error_label : String
  doc_anchor : String
  doc_visibility : MappingDocVisibility
}

pub fn mapping_matrix_entries() -> Array[MappingMatrixEntry]

`MappingCaseKind`、`mapping_case_positive`、`mapping_case_negative` 和 `mapping_case_unfinished`

MappingCaseKind 表示一个用例是正例、反例还是未完成；这三个函数返回它的构造子。

pub enum MappingCaseKind {
  PositiveCase
  NegativeCase
  UnfinishedCase
}

pub fn mapping_case_positive() -> MappingCaseKind
pub fn mapping_case_negative() -> MappingCaseKind
pub fn mapping_case_unfinished() -> MappingCaseKind

`MappingDocVisibility` 及其构造函数

MappingDocVisibility 表示一个用例是否可以在文档中作为示例引用、作为失败示例引用，或完全不可引用。mapping_doc_visibility_public_unfinished_example 返回 PublicExample：未完成的示例属于公开示例。

pub enum MappingDocVisibility {
  PublicExample
  PublicFailureExample
  InternalOnly
}

pub fn mapping_doc_visibility_public_example() -> MappingDocVisibility
pub fn mapping_doc_visibility_public_failure_example() -> MappingDocVisibility
pub fn mapping_doc_visibility_public_unfinished_example() -> MappingDocVisibility
pub fn mapping_doc_visibility_internal_only() -> MappingDocVisibility

test "corpus" {
  let first = @prover.positive_corpus_cases()[0]
  inspect(first.case_id, content="pos_intro_exact_identity")
  inspect(first.script, content="theorem pos_intro_exact_identity : ⊢ P -> P := by intro h; exact h")
  inspect(@prover.capability_label(first.capability), content="intro_exact")
  // every corpus case appears in the mapping matrix with an anchor
  let entry = @prover.mapping_matrix_entries().search_by(e => e.case_id == first.case_id).unwrap()
  inspect(@prover.mapping_matrix_entries()[entry].doc_anchor, content="manual:runnable_examples")
}

prover API 参考

选项

ProverOptions、default_prover_options 与 prover_options

运行脚本

prove_theorem_script_detailed

prove_theorem_script 与 prove_theorem_script_with_diagnostics

prove_theorem_file_results_detailed

prove_theorem_file_detailed

结果

ProverRunResult

ProverSuccess

ProverFailure

ProverUnfinished

ProverLocalHyp 与 prover_local_hyp

prover_unfinished

ProverError 与 ProverDiagnosticKind

ProverScriptError

ProverFileRunResult、ProverFileReport 与 ProverFileItemResult