6. 構造体
現代の数学では，代数的な構造を本質的に利用しており，この構造はさまざまな状況下でインスタンス化されるパターンを内包しています．このような構造は定義方法と，特定のインスタンスを構築する様々な方法を提供します．
Leanはこのような構造に対する形式的な定義方法と，その扱い方に対応する方法を提供しています．Leanでの代数的な構造の例は Chapter 2 で説明した環や束ですでに見てきました．この章では，そこで見た不思議な角括弧の注釈 [Ring α] と [Lattice α] についても説明します．また，代数的構造を自分で定義して使う方法も紹介します．
技術的詳細を知りたい場合は， Theorem Proving in Lean [1] とAnne Baanenによる記事 Use and abuse of instance parameters in the Lean mathematical library にあたるとよいでしょう．
6.1. 構造体の定義
広義の意味において， 構造体 （structure）はあるデータの集まりについての仕様であり，場合によってはデータが満たすべき制約を伴います．構造体の インスタンス （instance）はこの制約を満たすような特定のデータを束ねたものです．例えば，点とは次のように3つの実数からなるタプルであると指定できます：
@[ext]
structure Point where
x : ℝ
y : ℝ
z : ℝ
@[ext] 注釈によって 外延性 （extensionality）として知られている，構造体の2つのインスタンスが等しいことを証明する定理が自動的に生成されます．
#check Point.ext
example (a b : Point) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) : a = b := by
ext
repeat' assumption
Point 構造体の具体的なインスタンスを定義することもできます．Leanではいくつかの方法で定義することができます．
def myPoint1 : Point where
x := 2
y := -1
z := 4
def myPoint2 : Point :=
⟨2, -1, 4⟩
def myPoint3 :=
Point.mk 2 (-1) 4
最初の例では，構造体のフィールドには明示的に名前が付けられています． myPoint3 の定義で参照されている関数 Point.mk は Point 構造体の コンストラクタ （constructor）として知られているものです．この名前は要素を構築するためのものであることから来ています．必要であれば build など別の名前を指定することもできます．
structure Point' where build ::
x : ℝ
y : ℝ
z : ℝ
#check Point'.build 2 (-1) 4
次の2つの例では構造体上の関数を定義する方法を示しています．2つ目の例では Point.mk コンストラクタを明示的に用いていますが，1つ目の例では簡潔にするために無名コンストラクタを使用しています．Leanは add の型から関連するコンストラクタを推測することができます．Point のような構造体に関連する定義や定理は，同じ名前の名前空間に置くことが通例です．以下の例では， Point 名前空間を開いているため， add の完全な名前は Point.add となります．名前空間が開かれていない場合，フルネームを使用する必要があります．しかし，無名の射影記法を使用すると便利な場合が多いことを思い出してください．無名の射影記法を使用すると， Point.add a b の代わりに a.add b と書くことができます．Leanは前者を後者として解釈しますが，これは a が Point 型を持っているからです．
namespace Point
def add (a b : Point) : Point :=
⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
def add' (a b : Point) : Point where
x := a.x + b.x
y := a.y + b.y
z := a.z + b.z
#check add myPoint1 myPoint2
#check myPoint1.add myPoint2
end Point
#check Point.add myPoint1 myPoint2
#check myPoint1.add myPoint2
以下のコードスニペットからは名前空間コマンドが除外されていますが，関連する名前空間に定義を置いていっています．足し算関数の性質を証明するために， rw を使って定義を展開し， ext を使って構造体の2つの要素間の等式をその構成要素間の等式に落とし込むことができます．以下では protected キーワードを使用して，名前空間が開いていても定理の名前が Point.add_comm になるようにしています．これは add_comm のような一般的な定理とのあいまいさを避けたいときに便利です．
protected theorem add_comm (a b : Point) : add a b = add b a := by
rw [add, add]
ext <;> dsimp
repeat' apply add_comm
example (a b : Point) : add a b = add b a := by simp [add, add_comm]
Leanは内部的に定義を展開し，射影を単純化することができるため，欲しい等式が定義的に成立することもあります．
theorem add_x (a b : Point) : (a.add b).x = a.x + b.x :=
rfl
Section 5.2 で再帰関数を定義した時と同じように，パターンマッチを使って構造体に対する関数を定義することもできます．以下の addAlt と addAlt' の定義は本質的には同じです；唯一の違いは，後者では無名コンストラクタを使用している点です．このような関数の定義方法は便利な場合もありますし，構造的にはη簡約によってこの代替的な定義と等価になりますが，この後の証明では使い勝手が悪くなります．特に， rw [addAlt] は match 文を含んだより面倒なゴールをinfoviewに残します．
def addAlt : Point → Point → Point
| Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩
def addAlt' : Point → Point → Point
| ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩
theorem addAlt_x (a b : Point) : (a.addAlt b).x = a.x + b.x := by
rfl
theorem addAlt_comm (a b : Point) : addAlt a b = addAlt b a := by
rw [addAlt, addAlt]
-- the same proof still works, but the goal view here is harder to read
ext <;> dsimp
repeat' apply add_comm
数学的な構成ではまとまった情報をバラバラにして，それをまた別の方法で組み立てることが多いです．そのためLeanとMathlibがこれを効率的に行う方法を数多く提供しているのは理にかなっています．演習として， Point.add が結合的であることを証明してみましょう．その後に点のスカラー倍を定義し，それが加算に対して分配することを示します．
protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by
sorry
def smul (r : ℝ) (a : Point) : Point :=
sorry
theorem smul_distrib (r : ℝ) (a b : Point) :
(smul r a).add (smul r b) = smul r (a.add b) := by
sorry
構造体を使用することは代数的抽象化への第一歩にすぎません．まだ Point.add を一般的な + 記号に結び付けたり， Point.add_comm と Point.add_assoc を一般的な add_comm と add_assoc の定理に結び付けたりする方法がありません．これらのタスクは，構造体を使用する際の 代数的な 側面に属しており，この実行方法については次節で説明します．今のところは構造体はオブジェクトと情報を束ねる方法だと考えてください．
構造体においてはデータ型だけでなく，データが満たすべき制約も指定できる点が特に便利です．Leanでは後者は Prop 型のフィールドとして表現されます．例えば， 標準2単体 （standard 2-simplex）は \(x ≥ 0\) ， \(y ≥ 0\) ， \(z ≥ 0\) および \(x + y + z = 1\) を満たす点 \((x, y, z)\) の集合として定義されます．もしこの概念に馴染みがなければ，絵を描いみてこの集合が \((1, 0, 0)\) ， \((0, 1, 0)\) ， and \((0, 0, 1)\) を頂点とする3空間の二等辺三角形とその内部であることを確かめてください．これをLeanで表すと次のようになります：
structure StandardTwoSimplex where
x : ℝ
y : ℝ
z : ℝ
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
z_nonneg : 0 ≤ z
sum_eq : x + y + z = 1
最後の4つのフィールドはその前にある3つのフィールド x と y ， z を参照している点に注目してください．この2単体について x と y を入れ替える2単体からそれ自身への写像を定義することができます：
def swapXy (a : StandardTwoSimplex) : StandardTwoSimplex
where
x := a.y
y := a.x
z := a.z
x_nonneg := a.y_nonneg
y_nonneg := a.x_nonneg
z_nonneg := a.z_nonneg
sum_eq := by rw [add_comm a.y a.x, a.sum_eq]
さらに興味深いことに，単体上の2点の中点を計算することができます．ここで実数上の除算を使うためにこのファイルの冒頭に noncomputable section というフレーズを追加しています．
noncomputable section
def midpoint (a b : StandardTwoSimplex) : StandardTwoSimplex
where
x := (a.x + b.x) / 2
y := (a.y + b.y) / 2
z := (a.z + b.z) / 2
x_nonneg := div_nonneg (add_nonneg a.x_nonneg b.x_nonneg) (by norm_num)
y_nonneg := div_nonneg (add_nonneg a.y_nonneg b.y_nonneg) (by norm_num)
z_nonneg := div_nonneg (add_nonneg a.z_nonneg b.z_nonneg) (by norm_num)
sum_eq := by field_simp; linarith [a.sum_eq, b.sum_eq]
ここでは x_nonneg と y_nonneg ， z_nonneg を簡潔な証明項で確立しましたが， sum_eq は by を使ってタクティクモードで証明しています．
あるパラメータ \(\lambda\) が \(0 \le \lambda \le 1\) を満たす場合，標準2単体の2点 \(a\) と \(b\) の加重平均 \(\lambda a + (1 - \lambda) b\) を取ることができます．上記の midpoint 関数になぞらえて，その関数の定義に挑戦してみましょう．
def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
(a b : StandardTwoSimplex) : StandardTwoSimplex :=
sorry
構造体はパラメータに依存することができます．例えば，任意の \(n\) に対して標準2単体を標準 \(n\) 単体に一般化することができます．現時点では型 Fin n が \(n\) 個の要素を持つことと，Leanがその和の取り方を知っていること以外は何も知る必要はありません．
open BigOperators
structure StandardSimplex (n : ℕ) where
V : Fin n → ℝ
NonNeg : ∀ i : Fin n, 0 ≤ V i
sum_eq_one : (∑ i, V i) = 1
namespace StandardSimplex
def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
where
V i := (a.V i + b.V i) / 2
NonNeg := by
intro i
apply div_nonneg
· linarith [a.NonNeg i, b.NonNeg i]
norm_num
sum_eq_one := by
simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib,
a.sum_eq_one, b.sum_eq_one]
field_simp
end StandardSimplex
演習問題として，2点の加重平均を標準 \(n\) 単体に対して定義できるか試してみましょう．ここで関連する合計の操作として Finset.sum_add_distrib と Finset.mul_sum を使うことができます．
構造体は，データとその性質を束ねるために使用できることを見てきました．興味深いことに，構造体はデータなしで性質を束ねることもできます．例えば，次の構造体 IsLinear は線形性についての2つの要素を束ねたものです．
structure IsLinear (f : ℝ → ℝ) where
is_additive : ∀ x y, f (x + y) = f x + f y
preserves_mul : ∀ x c, f (c * x) = c * f x
section
variable (f : ℝ → ℝ) (linf : IsLinear f)
#check linf.is_additive
#check linf.preserves_mul
end
構造体だけがデータを束ねる唯一の方法ではないことは指摘しておくべきことでしょう．データ構造 Point は一般的な型の積で定義することができ， IsLinear は単純な and で定義することができます．
def Point'' :=
ℝ × ℝ × ℝ
def IsLinear' (f : ℝ → ℝ) :=
(∀ x y, f (x + y) = f x + f y) ∧ ∀ x c, f (c * x) = c * f x
一般的な型の構築においては，構成要素間の依存関係を持つ構造体の代わりに使うこともできます．例えば 部分型 （subtype）構成はあるデータの一部とその性質を結合します．次の例の PReal 型は正の実数の型であると考えることができます．任意の x : PReal は2つの要素をもちます：すなわちその値とそれが正であることの性質です．これらのコンポーネントにアクセスすることができ， x.val は ℝ 型を持ち， x.property は 0 < x.val を表します．
def PReal :=
{ y : ℝ // 0 < y }
section
variable (x : PReal)
#check x.val
#check x.property
#check x.1
#check x.2
end
標準2単体を定義するために部分型を使うこともでき，また同じように任意の \(n\) に対する標準 \(n\) 単体も定義することができます．
def StandardTwoSimplex' :=
{ p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 }
def StandardSimplex' (n : ℕ) :=
{ v : Fin n → ℝ // (∀ i : Fin n, 0 ≤ v i) ∧ (∑ i, v i) = 1 }
同様に， シグマ型 （Sigma type）は順序対の一般化であり，2番目の要素の型は1番目の要素の型に依存します．
def StdSimplex := Σ n : ℕ, StandardSimplex n
section
variable (s : StdSimplex)
#check s.fst
#check s.snd
#check s.1
#check s.2
end
s : StdSimplex が与えられた時，第一成分 s.fst は自然数であり，第二成分は対応する単体 StandardSimplex s.fst の要素です．シグマ型と部分型の違いは，シグマ型の第二成分が命題ではなくデータであることです．
しかし，構造体の代わりに積，部分型，シグマ型を使うことができるとしても，構造体を使うことには多くの利点があります．構造体を定義することで，基礎となる表現が抽象化され，構成要素にアクセスする関数名をカスタムできます．これは証明をより頑強にします：構造体へのインタフェースにのみ依存する証明では一般的に，古いアクセサを新しい定義に基づいて再定義する限り，定義を変更しても機能し続けます．さらに，これから説明するように，Leanは構造体を豊かで相互接続された階層に編み上げることができ，それらの間の相互作用を管理するためのサポートを提供します．
6.2. 代数構造
一口に「代数構造」といっても本書に置いて何を意味するかということを明確にするために，ここでいくつか例を挙げましょう．
半順序集合 （partially ordered set）は集合 \(P\) と推移律と反射律を持った \(P\) 上の二項演算子 \(\le\) からなります．
群 （group）は集合 \(G\) に結合的な二項演算子と単位元 \(1\) ， \(G\) の各 \(g\) の逆元を返す関数 \(g \mapsto g^{-1}\) を加えたものから成ります．群が アーベル （abelian）もしくは 可換 （commutative）であるとは二項演算子が可換であることを指します．
束 （lattice）は交わりと結びを備えた半順序集合です．
環 （ring）は（加法的と言われる）アーベル群 \((R, +, 0, x \mapsto -x)\) に加法上に分配される結合的な乗法の演算子 \(\cdot\) と単位元 \(1\) を加えたものから成ります．環が 可換 であるとは乗法が可換であることを指します．
順序環 （ordered ring） \((R, +, 0, -, \cdot, 1, \le)\) は環に， \(a + c \le b + c\) が \(R\) のすべての元 \(a\) ， \(b\) ， \(c\) に対して成り立ち，また \(R\) のすべての元 \(a\) と \(b\) が \(0 \le a\) と \(0 \le b\) を満たすときに \(0 \le a b\) を成り立たせるような半順序を備えたものです．
距離空間 （metric space）は集合 \(X\) と以下を満たすような関数 \(d : X \times X \to \mathbb{R}\) から構成されます．
\(X\) の各 \(x\) と \(y\) に対して \(d(x, y) \ge 0\) となる．
\(d(x, y) = 0\) となるのは \(x = y\) かつそのときに限る．
\(X\) の各 \(x\) と \(y\) に対して \(d(x, y) = d(y, x)\) が成り立つ．
\(X\) の各 \(x\) と \(y\) ， \(z\) に対して \(d(x, z) \le d(x, y) + d(y, z)\) が成り立つ．
位相空間 （topological space）は集合 \(X\) と， \(X\) の 開集合 （open subsets）と呼ばれる以下を満たすような \(X\) の部分集合のあつまり \(\mathcal T\) から構成されます．
空集合と \(X\) は開集合である．
2つの開集合の交わりは開集合である．
任意の数の開集合の合併は開集合である．
これらの例では，各構造の元は 台集合 （carrier set）と呼ばれる集合に属し，この集合でその構造全体のことを指す場合もあります．例えば「 \(G\) が群である」と言ってから「 \(g \in G\) 」と言う時，私達は \(G\) をそれぞれ構造と台集合の意味として使っています．すべての代数構造がこのように1つの台集合に関連付けられるわけではありません．例えば 2部グラフ （bipartite graph）には ガロア接続 （Galois connection）のように2つの集合間の関係がふくまれます． 圏 （category）も一般に 対象 （object）と 射 （morphism）と呼ばれる2つの集合を中心として構成されます．
これらの例は代数的推論について証明支援系がサポートするにあたって必要なポイントをいくつか示しています．まず，構造の具体例を認識している必要があります．数体系 \(\mathbb{Z}\) と \(\mathbb{Q}\) ， \(\mathbb{R}\) はすべて順序環であり，順序環に関する一般的な定理をこれらのインスタンスに適用出来なければなりません．ある集合を何かしらの構造のインスタンスにする場合，複数の方法が存在する場合があります．例えば，実解析の基礎となる \(\mathbb{R}\) 上の通常の位相構造に加え，すべての集合が開である \(\mathbb{R}\) 上の 離散 （discrete）位相構造を考えることができます．
第二に，証明支援系は構造上の一般的な表記法をサポートする必要があります．Leanでは * という記法は通常の数体系での乗算に使われるだけでなく，一般的な群や環での乗算にも使われます．例えば f x * y のような式を取り扱う際には，Leanは f と x ， y の型に関する情報を用いて，どの乗法を考えているかを判断しなければなりません．
第三に，構造が他の構造から定義と定理，表記法を様々な方法で継承できるという事実に対処出来る必要があります．構造によっては公理を追加することで他の構造を拡張するものもあります．可換環は環でもあるので，環で成り立つ定義は可換環でも成り立ち，環で成り立つ定理は可換環でも成り立ちます．構造によってはデータを追加することで他の構造を拡張することもあります．例えば環の加法についての部分は加法群です．環の構造はこの加法的な部分に乗法とその単位元，およびそれらを支配・関連する公理を追加します．ある構造を別の構造で定義出来ることもあります．任意の距離空間にはそれに関連する正準位相である 距離空間位相 （metric space topology）があり，任意の線形順序に関連付けることができる様々な位相があります．
最後に，数学において数を定義するために関数や演算を使うのと同じように，構造を定義するために関数や演算を使うことができるということを覚えておくことが重要です．群の積と累乗もまた群です．すべての \(n\) に対して， \(n\) を法として合同な整数は環を形成し，すべての \(k > 0\) に対して，その環に係数を持つ多項式の \(k \times k\) 行列もまた環を形成します．このように，構造を使って計算することは，その要素を使って計算することと同じくらい簡単です．このことは代数的構造が数学に置いて対象のあつまりのためのコンテナとしてと，またそれ自身の対象としてとの二重の生活を送っていることを意味します．証明支援系はこの二重の役割に対応しなければなりません．
代数的構造を持つ型の要素を扱う時，証明支援系はその構造を認識し，関連する定義と定理・記法を見つける必要があります．この一連の流れはとても大変な作業のように聞こえるでしょう．しかし，Leanはこれらのタスクを実行するためには基本的な仕組みのうちのわずかなものしか使用しません．この節の目標はこれらのメカニズムを説明し，それらの使い方を紹介することです．
最初の素材はわざわざ言うほどではないほど明白なものです:形式的に言えば，代数構造は Section 6.1 の意味での構造です．代数構造はいくつかの公理的な仮説を満たすデータを束ねたものの仕様であり，これこそが structure コマンドが対応するように設計されていることを Section 6.1 で見ました．まさにこれ以上無いほどのお似合いの関係です！
与えられた α 型について，群の構造を以下のように α 上に定義することができます．
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
inv_mul_cancel : ∀ x : α, mul (inv x) x = one
ここで型 α は group₁ の定義における パラメータ （parameter）であることに注意してください．したがってオブジェクト struc : Group₁ α は α 上の群構造であると考えると良いでしょう．他の群の公理から inv_mul_cancel と対になる mul_inv_cancel が成り立つことは Section 2.2 で見たため，定義に追加する必要はありません．
この群の定義はMathlibの Group の定義と似ているため，区別するために本書のバージョンは Group₁ という名前にしました．もし #check Group と書いてその定義をctrlを押しながらクリックすると，Mathlib版の Group が別の構造体を拡張するように定義されていることがわかります．また， #print Group と入力すると，Mathlibバージョンの Group にはいくつかのフィールドが追加されていることがわかります．あとで説明しますが，構造体に冗長な情報を追加して，コアデータから定義できるオブジェクトや関数のフィールドを追加しておくと便利な場合があります．今は気にしないでください．本書の簡略版 Group₁ はMathlibが使用している群の定義と概念上は同じですのでご安心ください．
構造体に型を組み合わせることが便利である場合がときどきあるため，Mathlibは以下のような GroupCat 構造体の定義を有しています:
structure Group₁Cat where
α : Type*
str : Group₁ α
Mathlib版は Mathlib.Algebra.Category.GroupCat.Basic にあり，これをサンプルファイルの最初のimportに追加すれば #check することができます．
理由は後ほど明らかに成りますが，型 α と構造体 Group α を分けておいたほうが便利なことが多いです．このような2つの対象を合わせて 部分的に束ねられた構造体 （partially bundled structure）と呼びます．これは全てではないですが，多くの部分の成分を一つの構造に組み込む表現になっているからです．Mathlibでは群の台の型として使用する場合，型名としては大文字のアルファベット G を使用するのが一般的です．
さて，群を，つまり Group₁ 型の元を構成してみましょう．型 α と β の任意のペアに対して，Mathlibは α と β の間の 同値 （equivalences）を示す型 Equiv α β を定義しています．また，Mathlibはこの型に対して α ≃ β という示唆的な記法を定義しています．この型の要素 f : α ≃ β は α と β の間の全単射で，4つの要素で表現されます: α から β への関数 f.toFun ， β から α への逆関数 f.invFun ，そしてこれらの関数が互いに逆であることを示す2つの性質です．
variable (α β γ : Type*)
variable (f : α ≃ β) (g : β ≃ γ)
#check Equiv α β
#check (f.toFun : α → β)
#check (f.invFun : β → α)
#check (f.right_inv : ∀ x : β, f (f.invFun x) = x)
#check (f.left_inv : ∀ x : α, f.invFun (f x) = x)
#check (Equiv.refl α : α ≃ α)
#check (f.symm : β ≃ α)
#check (f.trans g : α ≃ γ)
最後の3つの構文の特徴的な命名に注目してください．恒等関数 Equiv.refl ，逆演算 Equiv.symm ，合成演算 Equiv.trans は全単射という性質が同値関係であることの明示的な証拠であると考えられます．
また， f.tans g は逆順に前方の関数を合成する必要があることにも注意してください．Mathlibは Equiv α β から関数型 α → β への 型の強制 （coercion）を宣言しているため， .toFun を書くのを省略して，代わりにLeanに入れてもらうことができます．
example (x : α) : (f.trans g).toFun x = g.toFun (f.toFun x) :=
rfl
example (x : α) : (f.trans g) x = g (f x) :=
rfl
example : (f.trans g : α → γ) = g ∘ f :=
rfl
また，Mathlibは α とそれ自身との間の同値性を示す perm α 型も定義しています．
example (α : Type*) : Equiv.Perm α = (α ≃ α) :=
rfl
この Equiv.Perm α が同値の合成で群を形成することは明らかでしょう． mul f g は g.trans f と等しく，これで導かれる関数は f ∘ g です．言い換えれば，乗法は通常，全単射の合成と考えられているもののことです．ここでこの群を定義します:
def permGroup {α : Type*} : Group₁ (Equiv.Perm α)
where
mul f g := Equiv.trans g f
one := Equiv.refl α
inv := Equiv.symm
mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm
one_mul := Equiv.trans_refl
mul_one := Equiv.refl_trans
inv_mul_cancel := Equiv.self_trans_symm
実際，Mathlibは GroupTheory.Perm.Basic というファイルの Equiv.Perm α でまさにこの Group 構造を定義しています．いつものように， permGroup の定義で使用されている定理にカーソルを合わせるとその命題を見ることができ，その元ファイルの定義元に飛んでどのように実装されているか見ることができます．
通常の数学では，表記法は構造に依存しないと考えるのが一般的です．例えば，群として \((G_1, \cdot, 1, \cdot^{-1})\) と \((G_2, \circ, e, i(\cdot))\) ， \((G_3, +, 0, -)\) を考えることが出来ます．最初のケースでは，二項演算を \(\cdot\) と，単位元を \(1\) ，逆関数を \(x \mapsto x^{-1}\) と書きます．2番目と3番目のケースでは，同様にそれぞれ先程示した表記法を使用します．しかし，Leanで群の概念を形式化する場合，表記法は構造とより密接に結びつきます．Leanでは任意の Group の構成要素は mul と one ， inv という名付けられます．これらを参照するために乗法の表記がどのように設定されているかはこの後すぐ見ていきます．もし加法の表記を使いたい場合は，代わりに同型な構造体 AddGroup （加法群の基礎となる構造体）を使います．この構成要素は add と zero ， neg という名前で，関連する記法も加法に対して想像される通りのものです．
Section 6.1 で定義した Point 型とそこで定義した加算関数を思い出してください．これらの定義はこの節に紐付いているサンプルファイルで再定義しています．演習として，上で定義した Group₁ 構造体に似た AddGroup₁ 構造体を定義してみましょう．続いて Point データ型に逆元と0を定義し， Point に AddGroup₁ 構造体を定義しましょう．
structure AddGroup₁ (α : Type*) where
(add : α → α → α)
-- fill in the rest
@[ext]
structure Point where
x : ℝ
y : ℝ
z : ℝ
namespace Point
def add (a b : Point) : Point :=
⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
def neg (a : Point) : Point := sorry
def zero : Point := sorry
def addGroupPoint : AddGroup₁ Point := sorry
end Point
さて，だいぶLeanにおいての代数構造について習熟してきました．Leanで代数的構造を定義する方法とそれらの構造のインスタンスを定義する方法も学びました．しかし，それらのインスタンスで使用できるように，表記法を構造に関連付けたいでしょう．さらに，構造に対する演算を定義し，それを特定のインスタンスで使えるようにもしたいです．また，同様に構造に関する定理を証明し，それを任意のインスタンスで使えるようにもしたいです．
実は，Mathlibはすでに Equiv.Perm α に対して一般的な群の表記，定義，定理を使うことができるように設定しています．
variable {α : Type*} (f g : Equiv.Perm α) (n : ℕ)
#check f * g
#check mul_assoc f g g⁻¹
-- group power, defined for any group
#check g ^ n
example : f * g * g⁻¹ = f := by rw [mul_assoc, mul_inv_cancel, mul_one]
example : f * g * g⁻¹ = f :=
mul_inv_cancel_right f g
example {α : Type*} (f g : Equiv.Perm α) : g.symm.trans (g.trans f) = f :=
mul_inv_cancel_right f g
上で定義した Point 上の加法群構造ではこれらが使えないことを確認してみましょう．ここからの課題は Equiv.Perm α の例を同じように動作させるために，その背後で行われている仕組みを理解することです．
問題は，Leanは私達が入力する式の中にある情報を使って関連する表記と暗黙の群構造を 見つける ことが出来る必要がある，ということです．例えば， ℝ 型の x と y で x + y という式を書く時，Leanは + という記号を実数上の加算関数として解釈する必要があります．また，可換環の定義や定理をすべて利用できるように， ℝ 型を可換環のインスタンスとして認識する必要があります．別の例として，Leanにおいて連続性は2つの位相空間の関係として定義されます． f : ℝ → ℂ があり， Continuous f と書く時，Leanは ℝ と ℂ 上の関連する位相を見つけなければなりません．
この魔法は以下の3つのものの組み合わせで実現されています．
論理 （Logic）．任意の群で解釈されるべき定義は，群の型と群構造を引数として取ります．同様に，任意の群の要素に関する定理は，群の型と群構造に対する普遍量化子から始まります．
暗黙的な引数 （Implicit arguments）．型と構造の引数は一般的には暗黙的なままにしておき，私達が書いたり，Leanの情報ウィンドウで見たりする必要がないようにします．Leanがこっそり情報を埋めてくれます．
型クラスの推論 （Type class inference）．もしくは クラス推論 （class inference）とも呼ばれるこのメカニズムは，Leanが後で使用する情報を登録できるシンプルで強力な仕組みです．Leanが定義，定理，表記法の一部に対する暗黙の引数を埋めるために呼び出された時，この登録された情報を利用することができます．
(grp : Group G) という注釈はLeanにその引数が明示的に与えられることを期待するように指示するのに対し， {grp : Group G} という注釈は，Leanにその引数を式の文脈から理解するように指示し， [grp : Group G] はLeanが型クラス推論を用いて対応する引数が統合されるべきであることを示します．このような引数を使うことの要点は，一般的に明示的に参照する必要がないということなので，Leanは [Group G] と書いて引数の名前を匿名にしておくことができます．このようにした場合，Leanが _inst_1 のような名前を自動的に選択することはすでにお気づきでしょう． variables コマンドで匿名の角括弧注釈を使用すると，変数がスコープ内にある限り，Leanは自動的に G に言及する定義や定理に引数 [Group G] を追加します．
Leanがこのような情報を検索するために必要な情報はどのように登録すれば良いでしょうか？群の例に戻ると，必要な変更は2つだけです．まず，群構造を定義するために structure コマンドを使用する代わりに，クラス推論の候補であることを示すキーワード class を使用します．次に，特定のインスタンスを def で定義する代わりに，キーワード instance を使用して特定のインスタンスをLeanに登録します．クラス変数の名前と同様に，一般的にLeanは細かいことで私達を悩ませることなく，これらの定義を見つけて使ってもらうことを意図しているため，インスタンス定義の名前を無名にすることが許されています．
class 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
inv_mul_cancel : ∀ x : α, mul (inv x) x = one
instance {α : Type*} : Group₂ (Equiv.Perm α) where
mul f g := Equiv.trans g f
one := Equiv.refl α
inv := Equiv.symm
mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm
one_mul := Equiv.trans_refl
mul_one := Equiv.refl_trans
inv_mul_cancel := Equiv.self_trans_symm
これらの使い方は以下のようになります．
#check Group₂.mul
def mySquare {α : Type*} [Group₂ α] (x : α) :=
Group₂.mul x x
#check mySquare
section
variable {β : Type*} (f g : Equiv.Perm β)
example : Group₂.mul f g = g.trans f :=
rfl
example : mySquare f = f.trans f :=
rfl
end
#check コマンドは Group₂.mul がクラス推論で見つかること期待される暗黙の引数 [Group₂ α] を持っていることを示しています．ここで α は Group₂.mul の引数の型です．言い換えると， {α : Type*} は群要素の型を表す暗黙の引数であり， [Group₂ α] は α 上の群構造を表す暗黙の引数です．同様に，一般的な二乗関数 my_square を Group₂ に対して定義する場合，要素の型には暗黙の引数 {α : Type*} を， Group₂ 構造には暗黙の引数 [Group₂ α] を用います．
最初の例では， Group₂.mul f g とかくと， f と g の型は Group₂.mul の引数 α として， Equiv.Perm β をインスタンス化しなければならないことをLeanに伝えます．つまりLeanは Group₂ (Equiv.Perm β) の要素を見つけなければならないということです．これにあたって上記の instance 宣言はLeanにその方法を正確に伝えています．これで問題は解決しました！
Leanが必要なときに見つけられるように情報を登録するこのシンプルな仕組みは驚くほど便利です．ここで一つの方法を紹介しましょう．Leanの基礎では，データ型 α は空であることがあります．しかし，実用にあたって多くの場合には型に少なくとも1つの要素があることを知っておくと便利です．例えば，リストの最初の要素を返す関数 List.headl はリストが空の場合にデフォルト値を返すことができます．これを実現するために，Leanのライブラリでは Inhabited α クラスを定義しています． Point 型がこのインスタンスであることを示すことができます:
instance : Inhabited Point where default := ⟨0, 0, 0⟩
#check (default : Point)
example : ([] : List Point).headI = default :=
rfl
クラス推論のメカニズムは，一般的な表記法にも使用されます．式 x + y は Add.add x y の省略形であり， Add α は —予想がつくでしょうが，— α 上の二項関数を格納するクラスです． x + y と書くと，Leanは [Add.add α] の登録されたインスタンスを見つけて，対応する関数を使うように指示します．以下では， Potin の加算関数を登録しています．
instance : Add Point where add := Point.add
section
variable (x y : Point)
#check x + y
example : x + y = Point.add x y :=
rfl
end
このようにして，他の型に対する二項演算にも + という表記を割り当てることができます．
しかしこれはさらに推し進めることができます．これまで， * はどんな群でも， + はどんな加法群でも，そしてどちらもどんな環でも使えていたことを見てきました．Leanで環の新しいインスタンスを定義するとき，そのインスタンスに対して + と * を定義する必要はありません．なぜならLeanはこれらがすべての環に対して定義されていることを知っているからです．この方法を使って Group₂ クラスの記法を指定することができます:
instance hasMulGroup₂ {α : Type*} [Group₂ α] : Mul α :=
⟨Group₂.mul⟩
instance hasOneGroup₂ {α : Type*} [Group₂ α] : One α :=
⟨Group₂.one⟩
instance hasInvGroup₂ {α : Type*} [Group₂ α] : Inv α :=
⟨Group₂.inv⟩
section
variable {α : Type*} (f g : Equiv.Perm α)
#check f * 1 * g⁻¹
def foo : f * 1 * g⁻¹ = g.symm.trans ((Equiv.refl α).trans f) :=
rfl
end
この場合，インスタンスの名前を指定しなければなりません．というのもLeanは既定のものとして適切なものを見つけるのが難しいからです．この方法が機能するのはLeanが再帰的な検索を行うからです．ここで宣言したインスタンスによると，Leanは Group₂ (Equiv.Perm α) のインスタンスを見つけることで Mul (Equiv.Perm α) のインスタンスを見つけることができます．そしてこの Group₂ (Equiv.Perm α) はその前に私達がインスタンスを提供しているためLeanはこれを見つけることができます．Leanはこれら2つの事実を見つけ，連鎖させることができます．
ここで挙げた例は危険です．なぜなら，Leanのライブラリには Group (Equiv.Perm α) のインスタンスもあり，乗算は任意の群で定義されているからです．そのため，どちらのインスタンスが見つかるかは曖昧です．実際，Leanは明示的に優先順位を指定しない限り，より新しい宣言を優先します．また，ある構造体が別の構造体のインスタンスであることをLeanに伝えるには， extends キーワードを使う方法もあります．これは例えばMathlibにおいてすべての可換環が環であることの指定に使われています．より詳しい情報は Section 7 の節および Theorem Proving in Lean のクラス推論に関する節 section on class inference にあります． [2]
一般的に，すでに記法が定義されている代数構造のインスタンスに * の値を指定するのは良くない考えです．Leanで Group の概念を再定義するのは人為的な例です．しかし，この場合群の表記法の解釈はどちらも Equiv.trans と Equiv.refl ， Equiv.symm に同じように展開されます．
同様に人工的な演習として， Group₂ に類似したクラス AddGroup₂ を定義しましょう．クラス Add と Neg ， Zero を使って任意の AddGroup₂ 上の加算，否定，0の通常の記法を定義してください．そして， Point が AddGroup₂ のインスタンスであることを示してください．出来たら試しに加法群表記が Point の要素に対して機能することを確認しましょう．
class AddGroup₂ (α : Type*) where
add : α → α → α
-- fill in the rest
上記の Point に対して Add と Neg ， Zero のインスタンスをすでに宣言していることは大して問題ではありません．繰り返しになりますが，表記法を合成する2つの方法は同じ答えになるはずだからです．
クラス推論は微妙なものであり，使用する際には注意しなければなりません．というのも私達が入力した式に対する解釈を目に見えない形で支配する自動化を設定しているからです．しかし，賢く使えばクラス推論は強力なツールとなり，Leanで代数的推論を可能にしてくれます．
6.3. ガウス整数の構築
ここで重要な数学的対象である ガウス整数 （Gaussian integers）を構成し，そしてこれがユークリッド整域であることを示すことでLeanにおける代数的な階層の使い方を説明しましょう．これまで使ってきた用語に従って言い換えると，ガウス整数を定義し，それがユークリッド整域構造のインスタンスであることを示します．
通常の数学用語では，ガウス整数の集合 \(\Bbb{Z}[i]\) は複素数の集合 \(\{ a + b i \mid a, b \in \Bbb{Z}\}\) のことです．しかしこの集合を複素数の部分集合として定義するのではなく，複素数をそれ自体のデータ型として定義することがここでの目標です．これにあたってガウス整数を2つの整数の組をそれぞれ 実部 （real）と 虚部 （imaginary）と考えることで表現します．
@[ext]
structure GaussInt where
re : ℤ
im : ℤ
まずガウス整数が環の構造を持ち， 0 は ⟨0, 0⟩ で， 1 は ⟨1, 0⟩ と定義され，加法が実部と虚部それぞれにおいて定義されることを示します．乗法の定義を考えるには， ⟨0, 1⟩ で表される要素 \(i\) を \(-1\) の平方根としたいことを思い出してください．したがって次のように定義したいわけです．
これは以下の Mul の定義を説明するものです．
instance : Zero GaussInt :=
⟨⟨0, 0⟩⟩
instance : One GaussInt :=
⟨⟨1, 0⟩⟩
instance : Add GaussInt :=
⟨fun x y ↦ ⟨x.re + y.re, x.im + y.im⟩⟩
instance : Neg GaussInt :=
⟨fun x ↦ ⟨-x.re, -x.im⟩⟩
instance : Mul GaussInt :=
⟨fun x y ↦ ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩
Section 6.1 で述べたように，データ型に関連するすべての定義を同じ名前の名前空間に置くと良いでしょう．これに従い，この章に対応するLeanファイルではこれらの定義は GaussInt 名前空間内で行われています．
ここで 0 と 1 ， + ， - ， * の記法の解釈について， GaussInt.zero などの名前をつけてそれらに記法を割り当てるのではなく，直接定義していることに注意してください．この方法は，例えば simp や rewrite で使用する際に定義に明示的な名前をつけたい際にしばしば便利です．
theorem zero_def : (0 : GaussInt) = ⟨0, 0⟩ :=
rfl
theorem one_def : (1 : GaussInt) = ⟨1, 0⟩ :=
rfl
theorem add_def (x y : GaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ :=
rfl
theorem neg_def (x : GaussInt) : -x = ⟨-x.re, -x.im⟩ :=
rfl
theorem mul_def (x y : GaussInt) :
x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ :=
rfl
また実部と虚部を計算する規則に名前をつけ，単純化で用いるよう宣言することも有益です．
@[simp]
theorem zero_re : (0 : GaussInt).re = 0 :=
rfl
@[simp]
theorem zero_im : (0 : GaussInt).im = 0 :=
rfl
@[simp]
theorem one_re : (1 : GaussInt).re = 1 :=
rfl
@[simp]
theorem one_im : (1 : GaussInt).im = 0 :=
rfl
@[simp]
theorem add_re (x y : GaussInt) : (x + y).re = x.re + y.re :=
rfl
@[simp]
theorem add_im (x y : GaussInt) : (x + y).im = x.im + y.im :=
rfl
@[simp]
theorem neg_re (x : GaussInt) : (-x).re = -x.re :=
rfl
@[simp]
theorem neg_im (x : GaussInt) : (-x).im = -x.im :=
rfl
@[simp]
theorem mul_re (x y : GaussInt) : (x * y).re = x.re * y.re - x.im * y.im :=
rfl
@[simp]
theorem mul_im (x y : GaussInt) : (x * y).im = x.re * y.im + x.im * y.re :=
rfl
ガウス整数が可換環のインスタンスであることを示すのは驚くほど簡単です．秘訣は構造体の概念にあります．それぞれのガウス整数は gaussInt 構造体のインスタンスであり， gaussInt 型自体と関連する演算は CommRing 構造体のインスタンスです．この CommRing 構造体は Zero と One ， Add ， Neg ， Mul という表記構造を拡張したものです．
もし instance : CommRing GaussInt := _ と入力してvscodeに表示される電球マークをクリックし，Leanに構造体定義のスケルトンを埋めてもらうと，おびただしい数の項目が表示されます．しかし，構造体の定義に飛ぶと，多くのフィールドにはデフォルトの定義があり，これらはLeanが自動的に埋めてくれます．重要なものは以下の定義にあります． nsmul と zsmul は特殊なものですが，これは次章で説明するため現時点では無視してください．それぞれの場合に置いて，関連する恒等式は定義を展開し， ext を使って恒等式を実部と虚部に戻し，単純化し，必要であれば整数で関連する環の計算を行うことで証明されます．このコードをすべて繰り返さないようにすることは簡単ですが，これは現在の議論のテーマではないことに注意してください．
instance instCommRing : CommRing GaussInt where
zero := 0
one := 1
add := (· + ·)
neg x := -x
mul := (· * ·)
nsmul := nsmulRec
zsmul := zsmulRec
add_assoc := by
intros
ext <;> simp <;> ring
zero_add := by
intro
ext <;> simp
add_zero := by
intro
ext <;> simp
neg_add_cancel := by
intro
ext <;> simp
add_comm := by
intros
ext <;> simp <;> ring
mul_assoc := by
intros
ext <;> simp <;> ring
one_mul := by
intro
ext <;> simp
mul_one := by
intro
ext <;> simp
left_distrib := by
intros
ext <;> simp <;> ring
right_distrib := by
intros
ext <;> simp <;> ring
mul_comm := by
intros
ext <;> simp <;> ring
zero_mul := by
intros
ext <;> simp
mul_zero := by
intros
ext <;> simp
Leanのライブラリでは少なくとも2つの異なる要素を持つ型を nontrivial 型のクラスとして定義しています．環の文脈においては，これは0が1に等しくないということと同じです．いくつかの一般的な定理はこの事実に依存しているため，これは今確立したほうがよいでしょう．
instance : Nontrivial GaussInt := by
use 0, 1
rw [Ne, GaussInt.ext_iff]
simp
ここでガウス整数が追加で重要な性質を持つことを示します． ユークリッド整域 （Euclidean domain）とは以下の2つの性質を持つ ノルム （norm）関数 \(N : R \to \mathbb{N}\) を備えた環 \(R\) のことです:
\(R\) の各 \(a\) と \(b \ne 0\) に対して， \(a = bq + r\) と \(r = 0\) または N(r) < N(b) のどちらかを満たす \(R\) の \(q\) と \(r\) が存在する．
すべての \(a\) と \(b \ne 0\) について， \(N(a) \le N(ab)\) ．
example (a b : ℤ) : a = b * (a / b) + a % b :=
Eq.symm (Int.ediv_add_emod a b)
example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b :=
Int.emod_nonneg a
example (a b : ℤ) : b ≠ 0 → a % b < |b| :=
Int.emod_lt a
任意の環において，元 \(a\) が \(1\) を割る場合，その元は 単元 （unit）であると言います．0ではない元 \(a\) がどちらも単元ではない \(b\) と \(c\) を用いて \(a = bc\) の形で書けない場合， \(a\) は 既約 （irreducible）であるといいます．つまり，整数においては \(a\) が積 \(bc\) を割るときは必ず \(b\) か \(c\) のどちらかを割ることになるため，すべての既約元 \(a\) は 素元 （prime）のことです．しかし他の環ではこの性質が破綻することがあります．環 \(\Bbb{Z}[\sqrt{-5}]\) では次のようになります．
そして元 \(2\) と \(3\) ， \(1 + \sqrt{-5}\) ， \(1 - \sqrt{-5}\) はすべて既約元ですが，素元ではありません．例えば \(2\) は積 \((1 + \sqrt{-5})(1 - \sqrt{-5})\) を割りますが，どちらの因数も割ることができません．もっと言うなら数 \(6\) が複数の方法で既約元の因数に分解できることから，もはや一意な因数分解もできません．
これと対照的に，すべてのユークリッド整域は一意に因数分解ができる領域です．これはすべての既約元が素元であることを意味します．ユークリッド整域の公理はどんな0でない元も既約元の有限積として書けることを課します．またユークリッドの互助法を使って任意の2つの非零元 a と b の最大公約数，つまり他の公約数すべてを割り切れる元を求められることも要求します．このことは既約元への因数分解は単元の冪まで一意であることを意味します．
ここでガウス整数は \(N(a + bi) = (a + bi)(a - bi) = a^2 + b^2\) で定義されるノルムを持つユークリッド整域であることを示します．ガウス整数 \(a - bi\) は \(a + bi\) の 共役 （conjugate）と呼ばれます．任意の複素数 \(x\) と \(y\) に対して \(N(xy) = N(x)N(y)\) が成り立つことを確認するのは難しくありません．
このノルムの定義でガウス整数がユークリッド整域となることを見るにあたっては，最初の性質だけが難しいです．例えば適当な \(q\) と \(r\) に対して \(a + bi = (c + di)q + r\) と書きたいとしましょう． \(a + bi\) と \(c + di\) は複素数であるとして次の除算を行います．
実部と虚部は整数ではないかもしれませんが，最も近い整数 \(u\) と \(v\) に丸めることが出来ます．丸めた際の余った部分を \(u'+v'i\) として，右辺を \((u + vi) + (u' + v'i)\) と表現できます．ここで \(|u'| \le 1/2\) と \(|v'| \le 1/2\) という条件があることに注意すると以下のようになります．
\(c + di\) を掛けると次のようになります．
\(q = u + vi\) と \(r = (c + di) (u' + v'i)\) を設定すると， \(a + bi = (c + di) q + r\) となり， \(N(r)\) を束縛するだけで良いことになります．
ここまでの議論はガウス整数を複素数の部分集合としてみることを要求しています．したがって，これをLeanで形式化する1つの選択肢は，ガウス整数を複素数の中に埋め込み，整数をガウス整数の中に埋め込み，実数から整数への丸め関数を定義し，これらの数系の間を適切に行き来するよう細心の注意を払うことです．実際，これはMathlibで行われているアプローチと全く同じで，ガウス整数そのものは 二次体の整数 （quadratic integers）の環の特殊な場合として構成されています．詳しくはファイル GaussianInt.lean を見てください．
ただ，ここでは上記の選択肢の代わりに整数に留める議論を行います．この選択は数学を形式化する際によく直面するものです．ライブラリにない概念や機構を必要とする論題が与えられた時，それらを形式化するか，すでに持っている概念や機構を利用するように論題を適応させるかの2つの選択肢があります．最初の選択肢は，その結果が他の文脈でも使えるのであれば，一般的に見て時間を費やす価値があるでしょう．しかし実用的に言えば，より初歩的な証明を求めるほうが効率的な場合もあります．
整数の通常の商と剰余の定理はすべての \(a\) と0ではない \(b\) に対して， \(a = b q + r\) と \(0 \le r < b\) を満たす \(q\) と \(r\) が存在するというものです．ここでは， \(a = bq' + r'\) かつ \(|r'| \le b/2\) となるような \(q'\) と \(r'\) が存在するという以下の変種を利用します．最初の文の \(r\) の値が \(r \le b/2\) を満たす場合， \(q' = q\) と \(r' = r\) とすることができ，そうでない場合は \(q' = q + 1\) と \(r' = r - b\) とすることができることを確認できます．この形式化にあたってHeather Macbeth氏にはケース分割による定義を避けた，よりエレガントなアプローチを提案してもらい感謝しています．単純に割る前に a に b / 2 を加え，余りから引くのです．
def div' (a b : ℤ) :=
(a + b / 2) / b
def mod' (a b : ℤ) :=
(a + b / 2) % b - b / 2
theorem div'_add_mod' (a b : ℤ) : b * div' a b + mod' a b = a := by
rw [div', mod']
linarith [Int.ediv_add_emod (a + b / 2) b]
theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by
rw [mod', abs_le]
constructor
· linarith [Int.emod_nonneg (a + b / 2) h.ne']
have := Int.emod_lt_of_pos (a + b / 2) h
have := Int.ediv_add_emod b 2
have := Int.emod_lt_of_pos b zero_lt_two
revert this; intro this -- FIXME, this should not be needed
linarith
ここでおなじみの linarith を使っていることに注意してください．また， mod' を div' で表現する必要があります．
theorem mod'_eq (a b : ℤ) : mod' a b = a - b * div' a b := by linarith [div'_add_mod' a b]
ここでは \(x^2 + y^2\) が0に等しいのは， \(x\) と \(y\) の両方が0である場合だけであるという事実を用いています．演習としてこれが任意の順序環で成り立つことを証明してみましょう．
theorem sq_add_sq_eq_zero {α : Type*} [LinearOrderedRing α] (x y : α) :
x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
sorry
この節の残りの定義と定理はすべて GaussInt 名前空間に置くことにします．まず， norm 関数を定義し，その性質をいくつか定義してみましょう．これらの証明はすべて短く済みます．
def norm (x : GaussInt) :=
x.re ^ 2 + x.im ^ 2
@[simp]
theorem norm_nonneg (x : GaussInt) : 0 ≤ norm x := by
sorry
theorem norm_eq_zero (x : GaussInt) : norm x = 0 ↔ x = 0 := by
sorry
theorem norm_pos (x : GaussInt) : 0 < norm x ↔ x ≠ 0 := by
sorry
theorem norm_mul (x y : GaussInt) : norm (x * y) = norm x * norm y := by
sorry
次に共役を取る関数を定義します．
def conj (x : GaussInt) : GaussInt :=
⟨x.re, -x.im⟩
@[simp]
theorem conj_re (x : GaussInt) : (conj x).re = x.re :=
rfl
@[simp]
theorem conj_im (x : GaussInt) : (conj x).im = -x.im :=
rfl
theorem norm_conj (x : GaussInt) : norm (conj x) = norm x := by simp [norm]
最後に，複素数の商を最も近いガウス整数に丸めるガウス整数の除算を x / y という記法で定義します．そのために， Int.div を今回のためにこしらえて用います．上で計算したように， x が \(a + bi\) で y が \(c + di\) の場合， x / y の実部と虚部はそれぞれ最も近い整数となります．
ここで，分子は \((a + bi)(c + di)\) の実部と虚部であり，分母はどちらも \(c + di\) のノルムに等しくなります．
instance : Div GaussInt :=
⟨fun x y ↦ ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩⟩
x / y を定義した後， x % y を x - (x / y) * y の余りとして定義します．上記のように，定義の div_def と mod_def に定義を記録し， simp と rewrite で使用できるようにします．
instance : Mod GaussInt :=
⟨fun x y ↦ x - y * (x / y)⟩
theorem div_def (x y : GaussInt) :
x / y = ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩ :=
rfl
theorem mod_def (x y : GaussInt) : x % y = x - y * (x / y) :=
rfl
これらの定義から，すべての x と y に対して， x = y * (x / y) + x % y がすぐに得られるため，あとは y が0ではない時， x % y のノルムが y のノルムより小さいことを示せば良いです．
先程 x / y の実部と虚部をそれぞれ div' (x * conj y).re (norm y) と div' (x * conj y).im (norm y) と定義しました．これを用いて計算すると以下のようになります．
(x % y) * conj y = (x - x / y * y) * conj y = x * conj y - x / y * (y * conj y)
右辺の実部と虚部は mod' (x * conj y).re (norm y) と mod' (x * conj y).im (norm y) です． div' と mod' の性質により，これらは norm y / 2 以下であることが保証されています．従って以下のようになります．
norm ((x % y) * conj y) ≤ (norm y / 2)^2 + (norm y / 2)^2 ≤ (norm y / 2) * norm y.
また一方で以下を得ます．
norm ((x % y) * conj y) = norm (x % y) * norm (conj y) = norm (x % y) * norm y.
norm y で割ることで求めていた``norm (x % y) ≤ (norm y) / 2 < norm y`` を得ます．
この面倒な計算は次にお証明で行われます．証明をたどってみて，もっとすっきりした証明を見つけられるかどうか試してみることをお勧めします．
theorem norm_mod_lt (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
(x % y).norm < y.norm := by
have norm_y_pos : 0 < norm y := by rwa [norm_pos]
have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
· ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
· calc
norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
_ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
+ |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
_ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
_ = norm y / 2 * (norm y / 2 * 2) := by ring
_ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
calc norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right H2 norm_y_pos
_ < norm y := by
apply Int.ediv_lt_of_lt_mul
· norm_num
· linarith
いよいよ本番です．上記で定義した norm 関数はガウス整数を非負整数に写します．ここでさらにガウス整数を自然数に移す関数が必要であり，これは整数を自然数に移す関数 Int.natAbs と norm 関数を組み合わせることで実現できます．次の2つの補題のうち，最初の補題はノルムを自然数に写し，整数に戻しても値が変わらないことを証明するものです．2番めの定理はノルムが減少するという事実を再表現しています．
theorem coe_natAbs_norm (x : GaussInt) : (x.norm.natAbs : ℤ) = x.norm :=
Int.natAbs_of_nonneg (norm_nonneg _)
theorem natAbs_norm_mod_lt (x y : GaussInt) (hy : y ≠ 0) :
(x % y).norm.natAbs < y.norm.natAbs := by
apply Int.ofNat_lt.1
simp only [Int.natCast_natAbs, abs_of_nonneg, norm_nonneg]
apply norm_mod_lt x hy
またユークリッド整域上のノルム関数の2つ目の重要な性質を確立する必要があります．
theorem not_norm_mul_left_lt_norm (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
¬(norm (x * y)).natAbs < (norm x).natAbs := by
apply not_lt_of_ge
rw [norm_mul, Int.natAbs_mul]
apply le_mul_of_one_le_right (Nat.zero_le _)
apply Int.ofNat_le.1
rw [coe_natAbs_norm]
exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)
これをまとめて，ガウス整数がユークリッド整域のインスタンスであることを示しましょう．ここでは定義した商と剰余の関数を使います．Mathlibのユークリッド整域の定義は上の定義よりも一般的で，剰余が任意の整礎関係の測度に関しても減少することを示すことができます．自然数を返すノルム関数の値を比較することはそのような測度の一例にすぎず，その場合に必要な性質は定理 natAbs_norm_mod_lt と not_norm_mul_left_lt_norm になります．
instance : EuclideanDomain GaussInt :=
{ GaussInt.instCommRing with
quotient := (· / ·)
remainder := (· % ·)
quotient_mul_add_remainder_eq :=
fun x y ↦ by simp only; rw [mod_def, add_comm] ; ring
quotient_zero := fun x ↦ by
simp [div_def, norm, Int.div']
rfl
r := (measure (Int.natAbs ∘ norm)).1
r_wellFounded := (measure (Int.natAbs ∘ norm)).2
remainder_lt := natAbs_norm_mod_lt
mul_left_not_lt := not_norm_mul_left_lt_norm }
これらのことから直ちに得られる成果は，ガウス整数に置いて素元であることと既約元であることが一致するということです．
example (x : GaussInt) : Irreducible x ↔ Prime x :=
irreducible_iff_prime