Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界

0. この記事の要点

数学の証明を、人間が読むだけでなく、計算機に最後まで検査させるにはどうすればよいでしょうか。この記事では、群の基本性質のような身近な題材を、証明支援系 Lean の言葉に書き直す手順を追います。読み終えると、Lean で群や整数がどう定義されるか、紙の証明がコードのどの部分に対応するか、そして「計算機が検査した」ことが何を保証し、何を保証しないかが分かります。

• 型クラスは「構造をもつ型」を表す Lean の仕組みです。群の公理を class で書き、extends で「群はモノイドである」という階層を作ると、モノイドについて証明した定理がそのまま群に使えます。群論入門 の基本性質を、この方法で形式化します。
• 商（Quot。同値な元を同じものとみなしてできる型）を使うと、公理的集合論 ZFC で行った「対の同値類としての整数」の構成を、そのまま型として書けます。Mathlib の実数も、有理数のコーシー列の商として定義されています。
• Rikai の定理のうち、カントールの定理は標準ライブラリだけで完全に形式化して検査できます。バナッハの不動点定理とハーン–バナッハの定理は Mathlib に形式化があり、Rikai の証明の各段階と Mathlib の概念を対応させます。有限次元のハーン–バナッハの定理は、ここで選択公理を使わない証明を与えます（定理 4.2）。
• 形式化が保証するのは「書かれた主張が、使われた公理から導かれる」ことだけです。5 / 0 = 0 のような規約、主張の書き違い、公理の使用は、人間が確かめる必要があります。これが形式化の信頼境界です。
• この記事のコードのうち、標準ライブラリだけのものは Lean 4（4.34 系）で動作を確認しました。Mathlib に依存する部分はコードとしては載せず、名前だけを挙げます（Mathlib の名前は版によって変わります）。

この記事で使う事前知識

• 群: 結合法則・単位元・逆元をもつ演算を備えた集合。→ 群論入門
• 同値類: 同値関係で「同じ」とみなせる元をまとめた集まり。→ 同値類
• コーシー列: 項どうしが、先へ進むほどいくらでも近くなる数列。→ コーシー列
• 定義的同値: 定義を展開すれば同じ式になる、というカーネルの等しさ。→ 定義的同値
• 劣線形汎関数: 劣加法性 $p(x+y)\le p(x)+p(y)$ と正斉次性をもつ実数値関数。→ 劣線形汎関数
• 選択公理: 無限個の集合からそれぞれ元を一つずつ選べるという公理。→ 選択公理

1. 動機：Rikai の閉包と形式証明

Rikai では、定理の証明で使う事実を、記事内で証明するか既出の定理として参照するかのどちらかにしてきました。参照をたどると、数学の命題は ZFC の公理に行き着きます。これは人間が読む証明の網の目で、各リンクの正しさは書き手と監査者の目に頼っています。

形式証明は、同じ網の目を計算機が検査できる形で作るものです。証明支援系 Lean の仕組み で見たように、Lean で受理された証明は小さなカーネルが一歩ずつ検査した項であり、依存する公理も #print axioms で正確に列挙されます。

この章では、実際に形式化するときに何が起こるかを、三つの観点から見ます。

1. 定義をどう書くか。「群」「整数」「実数」を、型理論の中でどう表すか（§2、§3）。
2. 定理をどう証明するか。Rikai の記事の証明が、形式証明ではどのような部品に分かれるか（§4）。
3. 何を信じているか。形式化された定理が、人間の言葉で述べた定理と本当に同じものか（§5）。

2. 型クラスと代数構造の階層

2.1. 群を型クラスで定義する

群論入門 の群の定義（定義 3.1［群論入門］）は「集合と演算の組で、結合法則・単位元・逆元の公理を満たすもの」でした。Lean では、これを型 $G$ に付随する構造として書きます。

class MyMonoid (M : Type) extends Mul M, One M where
  mul_assoc : ∀ a b c : M, a * b * c = a * (b * c)
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

class MyGroup (G : Type) extends MyMonoid G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1

class は、フィールド（演算と公理の証明）をまとめた構造体の宣言です。extends Mul M, One M は「* と 1 の記法をもつ」こと、extends MyMonoid G, Inv G は「群はモノイドであって、さらに逆元をもつ」ことを表します。群の公理として左逆元 inv_mul だけを要求しているのは、右逆元が定理として導けるからです（下の mul_inv）。

