2. Dasar-dasar

Bab ini dirancang untuk memperkenalkan dasar-dasar praktis penalaran matematis dalam Lean: melakukan perhitungan, menerapkan lema dan teorema, serta bernalar tentang struktur umum.

2.1. Melakukan Perhitungan

Kita umumnya belajar melakukan perhitungan matematis tanpa memandangnya sebagai bukti. Namun, ketika kita memberikan justifikasi untuk setiap langkah dalam suatu perhitungan, sebagaimana diwajibkan oleh Lean, hasil akhirnya adalah bukti bahwa ruas kiri perhitungan tersebut sama dengan ruas kanannya.

Dalam Lean, menyatakan sebuah teorema sama artinya dengan menyatakan sebuah sasaran, yaitu sasaran untuk membuktikan teorema tersebut. Lean menyediakan taktik penulisan ulang rw untuk mengganti ruas kiri suatu identitas dengan ruas kanannya di dalam sasaran. Jika a, b, dan c adalah bilangan real, mul_assoc a b c adalah identitas a * b * c = a * (b * c), sedangkan mul_comm a b adalah identitas a * b = b * a. Lean menyediakan otomatisasi yang umumnya menghilangkan kebutuhan untuk merujuk fakta-fakta semacam ini secara eksplisit, tetapi fakta-fakta tersebut berguna sebagai ilustrasi. Dalam Lean, perkalian berasosiasi ke kiri, sehingga ruas kiri mul_assoc juga dapat ditulis sebagai (a * b) * c. Meskipun demikian, praktik yang baik adalah memperhatikan konvensi notasi Lean dan menghilangkan tanda kurung ketika Lean juga menghilangkannya.

Cobalah rw.

example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [mul_comm a b]
  rw [mul_assoc b a c]

Baris-baris import pada awal berkas contoh yang bersangkutan mengimpor teori bilangan real dari Mathlib beserta otomatisasi yang berguna. Demi keringkasan, informasi semacam ini biasanya tidak kami tampilkan di buku teks.

Silakan membuat perubahan untuk melihat apa yang terjadi. Anda dapat mengetik karakter ℝ sebagai \R atau \real di VS Code. Simbol tersebut baru muncul setelah Anda menekan spasi atau tombol tab. Jika Anda mengarahkan penunjuk ke suatu simbol ketika membaca berkas Lean, VS Code akan menunjukkan sintaks yang dapat digunakan untuk memasukkannya. Jika ingin melihat semua singkatan yang tersedia, Anda dapat menekan Ctrl-Shift-P, lalu mengetik abbreviations untuk mengakses perintah Lean 4: Show Unicode Input Abbreviations. Jika tanda garis miring terbalik sulit dijangkau pada papan ketik Anda, karakter awalan dapat diubah melalui pengaturan lean4.input.leader.

Ketika kursor berada di tengah bukti taktik, Lean melaporkan keadaan bukti saat ini di jendela Lean Infoview. Saat kursor digerakkan melewati setiap langkah bukti, Anda dapat melihat perubahan keadaannya. Keadaan bukti yang umum dalam Lean dapat tampak seperti berikut:

1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4

Baris-baris sebelum baris yang diawali ⊢ menyatakan konteks: baris-baris itu memuat objek dan asumsi yang sedang digunakan. Dalam contoh ini terdapat dua objek, x dan y, yang masing-masing merupakan bilangan asli. Terdapat pula tiga asumsi, yang diberi label h₁, h₂, dan h₃. Dalam Lean, segala sesuatu di dalam konteks diberi label berupa pengenal. Anda dapat mengetik label berindeks bawah ini sebagai h\1, h\2, dan h\3, tetapi pengenal sah apa pun dapat digunakan: Anda dapat memakai h1, h2, dan h3, atau foo, bar, dan baz. Baris terakhir menyatakan sasaran, yakni fakta yang harus dibuktikan. Kadang-kadang istilah target digunakan untuk fakta yang harus dibuktikan, sedangkan goal digunakan untuk gabungan konteks dan target. Dalam praktiknya, makna yang dimaksud biasanya jelas.

Cobalah membuktikan identitas-identitas berikut, dengan mengganti sorry pada setiap kasus dengan bukti taktik. Dengan taktik rw, Anda dapat menggunakan panah kiri (\l) untuk membalik arah suatu identitas. Sebagai contoh, rw [← mul_assoc a b c] mengganti a * (b * c) dengan a * b * c pada sasaran saat ini. Perhatikan bahwa panah kiri berarti bergerak dari kanan ke kiri dalam identitas yang diberikan oleh mul_assoc; panah itu tidak berkaitan dengan ruas kiri atau kanan sasaran.

example (a b c : ℝ) : c * b * a = b * (a * c) := by
  sorry

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry

Anda juga dapat menggunakan identitas seperti mul_assoc dan mul_comm tanpa argumen. Dalam hal ini, taktik penulisan ulang mencoba mencocokkan ruas kiri dengan suatu ekspresi dalam sasaran, dengan menggunakan pola pertama yang ditemukannya.

example (a b c : ℝ) : a * b * c = b * c * a := by
  rw [mul_assoc]
  rw [mul_comm]

Anda juga dapat memberikan informasi parsial. Sebagai contoh, mul_comm a cocok dengan pola apa pun berbentuk a * ? dan menulisnya ulang menjadi ? * a. Cobalah mengerjakan contoh pertama tanpa memberikan argumen sama sekali, dan contoh kedua hanya dengan satu argumen.

example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
  sorry

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry

Anda juga dapat menggunakan rw dengan fakta-fakta dari konteks lokal.

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h']
  rw [← mul_assoc]
  rw [h]
  rw [mul_assoc]

Cobalah soal-soal berikut; gunakan teorema sub_self untuk soal kedua:

example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by
  sorry

