Leanとは
Leanは普通の関数型言語であり、なおかつ定理証明支援系でもある大変パワフルな言語です。つまり原理上実行前にわかる性質は、型に埋め込んだり、頑張って自分で証明したりすることができます。そう考えるとワクワクしてきますね！
またコンパイラフロントエンドのAPIを自由にユーザーが使えるので、標準の文法や意味論とまったく同じレベルで自分の拡張を安全に仕込むことができるという、強力な拡張性を持つおもしろい言語でもあります。
今回紹介するLeanの環境構築は、lean4とよばれているバージョンのもので、lean3という古いバージョンとは異なります。
elan
開発環境の構築にはLean Manualのセットアップにしたがって、開発環境管理コマンドであるelanのインストールから始めます。
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
elanはRustでいうrustup、Haskellでいうghcupで、lakeなどの必要なコマンドのインストール・アップデートを担当します。（ちなみにelanはrustupのforkだそうで、rustupを使っているなら見慣れたプロンプトが表示されると思います）
LinuxやmacOSでは上記のコマンドですが、Windowsやbrew、Nixでは別途インストール方法があるようです。
また、VSCodeではlean4の拡張をインストールするときに、Install Lean using Elanボタンを押すだけで裏でelanが走ってくれるようです。
lake
lakeはプロジェクト管理コマンドで、プロジェクトを新規作成したりビルドしてくれたりします。Rustでいうcargo、Haskellでいうstackやcabalです。
$ lake new leanhello
でプロジェクトの新規作成ができ、
$ tree
.
├── Leanhello.lean # ライブラリのソースコード
├── Main.lean # 実行ファイルのソースコード
└── lakefile.lean # 依存や設定など、このプロジェクトを管理するファイル
0 directories, 3 files
このようにプロジェクトを初期化できます。試しにMain.leanをのぞいてみると、
import Leanhello
def main : IO Unit :=
IO.println s!"Hello, {hello}!"
このようにHello worldと、プロジェクトのライブラリ（Leanhello）をインポートするコードが書いてあります。
エディタのセットアップ
leanのコンパイラはLSPをしゃべるので、原理上どのエディタでもセットアップは簡単で、同じ機能がつかえます。（定義ジャンプやエラー一覧の表示とジャンプ、補完など）
VSCodeでは、最初に拡張を入れた時点でセットアップは終わるのでやることはないです。
筆者はEmacsを使うため、lean4-modeをインストールしました。（lean-modeというのがmelpaにありますが、古いlean3用なので使いません）
(leaf lean4-mode
:el-get "leanprover/lean4-mode"
)
VSCodeに出るものと同様のInfoView（カーソル位置に該当する証明途中のゴールや型が表示されるパネル）はC-c TABかC-c C-iで表示されます。
またNeovim用にはlean.nvimがあり、開発も活発なようです。
終わりに
ここまでで環境構築は終わりです。興味のある公式ドキュメントを読みながらコードを書いたり証明を書いたりすると楽しいと思います。
-
Theorem Proving in Lean 4
- 例題つきのチュートリアルで、定理証明をやってみたい人によさそう
- 依存型、命題と証明、証明の記述方法、Leanの文法（型クラスなど）
- 有志の方々による非公式日本語版もある
-
Lean Manual
- 言語の概観を知るための資料
- 基本的な文法に加えて、言語拡張などのちょっと込み入った機能や、FAQ、開発者むけガイドなどもある
-
Functional Programming in Lean
- 普通にプログラミング言語としての使い方が書いてある
- 言語の概観やHello World、モナドトランスフォーマー、依存型を使ったプログラミング、パフォーマンスに関する話など
-
Mathematics in Lean
- 普通の数学を対象に、Leanで定理証明をする資料
- 最近lean3からlean4への対応が完了しており、
Theorem Proving in Lean 4よりも分量がある
-
A Lean 4 Metaprogramming Book
- Lean4はElaborationという強力なメタプログラミングの機能があり、コンパイラフロントエンド自体が大体このElaborationを使ってかかれている。この記事はその概略が書いてある
- 似たようなものを知らない人にとっては読むのがすごく大変と思われる
また、数学系のためのLean勉強会というイベントも2023/9/3に開催され るようです。GitHubで資料も公開されるようなので、数学に興味のある方はこちらに参加するのもいいかもしれません。 ました。リンク先にLeanのインストール方法や、Leanの基礎の解説スライドへのリンク、演習資料などがまとまっています。
他のLeanの記事
-
プログラミング言語Lean 4の現状
- この記事の半年前に書かれており、より詳しく書いてある
Discussion