型クラスの要点は、[MyGroup G] と書いた引数（インスタンス引数）を、Lean が型から自動で探して埋めることです。定理を「任意の群 $G$ について」の形で書いておけば、具体的な群に使うときに構造を明示的に渡す必要がありません。たとえば §2.3 で整数の加法群を登録しておくと、その型に定理を使うときに、Lean が登録済みの構造を探して渡してくれます。

2.2. 群の基本性質の形式化

命題 3.2［群論入門］ の単位元の一意性・消約律・逆元の一意性・$(ab)^{-1}=b^{-1}a^{-1}$ を形式化します。

namespace MyMonoid
variable {M : Type} [MyMonoid M]

theorem one_unique (e : M) (h : ∀ a : M, e * a = a) : e = 1 := by
  have h1 := h 1
  rw [mul_one] at h1
  exact h1
end MyMonoid

namespace MyGroup
open MyMonoid
variable {G : Type} [MyGroup G]

theorem cancel_left (a x y : G) (h : a * x = a * y) : x = y := by
  calc x = 1 * x := (one_mul x).symm
    _ = a⁻¹ * a * x := by rw [inv_mul]
    _ = a⁻¹ * (a * x) := mul_assoc _ _ _
    _ = a⁻¹ * (a * y) := by rw [h]
    _ = a⁻¹ * a * y := (mul_assoc _ _ _).symm
    _ = 1 * y := by rw [inv_mul]
    _ = y := one_mul y

theorem mul_inv (a : G) : a * a⁻¹ = 1 := by
  apply cancel_left a⁻¹
  rw [← mul_assoc, inv_mul, one_mul, mul_one]

theorem inv_unique (a b : G) (h : b * a = 1) : b = a⁻¹ := by
  calc b = b * 1 := (mul_one b).symm
    _ = b * (a * a⁻¹) := by rw [mul_inv]
    _ = b * a * a⁻¹ := (mul_assoc b a a⁻¹).symm
    _ = 1 * a⁻¹ := by rw [h]
    _ = a⁻¹ := one_mul a⁻¹

theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  apply Eq.symm
  apply inv_unique
  rw [mul_assoc, ← mul_assoc a⁻¹, inv_mul, one_mul, inv_mul]
end MyGroup

読み方を補います。variable {G : Type} [MyGroup G] は「以下の定理はすべて、任意の型 $G$ とその上の群構造について述べる」という宣言です。calc は等式の連鎖で、紙の上の計算 $x=1x=(a^{-1}a)x=a^{-1}(ax)=\cdots$ をそのまま書いたものです。各段の := の後ろが、その一段の根拠（公理の適用か、rw による書き換え）です。rw [← mul_assoc] は結合法則を右辺から左辺の向きに使う書き換えです。

MyGroup の中で MyMonoid の公理 one_mul や mul_assoc がそのまま使えていることに注意してください。extends によって、群構造から自動的にモノイド構造が取り出されています。one_unique は群でも使えます。

2.3. 具体的な群とインスタンス

整数の加法群を、この型クラスのインスタンスとして登録してみます（Int の * と衝突しないように、新しい型 AddInt で包みます）。

structure AddInt where
  val : Int

instance : MyGroup AddInt where
  mul a b := ⟨a.val + b.val⟩
  one := ⟨0⟩
  inv a := ⟨-a.val⟩
  mul_assoc a b c := by
    show AddInt.mk (a.val + b.val + c.val) = AddInt.mk (a.val + (b.val + c.val))
    rw [Int.add_assoc]
  one_mul a := by
    show AddInt.mk (0 + a.val) = a
    rw [Int.zero_add]
  mul_one a := by
    show AddInt.mk (a.val + 0) = a
    rw [Int.add_zero]
  inv_mul a := by
    show AddInt.mk (-a.val + a.val) = AddInt.mk 0
    rw [Int.add_left_neg]

#eval ((⟨3⟩ : AddInt) * ⟨4⟩).val   -- 7
example (a b : AddInt) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := MyGroup.mul_inv_rev a b

