5. 초등 정수론

이 장에서는 정수론의 몇 가지 초등적인 결과를 형식화하는 방법을 보여드립니다. 더 본격적인 수학적 내용을 다루게 되면서, 이미 익힌 기술들을 바탕으로 증명은 더 길고 복잡해질 것입니다.

5.1. 무리수 근

고대 그리스인들에게 알려진 사실, 즉 2의 제곱근이 무리수라는 사실부터 시작해 봅시다. 그렇지 않다고 가정하면, \(\sqrt{2} = a / b\)를 기약분수로 쓸 수 있습니다. 양변을 제곱하면 \(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\)가 공통 인수를 갖지 않는다는 것을 뜻하며, 다시 말해 두 수가 서로소임을 의미합니다. Mathlib은 술어 Nat.Coprime m n을 Nat.gcd m n = 1로 정의합니다. Lean의 익명 투영 표기법을 사용하면, s와 t가 Nat 타입의 식일 때 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

우리는 제 2.4 절에서 이미 gcd 함수를 접한 바 있습니다. 정수에 대한 gcd의 버전도 있으며, 서로 다른 수 체계 사이의 관계에 대한 논의는 아래에서 다시 다루겠습니다. 일반적인 대수적 구조의 클래스에서 의미가 통하는 일반화된 gcd 함수와 일반화된 Prime, Coprime 개념도 존재합니다. 다음 장에서 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

자연수에서 소수는 자명하지 않은 인수들의 곱으로 표현될 수 없다는 성질을 가집니다. 더 넓은 수학적 맥락에서, 이러한 성질을 가지는 환의 원소는 기약원이라고 합니다. 환의 원소가 어떤 곱을 나눌 때마다 그 인수들 중 하나를 나눈다면, 그 원소는 소원이라고 합니다. 자연수에서는 이 두 개념이 일치한다는 것이 중요한 성질이며, 이로부터 정리 Nat.Prime.dvd_mul이 도출됩니다.

우리는 이 사실을 이용하여 위 논증에서 핵심적인 성질을 확립할 수 있습니다: 어떤 수의 제곱이 짝수이면, 그 수 역시 짝수입니다. 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

진행하면서, 여러분은 필요한 사실을 찾는 데 능숙해져야 합니다. 이름의 접두사를 추측할 수 있고 관련 라이브러리를 임포트했다면, 탭 완성(때로는 ctrl-tab을 사용)을 이용해 찾고자 하는 것을 찾을 수 있다는 점을 기억하십시오. 어떤 식별자에서든 ctrl-click을 사용하면 그것이 정의된 파일로 이동할 수 있으며, 이를 통해 근처의 정의와 정리를 둘러볼 수 있습니다. Lean community web pages의 검색 엔진을 사용할 수도 있으며, 그래도 안 되면 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를 사용하여 증명 스케치를 완성할 수 있는지 시도해 보십시오.

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_le와 Nat.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 \ne p n^2\)임을 보이는 간단한 증명입니다. \(m^2 = p n^2\)라고 가정하고 \(m\)과 \(n\)을 소인수분해하여 살펴보면, \(p\)는 등식의 좌변에서는 짝수 번 나타나고 우변에서는 홀수 번 나타나므로 모순입니다. 이 논증에서는 \(n\)이, 그리고 따라서 \(m\)도 0이 아니어야 한다는 점에 유의하십시오. 아래의 형식화는 이 가정이 충분함을 확인해 줍니다.

유일 인수분해 정리는 0이 아닌 임의의 자연수가 소수들의 곱으로 유일하게 표현될 수 있음을 말합니다. Mathlib은 이에 대한 형식적 버전을, 어떤 수의 소인수 목록을 감소하지 않는 순서로 반환하는 Nat.primeFactorsList 함수로 표현하여 담고 있습니다. 이 라이브러리는 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 함수가 있다는 사실을 사용하겠습니다. 구체적으로, n.factorization p라고도 쓸 수 있는 Nat.factorization n p는 n의 소인수분해에서 p의 중복도를 반환합니다. 다음 세 가지 사실을 사용하겠습니다.

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에서 유한 지지를 갖는 함수로 정의되어 있으며, 이는 위의 증명을 단계별로 살펴볼 때 보게 될 이상한 표기법을 설명해 줍니다. 지금은 이 부분에 대해 걱정하지 않으셔도 됩니다. 여기서의 목적을 위해서는 위의 세 정리를 블랙박스로 사용할 수 있습니다.

