5. Teori Bilangan Elementer

Dalam bab ini, kami menunjukkan cara memformalkan beberapa hasil dasar dalam teori bilangan. Ketika kita beralih ke materi matematika yang lebih substantif, bukti-buktinya akan semakin panjang dan rumit, dengan bertumpu pada keterampilan yang telah Anda kuasai.

5.1. Akar Irasional

Mari kita mulai dengan fakta yang telah dikenal oleh bangsa Yunani kuno, yaitu bahwa akar kuadrat dari 2 merupakan bilangan irasional. Jika kita mengandaikan sebaliknya, kita dapat menulis \(\sqrt{2} = a / b\) sebagai pecahan dalam bentuk paling sederhana. Menguadratkan kedua ruas menghasilkan \(a^2 = 2 b^2\), yang menyiratkan bahwa \(a\) genap. Jika kita menulis \(a = 2c\), kita memperoleh \(4c^2 = 2 b^2\) dan dengan demikian \(b^2 = 2 c^2\). Ini menyiratkan bahwa \(b\) juga genap, bertentangan dengan asumsi bahwa \(a / b\) telah disederhanakan ke bentuk paling sederhana.

Pernyataan bahwa \(a / b\) merupakan pecahan dalam bentuk paling sederhana berarti bahwa \(a\) dan \(b\) tidak memiliki faktor persekutuan, atau dengan kata lain, keduanya saling prima. Mathlib mendefinisikan predikat Nat.Coprime m n sebagai Nat.gcd m n = 1. Dengan notasi proyeksi anonim Lean, jika s dan t adalah ekspresi bertipe Nat, kita dapat menulis s.Coprime t sebagai pengganti Nat.Coprime s t, dan hal serupa berlaku untuk Nat.gcd. Seperti biasa, Lean sering kali menguraikan definisi Nat.Coprime secara otomatis ketika diperlukan, tetapi kita juga dapat melakukannya secara manual dengan menulis ulang atau menyederhanakan menggunakan pengidentifikasi Nat.Coprime. Taktik norm_num cukup cerdas untuk menghitung nilai konkret.

#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

Kita telah menjumpai fungsi gcd di Bab 2.4. Tersedia pula versi gcd untuk bilangan bulat; nanti kita akan kembali membahas hubungan antara berbagai sistem bilangan. Bahkan tersedia fungsi gcd generik serta gagasan generik tentang Prime dan Coprime yang bermakna pada kelas umum struktur aljabar. Dalam bab berikutnya, kita akan memahami cara Lean menangani tingkat keumuman ini. Sementara itu, dalam bagian ini kita akan membatasi perhatian pada bilangan asli.

Kita juga memerlukan gagasan bilangan prima, Nat.Prime. Teorema Nat.prime_def_lt memberikan salah satu karakterisasi yang sudah dikenal, sedangkan Nat.Prime.eq_one_or_self_of_dvd memberikan karakterisasi lainnya.

#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

-- sering digunakan
example : Nat.Prime 2 :=
  Nat.prime_two

example : Nat.Prime 3 :=
  Nat.prime_three

Pada bilangan asli, bilangan prima memiliki sifat bahwa ia tidak dapat ditulis sebagai hasil kali faktor-faktor nontrivial. Dalam konteks matematika yang lebih luas, elemen gelanggang dengan sifat ini disebut tak tereduksi. Suatu elemen gelanggang disebut prima jika setiap kali ia membagi suatu hasil kali, ia membagi salah satu faktornya. Salah satu sifat penting bilangan asli ialah bahwa dalam konteks ini kedua gagasan tersebut berimpit, yang menghasilkan teorema Nat.Prime.dvd_mul.

Kita dapat menggunakan fakta ini untuk menetapkan sifat kunci dalam argumen di atas: jika kuadrat suatu bilangan adalah genap, maka bilangan tersebut juga genap. Mathlib mendefinisikan predikat Even dalam Algebra.Group.Even, tetapi karena alasan yang akan menjadi jelas di bawah ini, kita cukup menggunakan 2 ∣ m untuk menyatakan bahwa m genap.

#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

Seiring melanjutkan pembahasan, Anda perlu mahir menemukan fakta-fakta yang diperlukan. Ingatlah bahwa jika Anda dapat menebak awalan suatu nama dan telah mengimpor pustaka yang relevan, Anda dapat menggunakan pelengkapan tab (kadang-kadang dengan ctrl-tab) untuk menemukan hal yang dicari. Anda dapat menggunakan ctrl-click pada pengidentifikasi mana pun untuk melompat ke berkas tempat pengidentifikasi tersebut didefinisikan, sehingga Anda dapat menelusuri definisi dan teorema di sekitarnya. Anda juga dapat memakai mesin pencari pada laman web komunitas Lean, dan jika semua cara lain tidak berhasil, jangan ragu bertanya di Zulip.

