Zenn
🦆

Lean 入門

に公開
lean4
tech

書籍「ゼロから始める Lean 言語入門」を買ったので試してみることにしました。

インストール

書籍には Lean 処理系のインストール方法がはっきり載っていなかったので書きます。（Macの場合のみ。なお　MacOS は Ventura 13.7.8 です。）

Leanのサイト のトップページに install ボタンがあるので押します。
Step 1 で VS Code を入れろ (Install VS Code) と言われます。VS Code は既にインストール済みなのでここはスキップ。
Step 2 で Lean 4 VS Code 拡張を入れろ (Install the extension) と言われます。

  • VS Code 画面左の、機能拡張のアイコンを押す
  • "Lean 4" を検索してインストールを押す
  • 画面右上にの "∀" のアイコン → New Project → Create Standalone Project (プロジェクト名に "LeanBook" を指定)
  • Elan がインストールされていないと表示されるのでインストール
  • その後、lean:stable がインストールされていないと表示されるのでインストール (lean 4.22.0 がインストールされた)
  • プロジェクトを開く

NaturalNumber.lean

書籍 p.15 の自然数のところをやってみます。

  • LeanBookフォルダ下に FirstProof フォルダを作って、その中に NaturalNumber.lean というファイルを作る。
  • 下記の内容を書き込む
inductive MyNat where
  | zero
  | succ (n: MyNat)

#check MyNat.zero
#check MyNat.succ
  • VS Code 上で、｀MyNat.zero｀ の上にカーソルを持っていくと ｀MyNat.zero : MyNat｀ と表示されます。

という訳で、書籍 p.17 の記述通り動いているので、ひとまず環境構築は成功したものと考えます。

lakefile.toml → lakefile.lean

書籍では p.23 に lakefile.lean ファイルを作ると書かれていますが、既に lakefile.toml ファイルが存在しています。Grok にファイルを変換してもらったので、lakefile.lean を新規作成して lakefile.toml を消します。

lakefile.toml
name = "LeanBook"
version = "0.1.0"
defaultTargets = ["leanbook"]

[[lean_lib]]
name = "LeanBook"

[[lean_exe]]
name = "leanbook"
root = "Main"
lakefile.lean
import Lake
open Lake DSL

package "LeanBook" where
  version := "0.1.0"
  defaultTargets := #["leanbook"]

lean_lib "LeanBook" where
  -- ライブラリの設定（デフォルト設定で十分な場合、追加のプロパティは不要）
  name := "LeanBook"

lean_exe "leanbook" where
  root := "Main"

が、lakefile.lean でエラーが出ます。という訳で toml から lean への書き換えはひとまず断念。書籍 2.2.6 節の設定はひとまず諦めます。

あるいはプロジェクト管理とかに関しては VS Code からではなく書籍のように CLI で行うべきかもしれません。一応、CLI ツールも使えるみたい。

$ which lake
~/.elan/bin/lake
$

あとは書籍の通りにやってみて、上手くいかないことがあればまた報告します。

Discussion