インスタンスを作るときに、各公理の証明を義務として課されます（show で目標を定義に沿って書き直し、整数の性質で閉じています）。一度登録すれば、群について証明したすべての定理が AddInt に使えます。最後の行では、一般の群の定理 mul_inv_rev を AddInt に適用しています。

注意 2.1（Mathlib の代数階層）

Mathlib はこの方法で、半群・モノイド・群・可換群・環・体・加群・ノルム空間・内積空間などの数百のクラスを階層にしています（Monoid、Group、CommRing、Field、NormedSpace などの名前で、版によって整理が変わります）。数学でいう「体は環である」「ノルム空間は距離空間である」が、すべて型クラスの継承として表されます。複数の道筋で同じ構造が得られるとき（たとえば実数の距離が「ノルムから」と「順序から」の二通りで得られるとき）、それらが定義的に一致するように設計する必要があり、これは形式化特有の難しさです（「ダイヤモンド問題」と呼ばれます）。

3. 商による構成：整数から実数へ

3.1. 対の同値類としての整数

公理的集合論 ZFC では、整数を $\omega\times\omega$ の対 $(a,b)$（「$a-b$」のつもり）の同値類として作りました（定義 4.1［公理的集合論 ZFC］）。Lean では商型 Quot で同じことができます。

def IntRel (a b : Nat × Nat) : Prop := a.1 + b.2 = b.1 + a.2
def MyInt : Type := Quot IntRel
def MyInt.mk (m n : Nat) : MyInt := Quot.mk IntRel (m, n)

def MyInt.neg : MyInt → MyInt :=
  Quot.lift (fun p => Quot.mk IntRel (p.2, p.1)) (by
    intro a b h
    apply Quot.sound
    show a.2 + b.1 = b.2 + a.1
    unfold IntRel at h
    omega)

theorem MyInt.mk_succ (m n : Nat) : MyInt.mk (m + 1) (n + 1) = MyInt.mk m n := by
  apply Quot.sound
  show m + 1 + n = m + (n + 1)
  omega

theorem MyInt.neg_neg (x : MyInt) : x.neg.neg = x := by
  induction x using Quot.ind with
  | mk p => rfl

上のコードの読み方を先に述べます。Quot IntRel は、自然数の対の型を関係 IntRel で割った商の型で、Quot.mk IntRel (m, n) が対 $(m,n)$ の属する類を表します。Quot.sound は「関係で結ばれた 2 つの対は、商の中で等しい」と述べる規則です。商の元は代表元の選び方に依らない形でしか扱えないので、商の上の関数は次のように定義します。

Quot.lift で商の上の関数を定義するときには、代表元によらないことの証明を必ず渡さなければなりません。紙の上では「well-defined であることは容易に確かめられる」と書き流しがちな部分が、形式化では証明義務として明示されます。

命題 3.1（符号反転の well-defined 性）✓

$(a_1,a_2)\sim(b_1,b_2)$、すなわち $a_1+b_2=b_1+a_2$ ならば、$(a_2,a_1)\sim(b_2,b_1)$、すなわち $a_2+b_1=b_2+a_1$。

証明（命題 3.1）

自然数の加法の可換性から、仮定の等式の両辺を入れ替えて書き直すと $b_1+a_2=a_1+b_2$、さらに各辺の和の順序を入れ替えて $a_2+b_1=b_2+a_1$。

∎

コードの by intro a b h; …; omega がこの証明です。omega は整数・自然数の線形算術の決定手続きで、この程度の等式変形を自動で行います。neg_neg は、Quot.ind（商の元についての帰納法）で代表元 p の場合に帰着させると、(p.2, p.1) を 2 回入れ替えたものが p に定義的に等しい（構造体 η）ので rfl で閉じます。なお #print axioms MyInt.neg_neg は propext と Quot.sound を表示します。Quot.sound は商を使ったため、propext は omega が内部で使うためです。

3.2. Mathlib の実数

Mathlib の実数 Real（記号 ℝ）は、有理数のコーシー列の同値類として定義されています。本稿執筆時点では、CauSeq.Completion.Cauchy (abs : ℚ → ℚ)（絶対値に関する有理数のコーシー列を「差が 0 に収束する」で割った商）を包む構造体です。その上に四則・順序を定義し、上限性質（sSup が上に有界な空でない集合の最小上界であること）や完備性を定理として証明しています。