example (a b c : Nat) (h : a * b = a * c) (h' : a ≠ 0) : b = c :=
  -- apply? menyarankan yang berikut:
  (mul_right_inj' h').mp h

Inti bukti kita bahwa akar kuadrat dari dua bersifat irasional terkandung dalam teorema berikut. Cobalah lengkapi sketsa buktinya dengan menggunakan even_of_even_sqr dan teorema 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

Sebenarnya, dengan sangat sedikit perubahan, kita dapat mengganti 2 dengan sembarang bilangan prima. Cobalah pada contoh berikutnya. Di akhir bukti, Anda perlu menurunkan kontradiksi dari p ∣ 1. Anda dapat menggunakan Nat.Prime.two_le, yang menyatakan bahwa setiap bilangan prima lebih besar dari atau sama dengan dua, serta Nat.le_of_dvd.

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

Mari kita pertimbangkan pendekatan lain. Berikut bukti singkat bahwa jika \(p\) prima, maka \(m^2 \ne p n^2\): jika kita mengasumsikan \(m^2 = p n^2\) dan meninjau faktorisasi prima \(m\) dan \(n\), maka jumlah kemunculan \(p\) di ruas kiri persamaan genap dan jumlah kemunculannya di ruas kanan ganjil, suatu kontradiksi. Perhatikan bahwa argumen ini mengharuskan \(n\), dan karenanya \(m\), tidak sama dengan nol. Formalisasi di bawah ini menegaskan bahwa asumsi tersebut sudah memadai.

Teorema faktorisasi tunggal menyatakan bahwa setiap bilangan asli selain nol dapat ditulis secara unik sebagai hasil kali bilangan-bilangan prima. Mathlib memuat versi formal teorema ini melalui fungsi Nat.primeFactorsList, yang mengembalikan daftar faktor prima suatu bilangan dalam urutan tak menurun. Pustaka membuktikan bahwa semua elemen Nat.primeFactorsList n bersifat prima, bahwa setiap n yang lebih besar dari nol sama dengan hasil kali faktor-faktornya, dan bahwa jika n sama dengan hasil kali daftar bilangan prima lainnya, maka daftar tersebut merupakan permutasi dari Nat.primeFactorsList n.

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

Anda dapat menelusuri teorema-teorema ini dan teorema lain di sekitarnya, meskipun kita belum membahas keanggotaan daftar, hasil kali, atau permutasi. Kita tidak memerlukan semua itu untuk keperluan saat ini. Sebagai gantinya, kita akan menggunakan fakta bahwa Mathlib memiliki fungsi Nat.factorization, yang merepresentasikan data yang sama sebagai sebuah fungsi. Secara khusus, Nat.factorization n p, yang juga dapat kita tulis sebagai n.factorization p, mengembalikan multiplisitas p dalam faktorisasi prima n. Kita akan menggunakan tiga fakta berikut.

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

Sebenarnya, n.factorization didefinisikan di Lean sebagai fungsi dengan dukungan berhingga, yang menjelaskan notasi tak biasa yang akan Anda lihat ketika menelusuri bukti-bukti di atas. Jangan khawatirkan hal ini sekarang. Untuk keperluan kita di sini, kita dapat menggunakan ketiga teorema di atas sebagai kotak hitam.

Contoh berikut menunjukkan bahwa penyederhana cukup cerdas untuk mengganti n^2 ≠ 0 dengan n ≠ 0. Taktik simpa hanya memanggil simp yang diikuti dengan assumption.

Cobalah gunakan identitas-identitas di atas untuk melengkapi bagian bukti yang masih kosong.

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

Salah satu hal menarik tentang bukti ini adalah bahwa bukti tersebut juga dapat digeneralisasi. Tidak ada yang istimewa tentang 2; dengan sedikit perubahan, bukti ini menunjukkan bahwa setiap kali kita menulis m^k = r * n^k, multiplisitas setiap bilangan prima p di dalam r harus merupakan kelipatan k.

Untuk menggunakan factorization_mul' pada r * n^k, kita perlu mengetahui bahwa r tidak sama dengan nol. Namun, ketika r sama dengan nol, teorema di bawah ini bersifat trivial dan mudah dibuktikan oleh penyederhana. Karena itu, bukti dijalankan dengan pemisahan kasus. Baris rcases r with _ | r mengganti sasaran dengan dua versi: satu versi yang mengganti r dengan 0, dan versi lain yang mengganti r dengan r + 1. Dalam kasus kedua, kita dapat menggunakan teorema r.succ_ne_zero, yang menetapkan r + 1 ≠ 0 (succ merupakan singkatan dari successor atau penerus).

Perhatikan pula bahwa baris yang dimulai dengan have npow_nz : memberikan term bukti singkat untuk n^k ≠ 0. Untuk memahami cara kerjanya, cobalah menggantinya dengan bukti taktik, lalu pikirkan bagaimana taktik-taktik tersebut mendeskripsikan term bukti.

Cobalah lengkapi bagian-bagian bukti di bawah ini yang masih kosong. Di bagian paling akhir, Anda dapat menggunakan Nat.dvd_sub dan Nat.dvd_mul_right untuk menyelesaikannya.

Perhatikan bahwa contoh ini tidak mengasumsikan p prima, tetapi kesimpulannya bersifat trivial ketika p tidak prima karena r.factorization p menurut definisi bernilai nol, dan bukti tersebut tetap berlaku dalam semua kasus.

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

Ada beberapa cara yang mungkin kita tempuh untuk menyempurnakan hasil-hasil ini. Pertama-tama, bukti bahwa akar kuadrat dari dua bersifat irasional seharusnya benar-benar membahas akar kuadrat dari dua, yang dapat dipahami sebagai bilangan real atau kompleks. Pernyataan bahwa bilangan itu irasional juga seharusnya membahas bilangan rasional, yakni bahwa tidak ada bilangan rasional yang sama dengannya. Selain itu, kita seharusnya memperluas teorema-teorema dalam bagian ini ke bilangan bulat. Meskipun secara matematis jelas bahwa jika akar kuadrat dari dua dapat ditulis sebagai hasil bagi dua bilangan bulat, maka ia juga dapat ditulis sebagai hasil bagi dua bilangan asli, pembuktian formalnya memerlukan sejumlah usaha.

Di Mathlib, bilangan asli, bilangan bulat, bilangan rasional, bilangan real, dan bilangan kompleks direpresentasikan oleh tipe data yang terpisah. Membatasi perhatian pada masing-masing domain sering kali membantu: kita akan melihat bahwa induksi pada bilangan asli mudah dilakukan, dan penalaran tentang keterbagian bilangan bulat paling mudah ketika bilangan real tidak ikut terlibat. Namun, menjembatani berbagai domain tersebut cukup merepotkan, dan kita harus menghadapinya. Kita akan kembali ke persoalan ini nanti dalam bab ini.

Kita juga patut berharap dapat memperkuat kesimpulan teorema terakhir untuk menyatakan bahwa bilangan r merupakan pangkat ke-k, karena akar ke-k-nya diperoleh dengan mengalikan setiap bilangan prima yang membagi r, masing-masing dipangkatkan dengan multiplisitasnya di r setelah dibagi k. Untuk melakukan hal itu, kita memerlukan sarana yang lebih baik untuk menalar tentang hasil kali dan jumlah pada himpunan berhingga, yang juga akan kita bahas kembali nanti.

Sebenarnya, semua hasil dalam bagian ini telah dibuktikan di Mathlib dengan tingkat keumuman yang jauh lebih tinggi, dalam Data.Real.Irrational. Gagasan multiplicity didefinisikan untuk sembarang monoid komutatif, dan nilainya berupa bilangan asli yang diperluas, enat, yang menambahkan nilai tak hingga pada bilangan asli. Dalam bab berikutnya, kita akan mulai mengembangkan sarana untuk memahami cara Lean mendukung tingkat keumuman semacam ini.

5.2. Induksi dan Rekursi

Himpunan bilangan asli \(\mathbb{N} = \{ 0, 1, 2, \ldots \}\) bukan hanya penting secara fundamental, melainkan juga berperan sentral dalam membangun objek matematika baru. Fondasi Lean memungkinkan kita mendeklarasikan tipe induktif, yaitu tipe yang dibangkitkan secara induktif oleh suatu daftar konstruktor. Di Lean, bilangan asli dideklarasikan sebagai berikut.

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

Anda dapat menemukan deklarasi ini di pustaka dengan menulis #check Nat, lalu menggunakan ctrl-click pada pengidentifikasi Nat. Perintah tersebut menetapkan bahwa Nat adalah tipe data yang dibangkitkan secara bebas dan induktif oleh dua konstruktor zero : Nat dan succ : Nat → Nat. Tentu saja, pustaka memperkenalkan notasi ℕ dan 0 masing-masing untuk Nat dan zero. (Lambang bilangan diterjemahkan menjadi representasi biner, tetapi kita belum perlu memikirkan rinciannya sekarang.)

Bagi matematikawan dalam praktik, kata "bebas" berarti bahwa tipe Nat memiliki elemen zero dan fungsi penerus injektif succ yang citranya tidak memuat 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

Bagi matematikawan dalam praktik, kata "induktif" berarti bahwa bilangan asli dilengkapi dengan prinsip pembuktian melalui induksi dan prinsip pendefinisian melalui rekursi. Bagian ini akan menunjukkan cara menggunakan kedua prinsip tersebut.

Berikut contoh definisi rekursif untuk fungsi faktorial.

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

Sintaks ini memerlukan sedikit pembiasaan. Perhatikan bahwa tidak ada := pada baris pertama. Dua baris berikutnya memberikan kasus dasar dan langkah induktif untuk definisi rekursif tersebut. Persamaan-persamaan ini berlaku secara definisional, tetapi juga dapat digunakan secara manual dengan memberikan fac sebagai argumen kepada simp atau rw.

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]

