5. 初等整数論

この章では,整数論の初等的な結果の形式化方法について説明します.より本質的な数学的内容を扱うにつれて,証明はより長く,より複雑になっていきますが,そこで用いられるスキルはこれまでですでに学んだものです.

5.1. 無理根

古代ギリシャの時代から知られていた事実から初めていきましょう.すなわち2の平方根が無理数であるということです.もしここでそうでないと仮定すると, \(\sqrt{2} = a / b\) のようにとある既約分数として書くことができます.両辺を2乗すると \(a^2 = 2 b^2\) となります.これは \(a\) が偶数であることを意味します.そこで \(a = 2c\) と書くと \(4c^2 = 2 b^2\) となり整理して \(b^2 = 2 c^2\) を得ます.これは \(b\) も偶数であることを意味し, \(a / b\) が既約分数という仮定に矛盾します.

\(a / b\) が既約分数であるということは, \(a\)\(b\) は共通の因数がない,つまり 互いに素 (coprime)であることを意味します.Mathlibは述語 Nat.Coprime m nNat.gcd m n = 1 と定義しています.Leanの無名の射影による記法を使うと, stNat 型の式であれば, Nat.Coprime s t の代わりに s.coprime t と書くことができます.これは Nat.gcd についても同様です.いつものように,Leanはしばしば Nat.Coprime の定義を必要に応じて自動的に展開しますが, Nat.Coprime 識別子を用いて手動で書き換えや単純化することもできます. norm_num タクティクは具体的な値を計算するにあたって十分な賢さを備えています.

#print Nat.Coprime

