Luna Flow
日本語

cmd チュートリアル

このチュートリアルでは、コマンドラインツール qed-cmd で定理スクリプトファイルを検査する。examples/ に同梱された例を実行し、成功、エラー、未完了の証明の出力を読み、スクリプトで終了ステータスを利用する。MoonBit のコードは不要である。

クイックスタート

MoonBit ツールチェーンをインストールした状態で、リポジトリのルートから次を実行する。

moon run src/cmd examples/truth_file.qed
ok truth_file

このファイルには定理が一つ含まれている。

theorem truth_file : ⊢ T := by exact truth

moon run src/cmd はツールをビルドして実行する。ツール自体への引数は moon run src/cmd -- -d <file> のように -- の後に置く。単体の実行ファイルとしてビルドした後は、同じ呼び出しは qed-cmd -d <file> となる。

日常的な作業

複数の定理を検査する

定理と定理の間は qed だけを含む行で区切る。examples/multi_theorems.qed：

theorem truth_demo : ⊢ T := by exact truth
qed

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

theorem dup_bool_demo (x : bool) : ⊢ x -> x ∧ x := by
  intro h
  split { exact h } { exact h }
qed
moon run src/cmd examples/multi_theorems.qed
ok truth_demo
ok id_bool_demo
ok dup_bool_demo

終了ステータスは 0 である。

何が証明されたかを見る

-d は各定理の結論を、カーネルの構造的な記法で出力する。

moon run src/cmd -- -d examples/truth_file.qed
ok truth_file: Const(T#1 : bool)

結合子は定義として出力されるため、大きなゴールでは結論が長くなる。

エラーを読む

examples/bad_branch.qed は、x ∨ x の左の分岐 x を truth で証明しようとしている。

theorem bad_branch (x : bool) : ⊢ x -> x ∨ x := by
  intro h
  left { exact truth }
moon run src/cmd examples/bad_branch.qed
error[tactic] examples/bad_branch.qed (bad_branch): GoalShapeMismatch(exact witness does not directly close current goal)
step: 3
branch: 1
goal: [Var(x : bool)] |- Var(x : bool)
locals: h: Var(x : bool)

ステップ 3 は exact truth であり、そこでのゴールは仮定 x の下での x、ローカルは h である。exact truth を exact h に置き換えれば定理は証明される。終了ステータスは 1 である。

hole を残して先に進む

hole は証明の欠落箇所を示す。ツールはそれを警告として報告し、残りの定理を検査する。examples/multi_with_hole.qed：

moon run src/cmd examples/multi_with_hole.qed
ok before_hole
warning[unfinished] examples/multi_with_hole.qed (unfinished_demo): proof contains an unfinished hole
theorem: unfinished_demo
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
ok after_hole

hole を含むファイルは完了していないため、ステータスは 1 になる。開発中は警告を許容する。

moon run src/cmd -- --no-warn examples/multi_with_hole.qed
echo $?
0

出力は同じで、ステータスだけが変わる。

さらに進む

CI で使う。 各証明ファイルに対してツールを実行し、ステータスを頼りにする。0 はすべての定理が証明されたことを意味する。hole でビルドが失敗するよう、CI では --no-warn を付けない。

単体のバイナリをビルドする。 moon build はデフォルトのターゲット向けにツールを生成する。ネイティブターゲットでは、実行ファイルを -- なしで qed-cmd -d --no-warn <file> として呼び出せる。

サブセットの外へ進む。 ツールは prover が受け付けるものを受け付ける。すなわち、構文ガイドに挙げられたステップと定理名、そしてユーザーマニュアルのサポート表である。プログラムから使うには、MoonBit から prover を呼び出す。

よくある落とし穴

  • moon run で -- を忘れる。 moon run src/cmd -d file は -d をツールではなく moon に渡してしまう。
  • qed 区切りの欠落。 複数の定理を含むファイルで qed が欠けていると、ファイルのパースが失敗し（error[parse] <file>: offset …: missing qed before next theorem）、何も検査されない。
  • 自由な名前。 ゴールに書けるのは (x : bool) のようなヘッダの束縛子と T、F だけである。それ以外の名前は未知の定数となり、定理は error[sig] <file> (<name>): UnknownConst で失敗する。
  • --no-warn で警告が消えると思い込む。 変わるのはステータスだけである。
  • 前の定理を引用する。 ファイル内の定理は互いに独立しており、exact before_hole は上にある定理を指さない。

次のステップ