Sebenarnya, fungsi faktorial telah didefinisikan di Mathlib sebagai Nat.factorial. Sekali lagi, Anda dapat melompat ke definisinya dengan mengetik #check Nat.factorial dan menggunakan ctrl-click. Untuk keperluan ilustrasi, kita akan tetap menggunakan fac dalam contoh-contoh. Anotasi @[simp] sebelum definisi Nat.factorial menetapkan bahwa persamaan definisinya harus ditambahkan ke basis data identitas yang digunakan penyederhana secara bawaan.

Prinsip induksi menyatakan bahwa kita dapat membuktikan pernyataan umum tentang bilangan asli dengan membuktikan bahwa pernyataan tersebut berlaku untuk 0 dan bahwa setiap kali pernyataan itu berlaku untuk bilangan asli \(n\), ia juga berlaku untuk \(n + 1\). Karena itu, baris induction' n with n ih dalam bukti di bawah ini menghasilkan dua sasaran: pada sasaran pertama kita perlu membuktikan 0 < fac 0, sedangkan pada sasaran kedua kita memperoleh asumsi tambahan ih : 0 < fac n dan harus membuktikan 0 < fac (n + 1). Frasa with n ih digunakan untuk menamai variabel dan asumsi hipotesis induksi, dan Anda bebas memilih nama apa pun untuk keduanya.

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

Taktik induction' cukup cerdas untuk menyertakan hipotesis yang bergantung pada variabel induksi sebagai bagian dari hipotesis induksi. Telusurilah contoh berikut untuk melihat apa yang terjadi.

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

