Lean をいじる

Lean をいじります。

Lean の公式サイトを見ると、macOS を使っているあなたは VSCode の拡張機能の lean4 というやつをインストールして、ごにょごにょせよと書いてあったのでその通りにして、アプリケーションウィンドウの右上方に現れる全称量化子をクリックして、Documentation から Show Setup Guide をクリックする。羅列された ToDo リストの中にインストールする項があるのでクリックすると Lean 4 のバージョンマネージャーと Lean 4 がインストールされた。Prerequisites は Homebrew と Git と curl。

全称量化子をクリックして、New Project から Create Standalone Project をクリックしてプロジェクト名とディレクトリの場所を決定し、作成し開く。

そもそも Lean がなにか説明していなかったが

• プログラミング言語 (programming language)
• 定理証明器 (theorem prover)

としての利用が想定されているソフトウェアである。

プログラミング言語としても、定理証明器としても興味があるので双方を勉強していくつもり。

プロジェクトの構造はこうなっている。

$ tree .
.
├── Main.lean
├── README.md
├── TestLean4
│   └── Basic.lean
├── TestLean4.lean
├── lake-manifest.json
├── lakefile.lean
└── lean-toolchain

2 directories, 7 files

プログラミング言語としての方を先に学ぶことにする。よく分からないが、Main.lean の適当なところに

#eval 1 + 2

と書くと Lean Infoview タブに結果が表示される。

函数は String.append "Hello, " "Lean!" のように半角スペースで繋いで引数を渡すタイプの言語のようだ。優先順位は半角丸括弧で区切る。

Lean の表現は評価される前に型がついていなければならない。Nat は \mathbb{N}_0。自然数のデフォルトの型は Nat なので、1 - 2 は 0 と評価される。整数として扱いたいときは (1 - 2 : Int) とする。

表現を評価せずに型だけ調べたいときは、#eval ではなく #check を使う。

名前に表現＝値を定義するときは、

def message := "Hello!"

とする。型を指定するときは、

def message : String := "Hello!"

とする。名前はそのままで（Unix shell とか Perl と違って）その表現の意味になる。

def message := "Hello!"
def lean : String = "Lean"
#eval String.append message (String.append " " lean)

Lean では名前を定義した後でしかその名前は使えない。

函数の定義と利用はこんな感じ。

def add1 (n : Nat) : Nat := n + 1

#eval add1 7

def maximum (n: Nat) (k : Nat) : Nat := if n < k then k else n

#eval maximum (5 + 8) (2 * 7)

Haskell みたいに函数はカリー化される。

型も表現なので新しい名前の表現として型を定義できるが、Lean は数値リテラルをオーバーロードしているので、

def NaturalNumber : Type = Nat
def n : NaturalNumber = 42

はエラーになる。

とりあえず、名前を略したいなら def ではなく abbrev を使う。

合成型 (C++ の struct とか Rust の struct)を作るには、

structure Point where
  x : Float
  y : Float
deriving Repr

みたいにする。Float は浮動小数点型。deriving Repr は Python の __repr__ とか Rust の [#derive(debug)] とか Julia の Base.show みたいなやつ。

使うときは以下のようにする。

def origin : Point := { x := (0 : Float), y := (0 : Float) }

#eval origin
#eval origin.x
#eval origin.y

要素のアクセスは Python とか Rust とかと同じ。

型決定できない場合は

{ x := 0.0, y := 0.0 } : Point

などと書く。

{ x := 0.0, y := 0.0 : Point}

という記法がその別記法として使える。

以下の２つの定義は同じ。

def zeroX1 (p : Point) : Point :=
  { x := 0, y := p.y }

def zeroX2 (p : Point) : Point :=
  { p with x := 0 }

全ての構造体は構築子を持つ。任意の名前 S について、デフォルトでは構造体 S の構築子は S.mk である。

構築子を直接使って構造体の表現を作れるが、良くないスタイルとされる。

Point.mk 1.0 2.0

構築子の名前は違うものを使用できる。

structure Point where
  point ::
  x : Float
  y : Float
deriving Repr

構築子以外に到達子も作成される。

#check (Point.x)
#eval Point.x origin
#eval Point.y origin

• sum type := datatype that allows choices
• recursive datatype := datatype that can include instances of itself
• inductive datatype := recursive sum type

Bool は inductive datatype として定義されているようだが、sum type なのは分かるが、recursive datatype である理由が分からない。

ターミナルから lean を呼び出そうとしたが見つからない。Fish を使っているせいかと思って Bash にしても見つからない。どこにインストールされているんだ？

Zulip で尋ねたら、$HOME/.elan/bin 以下にインストールされるようだ。シェルのパスを通したら使えるようになった。