Chapter 02: Lean の基本構文・型・データ構造¶

この章では，Lean のファイルを読むために必要な基本語彙を整理します．前章では命題論理・述語論理の証明規則を見ました．ここでは，それらの証明を書くための「言語としての Lean」を見ます．

扱う内容は次の通りです．

コマンドと式
def，fun，example，theorem，lemma
variable，section，引数に現れる ( )，{ }，[ ]
notation
Prop，Type，Sort と universe
関数型・依存関数型
inductive 型，structure，class
Chapter 01 で使った論理記号の実体
namespace，open
abbrev
積，直和型（非交和），Option，List などのデータ構造
if，match，let，do などの制御構文

Lean では「プログラム」と「証明」は同じ構文で書かれます．自然数を返す関数も，命題の証明も，どちらも型をもつ項です．したがって，Lean のファイルを読むときは，まず「いま見ているものは環境に名前を追加するコマンドなのか，それとも型をもつ式なのか」を区別すると見通しがよくなります．

もう 1 つ重要なのは，「型」と呼ばれているものをいくつかの観点に分けて見ることです． Prop や Type は型が住む階層です． α → β や ∀ x : α, P x は関数型・依存関数型です． Nat，List α，Option α，P ∨ Q，∃ x, P x は inductive 型です． α × β，P ∧ Q，Subtype は structure として実装された積型です． LE α や Add α は型クラスで，≤ や + の意味を型ごとに与えます．

この章では，Chapter 01 で使った And，Or，Eq，LE，LT，True，False，Not，Exists，∀ なども，単なる論理記号ではなく，Lean の具体的な定義・構文・型クラスとして見直します．

namespace Chapter02