Lean4を使って有理数を構成してから実数を構成し、任意の有理数に対してそれに対応する実数の構成が確かにできることを示した。その過程をまとめたい。
構成と証明したことの概要 見出しへのリンク
まず前提として、Lean4の標準ライブラリにある、自然数を表現するNat, 整数を表現するIntとそれに関する諸定理は断りなく使った。
その上で、整数と自然数の組\(\mathbb{Z}\times \mathbb{N}_{>0}\)(NumPairと命名)を定義し、これに対して、適当な同値関係\(\sim\)を定義した。この同値関係は、\((a, b) \sim (c, d) \Leftrightarrow ad = cb\)となるようなもので、整数の方を分子、自然数の方を分母とみなした時の分数のよくある同値関係を意味している。
次に、上記の同値関係を用いて、同値類\(\mathbb{Z}\times\mathbb{N}_{>0}/\sim\)をとり、その元を有理数Rationalとした。
最後に、Rationalの集合を用いて、Dedekind cutをとり実数Realを構成した。
証明については、任意の有理数\(r\)について\(\{x \in \mathbb{Q}|x < r \}\)が、確かに実数の元となっていることを示した。この証明に際して\(\mathbb{Q}\)が稠密であることを示した。
設けた縛り 見出しへのリンク
今回、この構成と証明をするにあたって、個人的に以下の縛りを設けた。
- 証明は排中律を使わずに行う。
- Mathlibは使わない。
まず、排中律を使わなかったことについて。今回は、構成的な証明にすることを目標としたので、排中律ならびにそれと同値の公理を利用しなかった。これにより、二重否定除去や背理法による証明ができなくなったが、今回の場合はなんとかなった。
次に、Mathlibを使わないことについて。理由は主に2つある。1つはMathlibにはさまざまな有用な定理が収録されており、あまりにも便利すぎるから。そして、Mathlibのライブラリには背理法を行うtactic by_contraを用いた証明がかなり収録されていたはず1なので、意図しないうちに前述のルールを破ってしまう可能性があるからである。
ちなみにMathlibではMathlib.Data.Real.Basicにおいて実数を表現するRealが定義されており、これはCauchy列を用いて定義されている。
1. 有理数の構成 見出しへのリンク
前置きはこれくらいにして、実際に実数を構成した過程を見ていく。
まず、有理数を構成するために、整数と自然数の組\(\mathbb{Z}\times \mathbb{N}_{>0}\), NumPairを定義した。
structure NumPair where
num: Int
denom: Nat
denom_non_zero: denom ≠ 0
ここでのポイントは、分母が0でないことを保証するために、denom_non_zeroという要素をNumPairに追加している点である。
次に、NumPairに対して同値関係を定義した。これからこの関係を用いて有理数を定義するのだから、同値関係は以下のようになる。
fun a b => a.num * b.denom = b.num * a.denom
さて、この同値関係を持ちいて同値類をとりたいわけだが、Lean4では同値類Quotientをとるためには、数学でいうところの\((X, \sim)\)に相当するSetoidのインスタンスを定義する必要がある。そして、このSetoidのインスタンス定義には、ちゃんとこの2項関係が同値関係になっていることを示す必要がある。
このSetoidのインスタンス定義を行うと以下のようになる。rの部分が同値関係の定義を、iseqvの部分がそれがちゃんと同値関係になっていることの証明になっている。case reflと書いてあるところが反射律を、case symmが対称律を、case transが推移律を示している部分である。推移律に関しては、掛け算の交換法則や結合法則を駆使して証明しているので、そこまで特別なことをしていないのに証明が長くなっている。↑はもちろんKnuthの矢印記法…ではなく、NatをIntに変換するための記号である。
instance NumPairSetoid : Setoid NumPair where
r := fun a b => a.num * b.denom = b.num * a.denom
iseqv := by
constructor
case refl =>
intros x
rfl
case symm =>
intros x y h
rw [Int.mul_comm]
rw [h]
rw [Int.mul_comm]
case trans =>
intros x y z h1 h2
have h1_mod: x.num * ↑y.denom * ↑z.denom = y.num * ↑x.denom * ↑z.denom := by
rw [h1]
have h2_mod: y.num * ↑z.denom * ↑x.denom = z.num * ↑y.denom * ↑x.denom := by
rw [h2]
have: y.num * ↑x.denom * ↑z.denom = y.num * ↑z.denom * ↑x.denom := by
rw [Int.mul_assoc]
rw [Int.mul_assoc]
conv =>
lhs
conv =>
rhs
rw [Int.mul_comm]
have: y.denom * (x.num * ↑z.denom) = y.denom * (z.num * ↑x.denom) := by
rw [←h1_mod] at this
rw [h2_mod] at this
conv at this =>
lhs
conv =>
lhs
rw [Int.mul_comm]
rw [Int.mul_assoc]
conv at this =>
rhs
conv =>
lhs
rw [Int.mul_comm]
rw [Int.mul_assoc]
exact this
have y_denom_zero: (↑y.denom: Int) ≠ 0 := by
rw [Int.ofNat_ne_zero]
exact y.denom_non_zero
rw [Int.mul_eq_mul_left_iff y_denom_zero] at this
exact this
正直この証明は長いだけである。
このSetoidさえ定義してしまえば、有理数は以下のように定義できる。
def Rational := Quotient NumPairSetoid
2. 有理数の順序 見出しへのリンク
有理数の定義はできたので、次は順序を定義する。
まず、\(\mathbb{Z}\times \mathbb{N}_{>0}\), NumPairに対して以下のように順序を定義した。Lean4において順序を定義するためには、LTのインスタンスを定義する必要がある。
instance NumPairLT : LT NumPair where
lt a b := a.num * b.denom < b.num * a.denom
さて、あとはこの順序を有理数にliftして持ち込みたいが、そのためには、この順序が同値関係において保たれることを証明する必要がある。 つまり、\(a_1\sim a_2\)かつ\(b_1\sim b_2\)ならば、\(a_1< b_1\)と\(a_2< b_2\)は同値であることを示す必要がある。
これは\(a_1\sim a_2\)ならば、\(a_1< b\)と\(a_2< b\)は同値という補題num_pair_lt_universal_leftと\(b_1\sim b_2\)ならば、\(a< b_1\)と\(a< b_2\)は同値という補題num_pair_lt_universal_rightを証明してから示した。
証明は長いので省略する。標準ライブラリにあるInt.mul_lt_mul_of_pos_{left,right}とInt.lt_of_mul_lt_mul_{left,right}を用いれば、面倒なものの比較的簡単に証明できる。最初はこの定理の存在に気づかず、帰納法を回してかなり大変なことになっていた。2
theorem Int.mul_lt_mul_of_pos_left {a b c: Int} (h₁: a < b) (h₂: 0 < c): c * a < c * b
theorem Int.mul_lt_mul_of_pos_right {a b c: Int} (h₁: a < b) (h₂: 0 < c): a * c < b * c
theorem Int.lt_of_mul_lt_mul_left {a b c: Int} (w: a * b < a * c) (h: 0 ≤ a): b < c
theorem Int.lt_of_mul_lt_mul_left {a b c: Int} (w: b * a < c * a) (h: 0 ≤ a): b < c
こうして手に入れた定理num_pair_lt_universal
theorem num_pair_lt_universal{a1 a2 b1 b2: NumPair}: a1 ≈ a2 → b1 ≈ b2 → a1 < b1 → a2 < b2
を用いて、有理数の順序を定義した。by以降はこの順序が同値関係において保たれることを示す証明である。
instance RationalLT : LT Rational where
lt := Quotient.lift₂ (fun x y => x < y)
(
by
intros a_1 b_1 a_2 b_2 a_eq b_eq
simp
constructor
case mp =>
exact num_pair_lt_universal a_eq b_eq
case mpr =>
have a_eq': a_2 ≈ a_1 := by
exact NumPairSetoid.symm a_eq
have b_eq': b_2 ≈ b_1 := by
exact NumPairSetoid.symm b_eq
exact num_pair_lt_universal a_eq' b_eq'
)
ところで、順序をliftするのに使ったQuotient.lift₂は以下のような型を持つ。
abbrev Quotient.lift₂
{α: Sort uA} {β: Sort uB} {φ: Sort uC} {s₁: Setoid α} {s₂: Setoid β}
(f: α → β → φ) (c: ∀ (a₁: α) (b₁: β) (a₂: α) (b₂: β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
(q₁: Quotient s₁) (q₂: Quotient s₂)
: φ
ぱっと見だと面食らってしまうかもしれないが(実際私もLean4のドキュメントを眺めてて見つけた時には面食らった)、冷静に見てみると、2つの引数を取る関数fについて、同値関係によって結果が変わらないことの証明cを与えればそれをliftした関数を与えてくれることが読み取れるだろう。特に、fとcのみを与えることで、Quotient s₁ → Quotient s₂ → φになってくれるのは大変使い勝手が良くて嬉しい。
ちなみに、先にq₁: Quotient s₁, q₂: Quotient s₂を与えてしまうQuotient.liftOn₂というものも定義されているので、そちらを使うこともできる。
3. 集合の定義 見出しへのリンク
集合については、Lean3から続く慣習に従って
def Set α := α → Prop
と定義した。つまり、集合をある型を持つ値に対してそれが属すかどうかを返す関数として定義した。この定義においては、型によっては集合ではなくクラスになる気もするが、今回の場合には有理数全体は集合になるので問題にならないと考えている。
4. 実数の構成 見出しへのリンク
集合と有理数の順序を定義したので、あとは実数を構成するだけである。ここまで道具を揃えてしまえば、素直に書き下すだけで定義できてしまう。
structure Real where
partition: Set Rational
partition_non_empty: ∃x, x ∈ partition
partition_not_all: ∃x, x ∉ partition
partition_closed: ∀x y, x < y ∧ y ∈ partition → x ∈ partition
partition_open: ∀x, x ∈ partition → ∃y, x < y ∧ y ∈ partition
5. 有理数に対応する実数の構成 見出しへのリンク
最後に、任意の有理数に対してそれに対応する実数の構成が確かにDedekind cutになっていることを示した。
ここでいう「対応する実数の構成」とは、\(r\)という有理数に対して、\(\{x \in \mathbb{Q}|x < r \}\)を意味する。もちろん、有理数に対してどのような実数を対応づけるかの方法は無数にあるが、少なくとも私はこの構成がよく用いられていると認識しているのでこれを採用した。
命題を示すためには、Dedekind cutの定義から、以下の4つの定理を示せばよい。
- \(\forall r \in \mathbb{Q}, \exists r’ \in \mathbb{Q}, r’ < r\)
- \(\forall r \in \mathbb{Q}, \exists r’ \in \mathbb{Q}, \neg(r’ < r)\)
- \(\forall r\:r_1\:r_2 \in \mathbb{Q}, r_1 < r_2 \land r_2 < r \Rightarrow r_1 < r\)
- \(\forall r\:r’ \in \mathbb{Q}, r’ < r \Rightarrow \exists r’’ \in \mathbb{Q}, r’ < r’’ < r\)
特にこの定理のうち最後の1つは、有理数が稠密であることを意味している。
有理数は\(\mathbb{Z}\times \mathbb{N}_{>0}\), NumPairの同値類として定義したので、この定理の証明を得るためには、NumPairでこれらの定理を証明してliftすれば良い。
つまり、示すべきなのは以下の定理になる。
theorem num_pair_exists_lt(a: NumPair): ∃b: NumPair, b < a
theorem num_pair_exists_not_lt(a: NumPair): ∃b: NumPair, ¬b < a
theorem num_pair_lt_of_lt_lt{a b c: NumPair}: a < b → b < c → a < c
theorem num_pair_exists_between{a b: NumPair}: a < b → ∃c: NumPair, a < c ∧ c < b
1,2,4番目は実際にNumPairを構成することで証明できる。1番目は、\((a_1,a_2)\)に対して\((a_1 - 1,a_2)\)を、2番目は\((a_1,a_2)\)に対して\((a_1 + 1,a_2)\)を、4番目は\((a_1,a_2),(b_1,b_2)\)に対して\((a_1b_2 + b_1a_2, 2a_2b_2)\)を例として構成した。4番目は平均値に相当する。
余談だが、最初は4番目で\((2a_1b_2 + 1, 2a_2b_2)\)を例として出していた。これだと、途中で出てくる\(2a_1b_2 + 1 < 2b_1a_2\)の証明があまりにも煩雑になってしまうので、大変苦労した。実際に行った平均値を取る方法を用いれば、代わりに\(2a_1b_2 < a_1b_2 + b_1a_2\)と\(a_1b_2 + b_1a_2 < 2b_1a_2\)を証明することになる。これは
theorem int_two_mul{n: Int}: n * 2 = n + n := by
conv =>
rhs
congr
case a =>
rw [←Int.one_mul n]
case a =>
rw [←Int.one_mul n]
rw [←Int.add_mul]
simp [Int.mul_comm]
という風にn * 2をn + nに書き換える定理をあらかじめ証明しておくと瞬殺できる。例の選び方は証明の長さに直結することを実感した。
3番目の定理は、先述のInt.mul_lt_mul_of_pos_rightとInt.lt_of_mul_lt_mul_rightを使えばかなり簡潔に証明できた。
これらの定理を証明し、ついに有理数を実数に対応付ける関数を定義することができた。かなり長いが、やっていることは、同値類の代表元を取ってきて先ほどの定理を適用する作業を行なっているだけである。それぞれのbyが定理1, 2, 3, 4に対応している。
def real_of_rational(rational: Rational): Real :=
Real.mk (fun x => x < rational)
(by
simp
let ⟨rational', rational'_sat⟩ := Quotient.exists_rep rational
rw [←rational'_sat]
let ⟨x, x_sat⟩ := num_pair_exists_lt rational'
exact ⟨Quotient.mk NumPairSetoid x, x_sat⟩
)
(by
simp
let ⟨rational', rational'_sat⟩ := Quotient.exists_rep rational
rw [←rational'_sat]
let ⟨x, x_sat⟩ := num_pair_exists_not_lt rational'
exact ⟨Quotient.mk NumPairSetoid x, x_sat⟩
)
(by
simp
intros x y x_lt_y y_lt_r
let ⟨x', x'_sat⟩ := Quotient.exists_rep x
let ⟨y', y'_sat⟩ := Quotient.exists_rep y
let ⟨r', r'_sat⟩ := Quotient.exists_rep rational
rw [←x'_sat] at x_lt_y
rw [←y'_sat] at x_lt_y
rw [←y'_sat] at y_lt_r
rw [←r'_sat] at y_lt_r
let h := num_pair_lt_of_lt_lt x_lt_y y_lt_r
rw [←x'_sat]
rw [←r'_sat]
exact h
)
(by
simp
intros x h
let ⟨x', x'_sat⟩ := Quotient.exists_rep x
let ⟨r', r'_sat⟩ := Quotient.exists_rep rational
rw [←x'_sat]
rw [←r'_sat]
rw [←x'_sat] at h
rw [←r'_sat] at h
let ⟨c, ⟨c_x_sat, c_r_sat⟩⟩ := num_pair_exists_between h
exact ⟨Quotient.mk NumPairSetoid c, ⟨c_x_sat, c_r_sat⟩⟩
)
6. 使った公理の確認 見出しへのリンク
細心の注意を払ってきたが、念のために排中律と同等な公理を使っていないか確認する。Lean4では#print axiomsを使うことで、その定理が依存している公理を確認することができる。実際にやってると、
#print axioms real_of_rational
'real_of_rational' depends on axioms: [propext, Quot.sound]
となる。
propextは論理的な同値関係を数学的な等式として扱うことを許す公理である。つまり、\(a\leftrightarrow b\)ならば\(a = b\)とする公理である。Quot.soundは、同値な元の同値類を等号で結んで良いという公理である。つまり、\(a \sim b\)ならば\(a\)の同値類と\(b\)の同値類は等しいという公理である。3
Classical.choiceは空でないものから1つ具体的に値を取ってくることを許す公理であり、排中律と同値であることが知られている。今回の証明では、このClassical.choiceに依存していないことが確認できたので、目標は達成できたと言えるだろう。
8/13追記 見出しへのリンク
Classical.choiceと排中律が同値であることは知られていない。Diaconescuの定理からClassical.choiceならば排中律Classical.emは出るが、逆はそうではない。Classical.choiceは冷静に考えると選択公理そのもので、排中律から出たらかなりまずい。
よって、#print axiomsによって排中律を使っていないことを厳密には確認できないが、Classical.emを使っていたとしたらLeanにおける排中律の定義の問題でClassical.choiceが依存関係に出てくるので、少なくとも明示的に利用されている場所はないことがわかる。
最後に 見出しへのリンク
Mathlibと排中律を使わずに実数を構成し、よくある有理数に対応する実数の構成が確かにDedekind cutになっていることを示した。
証明にはかなりの時間を要した。これは「難しい証明を行なっているから」というよりは、自分が実数の構成についてちゃんと理解できているのかを確かめるために極力何かを参照せず定義を思い出しながら書いていったこと、証明でやるべきことが明快でもいざLean4を通してみると案の定コーナーケースが大量に出てきたこと、お世辞にも使いやすいとはいえない公式のドキュメントの検索を使って使えそうな定理を探す必要があったことに起因する。
おかげさまで、こういう定理は登録されていそう、登録されていなさそう、もし登録されているのなら、こういう名前で登録されているだろうという勘が少し働くようになった。HaskellでいうところのHoogleみたいなのがあると便利だと感じたので、もしかしたら作るかもしれない。
最後はLean4の愚痴っぽくなってしまったが、理解した気になっている定義・定理をLean4で書いてみると、「タイパ」は悪いかもしれないが楽しく自分の理解を深めることができるので、興味のある方はぜひ試してみてほしい。
8/13追記 見出しへのリンク
Hoogleのように定理を検索できるLoogleというものがあるらしい。次から使ってみる。
ソースコード 見出しへのリンク
証明を全文読みたい方は以下からどうぞ。