ユーザーマニュアル

• ステータス：active
• 対象読者：ユーザー、コントリビューター、実装者
• 権威：ユーザーガイド兼実装契約。QED 形式仕様と現在のコード／テストに従属する
• 範囲：現在リリース済みの挙動、初心者向けの使い方、信頼境界、サポート表、安定した例
• 最終レビュー: 2026-10-08

本書は、現在の QED ユーザーマニュアルであると同時に、その実装契約でもある。

本書は現在のリポジトリワークスペースにある MoonBit と Lean のコードに従い、次の三つの問いに答える。

• 一般のユーザーが今日、実際にどのように小さな証明を書いて実行するか。
• 今日、実際に何が実装されているか。
• 周辺ツールが現在、何をしてよく、何をしてはならないか。

HOL 初心者の方へ

HOL、Lean、HOL Light、Isabelle などの証明支援系を使ったことがない場合でも、QED が現在出荷しているサブセットを理解するには、次の直観で十分である。

• ここでの「証明」は自然言語の文章ではなく、カーネルが検査するスクリプトである。
• 現在出荷されているゴールは、主として最小限の命題論理のサブセットに、少量の等式と定理リプレイを加えたものである。
• ⊢ goal は「前提なしで goal を証明せよ」を意味する。
• A, B ⊢ goal は「仮定 A と B のもとで goal を証明せよ」を意味する。
• 直観的には、T を「常に真である命題」、F を「偽の命題」と読めばよい。
• A -> B は「A が与えられれば B を導ける」を意味する。
• A ∧ B は「A と B の両方を証明せよ」を意味する。
• A ∨ B は「A か B のどちらか一方を証明すれば十分だが、左右のどちらかを明示的に選ばなければならない」を意味する。
• P = Q は等式を表す。現在出荷されているサブセットは、等式に関する少量の定理リプレイもサポートする。

おおまかに言えば、定理スクリプトは現在、「ゴール駆動の証明ステップ」の列である。

• intro h: 現在のゴールが A -> B であれば、「h という名前の局所仮定 A を追加して B の証明を続ける」ことになる。
• exact h: h がすでに現在のゴールの直接の根拠であれば、ゴールを直ちに閉じる。
• assumption: 現在の局所仮定の中から、ゴールに合致する根拠を探す。
• apply th: 含意の定理または局所の含意仮定を現在のゴールに適用し、新たなサブゴールを生成する。
• split: ゴールが A ∧ B のとき、それを二つのサブゴールに分割する。
• left / right: ゴールが A ∨ B のとき、左または右の分岐を証明することを明示的に選ぶ。
• hole: ここがまだ証明されていないことを認める。システムは成功を偽装せず、構造化された未完了の結果を返す。

これらの直観があれば、本ユーザーマニュアルの最初のいくつかの例を読み始めるのに十分である。完全な境界、規則名、サポート表は後に続く。

始める順序

次の順序で始めることを推奨する。

1. まず moon build と moon test を実行し、ワークスペース自体が緑であることを確認する。
2. src/cmd を使って、状態を一切持たない定理ファイルを実行し、入力と出力の形式に慣れる。
3. 次に、定理ヘッダの束縛子を持つ例を試し、「局所変数が証明コンテキストにどう入るか」を理解する。
4. 最後に、サポート表、失敗表、実装契約を読み、どの機能が出荷済みで、どれが未出荷かを理解する。

クイックスタート

1. ビルド

moon build
moon test

2. 最初の証明ファイルを実行する

リポジトリのルートにファイルを作成する。たとえば truth_file.qed:

theorem truth_file : ⊢ T := by exact truth

次に実行する。

moon run src/cmd truth_file.qed

成功すると、現在は次のように出力される。

ok truth_file

結論の要約を全文で見るには、-d を付ける。

moon run src/cmd -- -d truth_file.qed

moon run 経由で起動する場合、-- は MoonBit ランナーの引数区切りである。これがないと moon が -d を自分で解釈してしまい、QED CLI はそのフラグを受け取れない。スタンドアロンの実行ファイルにコンパイルした後は、直接次のように書ける。

qed-cmd -d truth_file.qed

hole を含む定理は warning[unfinished] として報告される。定理は構築されず、後続のカーネル状態にも入らない。既定では警告があると全体の終了コードが非ゼロになる。本物のエラーがない限り警告を許容するには、--no-warn を使う。

moon run src/cmd -- --no-warn file.qed
qed-cmd --no-warn file.qed

この例は、追加の自由定数に依存せず、束縛子、分岐、定理インベントリを事前に理解する必要もないため、最初の一歩として適している。

3. 2 番目の例: 最小限の「仮定してそのまま返す」

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

ここで注意すべき層が二つある。

• (x : bool) は定理ヘッダの束縛子である。定理のゴールに局所変数 x を導入する。
• intro h は、ゴール x -> x を「h : x を仮定して x を証明する」に変える。
• exact h は、局所仮定 h が現在のゴールの直接の根拠になったことを述べる。

これは現在、HOL の知識がない読者に最も適したスクリプトでもある。「ゴールの書き換え」と「根拠による閉鎖」だけを示し、追加の定理名には依存しない。

4. 3 番目の例: 連言の構成

theorem dup_bool (x : bool) : ⊢ x -> x ∧ x := by
  intro h
  split { exact h } { exact h }

この例は次のことを示す。

• ゴール x ∧ x は、左辺と右辺を別々に証明する必要がある。
• split は二つの分岐を生成する。
• 各分岐は、ふたたび exact h で閉じられる。

逐次スタイルを好む場合は、先に split を行い、その後で二つのサブゴールを順に完了することもできる。ただし初心者には、split { ... } { ... } の構造化分岐ブロックのほうが直観的である。

5. 4 番目の例: 古典的な連言の可換性定理

