Zenn
🍆

証明支援システムLeanに入門する #1

2023/10/26に公開
math
lean
証明支援
tech

はじめに

こんにちは．理学部数学科で代数学をしているハーツホーンです．本人です．
この記事は，証明支援システムLeanに入門する私の備忘録であり，学習メモです．

Leanとは

公式サイトによると，

Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.

Leanは関数型のプログラミング言語であり，正しく，保守のしやすいプログラムをかくことが得意だそうです．
重要なのはここからで，「Leanを対話的な証明支援システムとして使うこともできる」と言います．続きを読むと，「Leanには主に型と関数の定義が含まれており，それによって，プログラムの細かい部分よりも問題の領域やデータの操作に集中できる．」とあります．
つまり，正直何を言っているかあまりわからないので，早速環境を構築してチュートリアルに取り掛かろうと思います．

環境構築

環境構築については先人の記事がたくさんでてくるのでそちらにおまかせしようと思いましたが，備忘録として残しておくことにします．

処理系の用意

(https://lean-lang.org/download/)に

  • バイナリ
    • 安定版
    • Nightly
  • ソースコード

が用意されています．バイナリに関しては

  • Darwin(MacOS)
  • Linux
  • Windows

に向けてのものが用意されており，zipファイルをダウンロードするだけで使える形になっているのだと思います．
ただ，Leanにはelanというツールチェインマネージャが存在するようなので，今回はそれを使って環境を構築します．
今回僕はArchLinuxを使用しているのでInstallationの指示に従って，

$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

を実行します．

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation

特にカスタマイズすることもないので1を選択．最後に実行ファイルのパスを通すために

$ source $HOME/.elan/env

を実行すればelanの準備は完了です．この時点でLeanの処理系も問題なくインストールされてパスが通っており，

$ lean --version
Lean (version 4.1.0, commit a832f398b80a, Release)

で確認することができます．それと同時にlakeというプロジェクトマネージャもインストールされているらしく，

$ lake new tutorial-proj
$ ls tutorial-proj
lakefile.lean  lean-toolchain  Main.lean  TutorialProj  TutorialProj.lean

で無事にLakeプロジェクトを作成することができました．

余談

Lean3ではフロントエンドはC++で書かれていたようですが，Lean4では一新し，全てをLean4自身でセルフホストしているようです．また，処理系はLeanコードをCにコンパイルし，LLVM clangによりネイティブコードにしているという記事がありましたが，詳しく説明したものは見つかりませんでした．

エディタ関連

Leanは主にEmacsとVSCodeに対してコーディング環境のサポートをしているようだったので，今回はVSCodeの環境を構築します．lean4という拡張機能が用意されているのでそれをインストールします．事前にLean処理系のパスが通っていない場合ここで処理系も同時にインストールすることを提案してくれるみたいですが，今回は関係ありません．

LSP

LeanのコンパイラはLSP(Language Server Protocol)に対応しており，要するにLSPに対応しているエディタであればほとんど変わらない機能を提供できるということになります．僕は生粋のVimmerなので，今度機会があればVimでも環境を作ってみたいです．

拡張機能のインストールが終わったところで早速Main.leanを開いてみると，右側にLean Infoviewというタブが自動的に開かれました．恐らくこのタブで証明の状態を確認しながらコードを書き進めるという流れになるのでしょう．

次回，ようやくTutorialを開始します

Discussion