Luna Flow
日本語

QED

QED (Quite Easy Deduction) は、MoonBit で書かれた高階論理の定理証明器である。LCF の方式に従う。小さな信頼カーネルが HOL の基本推論規則を実装し、定理を作れる唯一のコードとなる。パーサからコマンドラインツールまで、それ以外のすべてはカーネルの上に、信頼されることなく構築される。証明はゴール指向のステップを持つ短い定理スクリプトとして書かれ、スクリプトはカーネルの定理を生むか、構造化された診断とともに失敗するか、未完了の証明を報告する。形式仕様がカーネルを定義し、formal_verification/ の Lean 4 パックが仕様の適合性の主張を検査する。

同梱の証明言語は、等号を伴う命題論理、定理ヘッダの束縛子、ゴールレベルの forall を扱う。正確なサポート表はユーザーマニュアルにある。

形式仕様

形式仕様はカーネルに関する唯一の規範的な情報源です。

QED 形式仕様

パッケージ

パッケージは階層化されている。各パッケージは左にあるパッケージにのみ依存し、kernel → logic/elab → parser → tactics → prover → cmd の順で、信頼されるのは kernel だけである。

パッケージ役割ページ
kernel信頼カーネル：型、項、抽象的な定理型、基本規則、スコープ付きシグネチャ、拡張ゲートAPI · 設計 · チュートリアル
logic定義としての命題結合子、導出規則、リプレイ補助関数、定理カタログAPI · 設計 · チュートリアル
elab定数の同一性を凍結する名前解決、コア型付け、カーネル項へのローワリングAPI · 設計 · チュートリアル
parserテキストフロントエンド：正規化、項、ゴール、定理スクリプト、ソース位置API · 設計 · チュートリアル
tactics後ろ向きの証明状態とステップ。前向きにリプレイしてカーネルの定理にするAPI · 設計 · チュートリアル
prover構造化された結果を返す定理スクリプトのドライバと、回帰コーパスAPI · 設計 · チュートリアル
cmdコマンドラインツール qed-cmd（実行可能パッケージ）API · 設計 · チュートリアル
research_rewrite研究専用の書き換えプロトタイプ。出荷対象外API · 設計 · チュートリアル

ブラックボックステストファイル（*_test.mbt）とエイリアスファイル alias.mbt および alias_test.mbt はそれぞれのパッケージに属し、その規則はコードガバナンスが定める。examples/ と prelude/ にある定理ファイルはコマンドラインツールへの入力であり、パッケージではない。

どこから始めるか

証明支援系が初めての場合。 ユーザーマニュアルの「HOL に不慣れな読者へ」とクイックスタートを読み、cmd チュートリアルで例を実行する。「このステップはどう書くのか」という疑問には構文ガイドが答える。

MoonBit から QED を使う場合。 スクリプトを実行して結果を読むには、まず prover チュートリアルから始める。証明をステップごとに進めるには tactics チュートリアルへ、定理を前向きに構築するには logic と kernel のチュートリアルへと下りていく。

健全である理由を確かめる場合。 規則を導出し、健全性がカーネルに帰着する理由を説明する kernel 設計を読み、次に上位層が何の権限も追加しないことを示す logic と tactics の設計を読む。規範となるのは上記の形式仕様である。

貢献する場合。 まずコードガバナンスとドキュメントガバナンスを読み、次にコードとテストの対応および例の規則について仕様適合性を読む。未解決のリスクはワークスペース監査に一覧があり、仕様の改訂は仕様変更履歴に記録されている。

ガイド

インストールとビルド

QED には moonc 0.10 以降を含む MoonBit ツールチェーンが必要であり、コマンドラインツールでのファイルアクセスのために moonbitlang/x に依存する。別のモジュールからライブラリを使うには次のようにする。

moon add Luna-Flow/QED@0.1.0

リポジトリで作業するには次のようにする。

moon check --target all
moon test
moon run src/cmd examples/truth_file.qed

Lean による形式化は、formal_verification/ で lake build を実行して別途ビルドする。