다음 예제는 단순화기가 n^2 ≠ 0을 n ≠ 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

이 증명의 좋은 점은 일반화도 가능하다는 것입니다. 2에는 특별한 점이 없습니다. 약간의 수정만으로도, m^k = r * n^k로 쓸 때마다 r에서 소수 p의 중복도가 k의 배수여야 함을 이 증명이 보여줍니다.

r * n^k에 대해 Nat.count_factors_mul_of_pos를 사용하려면 r이 양수임을 알아야 합니다. 그러나 r이 0일 때는 아래 정리가 자명하며, simplifier로 쉽게 증명됩니다. 따라서 이 증명은 경우를 나누어 진행됩니다. rcases r with _ | r 줄은 목표를 두 가지 버전으로 바꿉니다. 하나는 r이 0으로 대체된 것이고, 다른 하나는 r이 r + 1로 대체된 것입니다. 두 번째 경우에는 r + 1 ≠ 0을 증명하는 정리 r.succ_ne_zero를 사용할 수 있습니다(succ는 successor를 뜻합니다).

또한 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 (eq_zero_of_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의 제곱근을 두 정수의 몫으로 쓸 수 있다면 두 자연수의 몫으로도 쓸 수 있다는 것은 수학적으로 자명하지만, 이를 형식적으로 증명하는 데는 어느 정도 노력이 필요합니다.

Mathlib에서 자연수, 정수, 유리수, 실수, 복소수는 서로 별개의 데이터 타입으로 표현됩니다. 각 영역에 주의를 국한시키는 것이 흔히 도움이 됩니다. 자연수에 대해 귀납법을 적용하기가 쉽다는 것을 보게 될 것이며, 실수가 관여하지 않을 때 정수의 나눗셈 가능성을 추론하기가 가장 쉽습니다. 하지만 서로 다른 영역 사이를 중재해야 하는 것은 골칫거리이며, 이는 우리가 감당해야 할 문제입니다. 이 문제는 이 장의 뒷부분에서 다시 다루겠습니다.

마지막 정리의 결론도 강화하여 수 r이 k 제곱수라고 말할 수 있어야 하는데, 이는 그 k 제곱근이 r을 나누는 각 소수를 r에서의 중복도를 k로 나눈 값만큼 거듭제곱한 것들의 곱에 불과하기 때문입니다. 이를 위해서는 유한 집합에 대한 곱과 합을 추론하는 더 나은 방법이 필요하며, 이 역시 나중에 다시 다룰 주제입니다.

사실 이 절의 결과는 모두 Mathlib의 Data.Real.Irrational에서 훨씬 더 일반적인 형태로 확립되어 있습니다. multiplicity라는 개념은 임의의 가환 모노이드에 대해 정의되며, 자연수에 무한대 값을 추가한 확장된 자연수 enat에서 값을 취합니다. 다음 장에서는 Lean이 이러한 종류의 일반성을 지원하는 방식을 이해하기 위한 수단을 개발하기 시작하겠습니다.

5.2. 귀납법과 재귀

자연수의 집합 \(\mathbb{N} = \{ 0, 1, 2, \ldots \}\)은 그 자체로 근본적으로 중요할 뿐만 아니라, 새로운 수학적 대상을 구성하는 데에도 핵심적인 역할을 합니다. Lean의 기초는 귀납적 타입을 선언할 수 있게 해주며, 이는 주어진 생성자 목록에 의해 귀납적으로 생성되는 타입입니다. Lean에서 자연수는 다음과 같이 선언됩니다.

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

#check Nat을 작성한 다음 식별자 Nat에 ctrl-click을 사용하면 라이브러리에서 이를 찾을 수 있습니다. 이 명령은 Nat이 두 생성자 zero : Nat과 succ : Nat → Nat에 의해 자유롭고 귀납적으로 생성되는 데이터타입임을 명시합니다. 물론 라이브러리는 각각 Nat과 zero에 대해 ℕ과 0이라는 표기법을 도입합니다. (숫자는 이진 표현으로 변환되지만, 지금은 그 세부 사항에 대해 걱정할 필요가 없습니다.)

현업 수학자에게 “자유롭다”는 말이 의미하는 바는, 타입 Nat이 원소 zero와 단사 후속 함수 succ를 가지며, 이 함수의 치역에는 zero가 포함되지 않는다는 것입니다.

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

이 문법은 익숙해지는 데 다소 시간이 걸립니다. 첫 번째 줄에 :=가 없다는 점에 주목하십시오. 다음 두 줄은 재귀적 정의의 기저 사례와 귀납 단계를 제공합니다. 이 방정식들은 정의상 성립하지만, simp나 rw에 이름 fac을 제공함으로써 수동으로 사용할 수도 있습니다.

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-click을 사용하여 그곳으로 이동할 수 있습니다. 예시를 위해 이후에도 예제에서 fac을 계속 사용하겠습니다. Nat.factorial의 정의 앞에 있는 @[simp] 주석은 단순화기가 기본적으로 사용하는 항등식 데이터베이스에 정의 방정식을 추가해야 함을 명시합니다.

귀납법의 원리에 따르면, 어떤 명제가 0에 대해 성립함을 보이고, 자연수 \(n\)에 대해 성립할 때마다 \(n + 1\)에 대해서도 성립함을 보임으로써 자연수에 관한 일반적인 명제를 증명할 수 있습니다. 따라서 아래 증명의 induction' n with n ih 줄은 두 개의 목표를 만들어냅니다. 첫 번째 목표에서는 0 < fac 0을 증명해야 하고, 두 번째 목표에서는 추가된 가정 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_succ나 pow_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의 공역은 0을 갖는 교환적이고 결합적인 덧셈 연산을 지원하는 임의의 타입일 수 있습니다. Algebra.BigOperators.Ring을 임포트하고 open BigOperators 명령을 실행하면, 더 직관적인 표기법인 ∑ x ∈ 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 ∈ s, f x :=
  rfl

example : s.prod f = ∏ x ∈ s, f x :=
  rfl

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

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

Finset.sum_range_zero와 Finset.sum_range_succ 사실은 \(n\)까지의 합에 대한 재귀적 서술을 제공하며, 곱에 대해서도 마찬가지입니다.

example (f : ℕ → ℕ) : ∑ x ∈ range 0, f x = 0 :=
  Finset.sum_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∑ x ∈ range n.succ, f x = ∑ x ∈ range n, f x + f n :=
  Finset.sum_range_succ f n

example (f : ℕ → ℕ) : ∏ x ∈ range 0, f x = 1 :=
  Finset.prod_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∏ x ∈ range n.succ, f x = (∏ x ∈ range n, f x) * f n :=
  Finset.prod_range_succ f n

각 쌍의 첫 번째 항등식은 정의상 성립하는데, 다시 말해 증명을 rfl로 대체할 수 있습니다.

다음은 우리가 곱으로 정의한 계승 함수를 나타냅니다.

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

mul_comm을 단순화 규칙으로 포함시킨다는 사실은 언급할 만합니다. x * y = y * x라는 항등식으로 단순화하는 것은 보통 무한히 반복되므로 위험해 보일 것입니다. Lean의 단순화기는 이를 인식할 만큼 똑똑하며, 항들의 어떤 고정되었지만 임의적인 순서에서 결과 항이 더 작은 값을 가지는 경우에만 규칙을 적용합니다. 다음 예제는 mul_assoc, mul_comm, mul_left_comm 세 규칙을 사용한 단순화가 괄호의 배치와 변수의 순서를 제외하면 동일한 곱을 식별해낸다는 것을 보여줍니다.

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

대략적으로, 이 규칙들은 괄호를 오른쪽으로 밀어낸 다음 양쪽의 식을 동일한 표준 순서를 따를 때까지 재정렬하는 방식으로 작동합니다. 이러한 규칙들과 덧셈에 대응하는 규칙들로 단순화하는 것은 유용한 요령입니다.

합 항등식으로 돌아와서, 자연수를 \(n\)까지 포함해서 합한 값이 \(n (n + 1) / 2\)임을 보이는 다음 증명을 단계별로 따라가 볼 것을 권장합니다. 증명의 첫 단계는 분모를 제거합니다. 이는 항등식을 형식화할 때 일반적으로 유용한데, 나눗셈을 포함한 계산에는 대체로 부수 조건이 있기 때문입니다. (마찬가지로 가능하면 자연수에서 뺄셈을 사용하지 않는 것이 유용합니다.)

theorem sum_id (n : ℕ) : ∑ i ∈ 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 ∈ range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
  sorry

Lean의 core library에서 덧셈과 곱셈 자체가 재귀적 정의를 사용해 정의되며, 그 기본 성질은 귀납법을 사용해 증명됩니다. 이런 근본적인 주제에 대해 생각하는 것을 좋아한다면, 곱셈과 덧셈의 교환법칙과 결합법칙, 그리고 덧셈에 대한 곱셈의 분배법칙의 증명을 직접 해보는 것을 즐길 수 있을 것입니다. 아래의 개요를 따라 자연수의 사본에서 이를 해볼 수 있습니다. MyNat에 induction 택틱을 사용할 수 있다는 점에 주목하십시오. Lean은 관련된 귀납법 원리(이는 물론 Nat에 대한 것과 동일합니다)를 사용해야 한다는 것을 알아낼 만큼 충분히 똑똑합니다.

덧셈의 교환법칙부터 시작하겠습니다. 덧셈과 곱셈이 두 번째 인자에 대한 재귀로 정의되기 때문에, 일반적으로 그 위치에 나타나는 변수에 대한 귀납법으로 증명하는 것이 유리하다는 것이 좋은 경험법칙입니다. 결합법칙의 증명에서 어떤 변수를 사용할지 결정하는 것은 다소 까다롭습니다.

0, 1, 덧셈, 곱셈에 대한 일반적인 표기법 없이 작성하면 헷갈릴 수 있습니다. 이러한 표기법을 정의하는 방법은 나중에 배우겠습니다. MyNat 이름공간 안에서 작업한다는 것은 MyNat.zero와 MyNat.succ 대신 zero와 succ를 쓸 수 있다는 것, 그리고 이러한 이름 해석이 다른 것들보다 우선한다는 것을 의미합니다. 이름공간 밖에서는, 예를 들어 아래에서 정의된 add의 전체 이름은 MyNat.add입니다.

만약 이런 종류의 일을 정말로 즐긴다는 것을 알게 된다면, 절단 뺄셈과 거듭제곱을 정의하고 그 성질 중 일부도 증명해보십시오. 절단 뺄셈은 0에서 잘린다는 것을 기억하십시오. 이를 정의하려면, 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
  | _, 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\)도 나누므로, 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 Not 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 Not at h
  revert h0 h1
  revert h m
  decide

