定理証明支援系Leanのソースを表示

Leanは、比較的新しい定理証明支援系（Lean以外にはCoqやIsabelleなどがある）である。

== 概要 ==

学術研究用なのもあって特にメジャーバージョンアップでは大きな破壊的変化がある。

Lean2以前はよく調べていないがLean2にはHoTTサポートがあって3で無くなったらしい。3→4ではマクロシステムが刷新されたり、Leanの処理系のうちLean自体で書かれた部分がさらに増えたり？した。

<span id="lean3"></span>
=== Lean3 ===

[https://leanprover.github.io/ 公式]（githubでの名前はleanprover）と、[https://leanprover-community.github.io/ 半分公式みたいなコミュニティ]（githubでの名前はleanprover&#45;community）があって、公式では3.4.2まででアーカイブされているLean3もコミュニティversionでは3.47.0くらいになっている。また様々な分野の証明を集めたライブラリの[https://github.com/leanprover-community/mathlib mathlib]もコミュニティの成果物である。

もうほとんど使われていないだろう。

<span id="lean4"></span>
=== Lean4 ===

Lean4は現在のところ「公式」のみで扱われている。手元では、WindowsとMacではしばらく動かなかったが、2022年9月中旬頃にelanが1.4.2になったタイミングで動くようになった。しかしVSCode拡張は大文字/小文字の区別をうまく扱えずGo to definitionが失敗する（大文字/小文字の区別があるファイルシステムではおそらく問題なし？？）。既知のバグ。 や など。

VSCodeでの体感でもチェッカがLean3より明らかに速くなった。

== 学習用リソース ==

<span id="lean3-1"></span>
==== Lean3 ====

[https://leanprover-community.github.io/learn.html https&#58;//leanprover&#45;community.github.io/learn.html]にリストされている。

最も基本的な使い方の解説が[https://leanprover.github.io/theorem_proving_in_lean/ Theorem Proving in Lean]であり、Leanを使って定理証明をする方法の概略が掲載されている。とりあえずはこれを読んでいけばいい。比較的よくまとまった資料であるが、Curry&#45;Howard同型についてなど、型理論や証明論の事前知識が多少はないと読むのはやや大変かもしれない。そのあたりの知識から解説しているものもいちおう上記の一覧にある。

各tacticの動作など、辞書的な説明は[https://leanprover.github.io/reference/ reference manual]に載っている場合もあるが、こちらは未完成である。

Programming in leanというのもあるが、これも少なくとも最近はあまりメンテナンスされていない。

<div style="overflow:auto;width: 100%; max-width: 1200px; white-space:nowrap; border:1px solid; padding-left: 10px; padding-right: 10px;" class="mw-collapsible">
<div>Programming in leanに関する詳細</div>
<div class="mw-collapsible-content">

これまた未完成ではあるが[https://avigad.github.io/programming_in_lean/index.html Programming in Lean — Programming in Lean 3.4.2 documentation]を見ると説明が載っているかもしれない。programming in leanで検索すると、

[https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf https&#58;//leanprover.github.io/programming_in_lean/programming_in_lean.pdf]

[https://leanprover.github.io/programming_in_lean/ https&#58;//leanprover.github.io/programming_in_lean/]

（この2つは同じ内容）

も出てくるが、こちらはリポジトリ([https://github.com/avigad/programming_in_lean avigad/programming_in_lean])と比較すると古いバージョンのようである（リポジトリの”old”フォルダの内容に対応している）。

</div></div>

<span id="lean4-1"></span>
==== Lean4 ====

前述の各資料に対応して[https://leanprover.github.io/theorem_proving_in_lean4/title_page.html https&#58;//leanprover.github.io/theorem_proving_in_lean4/title_page.html]と[https://leanprover.github.io/lean4/doc/ https&#58;//leanprover.github.io/lean4/doc/]と[https://leanprover.github.io/functional_programming_in_lean/ Functional Programming in Lean]がある。

<span id="publications"></span>
== Publications ==

関連論文など

[https://leanprover.github.io/publications/ https&#58;//leanprover.github.io/publications/]

== 日本語情報 ==

[https://turgenev.hatenablog.com/entry/2020/11/25/095208 定理証明支援系Leanのインストールと初期設定（Linux）]（自分で書いたが、古いのでもう読まなくていい）

[https://manau.jp/lean/leaninstall/ 定理証明支援系 LEAN のインストール]

[http://myuon-myon.hatenablog.com/entry/2016/01/09/212750 Theorem Prover Leanの紹介 &#45; Just $ A sandbox]

[https://myuon.github.io/posts/start-learning-proof-assistant/ 定理証明リンク集]

くらい。あんまりないが、順調にいけば今後増えていきそうではある。

* 2025/6追記 最近はもっと増えてそう

== metaprogramming関連 ==

Leanの証明記述用言語（tactic）は、Leanそれ自体の上で実装されている。バージョン3→4によってさらにその傾向が強まりそうである。

tacticはmonadicな関数として実装されている。tacticをmonadで表現するというのはCoq用のMtac&#91;^ziliani2013Mtac&#93;などでも採用された手法である。

<span id="lean3での例"></span>
=== Lean3での例 ===

筆者は研究活動の一環として、Lean 3のソースコード上に構造的に関連付けられた形でコメントを書けるようにするライブラリであるNtac（[https://github.com/ge9/ntac https://github.com/ge9/ntac]）を公開している。これはLean 3のmetaprogrammingを活かした例である。

metaprogrammingについてはコミュニティのLearning resourcesの”Metaprogramming and tactic writing”の項目や[https://leanprover.github.io/papers/tactic.pdf https&#58;//leanprover.github.io/papers/tactic.pdf]を参考にした。また、独自のtacticシステムを作成するためのガイドとして、[https://leanprover-community.github.io/archive/stream/113488-general/topic/no.20lean.20messages.20output.20in.20hacked.20mode.html https&#58;//leanprover&#45;community.github.io/archive/stream/113488&#45;general/topic/no.20lean.20messages.20output.20in.20hacked.20mode.html]に実装上のヒントを得た。

* 基本的には、<code>tactic</code>という名前でStateモナドが定義されていて、各tacticはこのモナド値を返す関数として定義されている。しかし<code>tactic</code>は<strong>現在の状態</strong>しか持っておらず、コメントを紐づけたりするには証明の<strong>過程まで含めた全体の構造</strong>が欲しい。そこでntacでは、<code>tactic</code>の定義を変更して証明の「履歴」を木構造として保持するようにした<code>ntac</code>というモナドを定義し、既存のtacticを（適切な）<code>ntac</code>モナド値を持つような定義に変更した。

<span id="lean4-2"></span>
=== Lean4 ===

Schemeを参考に、強力な衛生的（hygienic）マクロシステムが実装された。柔軟なNotationの定義ができるようになる。論文としては&#91;^ullrich2020Notations&#93;に詳しく書いてある。

上記「ntac」のLean4版は現在開発中。構文解析中に外部のプログラムを呼び出すなど、なんでもできて面白い。

==== 例 ====

* replしてる例らしい [https://github.com/leanprover-community/repl https://github.com/leanprover-community/repl]

==== tacticの移行とか ====

Lean3までの証明（のうちtacticで書かれたもの）をLean4に移植する方法について。<br />
[https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20porting.20assignments/near/296694161 https&#58;//leanprover.zulipchat.com/&#35;narrow/stream/287929&#45;mathlib4/topic/Tactic.20porting.20assignments/near/296694161]

* とりあえず [[error_private_page|error_private_page]]  で基礎知識を得るのがよさそう？

== elan ==

* leanを管理（各バージョンのインストール/アンインストールなど）するためのツール
* 適当にフォルダだけ消すとtoolchainの再インストールで引っ掛かるので、update&#45;hashesも消すとよいかも
* rustupのforkらしい [https://zenn.dev/labbase/articles/b24dca38e0420d 関数型言語”兼”定理証明支援系Leanの環境構築]

<span id="lean3-2"></span>
== Lean3 ==

[https://leanprover-community.github.io/get_started.html https&#58;//leanprover&#45;community.github.io/get_started.html] を読む。elanってやつが入れば大丈夫で、mathlib&#45;toolsとかleanprojectは（今はもう案内ないか？）無視でいい（後述）

=== パッケージ ===

Leanでの開発はまずパッケージを作るところから始まる。

leanpkg.tomlっていうメインの管理ファイルがあって、ここにLeanのバージョンとかを指定しておくと、無ければ（VS Codeでフォルダ開くタイミングとかで）自動でelanが取ってきてくれる

* 特定パッケージと、そのパッケージに依存するパッケージの双方を依存関係として指定したとして、バージョンの齟齬があったら何が起きるのかは不明である。ちなみにLean4の話だが、mathlib4に関しては[https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4]に「If your project depends on <code>std4</code> or <code>quote4</code>, let <code>mathlib4</code> pull them transitively. That is, don&#39;t <code>require</code> them on your <code>lakefile.lean</code>」と明記されている。

=== mathlib ===

パッケージの一つ。半分標準のライブラリみたいなもの。数学の定理やリスト処理のプログラムなど、色々なものが形式化されている。文字列処理とかの便利関数も入ってるのでとりあえず入れて損はない

[https://leanprover-community.github.io/mathlib-overview.html https&#58;//leanprover&#45;community.github.io/mathlib&#45;overview.html]

=== mathlibの指定 ===

leanpkg.tomlで

<syntaxhighlight lang="javascript">mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "lean-3.49.1"}</syntaxhighlight>
のように指定しておくと

<syntaxhighlight lang="javascript">leanpkg upgrade</syntaxhighlight>
でlean&#45;3.49.1ブランチを取ってきてくれる。masterブランチ指定とかするとバージョンアップで互換性がなくなって困るのでこれがおすすめ。

=== mathlib&#45;toolsとleanprojectについて ===

* 基本Lean3用なのでもう使われないかも

leanprojectは[https://github.com/leanprover-community/mathlib-tools mathlib&#45;tools]の一部で、mathlibをうまく扱うのが目的っぽい。<code>python3 &#45;m pip install mathlibtools</code>で入る

prebuiltされた（ちなみに自前でビルドすると数時間かかる）mathlibを

<syntaxhighlight lang="javascript">https://oleanstorage.azureedge.net/mathlib/xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.tar.xz</syntaxhighlight>
（xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxはコミットID）からダウンロードして、oleanにtouchして最新版にしてくれるが、<strong>それだけの機能しかなく、動作もあまり分かりやすくない</strong>。しかもよくわからんが、Lean4には未対応っぽい（というか、mathlibというのはLean3のパッケージの名前なのでそれはそうか（Lean4用のmathlibはmathlib4））。このまま使われなくなりそう。

そこで、自分でそれをやるスクリプトを書いてpathに登録した。これで十分と感じる。

<syntaxhighlight style="margin-bottom:0.2em;" lang="javascript">#!/bin/sh
if ! cd ../../../_target/deps/mathlib ;then
echo "must be run in 'mathlib' folders.  exiting."; exit
fi
find src -name "*.olean" | xargs rm
curl -o olean.tar.xz https://oleanstorage.azureedge.net/mathlib/`cat .git/HEAD`.tar.xz
#touch all .olean (this is also done by leanproject in mathlib-tools)
find src -name "*.olean" | xargs touch
if tar xvf olean.tar.xz ; then
rm -f olean.tar.xz
fi</syntaxhighlight>
<div style='text-align: center;'>new-oleans.sh</div>

<span id="lean4-3"></span>
== Lean4 ==

=== 初期設定 ===

[https://github.com/leanprover/elan elan]をまず入れてそれからLeanを、ってのがv3以前のやり方だったと思うが[https://leanprover.github.io/lean4/doc/quickstart.html Setting Up Lean &#45; Lean Manual]によるとどうやらv4はVS Code拡張経由で入れられるようである。

<span id="パッケージlake"></span>
=== パッケージ(lake) ===

<code>lake new フォルダ名（この中にパッケージができる）</code>、または<code>lake init パッケージ名（パッケージはカレントディレクトリに作成される）</code>を実行。詳しいやり方は[https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4] とか。

lakeのドキュメントはここ [https://github.com/leanprover/lean4/tree/master/src/lake https&#58;//github.com/leanprover/lean4/tree/master/src/lake]

dependencyの書き方は [https://github.com/leanprover-community/mathlib4/blob/master/lakefile.lean https&#58;//github.com/leanprover&#45;community/mathlib4/blob/master/lakefile.lean] とかを参考に。stdのURLがここにある。

=== mathlib4 ===

prebuiltされたものの提供はないっぽい。[https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20use.20prebuilt.20release.3F https&#58;//leanprover.zulipchat.com/&#35;narrow/stream/287929&#45;mathlib4/topic/.E2.9C.94.20use.20prebuilt.20release.3F]

* いや、[https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4]を読むと、<code>lake exe cache get</code>で取ってこれるように最近なった？

そのかわりlake build Mathlibと打てば（lean3のmathlibに比べて）割とすぐにビルドが終わる（5分前後？）

<syntaxhighlight lang="javascript">require ml4 from git "https://github.com/leanprover-community/mathlib4" @ "master"</syntaxhighlight>
↑依存パッケージとしてはこういうふうに書くが、lake build ml4ではなくlake build Mathlibが正しいっぽい。

* そもそも、require ml4じゃなくてrequire <strong>mathlib</strong>と必ず書かなきゃいけない説もある
[[Category:IT]]{{#seo:|title={{FULLPAGENAME}} - Turgenev's Wiki}}