これは 数とは何か で紹介したコーシー列による構成（注意 5.2［数とは何か］）そのものです。公理的集合論 ZFC ではデデキント切断を使いましたが、上限性質をもつ順序体はすべて同型なので（注意 4.8［公理的集合論 ZFC］）、どちらの構成から出発しても同じ解析学が展開されます。形式化では、構成の詳細を一度証明した後は、ℝ を「完備な順序体」としてだけ扱い、構成に依存しない補題だけを使うのが普通です。

測度論も同じ方針で形式化されています。Mathlib の測度 MeasureTheory.Measure は外測度から Carathéodory の方法で作られ（測度空間と Carathéodory の拡張定理 と同じ道筋）、ℝ 上のルベーグ測度 MeasureTheory.volume、非負関数の積分 MeasureTheory.lintegral、ボホナー積分 MeasureTheory.integral などが定義されています（名前は本稿執筆時のもの）。

4. Rikai の定理を形式化する

4.1. カントールの定理（標準ライブラリだけで完結）

濃度と無限 のカントールの定理（定理 7.1［濃度と無限］）は、集合 $A$ から冪集合への全射が存在しないことでした。$A$ の部分集合を述語 $A\to\mathsf{Prop}$ で表すと、次のようになります。

theorem cantor {α : Type} (f : α → (α → Prop)) : ¬ Function.Surjective f := by
  intro hf
  obtain ⟨a, ha⟩ := hf (fun x => ¬ f x x)
  have h : f a a = ¬ f a a := congrFun ha a
  have hn : ¬ f a a := fun hfa => (Eq.mp h hfa) hfa
  exact hn (Eq.mpr h hn)

#print axioms cantor   -- 'cantor' does not depend on any axioms

紙の証明との対応は一対一です。対角集合 $D=\{x\mid x\notin f(x)\}$ が fun x => ¬ f x x、全射性から $f(a)=D$ となる $a$ をとるのが obtain、「$a\in f(a)\iff a\notin f(a)$」が h（congrFun は関数の等式を点 $a$ で評価する合同）です。最後の 2 行は、$a\in f(a)$ と仮定すると $a\notin f(a)$ が出て矛盾する、だから $a\notin f(a)$、すると $a\in f(a)$ になって矛盾、という二段階の議論です。#print axioms が示すとおり、この証明は公理を一つも使わない純粋な λ 項で、排中律すら要りません。

4.2. バナッハの不動点定理（Mathlib との対応）

距離空間 の縮小写像の原理（定理 6.2［距離空間］）は Mathlib に形式化されています。本稿執筆時点の Mathlib では、定数 $K$ の縮小写像であることを ContractingWith K f（$K<1$ かつ $f$ が $K$-リプシッツ）で表し、完備距離空間（CompleteSpace）上で不動点 ContractingWith.fixedPoint、それが不動点であること ContractingWith.fixedPoint_isFixedPt、一意性 ContractingWith.fixedPoint_unique を提供しています（Mathlib への依存が必要で、この記事の環境では実行していません。名前は版によって変わりえます）。

Rikai の証明の各段階が、形式化ではどの部品になるかを対応させると次のようになります。

Rikai の証明の段階	形式化での部品
$x_{n+1}=T(x_n)$ と反復する	反復 f^[n] x（Nat.iterate）
$d(x_{n+1},x_n)\le k^nd(x_1,x_0)$	帰納法とリプシッツ性
等比級数で $(x_n)$ がコーシー列	等比級数の和と、コーシー列の判定補題
完備性で極限 $x^{*}$ が存在	CompleteSpace の定義（コーシー列の収束）
連続性で $T(x^{*})=x^{*}$	極限と連続写像の交換
$d(x^{*},y^{*})\le k\,d(x^{*},y^{*})$ から一意性	実数の不等式

形式化の際に紙の証明と最も違うのは、「極限」「コーシー列」が Mathlib ではフィルターという一般的な枠組みで定義されていることです。ε-N 論法の命題は、フィルターの言葉から取り出す補題を経由して使います。証明の骨組みは同じでも、どの一般性で定義するかという設計が、形式化の手間を大きく左右します。

4.3. 有限次元のハーン–バナッハの定理