Contoh berikut memberikan batas bawah kasar untuk fungsi faktorial. Ternyata lebih mudah memulainya dengan pembuktian berdasarkan kasus, sehingga sisa bukti dimulai dari kasus \(n = 1\). Cobalah lengkapi argumennya dengan pembuktian melalui induksi menggunakan pow_succ atau pow_succ'.

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

Induksi sering digunakan untuk membuktikan identitas yang melibatkan jumlah dan hasil kali berhingga. Mathlib mendefinisikan ekspresi Finset.sum s f, dengan s : Finset α sebagai himpunan berhingga beranggotakan elemen bertipe α dan f sebagai fungsi yang didefinisikan pada α. Kodomain f dapat berupa tipe apa pun yang mendukung operasi penjumlahan komutatif dan asosiatif dengan elemen nol. Jika Anda mengimpor Algebra.BigOperators.Ring dan menjalankan perintah open BigOperators, Anda dapat menggunakan notasi yang lebih intuitif ∑ x ∈ s, f x. Tentu saja, tersedia operasi dan notasi analog untuk hasil kali berhingga.

Kita akan membahas tipe Finset dan operasi-operasi yang didukungnya dalam bagian berikutnya, lalu kembali membahasnya dalam bab selanjutnya. Untuk sekarang, kita hanya akan menggunakan Finset.range n, yaitu himpunan berhingga bilangan asli yang lebih kecil dari 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

Fakta Finset.sum_range_zero dan Finset.sum_range_succ memberikan deskripsi rekursif untuk penjumlahan hingga \(n\), dan hal serupa berlaku untuk hasil kali.

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

Identitas pertama dalam setiap pasangan berlaku secara definisional; artinya, Anda dapat mengganti buktinya dengan rfl.

Pernyataan berikut menyatakan fungsi faktorial yang kita definisikan sebagai suatu hasil kali.

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]

Fakta bahwa kita menyertakan mul_comm sebagai kaidah penyederhanaan perlu diberi penjelasan. Menyederhanakan dengan identitas x * y = y * x tampaknya berbahaya, karena biasanya hal itu akan berulang tanpa henti. Penyederhana Lean cukup cerdas untuk mengenali masalah tersebut dan hanya menerapkan kaidah ketika term yang dihasilkan memiliki nilai lebih kecil dalam suatu pengurutan term yang tetap tetapi arbitrer. Contoh berikut menunjukkan bahwa penyederhanaan menggunakan tiga kaidah mul_assoc, mul_comm, dan mul_left_comm berhasil mengenali hasil kali yang sama hingga perbedaan penempatan tanda kurung dan urutan variabel.

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]

Secara kasar, kaidah-kaidah tersebut bekerja dengan mendorong tanda kurung ke kanan, lalu mengurutkan ulang ekspresi pada kedua ruas hingga keduanya mengikuti urutan kanonik yang sama. Menyederhanakan dengan kaidah-kaidah ini, serta kaidah yang bersesuaian untuk penjumlahan, merupakan kiat yang berguna.

Kembali ke identitas penjumlahan, kami menyarankan Anda menelusuri bukti berikut bahwa jumlah bilangan asli sampai dengan \(n\) adalah \(n (n + 1) / 2\). Langkah pertama bukti tersebut menghilangkan penyebut. Cara ini umumnya berguna ketika memformalkan identitas, karena perhitungan dengan pembagian biasanya memiliki syarat samping. (Demikian pula, sebaiknya hindari pengurangan pada bilangan asli jika memungkinkan.)

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

Kami menganjurkan Anda membuktikan identitas analog untuk jumlah kuadrat, serta identitas lain yang dapat ditemukan di web.

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

Dalam pustaka inti Lean, penjumlahan dan perkalian sendiri didefinisikan menggunakan definisi rekursif, dan sifat-sifat dasarnya ditetapkan melalui induksi. Jika Anda senang memikirkan topik-topik fondasional semacam itu, Anda mungkin akan menikmati penelusuran bukti komutativitas dan asosiativitas perkalian dan penjumlahan, serta distributivitas perkalian terhadap penjumlahan. Anda dapat melakukannya pada suatu salinan tipe bilangan asli dengan mengikuti kerangka di bawah ini. Perhatikan bahwa kita dapat menggunakan taktik induction bersama MyNat; Lean cukup cerdas untuk mengetahui bahwa ia harus menggunakan prinsip induksi yang relevan (yang tentu saja sama dengan prinsip untuk Nat).

Kami membantu Anda memulai dengan komutativitas penjumlahan. Pedoman yang baik ialah bahwa karena penjumlahan dan perkalian didefinisikan secara rekursif pada argumen kedua, umumnya menguntungkan untuk melakukan pembuktian melalui induksi pada variabel yang muncul pada posisi tersebut. Menentukan variabel yang akan digunakan dalam bukti asosiativitas sedikit lebih rumit.

Menulis berbagai hal tanpa notasi yang lazim untuk nol, satu, penjumlahan, dan perkalian dapat membingungkan. Nanti kita akan mempelajari cara mendefinisikan notasi semacam itu. Bekerja dalam namespace MyNat berarti kita dapat menulis zero dan succ alih-alih MyNat.zero dan MyNat.succ, dan penafsiran nama-nama tersebut didahulukan daripada penafsiran lainnya. Di luar namespace, nama lengkap add yang didefinisikan di bawah ini, misalnya, adalah MyNat.add.

