Mathematics in Lean4 もいよいよ第6章まできました。「6.1 構造の定義」は今までの知識があればとても簡単に読み進むことができました。いわゆるレコード型のような構造およびそのレコード型に付随する関数（演算）、そしてレコード型の各フィールドあるいは各フィールド間で成り立つ命題（一種の制約ですね）をまとめて定義できるわけです。
そのレコード型のインスタンスを生成する関数を定義する場合、新たに生成されたインスタンスで制約が成り立つ必要があります。実際にその生成関数が正しくインスタンスを生成できていることを証明する必要があります。つまりインスタンスを生成するにあたり生成関数として各フィールドの値の計算方法を示すとともにその計算方法で制約が満たされていることの証明もつけなければなりません。ここはLean4らしいところだと思います。従来のオブジェクト指向言語に制約をつけたような言語では生成したインスタンスが制約を満たすことの保証はプログラマに委ねられてきた（及びせいぜい実行時のチェック程度）と思うからです。
まあとはいえ「6.1 構造の定義」はほぼ自明なことばかりで楽しく読み終わったのです。
「6.2 代数構造」では、6.1で学んだ構造を使って代数構造を定義する方法を学びます。いきなりギアが上がりました！典型的な例として、群(Group)を演算mul, one, inv及びそこに成り立つ制約(mulの結合法則、oneが左右単位元であること、invがmulでの左逆元を計算すること)を一まとまりの構造として定義できます。
structure Group₁ (α : Type*) where
mul : α → α → α
one : α
inv : α → α
mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
mul_one : ∀ x : α, mul x one = x
one_mul : ∀ x : α, mul one x = x
mul_left_inv : ∀ x : α, mul (inv x) x = one
またこのような抽象的な群の構造に対して適当な集合の要素とその間の関係を定義することで具体的な群を作ることができます。例えば２次元の点の集合に加法を演算として導入すると２次元の点の集合は群をなします。その結果、一般的な群で成り立つ全ての定理は２次元の点の集合でも成り立ちます。Lean4ではこの２つの群の定義の間を適切な記法で繋ぐことで群の各種定理を丸ごと２次元の点の集合に持ってくることができます。この辺をちゃんと理解して次の記事で紹介できればと思います。