theorem and_comm (p : bool) (q : bool) : ⊢ p ∧ q -> q ∧ p := by
  intro h
  split { exact and_elim_r } { exact and_elim_l }

このスクリプトは、最も古典的な命題論理のパターンの一つ、p ∧ q から q ∧ p を組み立て直すことを示す。x -> x よりも実際の数学的な主張に近く見えるが、現在出荷されている構文と機能の範囲に完全に収まっている。

6. 5 番目の例: 正直な失敗を見る

次のスクリプトは意図的に誤っている。

theorem bad_branch (x : bool) : ⊢ x -> x ∨ x := by
  intro h
  left { exact truth }

これは定理の成功を返さず、構造化された失敗を返す。理由は、現在の左分岐のゴールが実際には x であるのに対し、truth が直接閉じられるのは T のみだからである。

現在の正準な出力例については、本書の後述の manual:quantifier_failure_matrix を参照のこと。

7. 6 番目の例: 未完了の証明を見る

theorem unfinished_branch (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by
  intro h
  right { right { hole h1 } }

ここで hole h1 は、「証明義務が一つ欠けていることは分かっているが、今のところは空のままにしておく」という意味である。QED は未完了の結果を正直に返し、次を保持する。

• 定理名。
• ステップのインデックス。
• 分岐パス。
• 現在のゴール。
• 現在のローカル。
• hole 名。

これはインタラクティブなフロントエンド、IDE の診断、および今後の証明記述にとって重要であるが、定理ではない。

ユーザーから見た現在の入力モデル

「コマンドラインが受け付ける構文は正確には何か」を調べたい場合は、まず構文ガイドを参照のこと。本節では入力モデルの要約のみを保持する。サポート表、失敗の意味論、実装契約については、本書が引き続き正本である。

定理スクリプトの形

現在提供されている定理スクリプトの形は次のとおりである。

theorem <name> [(binder...)] : <goal> := by <steps>

ここで、

• <name> は定理名である。
• [(binder...)] は現在、(x : bool) 形式の定理ヘッダ束縛子を 0 個以上サポートする。
• <goal> はシーケントであり、例えば ⊢ T、P ⊢ P、⊢ x -> x ∧ x である。
• <steps> は、1 行に順に並べる、改行区切りのブロックとして書く、あるいは split / left / right の後に最小限の構造化分岐ブロックを置く形で書ける。この分岐構文はパーサが受理し、その実行は prover が統括する。

現在の主な制限事項

src/cmd を初めて使う場合、次の点が最も重要である。

• スクリプトをファイル優先で直接実行する場合は、T、F、定理ヘッダ束縛子 (x : bool) など、状態を必要としない例から始めること。
• ドキュメント中の P、Q などを使う多くの例はサポート表を説明するためのものであり、テストでは prover を呼ぶ前に、対応するカーネル状態にあらかじめ配置される。
• 定理ヘッダ束縛子はすでに提供済みのサーフェスである。素の forall (x : A), body / ∀ (x : A), body はゴール専用の糖衣構文として受理されるようになったが、依然として項レベルの構文ではない。
• サポートされるステップは intro、exact、apply、assumption、split、left、right、hole のみである。
• 未サポートのパスはフェイルクローズであり、定理の成功を偽装することは決してない。

コマンドラインのワークフロー

現在提供されている cmd のエントリポイントは次のとおりである。

moon run src/cmd <file>
moon run src/cmd -- -d <file>
moon run src/cmd -- --no-warn <file>

入力は定理スクリプトファイルである。単一定理のファイルでは末尾の qed を省略でき、複数定理のファイルでは小文字の qed で定理を区切る。出力は次の 3 種類である。

• 成功: 既定では定理ごとに 1 行 ok <theorem_name>。-d を付けると出力は ok <theorem_name>: <conclusion_summary> となる。
• 失敗: error[kind] ...。関連する場合は step、branch、goal、locals を伴う。
• 未完了: warning[unfinished] ...。hole、goal、locals などの文脈を伴う。定理の権威は生まれないが、後続の定理の検査は継続される。

moon run の下で -d / --no-warn を渡すには -- 区切りが必要である。スタンドアロンの実行ファイルでは qed-cmd -d --no-warn <file> を直接使える。

つまり、これはもはや「成功と失敗だけ」のブラックボックス CLI ではなく、現在の証明状態に関する主要な診断を公開するものである。

正本の階層

QED は現在、ドキュメントガバナンスで定められたドキュメント階層に従う。実装契約に関しては、関連する順序は次のとおりである。

1. QED 形式仕様が唯一の規範的な情報源であり、doc/attachments/qed_formal_spec.typがそのソースファイルである。
2. 現在のコードと回帰テストが「実際に提供されている状態」を決定する。
3. 本書および仕様適合性は、現在の実装契約と工学的な適合性を記述する。
4. README.md と CHANGELOG.md は外部向けの要約にすぎず、上記より上位には置かれない。
5. research/ は未提供の設計調査を記録するだけであり、製品契約ではない。

実装とドキュメントが矛盾する場合は、まずコードとテストから実際の状態を確定し、その後ドキュメントを更新する。実装と論文の仕様が矛盾する場合は、論文の仕様が引き続き優先する。

信頼境界

QED はカーネルファーストのアーキテクチャを採る。定理構築の唯一の境界は src/kernel である。

• kernel は、型、項、定理オブジェクト、シグネチャ状態、基本規則、および DefOK / TypeDefOK / SpecOK ゲートを所有する。
• logic は、検査済みカーネル API、定義・展開ヘルパー、リプレイヘルパー、および非権威的な定理参照の整理層に対する薄いラッパーにとどまらなければならない。新たな基本規則の権威を導入してはならない。
• elab はワンショットの解決、解決済み/コア型付け、およびローワリングを所有する。新たな論理は定義しない。
• parser はテキスト構文、正規化、パーサ所有のローワリング結果、およびローカル環境の管理を所有する。結合子の意味論やスコープ規則を黙って変更してはならず、タクティクの実行オブジェクトを直接所有してもならない。
• tactics はゴール状態の変換とリプレイの統括を所有する。定理の権威は一切持たず、定理スクリプトの構造化分岐構文も解釈しない。
• prover は parser + tactics + kernel に対する統括用のエントリポイントにすぎない。サポート対象の部分集合では信頼された Thm を返せ、未サポートのパスはフェイルクローズであり続けなければならない。パーサのローワリング結果を tactics.Goal に明示的にブリッジし、構造化分岐ブロックのスクリプトをスケジュールするが、タクティクのオブジェクトをパーサへ押し戻すことは決してない。
• リポジトリには旧来の phase0/デモ用 cmd パスはもう存在しない。現在の src/cmd はファイル優先で非権威的なエントリポイントであり、依然として第二の証明カーネルになってはならない。

Thm はパッケージ境界において不透明な型のままである。外部の呼び出し側は、検査済み/ステートフルなインターフェースを通じてやり取りしなければならない。

各パッケージには API リファレンス、設計ノート、チュートリアルもある。マニュアル概要にそれらの一覧がある。カーネル設計は、健全性がなぜカーネルに帰着するかを説明している。

実装済みのカーネル

カーネルのうち現在安定している部分は次のとおりである。

• 型コア: bool、ind、fun(a, b)、一般の TyApp、および型変数。
• 項の境界: 外部には名前付きの Term、内部には α 不変な規則コアを動かすための型付き DbTerm。
• 検査済みの基本規則インターフェース:
  • refl_checked
  • assume_checked
  • trans_checked
  • mk_comb_rule_checked
  • abs_rule_checked
  • beta_rule_checked
  • eq_mp_checked
  • deduct_antisym_rule_checked
  • inst_type
  • inst_checked
• 定理の許容性検査:
  • 定理の定数 ID の束縛は現在の状態と一致しなければならない。
  • 定数のインスタンス化は主スキーマのインスタンス関係を満たさなければならない。
  • 定義による定理は def_inst_coherent を通過しなければならない。
  • 定理/文に現れるすべての型は現在の Sigma_t に属さなければならない。
  • 型の代入は許容性ゲートを通過しなければならない。
• スコープ付きシグネチャ状態:
  • empty_kernel_state
  • ks_push_scope
  • ks_pop_scope
  • ks_add_const
  • ks_mk_const
  • ks_mk_const_instance
• 拡張ゲート:
  • ks_define_const
  • ks_define_const_thm
  • ks_register_type_definition
  • ks_specify_const
• 拡張規律によってすでにカバーされている主要な制約:
  • def-head の単調性
  • スコープの push/pop 規律
  • ゴースト型変数の拒否
  • 定義の閉包・循環の拒否
  • typedef ウィットネスの妥当性
  • 仕様ウィットネスの妥当性
• 監査およびリプレイのヘルパーインターフェース:
  • ks_extension_cert_count
  • ks_extension_cert_at
  • ks_conservative_replay_ok

これらの監査オブジェクトは可観測性と保存性の回帰のためだけに存在する。新たな証明オブジェクトではない。

フロントエンドの契約

解決済みエラボレーション

フロントエンドは現在、3 種類の項表現を保持している。

1. 名前付きの Term
2. 解決済みの RTerm
3. 型付きの DbTerm

RTerm はカーネルの項を置き換えるものではなく、ワンショット解決の結果を凍結するものである。現在 ResolvedConst は次を記録する。

• name
• const_id
• inst_ty
• schema_ty

つまり、定数はエラボレーション時にそのカーネル上の同一性へ束縛される。後続の push / pop / シャドーイングは将来の名前解決にのみ影響し、既存の解決済みオブジェクトへ書き戻されることは決してない。

現在の解決済み/コア型付けの契約は次のとおりである。

• RVar は現在のローカル文脈とその明示的な型にのみ照合される。
• RConst は依然として同じ const_id と schema_ty に対応していなければならない。
• inst_ty は依然として主スキーマのインスタンス関係を満たさなければならない。
• スコープの変更により凍結された同一性がもはや受理できなくなった場合、型付けは、同名の定数を黙って再び検索するのではなく、フェイルクローズしなければならない。

パーサ

パーサは現在、「テキスト構文 -> AST -> 解決済みエラボレーション -> パーサ所有のローワリング済みオブジェクト」の唯一のエントリポイントである。

安定した契約には次が含まれる。

• 名前解決の順序は常に local > const である。
• parse_goal / lower_syn_goal_with_env は現在、パーサ所有の ParsedGoal を返す。タクティクの実行オブジェクトは、上位層がブリッジするときにのみ構築される。
• 入力はまず normalize_parser_input を通る。
  • \not / \and / \or / \imp は正準形に正規化される。
  • |- は ⊢ に正規化される。
  • 基本的な冗長な空白は圧縮される。
  • この段階では AST レベルの整形出力は行わない。
• ParseError.offset は引き続きユーザーの元の入力に対応し、正規化後の文字列上の座標には対応しない。
• 正準な表示構文は主に Unicode である。
  • 項: ¬、∧、∨、->、=
  • ゴール: ⊢
• 互換入力は引き続き受理される。
  • \not, \and, \or, \imp
  • |-
• 旧来の ASCII による結合子の綴り /\ と \/ はもう受理されない
• 生の定理スクリプトのエントリポイントは現在、次をサポートする。
  • 定理ヘッダ内の (name : type) 束縛子 0 個以上
  • 1 行形式の theorem <name> : <goal> := by <step>; <step>; ...
  • ブロック形式の theorem <name> : <goal> := by に続く、改行区切りの逐次ステップ列
  • hole / hole <name> 未完了の証明ステップ
• 定理スクリプトの AST は現在、定理ヘッダ束縛子、定理のゴール、および各ステップの生ソーススパンを保持している。これらの位置は引き続きユーザーの元の入力を指し、正規化後の座標に黙って書き換えられることは決してない。
• 定理ヘッダ束縛子は現在、量化子向けに提供されているサーフェスである。ゴールのローワリング、証明状態のローカル、cmd の診断に束縛子名を導入するが、tactic/prover に新たな定理の権威を与えるものではない。
• forall (x : A), body / ∀ (x : A), body は現在、ゴール専用の糖衣構文として受理されるが、依然として項レベルの構文ではない。

パーサは現在、次も公開している。

• parse_let
• parse_def_function

これらは現在サポートされているパーサ側のユーティリティサーフェスであり、テストでカバーされ単独で呼び出すことができ、ローカル環境の拡張とクロージャ形式の関数定義のパースを扱う。ただし、定理スクリプトの主構文には含まれず、定理構築の権威を拡張するものでもない。

サーフェス結合子

¬ / -> / ∧ / ∨ は現在いずれもサーフェス結合子であり、カーネルの基本論理ではない。

共通の契約には次が含まれる。

• ローワリング中、parser/bridge は logic 層の basis に裏付けられたビルダーを通じて命題項を生成する。
• prop_mk_not / prop_mk_imp / prop_mk_and / prop_mk_or は、非 bool 入力に対して LogicError を返さなければならず、クラッシュしてはならない。
• これらの結合子の信頼された意味論的基盤は、カーネル項、等号 =、選択 @、および検査済みの基本規則に由来する。
• これらを tactics、prover、あるいは将来の cmd における追加の規則の権威として扱ってはならない。
• パーサは、これらの結合子をパースする前に、同名の通常の定数が状態に存在することをもはや要求しない。
• logic.install_prop_prelude は、同名の既存定数がすでに正準な定義定理を持つ場合にのみ、冪等な成功として扱われる。同名・同型だが正準な定義を持たないプレースホルダ定数は拒否されなければならない。
• prop_dest_not / prop_dest_imp / prop_dest_and / prop_dest_or は現在、状態に裏付けられた信頼された認識を用いる。受理するのは、正準な basis 項、または現在の状態で正準な定義定理を持つ結合子定数のみである。

論理ヘルパー

src/logic は現在、将来の定理リプレイ拡張のための基盤層として機能している。安定して見える機能には次が含まれる。

• 命題 basis の項ビルダー:
  • prop_mk_not
  • prop_mk_imp
  • prop_mk_and
  • prop_mk_or
• 命題デストラクタ:
  • prop_dest_not
  • prop_dest_imp
  • prop_dest_and
  • prop_dest_or
• 結合子の定義定理・展開ヘルパー:
  • logic_prop_def_imp
  • logic_prop_def_not
  • logic_prop_def_and
  • logic_prop_def_or
  • logic_prop_unfold_head
  • logic_prop_unfold_imp
  • logic_prop_unfold_not
  • logic_prop_unfold_and
  • logic_prop_unfold_or
• 等式の持ち上げ・正規化ヘルパー:
  • logic_apply_fun_eq
  • logic_apply_fun_eq2
  • logic_beta_normalize_eq
  • logic_eq_sym
  • logic_eq_mp_bool
• 命題リプレイヘルパー:
  • logic_prop_close_hypothesis
  • logic_prop_ensure_sequent
  • logic_prop_discharge_imp_prefix
  • logic_prop_replay_imp_elim_backward
  • logic_prop_merge_conjunction
  • logic_prop_or_wrap_left
  • logic_prop_or_wrap_right
• 定理カタログ・リゾルバヘルパー:
  • logic_prop_theorem_count
  • logic_prop_theorem_at
  • logic_prop_theorem_entry
  • logic_prop_resolve_exact_theorem
  • logic_prop_resolve_apply_theorem

これらのヘルパーの目的は、証明合成と定理カタログのリプレイ経路を、明示的にカーネル検査された経路上に保ち、フロントエンドで意味論上の近道を黙って追加しないようにすることである。

証明スクリプトの状況

サポートされるタクティクと prelude 規則については、証明スクリプト層は現在 logic のリプレイを通じてカーネルの Thm を構築する。未サポートの入力は引き続きフェイルクローズであり、定理を偽装することは決してない。

すでに実装済みのオブジェクトとエントリポイントには次が含まれる。

• Goal
• ProofState
• ps_init
• ps_current_goal
• ps_goal_count
• ps_apply
• ps_apply_script
• ps_qed
• prove_theorem_script
• prove_theorem_script_detailed
• prove_theorem_script_with_diagnostics

現在サポートされるステップは次のみである。

• intro
• exact
• apply
• assumption
• split
• left
• right
• hole

exact / apply は、ローカル名のみを対象とする操作に限定されなくなった。

• exact は現在、ウィットネスの意味論で動作する。まずローカルの仮定のウィットネスを解決し、ローカルに見つからない場合は exact 可能な定理エントリを解決して、それが現在のシーケントを直接ウィットネスすることを要求する。
• apply はまずローカルの含意を解決し、ローカルに見つからない場合は、少数の安定した命題定理名、または文脈から導出される命題定理を解決できる。
• 現在 exact 可能な定理名は次のとおりである。
  • imp_refl
  • truth
  • and_elim_l
  • and_elim_r
  • and_intro
  • not_elim
  • ex_falso
  • imp_elim
  • eq_refl
  • eq_sym
  • eq_mp
• 現在、含意に裏付けられた apply 名は次のとおりである。
  • and_elim_l
  • and_elim_r
  • or_intro_l
  • or_intro_r
  • eq_sym
• or_intro_l / or_intro_r は現在も apply 専用である。前提を構築するために後ろ向きのリプレイが必要であり、現在のゴールの直接的なウィットネスではない。
• 定理名の一覧は現在 logic により一箇所で公開され、tactics、prover、テスト、ドキュメントが共同で利用する。ProofState の内部で定理名の意味論を別途断片的に維持することは、二度と許されない。
• これらの名前はすべて、既存のカーネル検査済み Thm にリプレイされなければならない。新たな証明の権威ではない。
• exact が暗黙のうちに apply へ格下げされることはない。まず新たなサブゴールを必要とし、後ろ向きのリプレイで完成させる名前は exact には属さない。
• ローカルの exact h は現在、有効な仮定のエイリアスのみを受理する。名前がローカルにヒットした場合、同名の定理エントリへフォールバックすることは決してない。
• apply は含意の定理のみを受理する。truth / not_elim / ex_falso のような直接クローズ型の定理名に対しては、正直に失敗しなければならない。

現在の意味論上の境界は次のように理解すべきである。

• tactics は未解決ゴールのスタックを変換し、リプレイに必要な証拠を整理する。
• prover はスクリプトをパースし、ゴールを設定し、ステップを実行する。
• prove_theorem_script_detailed / prove_theorem_script_with_diagnostics は現在、正直な失敗の際に、定理名、ステップのインデックス、現在のゴール、ローカルの仮定、分岐パス、およびゴール/ステップの生ソース上の位置を保持する。これらの診断オブジェクトは工学上の補助であり、新たな証明オブジェクトではない。
• 定理スクリプトに hole が含まれる場合、現在は構造化された未完了の証明結果が返され、定理名、ステップのインデックス、現在のゴール、ローカルの仮定、分岐パス、hole 名、およびソース上の位置が保持される。未完了の証明結果は定理ではない。
• ps_qed は、リプレイが成功し、かつルートゴールのシーケントと一致する場合にのみ、最終的な Thm を返す。
• ps_qed は現在、厳密な正規化シーケント照合で最終定理を検証する。まず命題の β 正規化を一律に適用し、その後、仮定集合と結論の α 不変な一致を検査する。旧来の緩い形状照合はもう受理されない。
• 未サポートのパスは、ProofSynthesisUnavailable、Logic、あるいはタクティクのエラーなど、正直な失敗を返し続ける。

現在のサポート表

現在提供しているもの

• 検査済みカーネル + スコープ付きシグネチャ + ゲート規律
• 解決済みエラボレーションの境界
• パーサの正規化・生オフセット・定理スクリプトの生パース。逐次ブロック本体、構造化分岐ブロック、定理ヘッダ束縛子、hole ステップ、および束縛子/ゴール/ステップの生スパンを含む
• 定理ヘッダ束縛子で駆動される量化子向けのスクリプトサーフェス。対応する prover/cmd のゴール、ローカル、分岐、未完了の証明の要約を伴う
• パーサ側のユーティリティ API parse_let / parse_def_function
• 命題 prelude の定義定理 + 展開ヘルパー
• サポートされる命題タクティクのカーネル Thm へのリプレイ
• hole を含む定理スクリプトに対する未完了の証明の報告
• 任意の qed 終端子と複数の定理ブロックを持つ定理スクリプトファイル向けの、ファイル優先の cmd ワークフロー

明示的に未提供のもの

• より豊かな定理ブロック
• 昇格された rewrite/simplify タクティクまたはコマンドのサーフェス
• カーネルのメタ変数 / hole 補完の権威
• 辞書渡し / 型クラスのフロントエンド
• 任意の定理環境への参照
• 任意のスクリプトの完全性

現在の拡張契約

• 定理名の一覧、コーパス、対応表、ドキュメントは、提供済みの同一のアンカー集合を用いる。
• ネストした証明ブロックは、引き続き現在の検査済みリプレイ境界を通じて整理される。
• hole / 未完了の証明は引き続きフロントエンドの契約であり、カーネルのメタ変数の権威ではない。
• 定理ヘッダ束縛子は引き続き、現在提供されている量化子向け構文の一部であり、コーパス / 表と同期され続ける。
• 新たな公開例は、まず回帰テストに入り、その後でドキュメントのアンカーに入らなければならない。

安定した定理名のサーフェス

サーフェス	現在サポートされる機能	安定した定理名
exact	ローカルの仮定のウィットネス、exact 能力を持つ定理エントリ	imp_refl, truth, and_elim_l, and_elim_r, and_intro, not_elim, ex_falso, imp_elim, eq_refl, eq_sym, eq_mp
apply	ローカルの含意、含意に裏付けられた名前付き定理、含意に裏付けられた文脈定理	and_elim_l, and_elim_r, or_intro_l, or_intro_r, eq_sym

安定した契約には次が含まれる。

• exact は exact 能力のみを消費し、暗黙のうちに apply へ格下げされることはない。これは直接クローズ型のエントリと、文脈から導出される exact エントリの両方に当てはまる。ローカルの exact h も h を現在のシーケントの直接ウィットネスとして解釈しなければならず、h は依然として有効な仮定のエイリアスでなければならない。形状に基づく推測や他のローカルな成果物であってはならない。
• apply は含意に裏付けられた能力のみを消費する。直接クローズ型の定理名を含意として受理することは決してない。
• 誤ったモードでの定理の使用は引き続き正直に失敗する。exact or_intro_l は現在 GoalShapeMismatch を返し、ローカルの exact h も h が現在のゴールの直接ウィットネスでない場合は GoalShapeMismatch を返す。apply truth、apply ex_falso、apply not_elim は、いずれも現在 ApplyMismatch を返さなければならない。
• ローカル名の解決は引き続き local > theorem name に従う。

M3c コーパス / 対応表

現在提供されている部分集合の正準コーパスは「4 種類」を用いる。

• 実行可能コーパス:
  • src/prover/prover_positive_corpus_test.mbt
  • src/prover/prover_negative_corpus_test.mbt
  • src/prover/prover_test.mbt / src/cmd/cmd_corpus_wbtest.mbt にある、未完了の証明に関する正準回帰テスト
  • src/prover/corpus.mbt にある、量化子向けの束縛子 / 素の forall の正準ケース。src/cmd/cmd_corpus_wbtest.mbt と src/prover/prover_mapping_matrix_test.mbt が共同でアンカーとなる
  • src/prover/prover_mapping_matrix_test.mbt
• 可読な対応表:
  • 本節のサポート表と例のソースに関する注記

ここで、

• manual:runnable_examples は、現在公開されている実行可能な定理スクリプトの例を表す。
• manual:support_matrix は、現在公開されている、サポート表の肯定ケースを表す。
• manual:failure_matrix は、現在公開されている、正直な失敗 / 否定の例を表す。
• internal_only は、正準コーパスには属するが、現在はドキュメントの例の本文に直接は置かれていないケースを表す。

コーパスのケース	可視性 / アンカー	サーフェス	カタログ / 機能	現在の契約
pos_intro_exact_identity	public_example / manual:runnable_examples	intro + exact h	local_fact / intro_exact	ローカルの仮定がゴールを直接閉じる
pos_local_shadow_exact_named_theorem	public_example / manual:support_matrix	exact imp_refl	local_fact / mixed	local > theorem name
pos_exact_imp_refl	public_example / manual:support_matrix	exact imp_refl	direct_close / exact_named_direct_close	直接クローズ型の定理
pos_exact_and_elim_l	public_example / manual:support_matrix	exact and_elim_l	context_derived / exact_context_derived	文脈中の連言の所有者に依存する
pos_apply_and_elim_l	public_example / manual:runnable_examples	apply and_elim_l	implication_backed / apply_named_imp	含意に裏付けられた文脈リプレイ
pos_apply_or_intro_l	public_example / manual:support_matrix	apply or_intro_l	implication_backed / apply_named_imp	含意に裏付けられたゴール形状リプレイ
pos_split_conjunction	public_example / manual:support_matrix	split	structural_only / split	逐次的な構造ゴールの統括
pos_branch_split_conjunction	public_example / manual:support_matrix	split { ... } { ... }	structural_only / split	構造化された連言の分岐ブロック
pos_left_disjunction	public_example / manual:runnable_examples	left	structural_only / left	選言ゴールに対する逐次的な分岐選択
pos_branch_left_disjunction	public_example / manual:runnable_examples	left { ... }	structural_only / left	構造化された選言の分岐ブロック
pos_exact_truth	public_example / manual:runnable_examples	exact truth	direct_close / exact_named_direct_close	T ゴールを直接閉じる
pos_exact_ex_falso	public_example / manual:runnable_examples	exact ex_falso	context_derived / exact_context_derived	仮定 F の下で任意の bool ゴールを正直に閉じる
pos_quant_seq_identity	public_example / manual:quantifier_examples	(x : bool) 束縛子 + intro / exact	quantifier_surface / quantifier_intro_exact	定理ヘッダ束縛子で駆動される逐次的な量化子サーフェス
pos_quant_branch_split	public_example / manual:quantifier_examples	(x : bool) 束縛子 + split { ... } { ... }	quantifier_surface / quantifier_split_branch	束縛子 + 分岐ブロックの互換性のある肯定ケース
pos_quant_forall_seq_identity	public_example / manual:quantifier_examples	forall (x : bool), ... + intro / exact	quantifier_surface / quantifier_forall_intro_exact	素の定理ゴール糖衣構文で駆動される逐次的な量化子サーフェス
pos_quant_forall_branch_split	public_example / manual:quantifier_examples	forall (x : bool), ... + split { ... } { ... }	quantifier_surface / quantifier_forall_split_branch	素の定理ゴール糖衣構文 + 分岐ブロックの互換性のある肯定ケース
neg_exact_or_intro_wrong_mode	public_failure_example / manual:failure_matrix	exact or_intro_l	exact モードでの apply 専用定理の誤用	GoalShapeMismatch
neg_apply_truth_wrong_mode	public_failure_example / manual:failure_matrix	apply truth	直接クローズ型の定理の誤用	ApplyMismatch
neg_local_shadow_truth_is_not_implication	public_failure_example / manual:failure_matrix	apply truth	ローカルのシャドーイングによる失敗	依然としてまずローカルを解決し、その後で正直に失敗する
neg_exact_context_missing	public_failure_example / manual:failure_matrix	exact and_elim_l	文脈から導出される所有者の欠落	GoalShapeMismatch
neg_non_bool_connector_rejected	public_failure_example / manual:failure_matrix	f ∧ Q	フロントエンド境界での拒否	非 bool の結合子はフェイルクローズする
neg_quant_branch_goal_mismatch	public_failure_example / manual:quantifier_failure_matrix	(x : bool) 束縛子 + left { exact truth }	quantifier_surface / quantifier_goal_shape_mismatch	束縛子のローカルが保持され、分岐の責任箇所が安定している
neg_quant_forall_branch_goal_mismatch	public_failure_example / manual:quantifier_failure_matrix	forall (x : bool), ... + left { exact truth }	quantifier_surface / quantifier_forall_goal_shape_mismatch	素の定理ゴール糖衣構文の下でも、ローカルと分岐の責任箇所が安定している
unf_quant_nested_branch_hole	public_example / manual:quantifier_unfinished_examples	(x : bool) 束縛子 + ネストした hole	unfinished_proof / quantifier_unfinished_hole	束縛子のローカル、ネストした分岐パス、および未完了の表示
unf_quant_forall_nested_branch_hole	public_example / manual:quantifier_unfinished_examples	forall (x : bool), ... + ネストした hole	unfinished_proof / quantifier_forall_unfinished_hole	素の定理ゴール糖衣構文の下でのローカル、ネストした分岐パス、および未完了の表示

実行可能な定理スクリプトの例

以下のスクリプトはすべて、回帰コーパスに実際に存在する定理スクリプトの例であり、計画中の機能ではない。

ただし、次の 2 つは区別する必要がある。

• 「テスト内 / あらかじめ用意された状態で実行可能」
• 「ユーザーが moon run src/cmd <file> で直接実行可能」

成功した定理の結論の要約全体を見るには、moon run を通す場合は moon run src/cmd -- -d <file> を使う。スタンドアロンの実行ファイルにコンパイルした後は qed-cmd -d <file> を使う。

追加の自由定数に依存しない、状態を必要としないスクリプトのみが、最初のファイル優先の例として適している。このプロジェクトに不慣れなユーザーは、まず本マニュアルの前半にある truth_file、id_bool、dup_bool を見るとよい。

リポジトリのルートにある prelude/ ディレクトリには、HOL Light の bool-core に隣接する層に対応する、現在直接実行できる定理アセットがさらに集められている。これらのファイルはライブラリ形式の実行可能な例として機能するが、現在の定理名の一覧 / リゾルバにはまだ接続されていない。

以下の例は主に、現在提供されている定理スクリプトの部分集合のカバー範囲を公開ドキュメントとして示すためのものである。

theorem t1 : ⊢ P -> P := by intro h; exact h
theorem t2 : ⊢ P ∧ Q -> P := by intro h; apply and_elim_l; exact h
theorem t3 : ⊢ P -> P ∨ Q := by intro h; left; exact h
theorem t4 : P ⊢ P ∨ Q := by left { assumption }
theorem t5 : ⊢ T := by exact truth
theorem t6 : F ⊢ Q := by exact ex_falso

これらの例は現在、src/prover/prover_test.mbt、src/prover/prover_positive_corpus_test.mbt、src/tactics/proof_state_test.mbt の肯定回帰テストでカバーされている。公開例を追加・変更する場合は、まず対応するテストの事実を成立させ、その後でドキュメントを更新すること。

公開されている実行可能な例と正準ケース ID の現在の対応は次のとおりである。

例	コーパスのケース	現在のサポート経路
t1	pos_intro_exact_identity	ローカルの事実 / intro_exact
t2	pos_apply_and_elim_l	含意に裏付けられた / apply_named_imp
t3	pos_left_disjunction	構造のみ / left
t4	pos_branch_left_disjunction	構造のみ / left の構造化分岐
t5	pos_exact_truth	直接クローズ / exact_named_direct_close
t6	pos_exact_ex_falso	文脈から導出 / exact_context_derived

src/prover/prover_mapping_matrix_test.mbt は現在、コーパスのケース、機能ラベル、ドキュメントのアンカーの間の唯一のテスト上のアンカーである。ドキュメントで公開例を追加・変更・削除するには、まず対応する正準ケースを更新し、その後で対応表と本書をそれに合わせて更新すること。

量化子向けの例

現在提供されている量化子サーフェスには、定理ヘッダ束縛子と素の forall による定理ゴール糖衣構文という 2 つのユーザー経路がある。以下の 2 組のスクリプトは、いずれも回帰テストと対応表によってアンカーされている。

theorem q1 (x : bool) : ⊢ x -> x := by intro h; exact h
theorem q2 (x : bool) : ⊢ x -> x ∧ x := by intro h; split { exact h } { exact h }
theorem qbad (x : bool) : ⊢ x -> x ∨ x := by intro h; left { exact truth }
theorem qunf (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by intro h; right { right { hole h1 } }

theorem qf1 : ⊢ forall (x : bool), x -> x := by intro h; exact h
theorem qf2 : ⊢ forall (x : bool), x -> x ∧ x := by intro h; split { exact h } { exact h }
theorem qfbad : ⊢ forall (x : bool), x -> x ∨ x := by intro h; left { exact truth }
theorem qfunf : ⊢ forall (x : bool), x -> x ∨ (x ∨ x) := by intro h; right { right { hole h1 } }

これらの例と正準ケース ID の対応は次のとおりである。

例	コーパスのケース	現在のサポート経路
q1	pos_quant_seq_identity	量化子サーフェス / quantifier_intro_exact
q2	pos_quant_branch_split	量化子サーフェス / quantifier_split_branch
qbad	neg_quant_branch_goal_mismatch	量化子の失敗 / quantifier_goal_shape_mismatch
qunf	unf_quant_nested_branch_hole	量化子の未完了 / quantifier_unfinished_hole
qf1	pos_quant_forall_seq_identity	量化子サーフェス / quantifier_forall_intro_exact
qf2	pos_quant_forall_branch_split	量化子サーフェス / quantifier_forall_split_branch
qfbad	neg_quant_forall_branch_goal_mismatch	量化子の失敗 / quantifier_forall_goal_shape_mismatch
qfunf	unf_quant_forall_nested_branch_hole	量化子の未完了 / quantifier_forall_unfinished_hole

加えて、⊢ (forall (x : bool), x -> x) のように外側に括弧を付けた形も、現在パーサ / prover に受理される。これらは同じ素のゴール糖衣構文のローワリング経路をたどり、現時点では独自のコーパスケース ID を持たないだけである。

HOL の知識がない読者は、これらの量化子の例をまず次のように理解するとよい。

• 定理は、まず (x : bool) のようなローカル変数を宣言できる。
• 続くゴールは、この変数を直接参照できる。
• 素の forall 定理ゴールは、現在、同じ束縛子指向のリプレイ経路にローワリングされる。

現在提供されている量化子フロントエンドには、束縛子の入口と素の forall ゴール糖衣構文が含まれる。素の forall は依然として項の位置では受理されない。つまり、ユーザーは forall の定理ゴールを書いて証明できるようになったが、依然として一般的な項レベルの量化子構文ではなく、カーネルの基本的な量化子の権威を追加するものでもない。

未完了の証明の例

現在の正準な未完了の証明ケースも回帰テストのアンカーであり、定理を返さない。

theorem unf_hole_intro : ⊢ T -> T := by intro h; hole h1
theorem unf_nested_branch_hole : ⊢ T ∨ (T ∨ T) := by right { right { hole h1 } }

これら 2 つのケースは現在、src/prover/prover_test.mbt、src/prover/prover_mapping_matrix_test.mbt、src/cmd/cmd_corpus_wbtest.mbt が共同でアンカーとなっている。前者はルートレベルの未完了の契約を固定し、後者はネストした分岐パスと未完了の表示を固定する。

現在の量化子向けの未完了のアンカーは、束縛子経路と素の forall 経路の両方をカバーしている。

theorem unf_quant_nested_branch_hole (x : bool) : ⊢ x -> x ∨ (x ∨ x) := by intro h; right { right { hole h1 } }
theorem unf_quant_forall_nested_branch_hole : ⊢ forall (x : bool), x -> x ∨ (x ∨ x) := by intro h; right { right { hole h1 } }

これらはそれぞれ、束縛子 / 素のゴール糖衣構文のローカル、ネストした分岐パス、および CLI の未完了の表示を固定している。

ファイル優先のワークフロー

現在提供されている cmd のエントリポイントは次のとおりである。

moon run src/cmd <file>
moon run src/cmd -- -d <file>
moon run src/cmd -- --no-warn <file>

現在の契約は次のとおりである。

• 入力は定理スクリプトファイルである。単一定理のファイルでは末尾の qed を省略でき、複数定理のファイルでは小文字の qed で定理を区切る。
• 成功時の出力は、既定では定理ごとに 1 行 ok <theorem_name> である。-d を付けると出力は ok <theorem_name>: <conclusion_summary> となる。
• 失敗時の出力は error[kind]、ファイルパス、定理名を保持し、タクティクの失敗では加えて次を報告する。
  • step
  • branch
  • goal
  • locals
• スクリプトに hole が含まれる場合、現在の出力は warning[unfinished] ... であり、step、branch、goal、locals、hole、message の要約を伴う。空値のマーカーは常に <none> / <root> である。警告は定理を構築しないが、ファイルレベルのランナーは後続の定理の検査を続ける。
• --no-warn は警告のみのファイルの終了コードにだけ影響し、警告の出力を隠すものではない。
• moon run の下では、-- は後続の引数を QED CLI に転送するだけである。スタンドアロンの実行ファイルにコンパイルした後は qed-cmd -d --no-warn <file> で十分であり、-- は不要である。
• 定理ヘッダ束縛子のスクリプトと素の forall 定理ゴールのスクリプトは同じ CLI 契約を共有する。goal / locals の要約は現在カーネル項の文字列として固定されており、分岐/ステップの責任箇所と未完了の表示は src/cmd/cmd_corpus_wbtest.mbt と src/cmd/cmd_wbtest.mbt が共同でアンカーとなっている。

現在の、回帰テストで検査された最小の例は次のとおりである。

theorem truth_file : ⊢ T := by exact truth

環境とコマンドの連鎖が動作することだけを確認したい場合は、これを最初に実行するのが最適である。

素の forall 定理ゴールのファイルについて、現在の正準な CLI 出力例は次のとおりである。

error[tactic] quant_forall_fail.qed (quant_forall_bad): GoalShapeMismatch(exact theorem does not directly close current goal)
step: 3
branch: 1
goal: [Var(x : bool)] |- Var(x : bool)
locals: h: Var(x : bool)

warning[unfinished] quant_forall_unfinished.qed (quant_forall_hole): proof contains an unfinished hole
theorem: quant_forall_hole
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

定理ヘッダ束縛子の構文も、現在は同じフィールド集合と同種の責任箇所の報告を用いる。対応する正準コーパスのアンカーについては src/cmd/cmd_corpus_wbtest.mbt を参照のこと。

現在の拡張契約

実行可能なフロントエンドは、現在、提供済みの同じアンカー集合に沿ってのみ拡張してよい。

• 定理の一覧、モード対応リゾルバ、コーパス、対応表、ドキュメントは単一の情報源を保つ。
• 構造化分岐ブロックは、prover 側のスクリプト契約として、既存の検査済みリプレイ境界を再利用し続ける。
• hole / 未完了の証明は引き続きフロントエンド限定の契約であり、カーネルのメタ変数の権威には入らない。
• 定理ヘッダ束縛子は引き続き、現在提供されている量化子向けのユーザー構文の一部である。
• 素の forall 定理ゴールは引き続きゴール専用の糖衣構文としてサポートされ、項レベルの構文としてドキュメント化してはならない。
• ファイル優先のワークフローは同じコーパス / 対応表を再利用し続け、第二の意味論を分岐させない。

検証ゲート

コントリビューターは現在、実装とドキュメントが一致していることを確認するため、次のゲートを用いること。

moon build
moon test
cd formal_verification
lake build

.mbti の変更を伴う場合、またはマージの準備をしている場合は、さらに次も実行すること。

moon info
moon fmt
moon test

ローカルチェックの結果:

• 2026-10-08、MoonBit moonc v0.10.14: moon check --target all は警告なしで、moon test は wasm、wasm-gc、js、native の各ターゲットで通過した(357 テスト)
• 2026-04-05: lake build は通過した。formal_verification/ はそれ以降変更されていない

論文との整合、コードとテストの対応、および周辺ツールのチェックリストについては、仕様適合性を参照のこと。