Jika Anda benar-benar menikmati hal semacam ini, cobalah mendefinisikan pengurangan terpotong dan perpangkatan, lalu buktikan pula beberapa sifatnya. Ingatlah bahwa pengurangan terpotong berhenti pada nol. Untuk mendefinisikannya, sebaiknya definisikan fungsi pendahulu, pred, yang mengurangi satu dari setiap bilangan bukan nol dan mempertahankan nol. Fungsi pred dapat didefinisikan dengan rekursi sederhana.

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. Bilangan Prima yang Tak Berhingga Banyaknya

Mari lanjutkan penelusuran kita tentang induksi dan rekursi dengan satu lagi hasil matematika klasik: bukti bahwa bilangan prima tak berhingga banyaknya. Salah satu cara merumuskannya ialah dengan menyatakan bahwa untuk setiap bilangan asli \(n\), terdapat bilangan prima yang lebih besar dari \(n\). Untuk membuktikannya, misalkan \(p\) adalah sembarang faktor prima dari \(n! + 1\). Jika \(p\) lebih kecil dari atau sama dengan \(n\), maka ia membagi \(n!\). Karena ia juga membagi \(n! + 1\), ia membagi 1, suatu kontradiksi. Jadi, \(p\) lebih besar dari \(n\).

Untuk memformalkan bukti tersebut, kita perlu menunjukkan bahwa setiap bilangan yang lebih besar dari atau sama dengan 2 memiliki faktor prima. Untuk itu, kita perlu menunjukkan bahwa setiap bilangan asli yang tidak sama dengan 0 maupun 1 lebih besar dari atau sama dengan 2. Hal ini membawa kita pada salah satu keunikan formalisasi: sering kali justru pernyataan trivial semacam inilah yang paling merepotkan untuk diformalkan. Di sini kita membahas beberapa cara untuk melakukannya.

Sebagai permulaan, kita dapat menggunakan taktik cases dan fakta bahwa fungsi penerus mempertahankan pengurutan pada bilangan asli.

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

Strategi lain ialah menggunakan taktik interval_cases, yang secara otomatis memecah sasaran menjadi beberapa kasus ketika variabel yang dimaksud berada dalam suatu interval bilangan asli atau bilangan bulat. Ingatlah bahwa Anda dapat mengarahkan kursor ke taktik tersebut untuk melihat dokumentasinya.

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

Ingat bahwa titik koma setelah interval_cases m berarti taktik berikutnya diterapkan pada setiap kasus yang dihasilkannya. Pilihan lain adalah menggunakan taktik decide, yang mencoba menemukan prosedur keputusan untuk menyelesaikan masalah. Lean mengetahui bahwa nilai kebenaran pernyataan yang diawali kuantor terbatas ∀ x, x < n → ... atau ∃ x, x < n ∧ ... dapat diputuskan dengan memutuskan setiap instans yang jumlahnya berhingga.

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

Setelah memiliki teorema two_le, mari mulai dengan menunjukkan bahwa setiap bilangan asli yang lebih besar dari atau sama dengan dua memiliki pembagi prima. Mathlib memiliki fungsi Nat.minFac yang mengembalikan pembagi prima terkecil, tetapi demi mempelajari bagian baru dari pustaka, kita tidak akan menggunakannya dan akan membuktikan teorema tersebut secara langsung.

Di sini, induksi biasa tidak memadai. Kita ingin menggunakan induksi kuat, yang memungkinkan kita membuktikan bahwa setiap bilangan asli \(n\) memiliki sifat \(P\) dengan menunjukkan bahwa untuk setiap bilangan \(n\), jika \(P\) berlaku untuk semua nilai yang lebih kecil dari \(n\), maka ia juga berlaku pada \(n\). Di Lean, prinsip ini disebut Nat.strong_induction_on, dan kita dapat menggunakan kata kunci using untuk meminta taktik induksi menggunakannya. Perhatikan bahwa dengan cara ini tidak ada kasus dasar; kasus tersebut sudah tercakup dalam langkah induksi umum.

Argumennya sederhana. Dengan mengasumsikan \(n ≥ 2\), jika \(n\) prima, bukti selesai. Jika tidak, maka menurut salah satu karakterisasi bilangan prima, ia memiliki faktor nontrivial, \(m\), dan kita dapat menerapkan hipotesis induksi pada faktor tersebut. Telusurilah bukti berikut untuk melihat bagaimana argumen ini berlangsung.

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

Sekarang kita dapat membuktikan rumusan teorema berikut. Cobalah lengkapi sketsanya. Anda dapat menggunakan Nat.factorial_pos, Nat.dvd_factorial, dan 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_neg at ple
  have : p ∣ Nat.factorial n := by
    sorry
  have : p ∣ 1 := by
    sorry
  show False
  sorry

Mari kita pertimbangkan variasi bukti di atas. Alih-alih menggunakan fungsi faktorial, misalkan kita diberi himpunan berhingga \(\{ p_1, \ldots, p_n \}\) dan meninjau suatu faktor prima dari \(\prod_{i = 1}^n p_i + 1\). Faktor prima tersebut harus berbeda dari setiap \(p_i\), yang menunjukkan bahwa tidak ada himpunan berhingga yang memuat semua bilangan prima.

