Luna Flow
日本語

構文ガイド

  • ステータス：active
  • 対象読者：ユーザー、コントリビューター
  • 権威：現在リリース済みの入力面に関するユーザー向け構文リファレンス。QED 形式仕様、現在のコード／テスト、ユーザーマニュアルに従属する
  • 範囲：現在の theorem-script の表層構文、CLI 向けのファイル形式、サポートされる証明ステップ、既知の未サポート形式
  • 最終レビュー：2026-04-20

本書は、QED が現在提供しているユーザー入力構文のクイックリファレンスである。

本書が答えるのは次の 1 点のみである。src/cmd が現在どのような定理スクリプトを受け付けるか。機能の境界、サポート表、失敗の意味論、実装契約については、ユーザーマニュアルが引き続き主要な入口である。

クイックスタート

現在のコマンドラインのエントリポイントは次のとおりである。

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

-d は結論の要約全体を出力する。--no-warn は、警告のみでエラーがない場合に成功の終了コードを返す。moon run 経由で起動する場合は、-- を使って残りの引数を QED CLI に転送する。スタンドアロンの実行ファイルにコンパイルした後は、qed-cmd -d --no-warn <file> を直接実行できる。

入力は定理スクリプトファイルであり、例えば次のようなものである。

theorem truth_file : ⊢ T := by exact truth

リポジトリ内の実行可能な例:

  • examples/truth_file.qed
  • examples/demo_and.qed
  • examples/and_comm.qed
  • examples/multi_theorems.qed
  • examples/multi_with_hole.qed
  • examples/bad_branch.qed
  • examples/unfinished_branch.qed

リポジトリのルートには prelude/ もあり、直接実行できる定理アセットファイルを収めている。これらは実行可能なスクリプトであり、現在の定理名カタログの公開サーフェスではない。

ファイルの形

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

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

ファイルに複数の定理が含まれる場合は、先行する各定理ブロックを小文字の qed で終える。

theorem t1 : ⊢ T := by exact truth
qed

theorem t2 : ⊢ T := by exact truth
qed

ここで、

  • <name> は定理名である。
  • [(binder...)] は現在、定理ヘッダ束縛子を 0 個以上サポートする。
  • <goal> はシーケントである。
  • <steps> は証明ステップであり、1 行の逐次形式、または改行区切りのブロック形式で書く。

既存の例との互換性のため、単一定理のファイルでは末尾の qed を省略できる。複数定理のファイルでは、次のトップレベルの theorem の前に、先行する各定理の後ろに qed が必要である。

定理ヘッダ

定理名

最小の例:

theorem truth_file : ⊢ T := by exact truth

定理ヘッダ束縛子

現在提供されている束縛子の形式は次のとおりである。

(x : bool)

例えば次のとおりである。

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

現在のドキュメントと例において、ファイル優先で最も安全な使い方は、bool の束縛子から始めることである。

現在サポートされる量化ゴール

次のような素の forall 定理ゴールは、ゴール専用の糖衣構文として受理されるようになった。

theorem quant_raw_intro_ok : ⊢ forall (x : bool), x -> x := by
  intro h
  exact h
qed

括弧付きの形も受理される。

theorem quant_raw_intro_paren_ok : ⊢ (forall (x : bool), x -> x) := by
  intro h
  exact h
qed

言い換えると、

  • 定理ヘッダ束縛子 (x : bool) と、素の forall / ∀ 定理ゴールは、いずれも現在提供されている量化子向けのユーザー構文の一部である。
  • 素の forall (x : A), body / ∀ (x : A), body は、定理スクリプトのゴール / parse_goal のエントリポイントでのみ受理される。項レベルの構文ではない。
  • 素の forall 経路は現在ゴールの糖衣構文にすぎない。同じローワリング / リプレイ / CLI 診断の契約に従い、カーネルの新たな量化子の権威を導入しない。

ゴールの形

現在提供されているサーフェスはシーケントのゴールを用いる。

⊢ goal
A ⊢ B
A, B ⊢ goal

README と examples/ にある最小の実行可能な例は、主に次を用いる。

  • ⊢ T
  • ⊢ x -> x
  • ⊢ x -> x ∧ x
  • ⊢ x -> x ∨ x

CLI を初めて使う場合は、T、F、定理ヘッダ束縛子を使った、状態を必要としない例から始めるのが最も安全である。

証明ステップ

現在提供されているステップは次のものだけである。

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

intro

intro h

現在のゴールが A -> B のとき、ローカルの仮定を導入し、後件の証明に進む。

exact

exact h
exact truth

現在のゴールを直接閉じる。

apply

apply and_elim_l

含意に裏付けられた定理、またはローカルの含意の仮定を現在のゴールに適用し、新たなサブゴールを生成する。

assumption

assumption

現在のローカルの仮定の中から、現在のゴールに一致する証拠を探す。

split

逐次形式:

split

構造化分岐形式:

split { exact h } { exact h }

left / right

逐次形式:

left
right

構造化分岐形式:

left { exact h }
right { right { hole h1 } }

hole

hole
hole h1

hole は成功を偽装しない。現在は構造化された未完了の結果を返す。

逐次ブロックと構造化分岐ブロック

<steps> は現在、1 行で書ける。

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

あるいは複数行のブロックとして書ける。

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

ステップが明示的な分岐を必要とする場合、現在は最小限の構造化分岐ブロックがサポートされている。

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

古典命題論理に近い例:

theorem and_comm (p : bool) (q : bool) : ⊢ p ∧ q -> q ∧ p := by
  intro h
  split { exact and_elim_r } { exact and_elim_l }
qed
theorem bad_branch (x : bool) : ⊢ x -> x ∨ x := by
  intro h
  left { exact truth }
qed

現在の主な制限事項

  • 現在の src/cmd のワークフローはファイル優先である。単一定理のファイルでは末尾の qed を省略でき、複数定理のファイルでは qed を区切りとして用いる。
  • 直接実行できる公開例には、examples/ にある既存のスクリプトを優先して用いるのが望ましい。
  • 定理ヘッダ束縛子は提供済みである。素の forall 定理ゴールはゴール専用の糖衣構文としてサポートされるが、項レベルの形式は依然としてサポートされない。
  • 未サポートのパスはフェイルクローズでなければならず、定理の成功を偽装してはならない。
  • hole は未完了を返し、定理の成功は返さない。

出力の形

現在の CLI の出力は 3 種類に分かれる。

  • 成功: 既定では定理ごとに 1 行 ok <theorem_name>。-d を付けると出力は ok <theorem_name>: <conclusion_summary> となる。
  • 失敗: error[kind] ...
  • 未完了: warning[unfinished] ...。定理の権威は生まれないが、後続の定理の検査は継続される。

moon run src/cmd -- -d --no-warn <file> の -- は moon run の引数転送にのみ属する。スタンドアロンの実行ファイルでは不要なので、qed-cmd -d --no-warn <file> を直接実行すること。

失敗フィールド、未完了フィールド、および安定した例の全容については、ユーザーマニュアルを参照のこと。