example (a b c d : ℝ) (hyp : c = b * a - d) (hyp' : d = a * b) : c = 0 := by
  sorry

Beberapa perintah penulisan ulang dapat dijalankan dengan satu perintah, dengan mencantumkan identitas yang relevan, dipisahkan oleh koma, di dalam tanda kurung siku.

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

Anda tetap dapat melihat perkembangan langkah demi langkah dengan menempatkan kursor setelah koma mana pun dalam daftar penulisan ulang.

Trik lainnya adalah mendeklarasikan variabel satu kali di luar contoh atau teorema. Lean kemudian menyertakannya secara otomatis.

variable (a b c d e f : ℝ)

example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

Pemeriksaan keadaan taktik pada awal bukti di atas menunjukkan bahwa Lean memang menyertakan semua variabel. Kita dapat membatasi lingkup deklarasi dengan menempatkannya dalam blok section ... end. Terakhir, ingat kembali dari bagian pendahuluan bahwa Lean menyediakan perintah untuk menentukan tipe suatu ekspresi:

section
variable (a b c : ℝ)

#check a
#check a + b
#check (a : ℝ)
#check mul_comm a b
#check (mul_comm a b : a * b = b * a)
#check mul_assoc c a b
#check mul_comm a
#check mul_comm

end

Perintah #check dapat digunakan untuk objek maupun fakta. Sebagai tanggapan terhadap perintah #check a, Lean melaporkan bahwa a bertipe ℝ. Sebagai tanggapan terhadap perintah #check mul_comm a b, Lean melaporkan bahwa mul_comm a b adalah bukti untuk fakta a * b = b * a. Perintah #check (a : ℝ) menyatakan dugaan kita bahwa tipe a adalah ℝ, dan Lean akan memunculkan galat jika ternyata bukan demikian. Keluaran dari tiga perintah #check terakhir akan dijelaskan kemudian. Sementara itu, Anda dapat memeriksanya dan bereksperimen dengan beberapa perintah #check buatan Anda sendiri.

Mari mencoba beberapa contoh lagi. Teorema two_mul a menyatakan bahwa 2 * a = a + a. Teorema add_mul dan mul_add menyatakan sifat distributif perkalian terhadap penjumlahan, sedangkan teorema add_assoc menyatakan sifat asosiatif penjumlahan. Gunakan perintah #check untuk melihat pernyataan yang tepat.

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  rw [mul_add, add_mul, add_mul]
  rw [← add_assoc, add_assoc (a * a)]
  rw [mul_comm b a, ← two_mul]

Meskipun kita dapat memahami apa yang terjadi dalam bukti ini dengan menelusurinya langkah demi langkah di editor, bukti tersebut sulit dibaca jika berdiri sendiri. Lean menyediakan cara yang lebih terstruktur untuk menulis bukti semacam ini dengan menggunakan kata kunci calc.

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      rw [mul_add, add_mul, add_mul]
    _ = a * a + (b * a + a * b) + b * b := by
      rw [← add_assoc, add_assoc (a * a)]
    _ = a * a + 2 * (a * b) + b * b := by
      rw [mul_comm b a, ← two_mul]

Perhatikan bahwa bukti tersebut tidak diawali dengan by: ekspresi yang diawali calc adalah sebuah term bukti. Ekspresi calc juga dapat digunakan di dalam bukti taktik, tetapi Lean menafsirkannya sebagai instruksi untuk menggunakan term bukti yang dihasilkan guna menyelesaikan sasaran. Sintaks calc cukup peka: garis bawah dan justifikasinya harus mengikuti format yang ditunjukkan di atas. Lean menggunakan indentasi untuk menentukan, antara lain, tempat suatu blok taktik atau blok calc dimulai dan diakhiri; cobalah mengubah indentasi pada bukti di atas untuk melihat akibatnya.

Salah satu cara menulis bukti calc adalah membuat kerangkanya terlebih dahulu dengan menggunakan taktik sorry sebagai justifikasi, memastikan bahwa Lean menerima ekspresi tersebut dengan mengabaikan justifikasi sementara itu, lalu memberikan justifikasi untuk setiap langkah menggunakan taktik.

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      sorry
    _ = a * a + (b * a + a * b) + b * b := by
      sorry
    _ = a * a + 2 * (a * b) + b * b := by
      sorry

Cobalah membuktikan identitas berikut dengan bukti rw murni dan dengan bukti calc yang lebih terstruktur:

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
  sorry

Latihan berikut sedikit lebih menantang. Anda dapat menggunakan teorema-teorema yang tercantum di bawahnya.

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  sorry

#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a

Kita juga dapat melakukan penulisan ulang pada suatu asumsi dalam konteks. Sebagai contoh, rw [mul_comm a b] at hyp mengganti a * b dengan b * a di dalam asumsi hyp.

example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp'] at hyp
  rw [mul_comm d a] at hyp
  rw [← two_mul (a * d)] at hyp
  rw [← mul_assoc 2 a d] at hyp
  exact hyp

Pada langkah terakhir, taktik exact dapat menggunakan hyp untuk menyelesaikan sasaran karena pada saat itu hyp cocok tepat dengan sasaran.

Sebagai penutup bagian ini, perhatikan bahwa Mathlib menyediakan otomatisasi yang berguna melalui taktik ring. Taktik ini dirancang untuk membuktikan identitas dalam gelanggang komutatif apa pun, selama identitas tersebut semata-mata mengikuti aksioma gelanggang tanpa menggunakan asumsi lokal.

example : c * b * a = b * (a * c) := by
  ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring

Taktik ring diimpor secara tidak langsung ketika kita mengimpor Mathlib.Data.Real.Basic. Namun, pada bagian berikutnya kita akan melihat bahwa taktik ini dapat digunakan untuk perhitungan pada struktur selain bilangan real. Taktik ini dapat diimpor secara eksplisit dengan perintah import Mathlib.Tactic. Kita juga akan melihat bahwa tersedia taktik-taktik serupa untuk jenis struktur aljabar umum lainnya.

Terdapat variasi rw bernama nth_rw yang memungkinkan Anda mengganti hanya kemunculan tertentu dari suatu ekspresi dalam sasaran. Kecocokan yang mungkin diberi nomor mulai dari 1. Jadi, dalam contoh berikut, nth_rw 2 [h] mengganti kemunculan kedua a + b dengan c.

example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
  nth_rw 2 [h]
  rw [add_mul]

2.2. Membuktikan Identitas dalam Struktur Aljabar

Secara matematis, sebuah gelanggang terdiri atas sekumpulan objek \(R\), operasi \(+\) dan \(\times\), konstanta \(0\) dan \(1\), serta operasi \(x \mapsto -x\), sedemikian sehingga:

  • \(R\) dengan \(+\) merupakan grup abelian, dengan \(0\) sebagai identitas penjumlahan dan negasi sebagai invers.

  • Perkalian bersifat asosiatif dengan identitas \(1\), dan perkalian bersifat distributif terhadap penjumlahan.

Dalam Lean, kumpulan objek tersebut direpresentasikan sebagai sebuah tipe, R. Aksioma gelanggangnya adalah sebagai berikut:

variable (R : Type*) [Ring R]

#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (neg_add_cancel : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)

Anda akan mempelajari lebih lanjut tanda kurung siku pada baris pertama nanti. Untuk saat ini, cukup diketahui bahwa deklarasi tersebut memberi kita sebuah tipe R dan struktur gelanggang pada R. Lean kemudian memungkinkan kita menggunakan notasi gelanggang umum untuk elemen-elemen R serta memanfaatkan pustaka teorema tentang gelanggang.

Nama beberapa teorema seharusnya sudah terasa akrab: teorema-teorema itu persis seperti yang digunakan untuk menghitung dengan bilangan real pada bagian sebelumnya. Lean tidak hanya berguna untuk membuktikan hal-hal tentang struktur matematika konkret seperti bilangan asli dan bilangan bulat, tetapi juga untuk membuktikan hal-hal tentang struktur abstrak yang dicirikan secara aksiomatis, seperti gelanggang. Selain itu, Lean mendukung penalaran umum tentang struktur abstrak maupun konkret dan dapat diarahkan untuk mengenali instans yang sesuai. Dengan demikian, teorema apa pun tentang gelanggang dapat diterapkan pada gelanggang konkret seperti bilangan bulat ℤ, bilangan rasional ℚ, dan bilangan kompleks ℂ. Teorema itu juga dapat diterapkan pada setiap instans struktur abstrak yang memperluas gelanggang, seperti gelanggang terurut atau medan apa pun.

Meskipun demikian, tidak semua sifat penting bilangan real berlaku dalam gelanggang sembarang. Sebagai contoh, perkalian bilangan real bersifat komutatif, tetapi sifat tersebut tidak berlaku secara umum. Jika pernah mengikuti mata kuliah aljabar linear, Anda akan mengenali bahwa, untuk setiap \(n\), matriks \(n\) kali \(n\) dengan entri bilangan real membentuk gelanggang yang perkaliannya biasanya tidak komutatif. Jika kita mendeklarasikan R sebagai gelanggang komutatif, semua teorema pada bagian sebelumnya tetap berlaku ketika ℝ diganti dengan R.

variable (R : Type*) [CommRing R]
variable (a b c d : R)

example : c * b * a = b * (a * c) := by ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring

Silakan memeriksa bahwa semua bukti lainnya tetap berlaku tanpa perubahan. Perhatikan bahwa jika sebuah bukti pendek, seperti by ring, by linarith, atau by sorry, lazim (dan diperbolehkan) untuk menempatkannya pada baris yang sama setelah by. Gaya penulisan bukti yang baik perlu menyeimbangkan keringkasan dan keterbacaan.

Tujuan bagian ini adalah memperkuat keterampilan yang dikembangkan pada bagian sebelumnya dan menerapkannya pada penalaran aksiomatis tentang gelanggang. Kita akan mulai dari aksioma-aksioma yang tercantum di atas dan menggunakannya untuk menurunkan fakta-fakta lain. Sebagian besar fakta yang kita buktikan sudah terdapat di Mathlib. Versi yang kita buktikan akan diberi nama yang sama agar Anda sekaligus mempelajari isi pustaka dan konvensi penamaannya.

Lean menyediakan mekanisme pengorganisasian yang mirip dengan mekanisme dalam bahasa pemrograman: ketika definisi atau teorema foo diperkenalkan di dalam sebuah ruang nama (namespace) bar, nama lengkapnya adalah bar.foo. Perintah open bar kemudian membuka ruang nama tersebut sehingga kita dapat menggunakan nama yang lebih pendek, foo. Untuk menghindari galat akibat benturan nama, dalam contoh berikut kita menempatkan versi teorema pustaka buatan kita di ruang nama baru bernama MyRing.

Contoh berikut menunjukkan bahwa add_zero dan add_neg_cancel tidak perlu dijadikan aksioma gelanggang karena keduanya mengikuti aksioma-aksioma lainnya.

namespace MyRing
variable {R : Type*} [Ring R]

theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]