Untuk memformalkan argumen ini, kita perlu menalar tentang himpunan berhingga. Di Lean, untuk sembarang tipe α, tipe Finset α merepresentasikan himpunan berhingga beranggotakan elemen bertipe α. Penalaran komputasional tentang himpunan berhingga memerlukan prosedur untuk menguji kesamaan pada α; karena itulah cuplikan di bawah ini menyertakan asumsi [DecidableEq α]. Untuk tipe data konkret seperti ℕ, ℤ, dan ℚ, asumsi tersebut dipenuhi secara otomatis. Ketika menalar tentang bilangan real, asumsi itu dapat dipenuhi dengan menggunakan logika klasik dan melepaskan interpretasi komputasional.

Kita menggunakan perintah open Finset agar dapat memakai nama yang lebih pendek untuk teorema-teorema yang relevan. Tidak seperti pada himpunan, kebanyakan ekuivalensi yang melibatkan himpunan berhingga tidak berlaku secara definisional, sehingga perlu dijabarkan secara manual menggunakan ekuivalensi seperti Finset.subset_iff, Finset.mem_union, Finset.mem_inter, dan Finset.mem_sdiff. Taktik ext tetap dapat digunakan untuk menunjukkan bahwa dua himpunan berhingga sama dengan menunjukkan bahwa setiap elemen salah satunya juga berada dalam himpunan lainnya.

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

Kita telah menggunakan kiat baru: taktik tauto (serta versi yang diperkuat, tauto!, yang menggunakan logika klasik) dapat digunakan untuk menuntaskan tautologi proposisional. Cobalah gunakan metode-metode ini untuk membuktikan dua contoh di bawah ini.

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

Teorema Finset.dvd_prod_of_mem menyatakan bahwa jika n merupakan elemen himpunan berhingga s, maka n membagi ∏ i ∈ s, i.