Banach 空間の基本定理 のハーン–バナッハの拡張定理（定理 3.2［Banach 空間の基本定理］）は、一般の場合には Zorn の補題を使いました。有限次元では選択公理は要りません。ここで完全な証明を与えます。ねらいは次のとおりです。まず補題で、定義域を 1 次元だけ広げる 1 段の拡張を作ります。そこでは拡張の値 $c$ の候補が実数の上限と下限の間の幅として現れ、上限を選ぶ規則を決めておけば、選択の余地がなくなります。有限次元では、この 1 段を有限回繰り返せば全体に届きます。$p$ は劣線形汎関数（定義 3.1［Banach 空間の基本定理］）とします。

補題 4.1（1 次元の拡張）✓

$X$ を実ベクトル空間、$p$ を $X$ 上の劣線形汎関数、$M$ を部分空間、$f:M\to\mathbb{R}$ を $M$ 上で $f\le p$ を満たす線形汎関数、$x_0\in X\setminus M$ とする。このとき $M_1=M+\mathbb{R}x_0$ 上の線形汎関数 $F_1$ で、$F_1|_M=f$ かつ $M_1$ 上で $F_1\le p$ を満たすものが存在する。

証明（補題 4.1）

$m,m'\in M$ について、$f$ の線形性、$M$ 上の $f\le p$、$p$ の劣加法性から