theorem add_neg_cancel (a : R) : a + -a = 0 := by rw [add_comm, neg_add_cancel]

#check MyRing.add_zero
#check add_zero

end MyRing

Hasilnya, kita dapat membuktikan ulang suatu teorema pustaka untuk sementara, lalu kembali menggunakan versi pustakanya sesudah itu. Namun, jangan berbuat curang! Dalam latihan-latihan berikut, gunakan hanya fakta umum tentang gelanggang yang telah kita buktikan sebelumnya pada bagian ini.

(Jika memperhatikan dengan saksama, Anda mungkin menyadari bahwa kita mengganti tanda kurung biasa pada (R : Type*) dengan tanda kurung kurawal pada {R : Type*}. Ini mendeklarasikan R sebagai argumen implisit. Maknanya akan segera dijelaskan; untuk sementara, tidak perlu mengkhawatirkannya.)

Berikut sebuah teorema yang berguna:

theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by
  rw [← add_assoc, neg_add_cancel, zero_add]

Buktikan versi pasangannya:

theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
  sorry

Gunakan teorema-teorema tersebut untuk membuktikan pernyataan berikut:

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
  sorry

theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
  sorry

Dengan perencanaan yang memadai, masing-masing dapat dibuktikan dengan tiga penulisan ulang.

Sekarang kita akan menjelaskan penggunaan tanda kurung kurawal. Bayangkan suatu keadaan ketika konteks Anda memuat a, b, dan c, beserta hipotesis h : a + b = a + c, dan Anda ingin menarik kesimpulan b = c. Dalam Lean, sebuah teorema dapat diterapkan pada hipotesis dan fakta sebagaimana teorema dapat diterapkan pada objek. Karena itu, Anda mungkin mengira bahwa add_left_cancel a b c h merupakan bukti untuk fakta b = c. Namun, menuliskan a, b, dan c secara eksplisit sebenarnya mubazir, karena hipotesis h sudah memperjelas objek yang dimaksud. Dalam kasus ini, mengetik beberapa karakter tambahan tidak terlalu membebani. Namun, jika add_left_cancel hendak diterapkan pada ekspresi yang lebih rumit, penulisannya akan merepotkan. Dalam kasus semacam ini, Lean memungkinkan kita menandai argumen sebagai implisit: argumen tersebut semestinya tidak dituliskan dan akan disimpulkan melalui cara lain, misalnya dari argumen dan hipotesis sesudahnya. Tanda kurung kurawal pada {a b c : R} melakukan hal tersebut. Jadi, berdasarkan pernyataan teorema di atas, ekspresi yang benar cukup add_left_cancel h.

Sebagai ilustrasi, mari tunjukkan bahwa a * 0 = 0 mengikuti aksioma-aksioma gelanggang.