example (s : Finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ ∏ i ∈ s, i :=
  Finset.dvd_prod_of_mem _ h

Kita juga perlu mengetahui bahwa kebalikannya berlaku ketika n prima dan s merupakan himpunan bilangan prima. Untuk menunjukkannya, kita memerlukan lema berikut, yang seharusnya dapat Anda buktikan menggunakan teorema 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

Kita dapat menggunakan lema ini untuk menunjukkan bahwa jika bilangan prima p membagi hasil kali suatu himpunan berhingga bilangan prima, maka ia sama dengan salah satu anggotanya. Mathlib menyediakan prinsip induksi yang berguna pada himpunan berhingga: untuk menunjukkan bahwa suatu sifat berlaku pada sembarang himpunan berhingga s, tunjukkan bahwa sifat tersebut berlaku pada himpunan kosong, lalu tunjukkan bahwa sifat itu tetap berlaku ketika kita menambahkan satu elemen baru a ∉ s. Prinsip ini dikenal sebagai Finset.induction_on. Ketika meminta taktik induksi menggunakannya, kita juga dapat menentukan nama a dan s, nama untuk asumsi a ∉ s dalam langkah induktif, serta nama hipotesis induksi. Ekspresi Finset.insert a s menyatakan gabungan s dengan himpunan tunggal yang berisi a. Identitas Finset.prod_empty dan Finset.prod_insert kemudian memberikan kaidah penulisan ulang yang relevan untuk hasil kali. Dalam bukti di bawah ini, simp pertama menerapkan Finset.prod_empty. Telusurilah awal bukti untuk melihat induksi tersebut terurai, lalu selesaikan buktinya.

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

Kita memerlukan satu sifat terakhir dari himpunan berhingga. Diberikan himpunan s : Set α dan predikat P pada α, dalam Bab 4 kita menulis { x ∈ s | P x } untuk himpunan elemen s yang memenuhi P. Diberikan s : Finset α, gagasan analognya ditulis s.filter P.

example (s : Finset ℕ) (x : ℕ) : x ∈ s.filter Nat.Prime ↔ x ∈ s ∧ x.Prime :=
  mem_filter

Sekarang kita membuktikan rumusan alternatif dari pernyataan bahwa bilangan prima tak berhingga banyaknya: untuk setiap s : Finset ℕ, terdapat bilangan prima p yang bukan elemen s. Untuk memperoleh kontradiksi, kita mengasumsikan bahwa semua bilangan prima berada di s, lalu menyaringnya menjadi himpunan s' yang memuat semua bilangan prima dan tidak memuat unsur lain. Mengambil hasil kali himpunan itu, menambahkan satu, lalu mencari faktor prima dari hasilnya menghasilkan kontradiksi yang kita cari. Cobalah lengkapi sketsa di bawah ini. Anda dapat menggunakan Finset.prod_pos dalam bukti untuk have pertama.

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 ∈ 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

Dengan demikian, kita telah melihat dua cara untuk menyatakan bahwa bilangan prima tak berhingga banyaknya: menyatakan bahwa bilangan-bilangan tersebut tidak dibatasi oleh n mana pun, dan menyatakan bahwa bilangan-bilangan tersebut tidak termuat dalam himpunan berhingga s mana pun. Dua bukti di bawah ini menunjukkan bahwa kedua rumusan tersebut ekuivalen. Dalam bukti kedua, untuk membentuk s.filter Q, kita harus mengasumsikan adanya prosedur untuk memutuskan apakah Q berlaku. Lean mengetahui bahwa prosedur semacam itu tersedia untuk Nat.Prime. Secara umum, jika kita menggunakan logika klasik dengan menulis open Classical, kita tidak memerlukan asumsi tersebut.

Di Mathlib, Finset.sup s f menyatakan supremum nilai f x ketika x berkisar pada anggota s; hasilnya 0 ketika s kosong dan kodomain f adalah ℕ. Dalam bukti pertama, kita menggunakan s.sup id, dengan id sebagai fungsi identitas, untuk merujuk pada nilai maksimum di 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

Sedikit variasi pada bukti kedua kita bahwa bilangan prima tak berhingga banyaknya menunjukkan bahwa bilangan prima yang kongruen dengan 3 modulo 4 juga tak berhingga banyaknya. Argumennya sebagai berikut. Pertama, perhatikan bahwa jika hasil kali dua bilangan \(m\) dan \(n\) sama dengan 3 modulo 4, maka salah satu dari kedua bilangan tersebut kongruen dengan 3 modulo 4. Keduanya harus ganjil, dan jika keduanya kongruen dengan 1 modulo 4, hasil kalinya juga demikian. Kita dapat menggunakan pengamatan ini untuk menunjukkan bahwa jika suatu bilangan yang lebih besar dari 2 kongruen dengan 3 modulo 4, maka bilangan tersebut memiliki pembagi prima yang juga kongruen dengan 3 modulo 4.

Sekarang misalkan hanya terdapat berhingga banyak bilangan prima yang kongruen dengan 3 modulo 4, katakanlah \(p_1, \ldots, p_k\). Tanpa mengurangi keumuman, kita dapat mengasumsikan \(p_1 = 3\). Perhatikan bilangan \(4 \prod_{i = 2}^k p_i + 3\). Mudah dilihat bahwa bilangan ini kongruen dengan 3 modulo 4, sehingga ia memiliki faktor prima \(p\) yang kongruen dengan 3 modulo 4. Tidak mungkin \(p = 3\); karena \(p\) membagi \(4 \prod_{i = 2}^k p_i + 3\), jika \(p\) sama dengan 3, maka ia juga membagi \(\prod_{i = 2}^k p_i\), yang menyiratkan bahwa \(p\) sama dengan salah satu \(p_i\) untuk \(i = 2, \ldots, k\); padahal 3 telah kita keluarkan dari daftar ini. Jadi, \(p\) harus merupakan salah satu elemen \(p_i\) yang lain. Namun dalam hal itu, \(p\) membagi \(4 \prod_{i = 2}^k p_i\) dan karenanya membagi 3, bertentangan dengan fakta bahwa bilangan itu bukan 3.

Di Lean, notasi n % m, yang dibaca "n modulo m", menyatakan sisa pembagian n oleh m.

example : 27 % 4 = 3 := by norm_num

Dengan demikian, kita dapat menyatakan "n kongruen dengan 3 modulo 4" sebagai n % 4 = 3. Contoh dan teorema berikut merangkum fakta-fakta tentang fungsi ini yang akan kita gunakan di bawah. Teorema bernama pertama memberikan ilustrasi lain tentang penalaran berdasarkan sejumlah kecil kasus. Dalam teorema bernama kedua, ingat bahwa titik koma berarti blok taktik berikutnya diterapkan pada semua sasaran yang dibuat oleh taktik sebelumnya.

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

Kita juga memerlukan fakta berikut, yang menyatakan bahwa jika m merupakan pembagi nontrivial dari n, maka n / m juga demikian. Cobalah lengkapi buktinya menggunakan Nat.div_dvd_of_dvd dan 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

Sekarang satukan semua bagiannya untuk membuktikan bahwa setiap bilangan yang kongruen dengan 3 modulo 4 memiliki pembagi prima dengan sifat yang sama.

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

Kita sudah mendekati akhir. Diberikan himpunan s beranggotakan bilangan prima, kita perlu membahas hasil penghapusan 3 dari himpunan tersebut jika 3 memang ada di dalamnya. Fungsi Finset.erase menangani hal itu.

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

Sekarang kita siap membuktikan bahwa bilangan prima yang kongruen dengan 3 modulo 4 tak berhingga banyaknya. Lengkapi bagian-bagian yang masih kosong di bawah ini. Dalam prosesnya, solusi kita menggunakan Nat.dvd_add_iff_left dan Nat.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 ∈ 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

Jika Anda berhasil menyelesaikan bukti tersebut, selamat! Ini merupakan pencapaian formalisasi yang sungguh berarti.

5.4. Induksi Lebih Lanjut

Dalam Bab 5.2, kita telah melihat cara mendefinisikan fungsi faktorial melalui rekursi pada bilangan asli.

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

Kita juga telah melihat cara membuktikan teorema menggunakan taktik 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

Taktik induction (tanpa tanda prima) memungkinkan sintaks yang lebih terstruktur.

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

Seperti biasa, Anda dapat mengarahkan kursor ke kata kunci induction untuk membaca dokumentasinya. Nama kasus, zero dan succ, diambil dari definisi tipe ℕ. Perhatikan bahwa kasus succ memungkinkan Anda memilih nama apa pun untuk variabel induksi dan hipotesis induksi, yang di sini bernama n dan ih. Anda bahkan dapat membuktikan teorema dengan notasi yang sama seperti saat mendefinisikan fungsi rekursif.

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)

Perhatikan pula tidak adanya := dan ∀ n setelah titik dua, tidak adanya kata kunci by dalam setiap kasus, serta adanya pemanggilan induktif fac_pos' n. Seolah-olah teorema tersebut merupakan fungsi rekursif dari n, dan pada langkah induktif kita melakukan pemanggilan rekursif.