정리 two_le를 손에 넣었으니, 2보다 큰 모든 자연수가 소수 약수를 가진다는 것을 보이는 데서 시작해 봅시다. Mathlib에는 가장 작은 소수 약수를 반환하는 함수 Nat.minFac이 있지만, 라이브러리의 새로운 부분을 배우기 위해 이를 사용하지 않고 정리를 직접 증명하겠습니다.

여기서는 일반적인 귀납법만으로는 충분하지 않습니다. 우리는 강한 귀납법을 사용하려 하는데, 이는 모든 수 \(n\)에 대해 \(n\)보다 작은 모든 값에서 \(P\)가 성립하면 \(n\)에서도 성립함을 보임으로써, 모든 자연수 \(n\)이 성질 \(P\)를 가짐을 증명할 수 있게 해 줍니다. Lean에서 이 원리는 Nat.strong_induction_on이라고 불리며, using 키워드를 사용하여 귀납법 택틱이 이를 사용하도록 지정할 수 있습니다. 그렇게 하면 기본 단계(base case)가 없다는 점에 주목하십시오. 이는 일반적인 귀납법 단계에 포함됩니다.

논증은 간단히 다음과 같습니다. 조건 \(n ≥ 2\)를 가정할 때, \(n\)이 소수라면 이것으로 증명이 끝납니다. 그렇지 않다면, 소수라는 것이 무엇을 의미하는지에 대한 여러 특성화 중 하나에 따라 \(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 Not 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_pos, Nat.dvd_factorial, Nat.dvd_sub'를 사용할 수 있습니다.

theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by
  intro n
  have : 2 ≤ Nat.factorial n + 1 := by
    sorry
  rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
  refine ⟨p, ?_, pp⟩
  show p > n
  by_contra ple
  push Not at ple
  have : p ∣ Nat.factorial n := 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)과 관련된 대부분의 동치는 정의상 성립하지 않으므로, Finset.subset_iff, Finset.mem_union, Finset.mem_inter, Finset.mem_sdiff와 같은 동치를 사용하여 수동으로 전개해야 합니다. ext 택틱은 여전히 한쪽의 모든 원소가 다른 쪽의 원소임을 보임으로써 두 유한 집합이 같음을 보이는 데 사용할 수 있습니다.

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!)은 명제 항진식을 처리하는 데 사용할 수 있습니다. 이 방법들을 사용하여 아래 두 예제를 증명할 수 있는지 확인해 보십시오.

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 ∈ s, i를 나눈다는 것을 말해줍니다.