example (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 :=
  h

example (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 := by
  rw [Nat.Coprime] at h
  exact h

example : Nat.Coprime 12 7 := by norm_num

example : Nat.gcd 12 8 = 4 := by norm_num

関数 gcd についてはすでに Section 2.4 で説明しました. gcd には整数用のバージョンも存在します.このような異なる数体系間の関係については後述します.また gcd 関数や PrimeCoprime にはさらに一般的な概念も存在し,一般的な代数構造で意味を持ちます.Leanがこの一般性をどのように管理しているかについては次の章で説明します.それまでにこの節では自然数に限定して説明しましょう.

また素数の概念 Nat.Prime も必要です.定理 Nat.prime_def_lt は素数についておなじみの特徴を定義します.また Nat.Prime.eq_one_or_self_of_dvd では別の特徴づけをしています.

#check Nat.prime_def_lt

example (p : ) (prime_p : Nat.Prime p) : 2  p   m : , m < p  m  p  m = 1 := by
  rwa [Nat.prime_def_lt] at prime_p

#check Nat.Prime.eq_one_or_self_of_dvd

example (p : ) (prime_p : Nat.Prime p) :  m : , m  p  m = 1  m = p :=
  prime_p.eq_one_or_self_of_dvd

example : Nat.Prime 17 := by norm_num

-- commonly used
example : Nat.Prime 2 :=
  Nat.prime_two

example : Nat.Prime 3 :=
  Nat.prime_three

自然数において,素数は自明ではない因数の積として書けないという性質を持っています.より広い数学的な文脈では,この性質を持つ環の元は 既約元 (irreducible)と呼ばれます.環のある元が 素数 (prime)であるとは,この元が積を割れる時,必ずその積の因数のいずれかを割ることができることを指します.この2つの概念は一致し,自然数の重要な性質として定理 Nat.Prime.dvd_mul に集約されます.

この事実は上記で行った議論の重要な性質を確立することができます.すなわちある数の2乗が偶数であれば,その数も偶数であるということです.Mathlibは Algebra.Group.Even にて述語 Even を定義していますが,後ほど説明する理由から,ここでは m が偶数であることを表現するために 2 m を使用します.

#check Nat.Prime.dvd_mul
#check Nat.Prime.dvd_mul Nat.prime_two
#check Nat.prime_two.dvd_mul

theorem even_of_even_sqr {m : } (h : 2  m ^ 2) : 2  m := by
  rw [pow_two, Nat.prime_two.dvd_mul] at h
  cases h <;> assumption

example {m : } (h : 2  m ^ 2) : 2  m :=
  Nat.Prime.dvd_of_dvd_pow Nat.prime_two h

本書を読み進めるにあたって,Mathlibから必要な事実や定理を見つける技量が必要になってきます.もし名前の接頭辞が推測でき,関連するMathlibをimportしているのであれば,タブ補完( Ctrl+タブ を使うこともあります)を使って探しているものを見つけることができることを覚えておいてください.任意の識別子を Ctrl+クリック することでその識別子が定義されているファイルにジャンプすることができます.これでその識別子の定義とその近くにある定理を見ることが可能です.また LeanのコミュニティのWEBページ にある検索エンジンを使うこともできますし,もし他の方法がうまくいかなかったら遠慮なく Zulip で質問してください.

example (a b c : Nat) (h : a * b = a * c) (h' : a  0) : b = c :=
  -- apply? suggests the following:
  (mul_right_inj' h').mp h

2の平方根が無理数であることの証明の核心は次の定理にあります.この証明について even_of_even_sqr と定理 Nat.dvd_gcd を使ってby以降を埋めてみましょう.

example {m n : } (coprime_mn : m.Coprime n) : m ^ 2  2 * n ^ 2 := by
  intro sqr_eq
  have : 2  m := by
    sorry
  obtain k, meq := dvd_iff_exists_eq_mul_left.mp this
  have : 2 * (2 * k ^ 2) = 2 * n ^ 2 := by
    rw [ sqr_eq, meq]
    ring
  have : 2 * k ^ 2 = n ^ 2 :=
    sorry
  have : 2  n := by
    sorry
  have : 2  m.gcd n := by
    sorry
  have : 2  1 := by
    sorry
  norm_num at this

実は僅かな変更でこれまでの議論の 2 を任意の素数に置き換えることができます.次の例で試してみましょう.証明の最後で p 1 から矛盾を導く必要があります.ここで素数が2以上であるという Nat.Prime.two_leNat.le_of_dvd が使えます.

example {m n p : } (coprime_mn : m.Coprime n) (prime_p : p.Prime) : m ^ 2  p * n ^ 2 := by
  sorry

別のアプローチを考えてみましょう. \(p\) が素数のときに \(m^2 = p n^2\) を仮定すると, \(m\)\(n\) の素因数分解を考えることで \(p\) は方程式の左辺に偶数回,右辺に奇数回出現し,矛盾することから \(m^2 \ne p n^2\): となります.ここでこの議論は \(n\)\(m\) が0ではないことを仮定している点に注意してください.この仮定は以下の定式化で十分であることが確認されます.

素因数分解の一意性とは,0以外の自然数は素数の積として一意に書けるというものです.Mathlibにはこの定理が正式に含まれており, Nat.primeFactorsList という関数で表現され,与えられた数の素因数を小さい順に並べたリストを返します.Mathlibは Nat.primeFactorsList n のすべての要素が素数であること,0より大きい n はその因数の積に等しいこと,そして n が他の素数のリストの積に等しい場合,そのリストは Nat.primeFactorsList n の結果を順列に並べ替えたものであることを証明します.

#check Nat.primeFactorsList
#check Nat.prime_of_mem_primeFactorsList
#check Nat.prod_primeFactorsList
#check Nat.primeFactorsList_unique

これらの定理や他の定理についてその定義等を見ることができますが,リストの要素の参照や積,順列の話はまだしていません.ですがさしあたって今の問題においてはそれらの知識は不要です.その代わりに,Mathlibには同じデータを関数として表現する関数 Nat.factorization があることを利用します.具体的には, Nat.factorization n p (これは n.factorization p と書くこともできます)は n の素因数分解における p の指数を返します.この関数について以下の3つの事実を用います.

theorem factorization_mul' {m n : } (mnez : m  0) (nnez : n  0) (p : ) :
    (m * n).factorization p = m.factorization p + n.factorization p := by
  rw [Nat.factorization_mul mnez nnez]
  rfl

theorem factorization_pow' (n k p : ) :
    (n ^ k).factorization p = k * n.factorization p := by
  rw [Nat.factorization_pow]
  rfl

theorem Nat.Prime.factorization' {p : } (prime_p : p.Prime) :
    p.factorization p = 1 := by
  rw [prime_p.factorization]
  simp

上記の証明をステップごとに見ていくと奇妙な表記を見かけるでしょうが,これは n.factorization はLeanでは有限台として定義されているからです.ひとまず今はこのことを気にする必要はありません.ここでの目的では,上3つの定理の中身を気にせずブラックボックスとして使うことができます.

次の例は simp を使うことで n^2 0n 0 に置き換えられることを示しています. simpa タクティクはただ単に simp タクティクのあとに assumption タクティクを呼んでいるだけです.

証明中の抜けている箇所を埋めてみましょう.

example {m n p : } (nnz : n  0) (prime_p : p.Prime) : m ^ 2  p * n ^ 2 := by
  intro sqr_eq
  have nsqr_nez : n ^ 2  0 := by simpa
  have eq1 : Nat.factorization (m ^ 2) p = 2 * m.factorization p := by
    sorry
  have eq2 : (p * n ^ 2).factorization p = 2 * n.factorization p + 1 := by
    sorry
  have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by
    rw [ eq1, sqr_eq, eq2]
  rw [add_comm, Nat.add_mul_mod_self_left, Nat.mul_mod_right] at this
  norm_num at this

この証明のいいところは一般化できる点です.ちょっと変えるだけで m^k = r * n^k と書いたなら, r の任意の素数 p の倍数はかならず k の倍数でなければならないことを示す証明となり, k2 である必要はどこにもなくなります.

Nat.count_factors_mul_of_posr * n^k と一緒に使うには, r が正であることを知っている必要があります.しかし r が0の場合,以下の定理は自明であり, simp で簡単に証明できます.そこで証明は場合分けして行うことにします. rcases r with _ | r の行ではゴールを2つのバージョンへと置き換えています;一つは r0 に置き換えるもので,もう一つは rr + 1 に置き換えるものです.後者の場合,定理 r.succ_ne_zero を使うことができ, r + 1 0 が成立します( succ は後続を意味します).

また have : npow_nz から始まる行が n^k 0 の短い証明項の証明になっていることにも注目してください.この項がどのように機能するかを理解するために,これをタクティクによる証明でどのように記述されるかを考えてみましょう.

以下の証明の欠けている部分を埋めてみましょう.証明の一番最後は Nat.dvd_sub'Nat.dvd_mul_right で完成させることができます.

この例では p が素数であることを仮定していませんが, p が素数でない場合, r.factorization p は定義により0となることから,結論は自明となるため,いずれにせよ証明はすべての場合において有効であることに注意してください.

example {m n k r : } (nnz : n  0) (pow_eq : m ^ k = r * n ^ k) {p : } :
    k  r.factorization p := by
  rcases r with _ | r
  · simp
  have npow_nz : n ^ k  0 := fun npowz  nnz (pow_eq_zero npowz)
  have eq1 : (m ^ k).factorization p = k * m.factorization p := by
    sorry
  have eq2 : ((r + 1) * n ^ k).factorization p =
      k * n.factorization p + (r + 1).factorization p := by
    sorry
  have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by
    rw [ eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
  rw [this]
  sorry

ここまで行ってきた証明について改善するポイントがいくつかあります.まずはじめに,2の平方根が無理数であることの証明は,2の平方根そのものについて語るべきであり,これは実数または複素数の要素として理解されています.そして2の平方根が無理数であることを証明することは有理数について語るべきであり,すなわち2の平方根に等しい有理数は無いということを示すはずです.さらにこの節の定理を整数に拡張する必要があります.もし2の平方根を2つの整数の商として書くことができれば,自然数の商としても書くことができるのは数学的に明らかですが,これを正式に証明するには多少の努力が必要です.

Mathlibでは,自然数と整数,有理数,実数,複素数はすべて別々のデータ型で表現されます.このように分けられた領域ごとに注意を向けるのはしばしば有用です.例えば自然数に対して帰納法を適用するのは簡単であり,実数をふくまない整数の割り算を推論することも非常に簡単です.しかし,異なる領域にまたがる議論は頭痛の種であり,これは私達が対処しなければならない問題です.この問題については章の後半で触れることにします.

最後の定理については rk 乗された数であるという結論に強化できることを期待するでしょう.なぜなら rk 乗根は r を分割する各素数の積であり,これらの素数の r での指数は k で割ることができるからです.これを可能にするには有限集合上の積と和についての推論のためのより良い手段が必要です.この話題についても後ほど触れます.

実際,この節の結果はすべてMathlibの Data.Real.Irreational で遥かに一般的なものとして確立されています. multiplicity の概念は任意の可換モノイドに対して定義され,そこで使える概念も無限大の値を追加して拡張された自然数 enat を受け取るようになっています.次の章ではLeanがこのような一般正をサポートする方法を理解するために実際に実装をしていきましょう.

5.2. 帰納法と再帰

自然数の集合 \(\mathbb{N} = \{ 0, 1, 2, \ldots \}\) はその性質から数学の基礎において重要なだけでなく,新たな数学的対象の構成においても主要な役割を演じます.Leanの基礎では 帰納型 (inductive type)を宣言することができます.これは コンストラクタ (constructor)のリストによって帰納的に生成される型です.Leanでは自然数は次のように宣言されます.

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

この型はライブラリ中のにて定義されています.その定義は #check Nat と書いてから,識別子 Natctrl+クリック することで見つけることができます. inductive コマンドは Nat が2つのコンストラクタ zero : Natsucc : Nat Nat から自由かつ帰納的に生成されるデータ型であることを示しています.もちろん,ライブラリは natzero に対してそれぞれ 0 という記法を導入しています.(数値は二進数表現に変換されますが,今はその詳細を気にする必要はありません.)

ここで「自由」という言葉は現役の数学者にとって Nat 型が要素 zerozero をその像に含まない単射な後続関数 succ を持つことを指します.

example (n : Nat) : n.succ  Nat.zero :=
  Nat.succ_ne_zero n

example (m n : Nat) (h : m.succ = n.succ) : m = n :=
  Nat.succ.inj h

また現役の数学者にとって「帰納的」という言葉が意味するのは,自然数には帰納法による証明の原理と再帰による定義の原理が備わっているということです.この節ではこれらの使い方を紹介します.

以下が再帰的な定義による階乗関数の例です.

def fac :   
  | 0 => 1
  | n + 1 => (n + 1) * fac n

この構文には慣れが必要です.最初の行に := が無いことに注目してください.そして次の2行は再帰的定義の基本ケースと帰納的なステップを展開しています.以下の等式は定義上成り立ちますが, facsimprw に与えることで手動で使用することもできます.

example : fac 0 = 1 :=
  rfl

example : fac 0 = 1 := by
  rw [fac]

example : fac 0 = 1 := by
  simp [fac]

example (n : ) : fac (n + 1) = (n + 1) * fac n :=
  rfl

example (n : ) : fac (n + 1) = (n + 1) * fac n := by
  rw [fac]

example (n : ) : fac (n + 1) = (n + 1) * fac n := by
  simp [fac]

この階乗関数はMathlibではすでに Nat.factorial として定義されています.ここでも再度 #check Nat.factorial と入力し, ctrl+クリック することでこの関数の定義にジャンプすることができます.本書では説明のため,例題では fac を引き続き使用します. Nat.factorial の定義の前にある @[simp] という注釈は, simp がデフォルトで使用する等式のデータベースにそこで定義した等式を追加することを指示します.

帰納法の原理は,自然数に関する一般的な命題を証明するには,その命題が0について成り立ち,また自然数 \(n\) について成り立つときはいつでも \(n + 1\) についても成り立つことを証明すれば良いというものです.そのため,以下の証明の induction' n with n ih という行は2つのゴールを生み出します.1つ目は 0 < fac 0 を証明することであり,2つ目は ih : 0 < fac n という仮定から 0 < fac (n + 1) の証明が求められます. with n ih というフレーズは帰納法で用いられる仮定の変数と仮定に名前をつけるためのもので,好きな名前をつけることができます.

theorem fac_pos (n : ) : 0 < fac n := by
  induction' n with n ih
  · rw [fac]
    exact zero_lt_one
  rw [fac]
  exact mul_pos n.succ_pos ih

induction タクティクは賢いため,帰納法の変数に依存する仮定を帰納法の仮定の一部に含めることができます.これがどういうことなのか,次の例で見てみましょう.

theorem dvd_fac {i n : } (ipos : 0 < i) (ile : i  n) : i  fac n := by
  induction' n with n ih
  · exact absurd ipos (not_lt_of_ge ile)
  rw [fac]
  rcases Nat.of_le_succ ile with h | h
  · apply dvd_mul_of_dvd_right (ih h)
  rw [h]
  apply dvd_mul_right

次の例では階乗関数の粗い下界を示します.証明のはじめに場合分けをすると簡単になるため,証明の残りは \(n = 1\) の場合から始まるようにします. pow_succpow_succ' を使いつつ,帰納法による証明で論証を完成してみましょう.

theorem pow_two_le_fac (n : ) : 2 ^ (n - 1)  fac n := by
  rcases n with _ | n
  · simp [fac]
  sorry

有限の和や積を含む等式を証明するために帰納法がよく用いられます.Mathlibは Finset.sum s f という式を定義しています.ここで s : Finset αα 型の要素の有限集合であり, fα で定義される関数です. f の余域は零要素を持つ可換で結合的な加法をサポートする任意の型です. Algebra.BigOperators.Basic をインポートして open BigOperators コマンドを実行することで,より示唆的な表記である x in s, f x を使うことができます.もちろん有限積についても同様の操作と表記法があります.

この Finset 型とそれがサポートする演算については次の節で説明します.現時点では n より小さい自然数の有限集合である Finset.range n のみ取り扱います.

variable {α : Type*} (s : Finset ) (f :   ) (n : )

#check Finset.sum s f
#check Finset.prod s f

open BigOperators
open Finset

example : s.sum f =  x in s, f x :=
  rfl

example : s.prod f =  x in s, f x :=
  rfl

example : (range n).sum f =  x in range n, f x :=
  rfl

example : (range n).prod f =  x in range n, f x :=
  rfl

Finset.sum_range_zeroFinset.sum_range_succ は, \(n\) までの総和を再帰的に記述するもので,積についても同様のものがあります.

example (f :   ) :  x in range 0, f x = 0 :=
  Finset.sum_range_zero f

example (f :   ) (n : ) :  x in range n.succ, f x =  x in range n, f x + f n :=
  Finset.sum_range_succ f n

example (f :   ) :  x in range 0, f x = 1 :=
  Finset.prod_range_zero f

example (f :   ) (n : ) :  x in range n.succ, f x = ( x in range n, f x) * f n :=
  Finset.prod_range_succ f n

各ペアの1つ目の等式は定義上成り立ちます.つまり証明を rfl で置き換えることができます.

以下は先程定義した階乗関数を積として表現したものになります.

example (n : ) : fac n =  i in range n, (i + 1) := by
  induction' n with n ih
  · simp [fac, prod_range_zero]
  simp [fac, ih, prod_range_succ, mul_comm]

特筆すべきは単純化のルールとして mul_comm がふくまれていることです.等式 x * y = y * x を使って単純化しようとすると無限ループに陥ってしまうように思われるため,この等式で単純化するのは危険だと思われるでしょう.Leanの simp はその点を十分に認識しており,ある程度固定した上で任意の順序で項を並べたときに結果として得られる項の値が小さくなる場合にのみこの規則を適用するようにしています.次の例では mul_assomul_commmul_left_comm の3つのルールを使って簡約すると括弧の位置や変数の順序まで同じようにできることを示しています.

example (a b c d e f : ) : a * (b * c * f * (d * e)) = d * (a * f * e) * (c * b) := by
  simp [mul_assoc, mul_comm, mul_left_comm]

大まかには,括弧を右に押し出し,両辺の式が同じ標準的な順序になるまで並べ替えることでこのルールは機能します.これらのルールとそれに対応する加法のルールを使って単純化するのは便利なテクニックです.

和の等式の話に戻ると, \(n\) までの自然数の和が \(n (n + 1) / 2\) となることの証明は次のようになります.証明の最初のステップでは,まず分母を消去します.これは等式を形式化する際に一般的に便利です.なぜなら除算は一般的に副次的な条件を持つからです.(同様に可能な限り自然数に対して減算を使わないようにすることも有効です.)

theorem sum_id (n : ) :  i in range (n + 1), i = n * (n + 1) / 2 := by
  symm; apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
  induction' n with n ih
  · simp
  rw [Finset.sum_range_succ, mul_add 2,  ih]
  ring

ここで上記に似ている平方の和やググって出てくる様々な等式を証明することをお勧めします.

theorem sum_sqr (n : ) :  i in range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
  sorry

Leanのコアのライブラリでは,加法と乗法は再帰定義を使って定義されており,それらについての基本的な性質は帰納法を使って確立されています.もしこのような基礎的な話題に興味があるなら,乗法と加法の可換性と結合性,乗法と加法の分配性の証明に取り組むのも楽しいでしょう.これを自前定義の自然数を用いて行うには以下のような流れになります.ここで MyNatinduction を使うことができることに注意してください.Leanは賢いので関連する帰納法の原理(もちろん Nat の原理と同じです)が使えることを知っています.

まずは加法の可換性から初めましょう.経験的には加法と乗法は第二引数に対する再帰によって定義されるので,その位置に現れる変数に対する帰納法によって証明を行うのが一般的に有利です.これに対し結合則の証明でどの変数で再帰するか決めるのは少し難しいです.

0,1,加法,乗法の通常の表記を使わずに証明を進めていくのは混乱を起こすことがあります.こういう場合に記法を定義するやり方がありますが,それは後ほど学びます.名前空間 MyNat で作業するということは, MyNat.zeroMyNat.succ ではなく, zerosucc と書くことができるということであり,これらの名前の解釈が他のものより優先されることを意味します.名前空間の外では,例えば以下で定義する add の完全な名前は MyNat.add となります.

もしこれらを考えることが本当に 楽しい と感じたら,切り捨てる引き算と指数を定義し,それらの性質をいくつか証明してみましょう.切り捨て減算はゼロで切り捨てる計算方法です.これを定義するためには0ではない数から1を引き,0を固定する先行関数 pred を定義するのが便利です.関数 pred は単純な再帰のインスタンスで定義できます.

inductive MyNat where
  | zero : MyNat
  | succ : MyNat  MyNat

namespace MyNat

def add : MyNat  MyNat  MyNat
  | x, zero => x
  | x, succ y => succ (add x y)

def mul : MyNat  MyNat  MyNat
  | x, zero => zero
  | x, succ y => add (mul x y) x

theorem zero_add (n : MyNat) : add zero n = n := by
  induction' n with n ih
  · rfl
  rw [add, ih]

theorem succ_add (m n : MyNat) : add (succ m) n = succ (add m n) := by
  induction' n with n ih
  · rfl
  rw [add, ih]
  rfl

theorem add_comm (m n : MyNat) : add m n = add n m := by
  induction' n with n ih
  · rw [zero_add]
    rfl
  rw [add, succ_add, ih]

theorem add_assoc (m n k : MyNat) : add (add m n) k = add m (add n k) := by
  sorry
theorem mul_add (m n k : MyNat) : mul m (add n k) = add (mul m n) (mul m k) := by
  sorry
theorem zero_mul (n : MyNat) : mul zero n = zero := by
  sorry
theorem succ_mul (m n : MyNat) : mul (succ m) n = add (mul m n) n := by
  sorry
theorem mul_comm (m n : MyNat) : mul m n = mul n m := by
  sorry
end MyNat

5.3. 無限に存在する素数

帰納と再帰の探求を続けるにあたってもう一つの数学的な基本法則,すなわち素数が無限に存在することの証明を行いましょう.これの形式化された形として,すべての自然数 \(n\) に対して \(n\) より大きい素数が存在すると言うことができます.これを証明するために, \(p\)\(n! + 1\) の任意の素因数とします.もし, \(p\)\(n\) 以下ならば, \(n!\) も割ることができます.一方で \(n! + 1\) も割るため, \(p\) は1も割ることとなり,矛盾します.したがって \(p\)\(n\) より大きいことになります.

この証明を形式化するには,2以上の数が素因数を持つことを示す必要があります.そのためには,0と1のどちらでもない自然数が2以上であることを証明する必要があります.そしてこの事実から形式化の風変わりな特徴が導かれます.この手の自明な命題が時として形式化にあたって最も厄介なのです.ここでは証明にあたっていくつかの方法を考えます.

まず初めに, cases タクティクと,後続関数が自然数の順序を保持するという事実を使うことができます.

theorem two_le {m : } (h0 : m  0) (h1 : m  1) : 2  m := by
  cases m; contradiction
  case succ m =>
    cases m; contradiction
    repeat apply Nat.succ_le_succ
    apply zero_le

別の方法としては, interval_cases というタクティクを使う方法があります.これは問題の変数が自然数か整数の区間にふくまれる場合にゴールを自動的にケース分割してくれます.このタクティクにカーソルを合わせるとドキュメントを見ることができることを覚えておいてください.

example {m : } (h0 : m  0) (h1 : m  1) : 2  m := by
  by_contra h
  push_neg at h
  interval_cases m <;> contradiction

interval_cases m の後ろのセミコロンは,その次に来るタクティクが分割された各ケースそれぞれに適用されることを意味します.さらに別の選択肢として decide というタクティクを使うことで,問題を解決するための決定手順を自動で見つけることもできます.Leanは束縛された量化子 x, x < n ... もしくは x, x < n ... で始まる命題の真理値を,その命題を有限個生成してそれぞれについて決定することで求めることができることを知っています.

example {m : } (h0 : m  0) (h1 : m  1) : 2  m := by
  by_contra h
  push_neg at h
  revert h0 h1
  revert h m
  decide

定理 two_le 片手に2より大きい自然数にはすべて素因数があることを示すことから初めましょう.Mathlibには最小の素因数を帰す関数 Nat.minFac がありますが,ライブラリの新しい部分を学ぶために,この関数を使用せずに定理を直接証明することにしましょう.

これにあたっては普通の帰納法では不十分です.ここで必要なのはすべての自然数 \(n\) が性質 \(P\) を持つことを証明するために,すべての自然数 \(n\) についてもし \(P\)\(n\) より小さいすべての値で成り立つならば, \(n\) でも成り立つことで示すという 強帰納法 (strong induction)です.Leanでは,この原理を Nat.strong_induction_on と呼び, with キーワードを使って帰納法のタクティクにこれを使うように指示することができます.この場合,ベースケースは存在せず,一般的な帰納法のステップにふくまれることに注意してください.

議論の流れは単純に以下のとおりです. \(n ≥ 2\) を仮定し, \(n\) が素数であればそれでおしまいです.もし素数でなければ,素数の特徴の1つである,素数の非自明な因数 \(m\) を帰納法の仮説に適用することができます.次の証明を一行ずつ読めばこれがどのような役割を演じているかわかるでしょう.

theorem exists_prime_factor {n : Nat} (h : 2  n) :  p : Nat, p.Prime  p  n := by
  by_cases np : n.Prime
  · use n, np
  induction' n using Nat.strong_induction_on with n ih
  rw [Nat.prime_def_lt] at np
  push_neg at np
  rcases np h with m, mltn, mdvdn, mne1
  have : m  0 := by
    intro mz
    rw [mz, zero_dvd_iff] at mdvdn
    linarith
  have mgt2 : 2  m := two_le this mne1
  by_cases mp : m.Prime
  · use m, mp
  · rcases ih m mltn mgt2 mp with p, pp, pdvd
    use p, pp
    apply pdvd.trans mdvdn

これで本題の定理の形式化を証明することができます.以下のスケッチを埋めてみましょう.ここでは Nat.factorial_posNat.dvd_factorialNat.dvd_sub' が使えます.

theorem primes_infinite :  n,  p > n, Nat.Prime p := by
  intro n
  have : 2  Nat.factorial (n + 1) + 1 := by
    sorry
  rcases exists_prime_factor this with p, pp, pdvd
  refine p, ?_, pp
  show p > n
  by_contra ple
  push_neg  at ple
  have : p  Nat.factorial (n + 1) := by
    sorry
  have : p  1 := by
    sorry
  show False
  sorry

上記の証明について別解を考えましょう.階乗関数を使う代わりに,有限集合 \(\{ p_1, \ldots, p_n \}\) が与えられたとした時の \(\prod_{i = 1}^n p_i + 1\) の素因数を考えることにします.この素因数は各 \(p_i\) とは異なるものでなければならないため,すべての素数を含む有限集合は存在しないことがわかります.

この議論を形式化するには,有限集合を推論できる必要があります.Leanでは,任意の型 α に対して Finset α 型で α 型の要素の有限集合を表します.有限集合の計算を推論するには, α 型についての同値性を検証する手順が必要です.これが以下のスニペットに [DecidableEq α] という仮定が含まれている理由です. のような具体的なデータ型ではこの仮定は自動的に満たされます.実数について推論する際には古典論理によって仮定が成り立ち,計算的な解釈を放棄することができます.

open Finset コマンドを使うことで,関連する定理を短い名前で利用できるようにしています.集合の場合とは異なり,有限集合に関わる同値性はほとんどの場合定義的に成り立たないため, Finset.subset_iffFinset.mem_unionFinset.mem_interFinset.mem_sdiff などの等価の条件を使って手動で展開する必要があります. ext タクティクは2つの有限集合が等しいことを片方の各元がすべてもう片方の元であることによって示すために使うことができます.

open Finset

section
variable {α : Type*} [DecidableEq α] (r s t : Finset α)

example : r  (s  t)  r  s  r  t := by
  rw [subset_iff]
  intro x
  rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter]
  tauto

example : r  (s  t)  r  s  r  t := by
  simp [subset_iff]
  intro x
  tauto

example : r  s  r  t  r  (s  t) := by
  simp [subset_iff]
  intro x
  tauto

example : r  s  r  t = r  (s  t) := by
  ext x
  simp
  tauto

end

ここで新しい技法を使いました. tauto タクティク(と古典論理を使う強化版の tauto! )は命題の同語反復を省くために使うことができます.以下の2つの例を証明するためにこれらの手法が使えるか試してみましょう.

example : (r  s)  (r  t) = r  s  t := by
  sorry
example : (r \ s) \ t = r \ (s  t) := by
  sorry

定理 Finset.dvd_prod_of_mem は,もし n が有限集合 s の元であれば, n i in s, i を割ることができることを教えてくれます.

example (s : Finset ) (n : ) (h : n  s) : n   i in s, i :=
  Finset.dvd_prod_of_mem _ h

また n が素数で s が素数の集合である場合は上記の逆も成り立つことも知っておく必要があります.これを示すには次の補題が必要です.この証明には定理 Nat.Prime.eq_one_or_self_of_dvd を使うことができます.

theorem _root_.Nat.Prime.eq_of_dvd_of_prime {p q : }
      (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p  q) :
    p = q := by
  sorry

この補題を使って素数 p が素数の有限集合の積を割り切る場合,そのうちの1つと等しいことを示すことができます.Mathlibは有限集合の帰納法について便利な原理を提供しています.任意の有限集合 s の性質が成り立つことを示すには,空集合でその性質が成り立ち,新しい元 a s を1つ追加してもその性質が保たれることを示すことで出来るというものです.この原理は Finset.induction_on として知られています.これを使うように帰納法のタクティクに指示する際には, as の名前と帰納法のステップの仮定 a s の名前,帰納的仮説の名前を指定することもできます.式 Finset.insert a ssa の単集合の和を表します.恒等式 Finset.prod_emptyFinset.prod_insert は積に関連する書き換えルールです.以下の証明では最初の simpFinset.prod_empty を適用しています.帰納法がどのように展開され,そして完成されるかを見るために証明の冒頭から順を追って確認してください.

theorem mem_of_dvd_prod_primes {s : Finset } {p : } (prime_p : p.Prime) :
    ( n  s, Nat.Prime n)  (p   n in s, n)  p  s := by
  intro h₀ h₁
  induction' s using Finset.induction_on with a s ans ih
  · simp at h₁
    linarith [prime_p.two_le]
  simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
  rw [mem_insert]
  sorry

本題の証明を行うには有限集合についてあと一つの性質が必要です.ある元 s : Set αα についての述語 P が与えられた時, Chapter 4 では P を満たす s の元の集合を { x s | P x } と書いていました. s : Finset α の場合,同じような概念は s.filter P と書きます.

example (s : Finset ) (x : ) : x  s.filter Nat.Prime  x  s  x.Prime :=
  mem_filter

これで素数が無限にあることについての別の形式化を証明できます.すなわち,任意の s : Finset について,s の元ではない素数 p が存在します.矛盾を導くために,すべての素数が s に存在することを仮定し,そこからすべての素数のみを含む集合 s' に絞り込みます.この集合の積を取り,1を加え,その結果の素因数を求めることで期待している矛盾が導かれます.下のスケッチを完成させましょう.最初の have の証明では Finset.prod_pos を使うことができます.

theorem primes_infinite' :  s : Finset Nat,  p, Nat.Prime p  p  s := by
  intro s
  by_contra h
  push_neg at h
  set s' := s.filter Nat.Prime with s'_def
  have mem_s' :  {n : }, n  s'  n.Prime := by
    intro n
    simp [s'_def]
    apply h
  have : 2  ( i in s', i) + 1 := by
    sorry
  rcases exists_prime_factor this with p, pp, pdvd
  have : p   i in s', i := by
    sorry
  have : p  1 := by
    convert Nat.dvd_sub' pdvd this
    simp
  show False
  sorry

さて,ここまでで素数が無限に存在するということについて2通りの言及の仕方を見てきました.一つは素数がどのような n にも束縛されないという言い方で,もう一つは素数がどのような有限集合 s にも含まれないという言い方です.以下の2つの証明はこれらの形式化が等価であることを示しています.2つ目では s.filter Q を形式化するために, Q が成り立つかどうかを決定する手順があると仮定しなければなりません.これについてLeanは Nat.Prime 用の手続きがあることを知っています.一般的に, open Classical と書いて古典論理を使うことで,この仮定を省くことができます.

Mathlibでは, Finset.sup s fxs の範囲にある時の f x の上限を表します. s が空集合で f の余域が の場合は 0 を返します.最初の証明では s.sup idid は恒等関数です)を s の最大値を指すために使っています.

theorem bounded_of_ex_finset (Q :   Prop) :
    ( s : Finset ,  k, Q k  k  s)   n,  k, Q k  k < n := by
  rintro s, hs
  use s.sup id + 1
  intro k Qk
  apply Nat.lt_succ_of_le
  show id k  s.sup id
  apply le_sup (hs k Qk)

theorem ex_finset_of_bounded (Q :   Prop) [DecidablePred Q] :
    ( n,  k, Q k  k  n)   s : Finset ,  k, Q k  k  s := by
  rintro n, hn
  use (range (n + 1)).filter Q
  intro k
  simp [Nat.lt_succ_iff]
  exact hn k

無限に多くの素数が存在するということの2つ目の証明については4を法とした3に合同な素数が無限に存在することを示す別バージョンが存在します.この事実の証明の流れは次のようになります.まず,2つの数 \(m\)\(n\) の積が4を法として3に合同である場合,2つの数のどちらかが4を法として3に合同であることに気づきます.結局の所どちらも奇数でなければならず,もし両方共4を法として1に合同であればその積も同じとなるからです.この観察を使って2より大きいある数が4を法として3に合同であるならば,その数は4を法として3に合同である素因数を持つことを示すことができます.

ここで4を法として3に合同な素数が有限個だけあると仮定し, \(p_1, \ldots, p_k\) と書くことにします.そして \(p_1 = 3\) を仮定しても一般性を欠きません.ここで積 \(4 \prod_{i = 2}^k p_i + 3\) を考えてみます.これが4を法として3に合同であることは簡単にわかるため,4を法として3に合同な素因数 \(p\) を持つことになります.もし \(p\) が3だとすると, \(p\)\(4 \prod_{i = 2}^k p_i + 3\) を割り切れることになってしまうため, \(p=3\) はありえません.また \(\prod_{i = 2}^k p_i\) も割り切れることになり,これにより \(p\)\(i = 2, \ldots, k\)\(p_i\) のどれかと等しいことを導いてしまうことからもこのリストから3を除外しています.従って \(p\)\(p_i\) の他の元のどれかでなければなりません.しかしその場合, \(p\)\(4 \prod_{i = 2}^k p_i\) を割るため,3が導かれますが,これは \(p\) が3ではないとして事実に矛盾します.

Leanでは, n % m という表記は「 n modulo m 」と読み, nm で割ったあまりを表します.

example : 27 % 4 = 3 := by norm_num

n が4を法として3に合同である」という命題は n % 4 = 3 と表すことができます.以下の例と定理はこの後で使うこの関数についての事実を要約したものです.1つ目の名前付きの定理は先程利用した小さい数についてのケース分割による推論の別の例です.2つ目の名前付きの定理において,セミコロンがそれに続くタクティクのブロックを,その前に実行したタクティクによって生み出されたすべてのゴールそれぞれに適用していることを覚えておいてください.

example (n : ) : (4 * n + 3) % 4 = 3 := by
  rw [add_comm, Nat.add_mul_mod_self_left]

theorem mod_4_eq_3_or_mod_4_eq_3 {m n : } (h : m * n % 4 = 3) : m % 4 = 3  n % 4 = 3 := by
  revert h
  rw [Nat.mul_mod]
  have : m % 4 < 4 := Nat.mod_lt m (by norm_num)
  interval_cases m % 4 <;> simp [-Nat.mul_mod_mod]
  have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
  interval_cases n % 4 <;> simp

theorem two_le_of_mod_4_eq_3 {n : } (h : n % 4 = 3) : 2  n := by
  apply two_le <;>
    · intro neq
      rw [neq] at h
      norm_num at h

また以下に示す mn の自明ではない約数である場合, n / m もまた同様であるという事実も必要です. Nat.div_dvd_of_dvdNat.div_lt_self を使って証明を完成させてみましょう.

theorem aux {m n : } (h₀ : m  n) (h₁ : 2  m) (h₂ : m < n) : n / m  n  n / m < n := by
  sorry

さて,これらすべてのピースを組み合わせて4を法として3に合同な数には同じ性質を持つ素因数があることを証明しましょう.

theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) :
     p : Nat, p.Prime  p  n  p % 4 = 3 := by
  by_cases np : n.Prime
  · use n
  induction' n using Nat.strong_induction_on with n ih
  rw [Nat.prime_def_lt] at np
  push_neg at np
  rcases np (two_le_of_mod_4_eq_3 h) with m, mltn, mdvdn, mne1
  have mge2 : 2  m := by
    apply two_le _ mne1
    intro mz
    rw [mz, zero_dvd_iff] at mdvdn
    linarith
  have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn
  have : m % 4 = 3  n / m % 4 = 3 := by
    apply mod_4_eq_3_or_mod_4_eq_3
    rw [neq, h]
  rcases this with h1 | h1
  . sorry
  . sorry

ここからが本番です.素数の集合 s が与えられたときに,その集合から3が存在する場合に3を取り除いたものについて語る必要があります.関数 Finset.erase がこれを実現します.

example (m n : ) (s : Finset ) (h : m  erase s n) : m  n  m  s := by
  rwa [mem_erase] at h

example (m n : ) (s : Finset ) (h : m  erase s n) : m  n  m  s := by
  simp at h
  assumption

これで4を法とした3に合同な素数が無限にあることを証明する準備ができました.以下の欠けている箇所を埋めましょう.本書で用意している解答では Nat.dvd_add_iff_leftNat.dvd_sub' を途中で使っています.

theorem primes_mod_4_eq_3_infinite :  n,  p > n, Nat.Prime p  p % 4 = 3 := by
  by_contra h
  push_neg at h
  rcases h with n, hn
  have :  s : Finset Nat,  p : , p.Prime  p % 4 = 3  p  s := by
    apply ex_finset_of_bounded
    use n
    contrapose! hn
    rcases hn with p, pp, p4⟩, pltn
    exact p, pltn, pp, p4
  rcases this with s, hs
  have h₁ : ((4 *  i in erase s 3, i) + 3) % 4 = 3 := by
    sorry
  rcases exists_prime_factor_mod_4_eq_3 h₁ with p, pp, pdvd, p4eq
  have ps : p  s := by
    sorry
  have pne3 : p  3 := by
    sorry
  have : p  4 *  i in erase s 3, i := by
    sorry
  have : p  3 := by
    sorry
  have : p = 3 := by
    sorry
  contradiction

もしこの証明を完成させることができましたらおめでとうございます!これは形式化において重大な偉業です.