Zenn
Open6

定理証明支援系 学習記録

coq
定理証明支援系
lean4
wuhu1slandwuhu1sland

Leanとは(wikipedia)

https://ja.wikipedia.org/wiki/Lean_(証明アシスタント)

Lean は純粋関数型プログラミング言語のひとつである。また、同時に証明支援系(theorem prover)（英語版）でもある。帰納型（英語版）を伴うCalculus of constructions（英語版）と呼ばれる型システムに基づいている。純粋関数型言語であるが、functional but in-place と呼ばれるプログラミングパラダイムに基づいており、効率性を重視している。

現在はLean4が推奨されており、Lean3との互換性は保証しないようです。

Lean with VSCode

Lean4のリッチな開発環境がVSCodeの拡張機能として提供されています。
https://marketplace.visualstudio.com/items?itemName=leanprover.lean4
たまたまYouTubeで見かけた動画でこの拡張機能の存在を知り、Leanに興味を持ちました。

拡張機能が処理系のインストーラのような機能も兼ねているようです。
ただ私は自分のWindowsに直入れされるのを避けたかったので、普通にWSL上のUbuntuにCLIからインストールしました。
(Installing Lean 4 on Linux: https://leanprover-community.github.io/install/linux.html)

wuhu1slandwuhu1sland

Natural Number Game クリア

https://x.com/wuhu1sland/status/1840392434125083094
Lean4のチュートリアルとして公開されているNatural Number Gameというゲームをやってみました。
https://adam.math.hhu.de/#/g/leanprover-community/NNG4
ペアノの公理といくつかの基本操作から自然数の加算や乗算を定義し、交換法則や結合法則などをはじめとする自然数とその演算の性質を証明していくゲームです。

ブラウザで完結するので、環境構築は不要です。
ただし、進行状況はブラウザのローカルストレージにセーブされるので、しばらく時間を空ける場合は右上のメニューからDownloadしておいた方が良さそうです。

自分の英語力不足が原因だと思うのですが、tauto/simp/trivialあたりの理解が曖昧なまま終わってしまいました。

詰まった時はこちらの方の配信を見てカンニングしていました。
(Let's Play: Lean 4 Natural Number Game: https://youtu.be/136e2d8pWlc?si=t8b8dXJCVmVL2ubi)

wuhu1slandwuhu1sland

Coq/SSReflect/MathCompによる定理証明

https://www.morikita.co.jp/books/mid/006241

大学の図書室で発見して、つい手に取ってしまいました。

Coq

https://coq.inria.fr/

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.

古く(1989年)から存在する定理証明支援系で、2013年に登場したLeanにとっては大先輩です。

言明やその証明などを記述するのがSSReflectという言語で、それを検証するシステムがCoqです。

このCoqとSSReflectでFeit-Thompsonの定理の証明と検証を行うというプロジェクトが行われた際、必要になった補題の形式化をまとめたものがMathCompです。

Coqの標準ライブラリとMathCompを用いることで、多くの証明済み基礎概念を駆使して定理証明を行うことができます。(恐らくLeanで言うところのMathlibに当たるものです。)

環境構築メモ(mac)

公式からインストーラが提供されていますが、CoqIDEよりVSCodeを使いたかったので例の如くCLIでインストールします。
WindowsでもWSL上でopamさえインストールできればほとんど同じ手順でインストールできると思います。

  1. HomebrewでopamというOCamlのパッケージマネージャをインストール: brew install opam
  2. opamインストール終了後: opam init
  3. opamでcoqをインストール(pinで自動アプデを防ぐ): opam pin add coq 8.20.0
  4. opamでMathCompをインストール:
    opam repo add coq-released https://coq.inria.fr/opam/released
    opam install coq-mathcomp-ssreflect
  5. VSCodeに拡張機能vscoqをインストール
  6. vscoq用のLSを用意: opam install vscoq-language-server
  7. which vscoqtop等でパスを調べてvscodeの設定からVscoq: Pathに登録

以下参照
opamでcoqのインストール: https://coq.inria.fr/opam-using.html
opamでmathCompのインストール: https://math-comp.github.io/installation.html
vscoq: https://github.com/coq/vscoq

vscodeでリッチな環境が用意されてるのはLeanだけでは無かった様です。

wuhu1slandwuhu1sland

Coq本進捗メモ(2024/10/22(火))

  • 2.1 (2024/11/9追記)
    • サブゴールの一番右を除いたものが、スタック
  • 2.2 モーダスポネンスの形式化
    • もだぽね〜(挨拶)
  • 2.3 ヒルベルトの公理Sの形式化
wuhu1slandwuhu1sland

Coq本進捗メモ(2024/10/26(土))

  • 2.4
    • 自然数と和の形式化
      • 和の交換則addnCの型が(ssrfun.commutative addn)であることを知り、addnCが使われている部分をssrfun.commutative addnに置き換えてみようとしてエラーを出す(当たり前)
        • 証明してない補題を使えるわけない

      • applyでの補題適用が十分条件への変換であったのに対し、move / は必要条件へ変換します。

        • なるほど?
  • 2.5
    • 論理式の形式化
      • Inductive(帰納的)に定義された/\と\/の理解に時間がかかった
      • やっぱりcaseがよくわからない
        • Natural Number Gameの時も雰囲気で使ってた
wuhu1slandwuhu1sland

Coq本進捗メモ(2024/11/9(土))

  • 3.1
    • 用語の整理
      • タクティク : サブゴールとコンテキスト間の型・変数・関数の移動を行う命令
        • 例: move, apply, case 等
      • タクティカル : タクティクと組み合わせて、タクティクの機能を変化させる命令
        • 例: =>, in, split 等
      • コマンド : タクティク、タクティカル以外の命令の総称。スクリプトを構成する行の先頭に書く
        • 例: Definition, Lemma, Variable 等
      • クエリ : Coqへの一時的な問い合わせ。スクリプト完成時には削除する
        • 例: Print, Check, Compute 等
  • 3.2 move=>,move:, move: => 等
    • 所謂popとpush
  • 3.3 apply, apply=>, apply: => 等
    • (P -> Q) -> QをPに変形するのがapply
      • つまり、トップ以下のサブゴールに対してトップを適用
  • 3.4 case, case=>, case:, case: =>, case => [|] 等
    • 帰納的型の構成子に関する場合分けを行う
      • 例: natの場合、0とSによって構成されているのでn : natが0とS nに変化したサブゴールがそれぞれ作られる
      • ようやくcaseの動作が分かってきた
  • 3.5 elim, elim=>, elim:, elim: =>, elim=> [|] 等
    • 帰納的型で定義された証明項に対して、帰納法によるサブゴールの変形を行う
      • caseは場合分け、elimは帰納法
      • natの例で言うと、elimを使うとS nの方のサブゴールの前提にnでの成立が加わる
  • 3.6 rewrite, rewrite -, rewrite (_: ...=... ) 等
    • 等式を表す要素名を受け取り、サブゴール内のその等式の左辺と一致するものを右辺の要素に置き換える
      • あくまで等式の置き換え
  • 3.7 move/, apply/, case/ 等 (ビュー機能)
    • SSReflectの機能
    • トップやサブゴール全体に、同値な関係への置き換えや必要条件への置き換え、リフレクションなどを行う
    • 3.7.10 リフレクション
      • Prop型とbool型の交換・変換
      • コアーション
        • Coqによって暗黙的に加えられる関数
        • is_trueコアーションはbool型をProp型のように扱うことを可能にする
      • ポアンカレ原理
        • 推論よりbool計算の方が速い的な

色々と疑問が解消された点があり嬉しい
3章の内容の一部を切り出してまとめて別の記事にしてもいいかも
5章から実践編のよう