theorem mul_zero (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by
    rw [← mul_add, add_zero, add_zero]
  rw [add_left_cancel h]

Kita baru saja menggunakan trik baru! Jika menelusuri bukti tersebut langkah demi langkah, Anda dapat melihat apa yang terjadi. Taktik have memperkenalkan sasaran baru, a * 0 + a * 0 = a * 0 + 0, dengan konteks yang sama seperti sasaran asal. Indentasi pada baris berikutnya menunjukkan bahwa Lean mengharapkan sebuah blok taktik yang membuktikan sasaran baru tersebut. Dengan demikian, indentasi mendorong gaya pembuktian modular: subbukti yang menjorok ke dalam menetapkan sasaran yang diperkenalkan oleh have. Sesudah itu, kita kembali membuktikan sasaran asal, tetapi sebuah hipotesis baru h telah ditambahkan. Karena sudah dibuktikan, hipotesis itu kini bebas kita gunakan. Pada titik ini, sasaran persis merupakan hasil add_left_cancel h.

Kita juga dapat menutup bukti dengan apply add_left_cancel h atau exact add_left_cancel h. Taktik exact menerima sebuah term bukti yang sepenuhnya membuktikan sasaran saat ini tanpa membuat sasaran baru. Taktik apply merupakan variasi yang argumennya tidak harus berupa bukti lengkap. Bagian yang belum ada akan disimpulkan secara otomatis oleh Lean atau menjadi sasaran baru yang harus dibuktikan. Meskipun secara teknis exact berlebihan karena kemampuannya benar-benar lebih terbatas daripada apply, taktik tersebut membuat skrip bukti sedikit lebih jelas bagi pembaca manusia dan lebih mudah dirawat ketika pustaka berubah.

Ingat bahwa perkalian tidak diasumsikan komutatif, sehingga teorema berikut juga memerlukan usaha.

theorem zero_mul (a : R) : 0 * a = 0 := by
  sorry

Sekarang Anda semestinya juga dapat mengganti setiap sorry dalam latihan berikut dengan sebuah bukti, tetap hanya menggunakan fakta tentang gelanggang yang telah ditetapkan pada bagian ini beserta aksioma eq_symm.

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  sorry

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
  sorry

theorem neg_zero : (-0 : R) = 0 := by
  apply neg_eq_of_add_eq_zero
  rw [add_zero]

theorem neg_neg (a : R) : - -a = a := by
  sorry

Pada teorema ketiga, kita harus menggunakan anotasi (-0 : R) alih-alih 0. Tanpa menentukan R, Lean tidak mungkin menyimpulkan 0 mana yang dimaksud; secara bawaan, nilai tersebut akan ditafsirkan sebagai bilangan asli.

Dalam Lean, pengurangan pada gelanggang terbukti sama dengan penjumlahan dengan invers aditif.

example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b

Pada bilangan real, pengurangan didefinisikan dengan cara tersebut:

example (a b : ℝ) : a - b = a + -b :=
  rfl

example (a b : ℝ) : a - b = a + -b := by
  rfl

Term bukti rfl merupakan singkatan dari “refleksivitas”. Menyajikannya sebagai bukti untuk a - b = a + -b memaksa Lean membuka definisi dan mengenali bahwa kedua ruas sama. Taktik rfl melakukan hal yang sama. Ini merupakan contoh kesamaan definisional dalam logika yang mendasari Lean. Artinya, kita tidak hanya dapat menulis ulang dengan sub_eq_add_neg untuk mengganti a - b = a + -b; dalam konteks tertentu yang melibatkan bilangan real, kedua ruas persamaan tersebut juga dapat digunakan secara saling dipertukarkan. Sebagai contoh, sekarang Anda memiliki cukup informasi untuk membuktikan teorema self_sub dari bagian sebelumnya:

theorem self_sub (a : R) : a - a = 0 := by
  sorry

Tunjukkan bahwa teorema ini dapat dibuktikan menggunakan rw. Namun, jika gelanggang sembarang R diganti dengan bilangan real, Anda juga dapat membuktikannya menggunakan apply atau exact.

Lean mengetahui bahwa 1 + 1 = 2 berlaku di setiap gelanggang. Dengan sedikit usaha, fakta tersebut dapat digunakan untuk membuktikan teorema two_mul dari bagian sebelumnya:

theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
  norm_num

theorem two_mul (a : R) : 2 * a = a + a := by
  sorry

Sebagai penutup bagian ini, perhatikan bahwa beberapa fakta tentang penjumlahan dan negasi yang ditetapkan di atas tidak memerlukan seluruh kekuatan aksioma gelanggang, bahkan tidak memerlukan sifat komutatif penjumlahan. Gagasan grup yang lebih lemah dapat diaksiomatisasi sebagai berikut:

variable (A : Type*) [AddGroup A]

#check (add_assoc : ∀ a b c : A, a + b + c = a + (b + c))
#check (zero_add : ∀ a : A, 0 + a = a)
#check (neg_add_cancel : ∀ a : A, -a + a = 0)

Menurut konvensi, notasi aditif digunakan ketika operasi grup bersifat komutatif, sedangkan notasi multiplikatif digunakan jika tidak. Karena itu, Lean mendefinisikan versi multiplikatif maupun versi aditif (beserta varian abelian masing-masing, AddCommGroup dan CommGroup).

variable {G : Type*} [Group G]

#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1)

Jika merasa percaya diri, cobalah membuktikan fakta-fakta berikut tentang grup dengan hanya menggunakan aksioma-aksioma tersebut. Dalam prosesnya, Anda perlu membuktikan sejumlah lema bantu. Bukti-bukti yang telah kita kerjakan pada bagian ini memberikan beberapa petunjuk.

theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1 := by
  sorry

theorem mul_one (a : G) : a * 1 = a := by
  sorry

theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  sorry

Memanggil lema-lema tersebut secara eksplisit terasa melelahkan. Karena itu, Mathlib menyediakan taktik yang mirip dengan ring untuk mencakup sebagian besar kebutuhan: group digunakan untuk grup multiplikatif nonkomutatif, abel untuk grup aditif abelian, dan noncomm_ring untuk gelanggang nonkomutatif. Mungkin terasa ganjil bahwa struktur aljabarnya bernama Ring dan CommRing, sedangkan taktiknya bernama noncomm_ring dan ring. Hal ini sebagian disebabkan alasan historis, tetapi juga memudahkan penggunaan nama yang lebih pendek untuk taktik yang menangani gelanggang komutatif karena taktik tersebut lebih sering digunakan.

2.3. Menggunakan Teorema dan Lema

Menulis ulang sangat berguna untuk membuktikan persamaan, tetapi bagaimana dengan jenis teorema yang lain? Sebagai contoh, bagaimana kita dapat membuktikan sebuah pertidaksamaan, seperti fakta bahwa \(a + e^b \le a + e^c\) berlaku kapan pun \(b \le c\)? Kita telah melihat bahwa teorema dapat diterapkan pada argumen dan hipotesis, dan bahwa taktik apply dan exact dapat digunakan untuk menyelesaikan sasaran. Dalam bagian ini, kita akan memanfaatkan alat-alat tersebut dengan baik.

Perhatikan teorema pustaka le_refl dan le_trans:

#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)

Seperti yang dijelaskan secara lebih terperinci dalam Bab 3.1, tanda kurung implisit dalam pernyataan le_trans berasosiasi ke kanan, sehingga harus ditafsirkan sebagai a ≤ b → (b ≤ c → a ≤ c). Perancang pustaka telah menetapkan argumen a, b, dan c bagi le_trans sebagai argumen implisit, sehingga Lean tidak mengizinkan Anda memberikannya secara eksplisit (kecuali jika Anda benar-benar memaksa, seperti yang akan kita bahas nanti). Sebaliknya, Lean berharap dapat menyimpulkannya dari konteks tempat argumen itu digunakan. Sebagai contoh, ketika hipotesis h : a ≤ b dan h' : b ≤ c berada dalam konteks, semua bentuk berikut dapat digunakan:

variable (h : a ≤ b) (h' : b ≤ c)

#check (le_refl : ∀ a : Real, a ≤ a)
#check (le_refl a : a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (le_trans h : b ≤ c → a ≤ c)
#check (le_trans h h' : a ≤ c)

Taktik apply mengambil bukti dari suatu pernyataan umum atau implikasi, mencoba mencocokkan kesimpulannya dengan sasaran saat ini, dan menyisakan hipotesisnya, jika ada, sebagai sasaran baru. Jika bukti yang diberikan cocok tepat dengan sasaran (modulo kesamaan definisional), Anda dapat menggunakan taktik exact sebagai pengganti apply. Jadi, semua bentuk berikut dapat digunakan:

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans h₀
  apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
  le_trans h₀ h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

example (x : ℝ) : x ≤ x :=
  le_refl x

Dalam contoh pertama, menerapkan le_trans menghasilkan dua sasaran, dan kita menggunakan titik untuk menunjukkan tempat bukti bagi masing-masing sasaran dimulai. Titik-titik tersebut bersifat opsional, tetapi berfungsi untuk memusatkan sasaran: di dalam blok yang diawali oleh sebuah titik, hanya satu sasaran yang terlihat, dan sasaran itu harus diselesaikan sebelum akhir blok. Di sini kita mengakhiri blok pertama dengan memulai blok baru menggunakan titik lain. Kita juga dapat sekadar mengurangi indentasinya. Dalam contoh ketiga dan contoh terakhir, kita sama sekali tidak memasuki mode taktik: le_trans h₀ h₁ dan le_refl x adalah suku bukti yang kita perlukan.

Berikut beberapa teorema pustaka lainnya:

#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)

Gunakan teorema-teorema tersebut bersama apply dan exact untuk membuktikan pernyataan berikut:

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  sorry

Sebenarnya, Lean memiliki taktik yang melakukan hal semacam ini secara otomatis:

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  linarith

Taktik linarith dirancang untuk menangani aritmetika linear.

example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by
  linarith

Selain persamaan dan pertidaksamaan dalam konteks, linarith akan menggunakan pertidaksamaan tambahan yang Anda berikan sebagai argumen. Dalam contoh berikutnya, exp_le_exp.mpr h' merupakan bukti dari exp b ≤ exp c, seperti yang akan segera kita jelaskan. Perhatikan bahwa, dalam Lean, kita menulis f x untuk menyatakan penerapan fungsi f pada argumen x, persis seperti kita menulis h x untuk menyatakan hasil penerapan fakta atau teorema h pada argumen x. Tanda kurung hanya diperlukan untuk argumen majemuk, seperti dalam f (x + y). Tanpa tanda kurung, f x + y akan diuraikan sebagai (f x) + y.

example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
  linarith [exp_le_exp.mpr h']

Berikut beberapa teorema lain dalam pustaka yang dapat digunakan untuk membuktikan pertidaksamaan pada bilangan real.

#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → a ≤ b → log a ≤ log b)
#check (log_lt_log : 0 < a → a < b → log a < log b)
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_le_add_right : a ≤ b → ∀ c, c + a ≤ c + b)
#check (add_le_add_left : a ≤ b → ∀ c, a + c ≤ b + c)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d)
#check (add_lt_add_right : a < b → ∀ c, c + a < c + b)
#check (add_lt_add_left : a < b → ∀ c, a + c < b + c)
#check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
#check add_le_add_right

Beberapa teorema, yaitu exp_le_exp dan exp_lt_exp, menggunakan biimplikasi, yang menyatakan frasa "jika dan hanya jika". (Anda dapat mengetiknya di VS Code dengan \lr atau \iff). Kita akan membahas penghubung ini secara lebih terperinci dalam bab berikutnya. Teorema seperti itu dapat digunakan bersama rw untuk menulis ulang sasaran menjadi sasaran yang ekuivalen:

example (h : a ≤ b) : exp a ≤ exp b := by
  rw [exp_le_exp]
  exact h

Namun, dalam bagian ini kita akan menggunakan fakta bahwa jika h : A ↔ B merupakan suatu ekuivalensi, maka h.mp membuktikan arah maju, A → B, dan h.mpr membuktikan arah balik, B → A. Di sini, mp merupakan singkatan dari "modus ponens" dan mpr merupakan singkatan dari "modus ponens reverse" (modus ponens terbalik). Jika Anda lebih suka, Anda juga dapat menggunakan h.1 dan h.2 masing-masing sebagai pengganti h.mp dan h.mpr. Dengan demikian, bukti berikut dapat digunakan:

example (h₀ : a ≤ b) (h₁ : c < d) : a + exp c + e < b + exp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
    apply exp_lt_exp.mpr h₁
  apply le_refl

Baris pertama, apply add_lt_add_of_lt_of_le, menghasilkan dua sasaran, dan sekali lagi kita menggunakan titik untuk memisahkan bukti bagi sasaran pertama dari bukti bagi sasaran kedua.

Cobalah contoh-contoh berikut secara mandiri. Contoh di tengah menunjukkan bahwa taktik norm_num dapat digunakan untuk menyelesaikan sasaran numerik konkret.

example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry

example : (0 : ℝ) < 1 := by norm_num

example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
  have h₀ : 0 < 1 + exp a := by sorry
  apply log_le_log h₀
  sorry

Dari contoh-contoh tersebut, seharusnya jelas bahwa kemampuan untuk menemukan teorema pustaka yang Anda perlukan merupakan bagian penting dari formalisasi. Ada sejumlah strategi yang dapat Anda gunakan:

  • Anda dapat menjelajahi Mathlib dalam repositori GitHub-nya.

  • Anda dapat menggunakan dokumentasi API di laman web Mathlib.

  • Anda dapat menggunakan Loogle <https://loogle.lean-lang.org> untuk mencari definisi dan teorema Lean serta Mathlib berdasarkan pola.

  • Anda dapat mengandalkan konvensi penamaan Mathlib dan pelengkapan Ctrl-space dalam editor untuk menebak nama teorema (atau Cmd-space pada papan ketik Mac). Dalam Lean, teorema bernama A_of_B_of_C membuktikan sesuatu dalam bentuk A dari hipotesis berbentuk B dan C, dengan A, B, dan C kira-kira menggambarkan cara kita membaca sasaran tersebut dengan lantang. Jadi, teorema yang membuktikan sesuatu seperti x + y ≤ ... mungkin diawali dengan add_le. Mengetik add_le lalu menekan Ctrl-space akan menampilkan beberapa pilihan yang berguna. Perhatikan bahwa menekan Ctrl-space dua kali akan menampilkan lebih banyak informasi tentang pilihan pelengkapan yang tersedia.

  • Jika Anda mengeklik kanan nama teorema yang sudah ada di VS Code, editor akan menampilkan menu dengan opsi untuk berpindah ke berkas tempat teorema tersebut didefinisikan, dan Anda dapat menemukan teorema serupa di sekitarnya.

  • Anda dapat menggunakan taktik apply?, yang mencoba menemukan teorema yang relevan dalam pustaka.

example : 0 ≤ a ^ 2 := by
  -- apply?
  exact sq_nonneg a

Untuk mencoba apply? dalam contoh ini, hapus perintah exact dan hilangkan tanda komentar pada baris sebelumnya. Dengan menggunakan kiat-kiat ini, cobalah menemukan apa yang Anda perlukan untuk mengerjakan contoh berikutnya:

example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  sorry

Dengan menggunakan kiat yang sama, pastikan bahwa linarith sebagai pengganti apply? juga dapat menuntaskan pekerjaan tersebut.

Berikut contoh pertidaksamaan lainnya:

example : 2*a*b ≤ a^2 + b^2 := by
  have h : 0 ≤ a^2 - 2*a*b + b^2
  calc
    a^2 - 2*a*b + b^2 = (a - b)^2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg

  calc
    2*a*b = 2*a*b + 0 := by ring
    _ ≤ 2*a*b + (a^2 - 2*a*b + b^2) := add_le_add (le_refl _) h
    _ = a^2 + b^2 := by ring

Mathlib cenderung menempatkan spasi di sekitar operasi biner seperti * dan ^, tetapi dalam contoh ini, format yang lebih rapat meningkatkan keterbacaan. Ada beberapa hal yang patut diperhatikan. Pertama, ekspresi s ≥ t secara definisional ekuivalen dengan t ≤ s. Pada prinsipnya, ini berarti keduanya seharusnya dapat digunakan secara bergantian. Namun, sebagian otomatisasi Lean tidak mengenali ekuivalensi tersebut, sehingga Mathlib cenderung mengutamakan ≤ daripada ≥. Kedua, kita telah menggunakan taktik ring secara ekstensif. Taktik ini benar-benar menghemat waktu! Terakhir, perhatikan bahwa pada baris kedua dalam bukti calc yang kedua, alih-alih menulis by exact add_le_add (le_refl _) h, kita dapat langsung menulis suku bukti add_le_add (le_refl _) h.

Sebenarnya, satu-satunya bagian yang memerlukan kecerdikan dalam bukti di atas adalah menemukan hipotesis h. Setelah kita memilikinya, perhitungan kedua hanya melibatkan aritmetika linear, dan linarith dapat menanganinya:

example : 2*a*b ≤ a^2 + b^2 := by
  have h : 0 ≤ a^2 - 2*a*b + b^2
  calc
    a^2 - 2*a*b + b^2 = (a - b)^2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg
  linarith

Bagus sekali! Kami menantang Anda untuk menggunakan gagasan-gagasan ini guna membuktikan teorema berikut. Anda dapat menggunakan teorema abs_le'.mpr. Anda juga akan memerlukan taktik constructor untuk memecah sebuah konjungsi menjadi dua sasaran; lihat Bab 3.4.

example : |a*b| ≤ (a^2 + b^2)/2 := by
  sorry

#check abs_le'.mpr

Jika Anda berhasil menyelesaikannya, selamat! Anda sudah berada di jalur yang tepat untuk menjadi ahli formalisasi.

2.4. Lebih Banyak Contoh Menggunakan apply dan rw

Fungsi min pada bilangan real dicirikan secara unik oleh tiga fakta berikut:

#check (min_le_left a b : min a b ≤ a)
#check (min_le_right a b : min a b ≤ b)
#check (le_min : c ≤ a → c ≤ b → c ≤ min a b)

Dapatkah Anda menebak nama teorema-teorema yang mencirikan max dengan cara serupa?

Perhatikan bahwa kita harus menerapkan min pada sepasang argumen a dan b dengan menulis min a b, bukan min (a, b). Secara formal, min adalah fungsi bertipe ℝ → ℝ → ℝ. Ketika kita menulis tipe seperti ini dengan beberapa tanda panah, konvensinya adalah bahwa tanda kurung implisit berasosiasi ke kanan, sehingga tipe tersebut ditafsirkan sebagai ℝ → (ℝ → ℝ). Akibat akhirnya, jika a dan b bertipe ℝ, maka min a bertipe ℝ → ℝ dan min a b bertipe ℝ. Jadi, min bertindak seperti fungsi dengan dua argumen, sesuai dengan yang kita harapkan. Penanganan beberapa argumen dengan cara ini dikenal sebagai currying, mengikuti nama ahli logika Haskell Curry.

Urutan operasi dalam Lean juga mungkin memerlukan waktu untuk dibiasakan. Penerapan fungsi mengikat lebih kuat daripada operasi infiks, sehingga ekspresi min a b + c ditafsirkan sebagai (min a b) + c. Seiring waktu, konvensi-konvensi ini akan terasa alami.

Dengan menggunakan teorema le_antisymm, kita dapat menunjukkan bahwa dua bilangan real bernilai sama jika masing-masing kurang dari atau sama dengan yang lain. Dengan menggunakan teorema tersebut dan fakta-fakta di atas, kita dapat menunjukkan bahwa min bersifat komutatif:

example : min a b = min b a := by
  apply le_antisymm
  · show min a b ≤ min b a
    apply le_min
    · apply min_le_right
    apply min_le_left
  · show min b a ≤ min a b
    apply le_min
    · apply min_le_right
    apply min_le_left

Di sini kita menggunakan titik untuk memisahkan bukti bagi sasaran-sasaran yang berbeda. Penggunaan kita tidak konsisten: pada tingkat terluar, kita menggunakan titik dan indentasi untuk kedua sasaran, sedangkan dalam bukti-bukti bersarang, kita hanya menggunakan titik hingga tersisa satu sasaran. Kedua konvensi tersebut masuk akal dan berguna. Kita juga menggunakan taktik show untuk menata bukti dan menunjukkan apa yang sedang dibuktikan dalam setiap blok. Bukti tersebut tetap dapat digunakan tanpa perintah show, tetapi penggunaannya membuat bukti lebih mudah dibaca dan dipelihara.

Anda mungkin merasa terganggu karena bukti tersebut berulang-ulang. Sebagai gambaran awal tentang keterampilan yang akan Anda pelajari nanti, perhatikan bahwa salah satu cara menghindari pengulangan adalah dengan menyatakan lema lokal, lalu menggunakannya:

example : min a b = min b a := by
  have h : ∀ x y : ℝ, min x y ≤ min y x := by
    intro x y
    apply le_min
    apply min_le_right
    apply min_le_left
  apply le_antisymm
  apply h
  apply h

Kita akan membahas lebih lanjut kuantor universal dalam Bab 3.1, tetapi untuk saat ini cukup dikatakan bahwa hipotesis h menyatakan bahwa pertidaksamaan yang diinginkan berlaku untuk sembarang x dan y, dan taktik intro memperkenalkan x dan y sembarang untuk membuktikan kesimpulan tersebut. Perintah apply pertama setelah le_antisymm secara implisit menggunakan h a b, sedangkan yang kedua menggunakan h b a.

Penyelesaian lain adalah menggunakan taktik repeat, yang menerapkan suatu taktik (atau blok) sebanyak mungkin.

example : min a b = min b a := by
  apply le_antisymm
  repeat
    apply le_min
    apply min_le_right
    apply min_le_left

Kami mendorong Anda untuk membuktikan pernyataan-pernyataan berikut sebagai latihan. Anda dapat menggunakan salah satu dari dua kiat yang baru dijelaskan untuk mempersingkat bukti pertama.

example : max a b = max b a := by
  sorry
example : min (min a b) c = min a (min b c) := by
  sorry

Tentu saja, Anda juga dipersilakan membuktikan sifat asosiatif max.

Ada fakta menarik bahwa min bersifat distributif terhadap max seperti perkalian bersifat distributif terhadap penjumlahan, dan demikian pula sebaliknya. Dengan kata lain, pada bilangan real kita memiliki identitas min a (max b c) = max (min a b) (min a c) beserta versi yang bersesuaian dengan max dan min dipertukarkan. Namun, dalam bagian berikutnya kita akan melihat bahwa hal ini tidak mengikuti dari sifat transitif dan refleksif ≤ serta sifat-sifat penciri min dan max yang telah disebutkan di atas. Kita perlu menggunakan fakta bahwa ≤ pada bilangan real merupakan tatanan total, yakni memenuhi ∀ x y, x ≤ y ∨ y ≤ x. Di sini simbol disjungsi, ∨, menyatakan "atau". Dalam kasus pertama, kita memperoleh min x y = x, dan dalam kasus kedua, kita memperoleh min x y = y. Kita akan mempelajari cara bernalar berdasarkan kasus dalam Bab 3.5, tetapi untuk saat ini kita akan tetap menggunakan contoh yang tidak memerlukan pemisahan kasus.

Berikut salah satu contoh tersebut:

theorem aux : min a b + c ≤ min (a + c) (b + c) := by
  sorry
example : min a b + c = min (a + c) (b + c) := by
  sorry

Jelas bahwa aux menghasilkan salah satu dari dua pertidaksamaan yang diperlukan untuk membuktikan persamaan tersebut, tetapi menerapkannya pada nilai-nilai yang sesuai juga menghasilkan arah yang lain. Sebagai petunjuk, Anda dapat menggunakan teorema add_neg_cancel_right dan taktik linarith.

Konvensi penamaan Lean tampak jelas pada nama yang digunakan pustaka untuk pertidaksamaan segitiga:

#check (abs_add_le : ∀ a b : ℝ, |a + b| ≤ |a| + |b|)

Gunakan teorema tersebut untuk membuktikan varian berikut, dengan menggunakan pula add_sub_cancel_right:

example : |a| - |b| ≤ |a - b| :=
  sorry
end

Cobalah mengerjakannya dalam tiga baris atau kurang. Anda dapat menggunakan teorema sub_add_cancel.

Relasi penting lain yang akan kita gunakan dalam bagian-bagian berikutnya adalah relasi keterbagian pada bilangan asli, x ∣ y. Berhati-hatilah: simbol keterbagian bukanlah garis tegak biasa pada papan ketik Anda. Simbol tersebut merupakan karakter Unicode yang dapat dimasukkan dengan mengetik \| di VS Code. Menurut konvensi, Mathlib menggunakan dvd untuk merujuk padanya dalam nama teorema.

example (h₀ : x ∣ y) (h₁ : y ∣ z) : x ∣ z :=
  dvd_trans h₀ h₁

example : x ∣ y * x * z := by
  apply dvd_mul_of_dvd_left
  apply dvd_mul_left

example : x ∣ x ^ 2 := by
  apply dvd_mul_left

Dalam contoh terakhir, eksponennya adalah bilangan asli, dan menerapkan dvd_mul_left memaksa Lean mengembangkan definisi x^2 menjadi x^1 * x. Cobalah menebak nama teorema-teorema yang Anda perlukan untuk membuktikan pernyataan berikut:

example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by
  sorry
end

Dalam kaitannya dengan keterbagian, faktor persekutuan terbesar, gcd, dan kelipatan persekutuan terkecil, lcm, beranalogi dengan min dan max. Karena setiap bilangan membagi 0, 0 sebenarnya merupakan unsur terbesar dalam tatanan keterbagian:

variable (m n : ℕ)

#check (Nat.gcd_zero_right n : Nat.gcd n 0 = n)
#check (Nat.gcd_zero_left n : Nat.gcd 0 n = n)
#check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0)
#check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0)

Cobalah menebak nama teorema-teorema yang akan Anda perlukan untuk membuktikan pernyataan berikut:

example : Nat.gcd m n = Nat.gcd n m := by
  sorry

Petunjuk: Anda dapat menggunakan dvd_antisymm, tetapi jika Anda melakukannya, Lean akan mengeluh bahwa ekspresi tersebut ambigu antara teorema generik dan versi Nat.dvd_antisymm, yakni versi khusus untuk bilangan asli. Anda dapat menggunakan _root_.dvd_antisymm untuk menentukan versi generik; keduanya dapat digunakan.

2.5. Membuktikan Fakta tentang Struktur Aljabar

Dalam Bab 2.2, kita melihat bahwa banyak identitas umum yang berlaku pada bilangan real juga berlaku pada kelas struktur aljabar yang lebih umum, seperti gelanggang komutatif. Kita dapat menggunakan aksioma apa pun untuk mendeskripsikan suatu struktur aljabar, tidak hanya persamaan. Sebagai contoh, suatu tatanan parsial terdiri atas sebuah himpunan beserta relasi biner yang refleksif, transitif, dan antisimetris, seperti ≤ pada bilangan real. Lean mengenal tatanan parsial:

variable {α : Type*} [PartialOrder α]
variable (x y z : α)

#check x ≤ y
#check (le_refl x : x ≤ x)
#check (le_trans : x ≤ y → y ≤ z → x ≤ z)
#check (le_antisymm : x ≤ y → y ≤ x → x = y)

Di sini kita mengikuti konvensi Mathlib yang menggunakan huruf-huruf seperti α, β, dan γ (dimasukkan sebagai \a, \b, dan \g) untuk tipe sembarang. Pustaka ini sering menggunakan huruf seperti R dan G untuk himpunan dasar struktur aljabar seperti gelanggang dan grup, secara berurutan, tetapi secara umum huruf Yunani digunakan untuk tipe, terutama bila hanya sedikit atau bahkan tidak ada struktur yang dikaitkan dengannya.

Setiap tatanan parsial ≤ juga memiliki tatanan parsial ketat <, yang berperilaku kurang lebih seperti < pada bilangan real. Menyatakan bahwa x lebih kecil daripada y dalam tatanan ini setara dengan menyatakan bahwa unsur tersebut lebih kecil daripada atau sama dengan y dan tidak sama dengan y.

#check x < y
#check (lt_irrefl x : ¬ (x < x))
#check (lt_trans : x < y → y < z → x < z)
#check (lt_of_le_of_lt : x ≤ y → y < z → x < z)
#check (lt_of_lt_of_le : x < y → y ≤ z → x < z)

example : x < y ↔ x ≤ y ∧ x ≠ y :=
  lt_iff_le_and_ne

Dalam contoh ini, simbol ∧ menyatakan "dan", simbol ¬ menyatakan "tidak", dan x ≠ y merupakan singkatan dari ¬ (x = y). Dalam Bab 3, Anda akan mempelajari cara menggunakan penghubung-penghubung logis ini untuk membuktikan bahwa < memiliki sifat-sifat yang disebutkan.

Suatu kisi adalah struktur yang memperluas tatanan parsial dengan operasi ⊓ dan ⊔ yang serupa dengan min dan max pada bilangan real:

variable {α : Type*} [Lattice α]
variable (x y z : α)

#check x ⊓ y
#check (inf_le_left : x ⊓ y ≤ x)
#check (inf_le_right : x ⊓ y ≤ y)
#check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)
#check x ⊔ y
#check (le_sup_left : x ≤ x ⊔ y)
#check (le_sup_right : y ≤ x ⊔ y)
#check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z)

Sifat-sifat yang mencirikan ⊓ dan ⊔ membenarkan penyebutan keduanya sebagai batas bawah terbesar dan batas atas terkecil, secara berurutan. Anda dapat memasukkannya di VS Code dengan \glb dan \lub. Simbol-simbol tersebut juga sering disebut infimum dan supremum, dan Mathlib menyebutnya inf dan sup dalam nama teorema. Untuk makin merumitkan istilah, keduanya juga sering disebut meet dan join. Karena itu, jika Anda bekerja dengan kisi, Anda perlu mengingat kamus berikut:

  • ⊓ adalah batas bawah terbesar, infimum, atau meet.

  • ⊔ adalah batas atas terkecil, supremum, atau join.

Beberapa contoh kisi meliputi:

  • min dan max pada sembarang tatanan total, seperti bilangan bulat atau bilangan real dengan ≤

  • ∩ dan ∪ pada koleksi himpunan bagian dari suatu semesta, dengan tatanan ⊆

  • ∧ dan ∨ pada nilai kebenaran Boolean, dengan tatanan x ≤ y jika x bernilai salah atau y bernilai benar

  • gcd dan lcm pada bilangan asli (atau bilangan asli positif), dengan tatanan keterbagian ∣

  • koleksi subruang linear dari suatu ruang vektor, dengan batas bawah terbesar berupa irisan, batas atas terkecil berupa jumlah kedua ruang, dan tatanannya berupa inklusi

  • koleksi topologi pada suatu himpunan (atau, dalam Lean, suatu tipe), dengan batas bawah terbesar dari dua topologi berupa topologi yang dibangkitkan oleh gabungan keduanya, batas atas terkecil berupa irisan keduanya, dan tatanannya berupa inklusi terbalik

Anda dapat memeriksa bahwa, sebagaimana pada min / max dan gcd / lcm, komutativitas dan asosiativitas infimum dan supremum dapat dibuktikan hanya dengan menggunakan aksioma-aksioma pencirinya, bersama le_refl dan le_trans.

Menggunakan apply le_trans ketika menghadapi sasaran x ≤ z bukanlah pilihan yang baik. Lean memang tidak memiliki cara untuk menebak unsur perantara y mana yang ingin kita gunakan. Karena itu, apply le_trans menghasilkan tiga sasaran yang tampak seperti x ≤ ?a, ?a ≤ z, dan α, dengan ?a (kemungkinan bernama lebih rumit karena dibuat secara otomatis) mewakili y yang belum diketahui. Sasaran terakhir, yang bertipe α, meminta nilai y. Sasaran itu muncul terakhir karena Lean berharap dapat menyimpulkannya secara otomatis dari bukti sasaran pertama, x ≤ ?a. Untuk menghindari keadaan yang kurang nyaman ini, Anda dapat menggunakan taktik calc untuk memberikan y secara eksplisit. Sebagai alternatif, Anda dapat menggunakan taktik trans, yang menerima y sebagai argumen dan menghasilkan sasaran yang diharapkan, yaitu x ≤ y dan y ≤ z. Tentu saja Anda juga dapat menghindari persoalan ini dengan langsung memberikan bukti lengkap seperti exact le_trans inf_le_left inf_le_right, tetapi cara ini memerlukan jauh lebih banyak perencanaan.

example : x ⊓ y = y ⊓ x := by
  sorry

example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := by
  sorry

example : x ⊔ y = y ⊔ x := by
  sorry

example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := by
  sorry

Teorema-teorema ini tersedia di Mathlib dengan nama inf_comm, inf_assoc, sup_comm, dan sup_assoc, secara berurutan.

Latihan lain yang baik adalah membuktikan hukum absorpsi hanya dengan menggunakan aksioma-aksioma tersebut:

theorem absorb1 : x ⊓ (x ⊔ y) = x := by
  sorry

theorem absorb2 : x ⊔ x ⊓ y = x := by
  sorry

Kedua teorema ini tersedia di Mathlib dengan nama inf_sup_self dan sup_inf_self.

Kisi yang memenuhi identitas tambahan x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z) dan x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) disebut kisi distributif. Lean juga mengenal struktur ini:

variable {α : Type*} [DistribLattice α]
variable (x y z : α)

#check (inf_sup_left x y z : x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z)
#check (inf_sup_right x y z : (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z)
#check (sup_inf_left x y z : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z))
#check (sup_inf_right x y z : x ⊓ y ⊔ z = (x ⊔ z) ⊓ (y ⊔ z))

Versi kiri dan kanan mudah ditunjukkan ekuivalen dengan menggunakan komutativitas ⊓ dan ⊔. Latihan yang baik adalah menunjukkan bahwa tidak setiap kisi bersifat distributif dengan memberikan deskripsi eksplisit suatu kisi nondistributif dengan berhingga banyak unsur. Latihan baik lainnya adalah menunjukkan bahwa pada sembarang kisi, masing-masing hukum distributivitas mengimplikasikan hukum yang lain:

variable {α : Type*} [Lattice α]
variable (a b c : α)

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) := by
  sorry

example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
  sorry

Struktur-struktur aksiomatik dapat digabungkan menjadi struktur yang lebih besar. Sebagai contoh, gelanggang terurut ketat terdiri atas sebuah gelanggang beserta tatanan parsial pada himpunan dasarnya yang memenuhi aksioma tambahan yang menyatakan bahwa operasi gelanggang kompatibel dengan tatanan tersebut:

variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
variable (a b c : R)

#check (add_le_add_right : a ≤ b → ∀ c, c + a ≤ c + b)
#check (mul_pos : 0 < a → 0 < b → 0 < a * b)

Bab 3 akan memberikan sarana untuk menurunkan fakta berikut dari mul_pos dan definisi <:

#check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b)

Selanjutnya, sebagai latihan yang lebih panjang, tunjukkan bahwa banyak fakta umum yang digunakan untuk menalar aritmetika dan tatanan pada bilangan real berlaku secara umum pada sembarang gelanggang terurut. Berikut beberapa contoh yang dapat Anda coba, dengan hanya menggunakan sifat gelanggang, tatanan parsial, dan fakta-fakta yang disebutkan dalam dua contoh terakhir (ingat bahwa gelanggang tersebut tidak diasumsikan komutatif, sehingga taktik ring tidak tersedia):

example (h : a ≤ b) : 0 ≤ b - a := by
  sorry

example (h: 0 ≤ b - a) : a ≤ b := by
  sorry

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := by
  sorry

Sebagai penutup, berikut satu contoh terakhir. Suatu ruang metrik terdiri atas sebuah himpunan yang dilengkapi konsep jarak, dist x y, yang memetakan setiap pasangan unsur ke suatu bilangan real. Fungsi jarak diasumsikan memenuhi aksioma-aksioma berikut:

variable {X : Type*} [MetricSpace X]
variable (x y z : X)

#check (dist_self x : dist x x = 0)
#check (dist_comm x y : dist x y = dist y x)
#check (dist_triangle x y z : dist x z ≤ dist x y + dist y z)

Setelah menguasai bagian ini, Anda dapat menunjukkan bahwa aksioma-aksioma tersebut mengakibatkan jarak selalu tak negatif:

example (x y : X) : 0 ≤ dist x y := by
  sorry

Seperti yang mungkin telah Anda duga, teorema ini bernama dist_nonneg di Mathlib.