example (s : Finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ ∏ i ∈ 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가 유한한 소수 집합의 곱을 나눌 때, 그 소수가 그 집합의 원소 중 하나와 같음을 보일 수 있습니다. Mathlib은 유한 집합에 대한 유용한 귀납법 원리를 제공합니다: 임의의 유한 집합 s에 대해 어떤 성질이 성립함을 보이려면, 그 성질이 공집합에서 성립함을 보이고, 새로운 원소 a ∉ s 하나를 추가할 때 그 성질이 보존됨을 보이면 됩니다. 이 원리는 Finset.induction_on으로 알려져 있습니다. 귀납법 택틱에게 이를 사용하도록 지시할 때, 이름 a와 s, 귀납 단계에서의 가정 a ∉ s의 이름, 그리고 귀납 가설의 이름도 지정할 수 있습니다. 표현식 Finset.insert a s는 s와 단원소 집합 a의 합집합을 나타냅니다. 그러면 항등식 Finset.prod_empty와 Finset.prod_insert가 곱에 대한 관련 재작성 규칙을 제공합니다. 아래 증명에서 첫 번째 simp는 Finset.prod_empty를 적용합니다. 증명의 시작 부분을 단계별로 실행하여 귀납법이 전개되는 것을 확인한 다음, 나머지를 완성하십시오.

theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) :
    (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n ∈ 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 Not 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 ∈ s', i) + 1 := by
    sorry
  rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
  have : p ∣ ∏ i ∈ s', i := by
    sorry
  have : p ∣ 1 := by
    convert Nat.dvd_sub pdvd this
    simp
  show False
  sorry

이렇게 소수가 무한히 많다고 말하는 두 가지 방법을 살펴보았습니다: 어떤 n으로도 유계가 아니라고 말하는 방법과, 어떤 유한 집합 s에도 포함되지 않는다고 말하는 방법입니다. 아래의 두 증명은 이 두 표현이 동치임을 보여줍니다. 두 번째 증명에서는, s.filter Q를 구성하기 위해 Q가 성립하는지 여부를 판정하는 절차가 존재한다고 가정해야 합니다. Lean은 Nat.Prime에 대한 절차가 존재함을 알고 있습니다. 일반적으로 open Classical을 작성하여 고전 논리를 사용하면, 이 가정을 생략할 수 있습니다.

Mathlib에서 Finset.sup s f는 x가 s를 범위로 움직일 때 f x의 값들의 상한을 나타내며, s가 공집합이고 f의 공역이 ℕ인 경우에는 0을 반환합니다. 첫 번째 증명에서는, id가 항등 함수인 s.sup id를 사용하여 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
  simpa using hn k

소수가 무한히 많다는 두 번째 증명을 약간 변형하면, 4로 나눈 나머지가 3인 소수가 무한히 많음을 보일 수 있습니다. 논증은 다음과 같습니다. 먼저, 두 수 \(m\)과 \(n\)의 곱이 4로 나눈 나머지가 3이면, 그중 하나는 4로 나눈 나머지가 3임에 주목하십시오. 어차피 둘 다 홀수여야 하며, 만약 둘 다 4로 나눈 나머지가 1이라면 그 곱도 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도 나누게 되는데, 이는 그것이 3이 아니라는 사실과 모순됩니다.

Lean에서 표기법 n % m은 “n 모듈로 m”이라고 읽으며, n을 m으로 나눈 나머지를 나타냅니다.

example : 27 % 4 = 3 := by norm_num

그러면 “n은 4를 법으로 3과 합동임”이라는 명제를 n % 4 = 3으로 나타낼 수 있습니다. 다음 예제와 정리들은 이 함수에 대해 아래에서 사용할 사실들을 요약합니다. 이름이 붙은 첫 번째 정리는 적은 수의 경우로 나누어 추론하는 방식을 보여주는 또 다른 예시입니다. 이름이 붙은 두 번째 정리에서, 세미콜론은 뒤따르는 택틱 블록이 앞선 택틱에 의해 생성된 모든 목표에 적용됨을 뜻한다는 점을 기억하십시오.

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

다음 사실도 필요합니다. 이는 만약 m이 n의 자명하지 않은 약수라면, n / m도 마찬가지라는 것을 말합니다. Nat.div_dvd_of_dvd와 Nat.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 Not 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이 그 집합에 있다면 그것을 제거한 결과에 대해 이야기할 필요가 있습니다. 함수 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_left와 Nat.dvd_sub'을 사용합니다.

theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3 := by
  by_contra h
  push Not 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 ∈ 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 ∈ erase s 3, i := by
    sorry
  have : p ∣ 3 := by
    sorry
  have : p = 3 := by
    sorry
  contradiction

증명을 완성했다면, 축하합니다! 이는 상당한 형식화의 위업이었습니다.

5.4. 더 많은 귀납법

앞서 제 5.2 절에서 자연수에 대한 재귀법으로 계승 함수를 정의하는 방법을 살펴보았습니다.

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

또한 induction' 택틱을 사용하여 정리를 증명하는 방법도 살펴보았습니다.

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 택틱은 더 구조화된 구문을 허용합니다.

example (n : ℕ) : 0 < fac n := by
  induction n
  case zero =>
    rw [fac]
    exact zero_lt_one
  case succ n ih =>
    rw [fac]
    exact mul_pos n.succ_pos ih

example (n : ℕ) : 0 < fac n := by
  induction n with
  | zero =>
    rw [fac]
    exact zero_lt_one
  | succ n ih =>
    rw [fac]
    exact mul_pos n.succ_pos ih

평소와 같이 induction 키워드 위에 마우스를 올리면 문서를 읽을 수 있습니다. 경우들의 이름인 zero와 succ는 ℕ 타입의 정의에서 가져온 것입니다. succ 케이스에서는 귀납법 변수와 귀납적 가설에 원하는 이름을 자유롭게 선택할 수 있다는 점에 주목하십시오. 여기서는 각각 n과 ih입니다. 재귀 함수를 정의할 때 사용한 것과 같은 표기법으로 정리를 증명할 수도 있습니다.

theorem fac_pos' : ∀ n, 0 < fac n
  | 0 => by
    rw [fac]
    exact zero_lt_one
  | n + 1 => by
    rw [fac]
    exact mul_pos n.succ_pos (fac_pos' n)

:=가 없다는 점, 콜론 뒤에 ∀ n이 온다는 점, 각 경우마다 by 키워드가 있다는 점, 그리고 fac_pos' n에 대한 귀납적 호출이 있다는 점에도 주목하십시오. 마치 정리가 n에 대한 재귀 함수이고, 귀납 단계에서 재귀 호출을 하는 것과 같습니다.

이러한 정의 방식은 놀라울 정도로 유연합니다. Lean의 설계자들은 재귀 함수를 정의하는 정교한 수단을 내장했으며, 이는 귀납법에 의한 증명을 수행하는 것으로까지 확장됩니다. 예를 들어, 여러 기저 사례를 갖는 피보나치 함수를 정의할 수 있습니다.

@[simp] def fib : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

@[simp] 주석은 단순화기가 정의 방정식을 사용함을 의미합니다. rw [fib]라고 작성하여 이를 적용할 수도 있습니다. 아래에서는 n + 2 경우에 이름을 붙이는 것이 도움이 될 것입니다.

theorem fib_add_two (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := rfl

example (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := by rw [fib]

재귀 함수에 대한 Lean의 표기법을 사용하면, fib의 재귀적 정의를 반영하는 자연수에 대한 귀납법 증명을 수행할 수 있습니다. 다음 예제는 황금비 φ와 그 켤레 φ'를 이용하여 n번째 피보나치 수에 대한 명시적인 공식을 제공합니다. 실수에 대한 산술 연산은 계산 가능하지 않으므로, 우리의 정의가 코드를 생성하지 않을 것이라고 Lean에게 알려주어야 합니다.

계산을 수행하기 위해 grind 택틱을 사용할 것이며, phi와 phi’의 정의, 그리고 귀납적으로 가정된 fib_eq n과 fib_eq (n+1)을 사용하도록 지시합니다.

noncomputable section

def phi  : ℝ := (1 + √5) / 2
def phi' : ℝ := (1 - √5) / 2

theorem fib_eq : ∀ n, fib n = (phi^n - phi'^n) / √5
  | 0   => by simp
  | 1   => by unfold fib; grind [phi, phi']
  | n+2 => by unfold fib; simp [fib_eq n, fib_eq (n+1), phi, phi']; grind

end

피보나치 함수와 관련된 귀납법 증명이 반드시 그러한 형태를 취해야 하는 것은 아닙니다. 아래에서는 연속된 피보나치 수가 서로소임을 보이는 Mathlib의 증명을 재현합니다.

theorem fib_coprime_fib_succ (n : ℕ) : Nat.Coprime (fib n) (fib (n + 1)) := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [fib, Nat.coprime_add_self_right]
    exact ih.symm

Lean의 계산적 해석을 사용하여 피보나치 수를 계산할 수 있습니다.

#eval fib 6
#eval List.range 20 |>.map fib

fib의 직관적인 구현은 계산적으로 비효율적입니다. 실제로 이는 인자에 대해 지수 시간으로 실행됩니다. (왜 그런지 생각해 보십시오.) Lean에서는 실행 시간이 n에 대해 선형인 다음과 같은 꼬리 재귀 버전을 구현하고, 이것이 동일한 함수를 계산함을 증명할 수 있습니다.

def fib' (n : Nat) : Nat :=
  aux n 0 1
where aux
  | 0,   x, _ => x
  | n+1, x, y => aux n y (x + y)

theorem fib'.aux_eq (m n : ℕ) : fib'.aux n (fib m) (fib (m + 1)) = fib (n + m) := by
  induction n generalizing m with
  | zero => simp [fib'.aux]
  | succ n ih => rw [fib'.aux, ←fib_add_two, ih, add_assoc, add_comm 1]

theorem fib'_eq_fib : fib' = fib := by
  ext n
  erw [fib', fib'.aux_eq 0 n]; rfl

#eval fib' 10000

fib'.aux_eq의 증명에서 generalizing 키워드를 주목하십시오. 이는 귀납적 가설 앞에 ∀ m을 삽입하는 역할을 하며, 이를 통해 귀납법 단계에서 m이 다른 값을 취할 수 있습니다. 증명을 단계별로 따라가며 이 경우 귀납 단계에서 한정사가 m + 1로 구체화되어야 함을 확인할 수 있습니다.

rw 대신 erw(“extended rewrite”의 약자)를 사용한 점에도 주목하십시오. 이는 목표 fib'.aux_eq를 재작성하기 위해 fib 0과 fib 1이 각각 0과 1로 축약되어야 하기 때문에 사용됩니다. 택틱 erw는 매개변수를 일치시키기 위해 정의를 펼치는 데 있어 rw보다 더 적극적입니다. 이것이 항상 좋은 생각은 아닙니다. 어떤 경우에는 많은 시간을 낭비할 수 있으므로 erw는 신중하게 사용하십시오.

Mathlib에서 찾을 수 있는 또 다른 항등식의 증명에서 generalizing 키워드가 사용되는 또 다른 예시가 여기 있습니다. 이 항등식의 비형식적 증명은 여기에서 찾을 수 있습니다. 형식적 증명의 두 가지 변형을 제공합니다.

theorem fib_add (m n : ℕ) : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1) := by
  induction n generalizing m with
  | zero => simp
  | succ n ih =>
    specialize ih (m + 1)
    rw [add_assoc m 1 n, add_comm 1 n] at ih
    simp only [fib_add_two, ih]
    ring

theorem fib_add' : ∀ m n, fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
  | _, 0     => by simp
  | m, n + 1 => by
    have := fib_add' (m + 1) n
    rw [add_assoc m 1 n, add_comm 1 n] at this
    simp only [fib_add_two, this]
    ring

연습 문제로, fib_add를 사용하여 다음을 증명하십시오.

example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by
  sorry

재귀 함수를 정의하는 Lean의 메커니즘은 인자의 복잡도가 어떤 정초 측도에 따라 감소하는 한 임의의 재귀 호출을 허용할 만큼 유연합니다. 다음 예제에서는, n이 0이 아니면서 소수가 아닐 경우 그보다 작은 약수를 갖는다는 사실을 이용하여, 모든 자연수 n ≠ 1이 소수 약수를 가짐을 보입니다. (Mathlib에는 Nat 이름공간에 동일한 이름의 정리가 있지만, 여기서 제시하는 것과는 다른 증명을 사용한다는 것을 확인할 수 있습니다.)

#check (@Nat.not_prime_iff_exists_dvd_lt :
  ∀ {n : ℕ}, 2 ≤ n → (¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n))

theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime ∧ p ∣ n
  | 0 => by simpa using Exists.intro 2 Nat.prime_two
  | 1 => by simp [Nat.not_prime_one]
  | n + 2 => by
    have hn : n + 2 ≠ 1 := by omega
    simp only [Ne, not_false_iff, true_iff, hn]
    by_cases h : Nat.Prime (n + 2)
    · use n + 2, h
    · have : 2 ≤ n + 2 := by omega
      rw [Nat.not_prime_iff_exists_dvd_lt this] at h
      rcases h with ⟨m, mdvdn, mge2, -⟩
      have : m ≠ 1 := by omega
      rw [ne_one_iff_exists_prime_dvd] at this
      rcases this with ⟨p, primep, pdvdm⟩
      use p, primep
      exact pdvdm.trans mdvdn

rw [ne_one_iff_exists_prime_dvd] at this 줄은 마술 같은 트릭입니다: 우리는 증명하고 있는 바로 그 정리를 그 정리 자신의 증명 안에서 사용하고 있습니다. 이것이 작동하는 이유는 귀납적 호출이 m에서 인스턴스화되고, 현재 경우는 n + 2이며, 지역 문맥에 m < n + 2가 있기 때문입니다. Lean은 이 가설을 찾아 귀납법이 정초되어 있음을 보이는 데 사용할 수 있습니다. Lean은 무엇이 감소하는지 알아내는 데 상당히 능숙합니다; 이 경우, 정리의 진술에서 n의 선택과 미만 관계는 명백합니다. 더 복잡한 경우에는, Lean이 이 정보를 명시적으로 제공하기 위한 메커니즘을 제공합니다. Lean 참조 매뉴얼의 정초 재귀 섹션을 참고하십시오.

증명에서 때로는 후행자 경우에 귀납 가설을 필요로 하지 않으면서, 자연수 n이 0인지 후행자인지에 따라 경우를 나누어야 할 때가 있습니다. 이를 위해 cases와 rcases 택틱을 사용할 수 있습니다.

theorem zero_lt_of_mul_eq_one (m n : ℕ) : n * m = 1 → 0 < n ∧ 0 < m := by
  cases n <;> cases m <;> simp

example (m n : ℕ) : n*m = 1 → 0 < n ∧ 0 < m := by
  rcases m with (_ | m); simp
  rcases n with (_ | n) <;> simp

이는 유용한 요령입니다. 종종 자연수 n에 대한 정리가 있는데, 이때 0인 경우는 쉽습니다. n에 대해 경우를 나누어 0인 경우를 빠르게 처리하면, n이 n + 1로 치환된 원래 목표가 남습니다.