Gaya pendefinisian ini sangat fleksibel. Para perancang Lean telah menyediakan sarana yang canggih untuk mendefinisikan fungsi rekursif, dan sarana ini juga mencakup pembuktian melalui induksi. Sebagai contoh, kita dapat mendefinisikan fungsi Fibonacci dengan beberapa kasus dasar.

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

Anotasi @[simp] berarti bahwa penyederhana akan menggunakan persamaan definisinya. Anda juga dapat menerapkannya dengan menulis rw [fib]. Di bawah ini, akan berguna jika kasus n + 2 diberi nama.

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]

Dengan notasi Lean untuk fungsi rekursif, Anda dapat menjalankan pembuktian melalui induksi pada bilangan asli yang mencerminkan definisi rekursif fib. Contoh berikut memberikan rumus eksplisit untuk bilangan Fibonacci ke-n dalam bentuk rasio emas, φ, dan konjugatnya, φ'. Kita harus memberi tahu Lean bahwa definisi kita tidak diharapkan menghasilkan kode karena operasi aritmetika pada bilangan real tidak dapat dikomputasi.

Kita akan menggunakan taktik grind untuk melakukan komputasi dengan memintanya memakai definisi phi dan phi', serta asumsi induktif fib_eq n dan 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

Pembuktian induksi yang melibatkan fungsi Fibonacci tidak harus berbentuk demikian. Di bawah ini kita mereproduksi bukti Mathlib bahwa bilangan Fibonacci yang berurutan saling prima.

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

Dengan interpretasi komputasional Lean, kita dapat mengevaluasi bilangan Fibonacci.

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

Implementasi langsung fib tidak efisien secara komputasional. Bahkan, waktu jalannya eksponensial terhadap argumennya. (Cobalah pikirkan alasannya.) Di Lean, kita dapat mengimplementasikan versi rekursif ekor berikut, yang waktu jalannya linear terhadap n, lalu membuktikan bahwa versi tersebut menghitung fungsi yang sama.

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

Perhatikan kata kunci generalizing dalam bukti fib'.aux_eq. Kata kunci ini menyisipkan ∀ m di depan hipotesis induksi, sehingga dalam langkah induktif, m dapat mengambil nilai yang berbeda. Anda dapat menelusuri bukti tersebut dan memeriksa bahwa dalam kasus ini, kuantornya perlu diinstansiasi dengan m + 1 pada langkah induktif.

Perhatikan pula penggunaan erw (singkatan dari extended rewrite atau penulisan ulang diperluas) alih-alih rw. Hal ini diperlukan karena untuk menulis ulang sasaran fib'.aux_eq, fib 0 dan fib 1 harus direduksi masing-masing menjadi 0 dan 1. Taktik erw lebih agresif daripada rw dalam menguraikan definisi agar sesuai dengan parameter. Cara ini tidak selalu baik; dalam beberapa kasus ia dapat membuang banyak waktu, jadi gunakan erw secukupnya.

Berikut contoh lain penggunaan kata kunci generalizing dalam pembuktian identitas lain yang terdapat di Mathlib. Bukti informal identitas tersebut dapat ditemukan di sini. Kami memberikan dua varian bukti formalnya.

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

Sebagai latihan, gunakan fib_add untuk membuktikan pernyataan berikut.

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

Mekanisme Lean untuk mendefinisikan fungsi rekursif cukup fleksibel untuk mengizinkan sembarang pemanggilan rekursif, asalkan kompleksitas argumennya menurun menurut suatu ukuran yang menjamin terminasi. Dalam contoh berikut, kita menunjukkan bahwa setiap bilangan asli n ≠ 1 memiliki pembagi prima, dengan menggunakan fakta bahwa jika n bukan nol dan tidak prima, ia memiliki pembagi yang lebih kecil. (Anda dapat memeriksa bahwa Mathlib memiliki teorema bernama sama dalam namespace Nat, meskipun buktinya berbeda dari bukti yang kita berikan di sini.)

#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

Baris rw [ne_one_iff_exists_prime_dvd] at this menyerupai sulap: kita menggunakan teorema yang sedang dibuktikan di dalam buktinya sendiri. Hal ini dapat bekerja karena pemanggilan induktif diinstansiasi pada m, kasus saat ini adalah n + 2, dan konteks memuat m < n + 2. Lean dapat menemukan hipotesis tersebut dan menggunakannya untuk menunjukkan bahwa pemanggilan rekursif ini berakhir. Lean cukup pandai menentukan apa yang menurun; dalam kasus ini, pilihan n dalam pernyataan teorema dan relasi kurang-dari sudah jelas. Dalam kasus yang lebih rumit, Lean menyediakan mekanisme untuk memberikan informasi ini secara eksplisit. Lihat bagian tentang rekursi dengan jaminan terminasi dalam Manual Referensi Lean.

Kadang-kadang, dalam sebuah bukti, Anda perlu memisahkan kasus berdasarkan apakah bilangan asli n merupakan nol atau penerus, tanpa memerlukan hipotesis induksi dalam kasus penerus. Untuk itu, Anda dapat menggunakan taktik cases dan 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

Ini merupakan kiat yang berguna. Sering kali Anda memiliki teorema tentang bilangan asli n yang kasus nolnya mudah. Jika Anda memisahkan kasus pada n dan segera menyelesaikan kasus nol, sasaran asli akan tersisa dengan n diganti oleh n + 1.