prover API リファレンス

prover パッケージ (Luna-Flow/QED/prover) は定理スクリプトを実行する。スクリプトまたはスクリプトのファイルをパースし、求められれば命題プレリュードをインストールし、各ゴールをローワリングし、tactics パッケージでステップを実行し({ ... } の分岐ブロックは自身でスケジュールする)、カーネル定理、構造化された失敗、または hole を含むスクリプトに対する未完了の証明の報告のいずれかを返す。また、ユーザーマニュアルとテストを結びつける回帰コーパスも公開する。

このパッケージは調整と報告を行うのみで、論理上の権限は持たない。結果モデルは prover の設計で説明しており、prover チュートリアルでは MoonBit からスクリプトを実行する。

オプション

`ProverOptions`、`default_prover_options` と `prover_options`

ProverOptions のスイッチは 1 つだけで、実行前に命題プレリュードを状態にインストールするかどうかである。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) は 1 つの定理スクリプトを実行し、3 通りの結果を返す。

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

ヘッダの束縛子 (x : A) はゴールのローカルになる。ステップは順に実行され、分岐ブロックが続くステップはまず実行され、その後に各ブロックがそれぞれのフレームで自分のサブゴール上で実行される。最初に失敗したステップでスクリプトは停止する。hole はスクリプトを未完了として停止させる。すべてのステップが成功してもゴールが残る場合、結果は UnsolvedGoals による失敗となる。

`prove_theorem_script` と `prove_theorem_script_with_diagnostics`

これらの関数は 1 つのスクリプトを実行し、定理と状態を返す。失敗または未完了の報告はエラーとして返す。

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]

2 つの関数は現在のところ同一に振る舞い、どちらも完全な診断情報を ProverScriptError に持たせる。返される状態は証明が実行された状態であり、要求があればプレリュードがインストールされている。証明された定理はそこに追加されない。

`prove_theorem_file_results_detailed`

prove_theorem_file_results_detailed(state, src, opts) は、定理が qed 行で区切られたファイルのすべての定理を実行し、定理ごとに 1 つの結果を返す。

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

失敗または未完了の定理があってもファイルは停止せず、後続の定理も検査される。ファイル全体が失敗する (FileFailed) のは、パースできないか、プレリュードをインストールできない場合のみである。

`prove_theorem_file_detailed`

prove_theorem_file_detailed はファイルを実行し、1 つの結果に要約する。失敗があれば最初の失敗、なければ未完了の定理があれば最初のもの、それもなければ最後の成功である。

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

結果

`ProverRunResult`

ProverRunResult は 1 つのスクリプトの結果である。

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 は、定理名、ゴールのソース、ゴールのスパン、ステップのインデックス、分岐パス、ステップのスパン、ステップのソース、現在のゴール、ローカル、hole の名前、詳細、生のオフセットの順のフィールドから Unfinished の結果を構築する。

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`

ファイルの実行は、全体として失敗するか、定理ごとに順番に 1 つの項目を返す。

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 である。

回帰コーパス

コーパスは、テストが実行し、ドキュメントが引用してよいスクリプトの唯一のリストである。各ケースは、識別子、スクリプト、ステップのレイアウト、およびそれが示す機能または失敗を持つ。

`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`

これらの関数は、分類値の安定したスネークケースのラベルを返す。例えば 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