$$f(m)+f(m')=f(m+m')\le p(m+m')=p\bigl((m+x_0)+(m'-x_0)\bigr)\le p(m+x_0)+p(m'-x_0).$$

よって $f(m')-p(m'-x_0)\le p(m+x_0)-f(m)$。左辺の集合 $\{f(m')-p(m'-x_0)\mid m'\in M\}$ は空でなく（$0\in M$）、右辺の任意の値で上から抑えられるので、実数の上限性質（定理 4.3［公理的集合論 ZFC］）により上限 $a$ が存在して、すべての $m$ について $a\le b_m:=p(m+x_0)-f(m)$。$c=a$ とおく。

$x_0\notin M$ なので、$M_1$ の元は $m+tx_0$（$m\in M$、$t\in\mathbb{R}$）とただ一通りに表される（$m+tx_0=m'+t'x_0$ で $t\ne t'$ なら $x_0=(m'-m)/(t-t')\in M$ となり矛盾）。$F_1(m+tx_0):=f(m)+tc$ は well-defined で線形、$M$ 上で $f$ に一致する。$F_1\le p$ を示す。$t=0$ は仮定。$t>0$ なら、$c\le b_{m/t}$ と $p$ の正斉次性から

$$f(m)+tc\le f(m)+t\bigl(p(m/t+x_0)-f(m/t)\bigr)=p(m+tx_0).$$

$t=-s<0$ なら、$c\ge f(m/s)-p(m/s-x_0)$ から

$$f(m)-sc\le f(m)-s\bigl(f(m/s)-p(m/s-x_0)\bigr)=p(m-sx_0).$$∎

定理 4.2（有限次元のハーン–バナッハの定理）✓

$X$ を有限次元の実ベクトル空間とし、$p,M,f$ を 補題 4.1 と同じとする。このとき $X$ 上の線形汎関数 $F$ で、$F|_M=f$ かつ $X$ 上で $F\le p$ を満たすものが存在する。この証明は選択公理を使わない。

証明（定理 4.2）

$X$ は有限個のベクトル $v_1,\ldots,v_n$ で張られている。$M_0=M$、$f_0=f$ とし、$i=1,\ldots,n$ について順に、$v_i\in M_{i-1}$ なら $M_i=M_{i-1}$、$f_i=f_{i-1}$、$v_i\notin M_{i-1}$ なら 補題 4.1 を $x_0=v_i$ に使って $M_i=M_{i-1}+\mathbb{R}v_i$ 上の拡張 $f_i\le p$ を作る。各段で $M_i\supseteq M_{i-1}$、$v_i\in M_i$ なので $M_n$ はすべての $v_i$ を含み、$M_n=X$。$F=f_n$ が求める汎関数である。手順は $n$ 段で終わり、各段の選択（補題 4.1 の $c$）は上限という一意に定まる値なので、選択公理は使っていない。

∎

一般の場合（定理 3.2［Banach 空間の基本定理］）は、この 1 段の拡張を Zorn の補題で「超限回」繰り返すことに相当します。Mathlib には一般の場合が形式化されており（本稿執筆時点では exists_extension_of_le_sublinear などの名前。未実行）、そちらは Zorn の補題を使うので Classical.choice に依存します。Lean の数学ライブラリでは、有限次元の場合も一般の定理の特殊化として得るのが普通で、「選択公理を使わない証明がある」という情報は #print axioms には現れません。どの公理が本当に必要かは、形式化された証明を見るだけでは分からないこともある、という教訓です。

5. 形式化の信頼境界

5.1. カーネルが保証すること、しないこと

証明支援系 Lean の仕組み の de Bruijn 基準の節（定義 7.1［証明支援系 Lean の仕組み］）で、信頼の境界を表にしました。形式化の現場で最も問題になるのは、その表の「定義と主張が意図どおりに書かれていること」です。カーネルが保証するのは

書かれた主張（型）が、使われた公理と、書かれた定義から導かれる。

ということだけで、その主張が人間の意図した数学の命題と同じかどうかは、まったく保証しません。

形式化された定理の信頼の層。内側ほど機械的に検査され、外側は人間が確かめる。

5.2. 規約による「ゴミ値」

型理論の関数は全域的でなければならないので、数学では「定義しない」値にも何かを割り当てます。Lean の標準ライブラリでは次のとおりです。

#eval (5 : Nat) / 0      -- 0
#eval (2 : Nat) - 3      -- 0（自然数の引き算は 0 で打ち切る）
#eval (1 : Rat) / 0      -- 0

theorem not_div_cancel : ¬ ∀ a b : Nat, a / b * b = a := by
  intro h
  exact absurd (h 1 0) (by decide)

$x/0=0$ という規約は、数とは何か で論じたゼロ除算の問題（例 7.2［数とは何か］）とは矛盾しません。そこで示したのは「$0$ で割った結果に、乗法の逆元としての性質を要求すると壊れる」ことで、Lean の / は $b\ne0$ のときだけ逆元の性質をもつ、別の全域関数だからです。$x/0=0$ を定理の中で使っても矛盾は起きませんが、主張の読み違いの原因になります。たとえば「$a/b\cdot b=a$」を仮定 $b\ne0$ なしで形式化すると、上のとおり偽の主張になります（証明できないので、誤りは発見されます）。逆に、仮定の付け忘れで主張が弱くなる誤り（たとえば $\frac{1}{x}$ についての不等式が $x=0$ で自明に成り立ってしまう）は、証明が通ってしまうので発見されにくいのです。

5.3. 主張の忠実さを確かめる方法

形式化の実践では、主張の忠実さを次のような方法で確かめます。

• 定義の健全性検査：定義した概念について、既知の例と反例で期待どおりの結果になるかを証明してみる（「素数」を定義したら、$2$ が素数で $4$ が素数でないことを証明する）。
• 主張の否定の確認：仮定を一つ外した主張の反例を形式化して、仮定が本当に効いていることを確かめる。
• ブループリント：形式化の前に、人間の言葉の証明を補題に分解した文書を作り、補題ごとに形式化の主張と人間の主張を並べて査読する。Liquid Tensor Experiment で使われ、大規模な形式化の標準的な方法になりました。
• 公理の確認：最終的な定理に #print axioms を実行し、sorryAx や想定外の公理が混じっていないことを確かめる。

Rikai の記事は、まさにこの「ブループリント」に近い位置にあります。各定理の証明が、既出の定理への参照と記事内の補題に分解されていれば、それを形式化の作業単位にそのまま使えます。Rikai の閉包（ZFC までさかのぼれること）と、形式証明の閉包（カーネルと三つの公理までさかのぼれること）は、同じ考え方を人間の言葉と機械の言葉で実現したものだと言えます。

6. 演習

演習 6.1易

§2.2 の MyGroup について、$(a^{-1})^{-1}=a$ を Lean で証明せよ。（ヒント：inv_unique と mul_inv。）

解答

$a\cdot a^{-1}=1$ は「$a$ が $a^{-1}$ の左逆元である」ことを意味するので、逆元の一意性から $a=(a^{-1})^{-1}$。

namespace MyGroup
open MyMonoid
variable {G : Type} [MyGroup G]

theorem inv_inv (a : G) : (a⁻¹)⁻¹ = a := by
  apply Eq.symm
  apply inv_unique
  exact mul_inv a
end MyGroup

apply inv_unique で目標 a = a⁻¹⁻¹ が a * a⁻¹ = 1 に変わり、mul_inv a がちょうどその証明です。§2.2 のコードに続けて書けば、そのまま通ります。

演習 6.2標準

§3.1 の MyInt に加法 $[(a_1,a_2)]+[(b_1,b_2)]=[(a_1+b_1,\,a_2+b_2)]$ を定義するとき、Quot.lift に渡す必要のある証明義務を数式で書き、証明せよ。

解答

2 変数なので、各変数について代表元によらないことを示す。第 1 変数については、$(a_1,a_2)\sim(a'_1,a'_2)$（$a_1+a'_2=a'_1+a_2$）ならば $(a_1+b_1,a_2+b_2)\sim(a'_1+b_1,a'_2+b_2)$、すなわち $(a_1+b_1)+(a'_2+b_2)=(a'_1+b_1)+(a_2+b_2)$。左辺は $(a_1+a'_2)+(b_1+b_2)$、右辺は $(a'_1+a_2)+(b_1+b_2)$ と並べ替えられ、仮定から等しい。第 2 変数も同様。Lean では、Quot.lift を 2 回入れ子にするか、2 変数版の補助関数を使い、それぞれの義務を omega で閉じることになります。紙の上の「同様に確かめられる」が、形式化では 2 つの独立した証明義務になります。

演習 6.3標準

「自然数 $n$ について $n/n=1$」を Lean で ∀ n : Nat, n / n = 1 と形式化したとする。(1) この主張が偽であることを示せ。(2) 正しい形に直せ。(3) 逆に、仮定を付けすぎて主張が意図より弱くなる例を一つ考えよ。

解答

(1) $n=0$ のとき $0/0=0\ne1$。Lean では example : ¬ ∀ n : Nat, n / n = 1 := fun h => absurd (h 0) (by decide) で確かめられる。(2) ∀ n : Nat, 0 < n → n / n = 1。標準ライブラリの Nat.div_self がこの形の定理で、fun _ hn => Nat.div_self hn が証明になる。(3) たとえば「閉区間上の連続関数は有界である」を、「連続関数 f が ∀ x, |f x| ≤ 1 を満たすならば ∃ M, ∀ x, |f x| ≤ M」と書いてしまうと、結論に必要な性質（有界性）が仮定に紛れ込んでおり、M = 1 で自明に証明できるが、意図した定理とは無関係である。極端な場合、仮定が矛盾していれば（たとえば 0 < 0 を仮定に含めれば）どんな結論も証明できてしまう。仮定が充足可能であることを、具体例で確かめておくのが安全です。

演習 6.4標準

定理 4.2 の拡張が一意でない例を挙げよ。

解答

$X=\mathbb{R}^2$、$p(x,y)=|x|+|y|$（劣線形）、$M=\{(x,0)\}$、$f(x,0)=0$ とする。任意の $c\in[-1,1]$ について $F_c(x,y)=cy$ は線形で、$M$ 上で $0$、$F_c(x,y)=cy\le|y|\le p(x,y)$。よって拡張は無数にある。補題 4.1 の証明では $c$ を上限 $a=\sup_m(f(m)-p(m-x_0))$ に選んだが、この例では $x_0=(0,1)$ として $a=\sup_x(-|x|-1)=-1$、$b=\inf_x(|x|+1)=1$ で、$[a,b]=[-1,1]$ のどの値を選んでもよい。一意に定まる値（上限）を選ぶ規則を決めたことが、選択公理を避けられた理由です。

参考文献

• The mathlib Community, “The Lean Mathematical Library”, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 367–381. doi:10.1145/3372885.3373824
• J. Avigad and P. Massot, Mathematics in Lean — オンライン版（型クラスによる代数構造、位相と解析の形式化）。
• K. Buzzard, J. Commelin and P. Massot, “Formalising perfectoid spaces”, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 299–312.
• J. Avigad, L. de Moura, S. Kong and S. Ullrich, Theorem Proving in Lean 4 — オンライン版（型クラス、商、公理の章）。
• W. Rudin, Functional Analysis, 2nd ed., McGraw-Hill, 1991 — 第 3 章（ハーン–バナッハの定理）。