7. Struktur

Matematika modern menggunakan struktur aljabar secara mendasar. Struktur-struktur ini merangkum pola yang dapat diwujudkan dalam berbagai latar. Teori struktur aljabar menyediakan berbagai cara untuk mendefinisikan struktur semacam itu dan membangun instans tertentu.

Karena itu, Lean menyediakan cara-cara yang bersesuaian untuk mendefinisikan struktur secara formal dan bekerja dengannya. Anda telah melihat contoh struktur aljabar dalam Lean, seperti gelanggang dan kisi, yang dibahas dalam Bab 2. Bab ini akan menjelaskan anotasi kurung siku yang tampak misterius dan telah Anda jumpai di sana, yaitu [Ring α] dan [Lattice α]. Bab ini juga akan menunjukkan cara mendefinisikan dan menggunakan struktur aljabar sendiri.

Untuk uraian yang lebih teknis, Anda dapat membaca Theorem Proving in Lean dan makalah Anne Baanen, Use and abuse of instance parameters in the Lean mathematical library.

7.1. Mendefinisikan Struktur

Dalam arti yang paling luas, struktur adalah spesifikasi sekumpulan data, mungkin beserta syarat-syarat yang harus dipenuhi data tersebut. Sebuah instans struktur adalah bundel data tertentu yang memenuhi syarat-syarat itu. Sebagai contoh, kita dapat menetapkan bahwa sebuah titik merupakan tupel tiga bilangan real:

@[ext]
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ

Anotasi @[ext] memberi tahu Lean agar secara otomatis menghasilkan teorema yang dapat digunakan untuk membuktikan bahwa dua instans struktur sama ketika komponen-komponennya sama. Sifat ini dikenal sebagai ekstensionalitas.

#check Point.ext

example (a b : Point) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) : a = b := by
  ext
  repeat' assumption

Selanjutnya kita dapat mendefinisikan instans tertentu dari struktur Point. Lean menyediakan beberapa cara untuk melakukannya.

def myPoint1 : Point where
  x := 2
  y := -1
  z := 4

def myPoint2 : Point :=
  { x := 2, y := -1, z := 4 }

def myPoint3 : Point :=
  ⟨2, -1, 4⟩

def myPoint4 :=
  Point.mk 2 (-1) 4

Dalam contoh pertama, field struktur diberi nama secara eksplisit. Fungsi Point.mk yang digunakan dalam definisi myPoint4 dikenal sebagai konstruktor struktur Point karena berfungsi membangun elemen-elemennya. Jika diinginkan, Anda dapat menentukan nama lain, misalnya build.

structure Point' where build ::
  x : ℝ
  y : ℝ
  z : ℝ

#check Point'.build 2 (-1) 4

Dua contoh berikut menunjukkan cara mendefinisikan fungsi pada struktur. Contoh kedua menuliskan konstruktor Point.mk secara eksplisit, sedangkan contoh pertama menggunakan konstruktor anonim agar lebih ringkas. Lean dapat menyimpulkan konstruktor yang sesuai dari tipe add yang dinyatakan. Definisi dan teorema yang berkaitan dengan struktur seperti Point lazim ditempatkan dalam namespace dengan nama yang sama. Dalam contoh di bawah, karena namespace Point telah kita buka, nama lengkap add adalah Point.add. Ketika namespace tersebut tidak terbuka, kita harus menggunakan nama lengkapnya. Namun, ingat bahwa notasi proyeksi anonim sering kali lebih praktis. Notasi ini memungkinkan kita menulis a.add b sebagai pengganti Point.add a b. Lean menafsirkan bentuk pertama sebagai bentuk kedua karena a bertipe Point.

namespace Point

def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def add' (a b : Point) : Point where
  x := a.x + b.x
  y := a.y + b.y
  z := a.z + b.z

#check add myPoint1 myPoint2
#check myPoint1.add myPoint2

end Point

#check Point.add myPoint1 myPoint2
#check myPoint1.add myPoint2

Di bawah ini kita akan tetap menempatkan definisi dalam namespace yang sesuai, tetapi perintah namespace tidak akan ditampilkan dalam cuplikan yang dikutip. Untuk membuktikan sifat fungsi penjumlahan, kita dapat menggunakan rw untuk mengembangkan definisi dan ext untuk mereduksi persamaan antara dua elemen struktur menjadi persamaan antara komponen-komponennya. Di bawah ini kita menggunakan kata kunci protected agar nama teoremanya tetap Point.add_comm sekalipun namespace sedang terbuka. Cara ini berguna untuk menghindari ambiguitas dengan teorema generik seperti add_comm.

protected theorem add_comm (a b : Point) : add a b = add b a := by
  rw [add, add]
  ext <;> dsimp
  repeat' apply add_comm

example (a b : Point) : add a b = add b a := by simp [add, add_comm]

Karena Lean dapat membuka definisi dan menyederhanakan proyeksi secara internal, persamaan yang kita inginkan terkadang berlaku secara definisional.

theorem add_x (a b : Point) : (a.add b).x = a.x + b.x :=
  rfl

Fungsi pada struktur juga dapat didefinisikan menggunakan pencocokan pola, dengan cara yang serupa dengan pendefinisian fungsi rekursif dalam Bab 5.2. Definisi addAlt dan addAlt' di bawah pada dasarnya sama; satu-satunya perbedaan adalah penggunaan notasi konstruktor anonim pada definisi kedua. Mendefinisikan fungsi dengan cara ini terkadang praktis, dan reduksi eta struktural membuat definisi alternatif tersebut ekuivalen secara definisional. Namun, cara itu dapat menyulitkan pembuktian selanjutnya. Secara khusus, rw [addAlt] menyisakan tampilan sasaran yang lebih rumit dan memuat pernyataan match.

def addAlt : Point → Point → Point
  | Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

def addAlt' : Point → Point → Point
  | ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

theorem addAlt_x (a b : Point) : (a.addAlt b).x = a.x + b.x := by
  rfl

theorem addAlt_comm (a b : Point) : addAlt a b = addAlt b a := by
  rw [addAlt, addAlt]
  -- pembuktian yang sama tetap berlaku, tetapi tampilan sasaran di sini lebih sulit dibaca
  ext <;> dsimp
  repeat' apply add_comm

Konstruksi matematika sering melibatkan penguraian informasi yang terbundel, lalu penyusunannya kembali dengan cara berbeda. Karena itu, wajar jika Lean dan Mathlib menyediakan banyak cara untuk melakukannya secara efisien. Sebagai latihan, cobalah membuktikan bahwa Point.add bersifat asosiatif. Kemudian definisikan perkalian skalar pada titik dan tunjukkan bahwa operasi tersebut distributif terhadap penjumlahan.

protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by
  sorry

def smul (r : ℝ) (a : Point) : Point :=
  sorry

theorem smul_distrib (r : ℝ) (a b : Point) :
    (smul r a).add (smul r b) = smul r (a.add b) := by
  sorry

Menggunakan struktur hanyalah langkah pertama menuju abstraksi aljabar. Kita belum memiliki cara untuk menghubungkan Point.add dengan simbol generik +, atau menghubungkan Point.add_comm dan Point.add_assoc dengan teorema generik add_comm dan add_assoc. Tugas-tugas ini termasuk aspek aljabar dalam penggunaan struktur, dan bagian berikutnya akan menjelaskan cara melakukannya. Untuk saat ini, pandanglah struktur sebagai cara untuk membundel objek dan informasi.

Sangat berguna bahwa struktur dapat menentukan bukan hanya tipe data, tetapi juga syarat-syarat yang harus dipenuhi data tersebut. Dalam Lean, syarat-syarat itu direpresentasikan sebagai field bertipe Prop. Sebagai contoh, 2-simpleks standar didefinisikan sebagai himpunan titik \((x, y, z)\) yang memenuhi \(x ≥ 0\), \(y ≥ 0\), \(z ≥ 0\), dan \(x + y + z = 1\). Jika gagasan ini belum Anda kenal, gambarlah bentuknya dan yakinkan diri bahwa himpunan tersebut adalah segitiga sama sisi di ruang tiga dimensi dengan titik sudut \((1, 0, 0)\), \((0, 1, 0)\), dan \((0, 0, 1)\), beserta daerah dalamnya. Kita dapat merepresentasikannya dalam Lean sebagai berikut:

structure StandardTwoSimplex where
  x : ℝ
  y : ℝ
  z : ℝ
  x_nonneg : 0 ≤ x
  y_nonneg : 0 ≤ y
  z_nonneg : 0 ≤ z
  sum_eq : x + y + z = 1

Perhatikan bahwa empat field terakhir mengacu pada x, y, dan z, yaitu tiga field pertama. Kita dapat mendefinisikan pemetaan dari 2-simpleks ke dirinya sendiri yang menukar x dan y:

def swapXy (a : StandardTwoSimplex) : StandardTwoSimplex
    where
  x := a.y
  y := a.x
  z := a.z
  x_nonneg := a.y_nonneg
  y_nonneg := a.x_nonneg
  z_nonneg := a.z_nonneg
  sum_eq := by rw [add_comm a.y a.x, a.sum_eq]

Yang lebih menarik, kita dapat menghitung titik tengah dua titik pada simpleks. Kita menambahkan frasa noncomputable section di awal berkas ini agar dapat menggunakan pembagian pada bilangan real.

noncomputable section

def midpoint (a b : StandardTwoSimplex) : StandardTwoSimplex
    where
  x := (a.x + b.x) / 2
  y := (a.y + b.y) / 2
  z := (a.z + b.z) / 2
  x_nonneg := div_nonneg (add_nonneg a.x_nonneg b.x_nonneg) (by norm_num)
  y_nonneg := div_nonneg (add_nonneg a.y_nonneg b.y_nonneg) (by norm_num)
  z_nonneg := div_nonneg (add_nonneg a.z_nonneg b.z_nonneg) (by norm_num)
  sum_eq := by field_simp; linarith [a.sum_eq, b.sum_eq]

Di sini kita membuktikan x_nonneg, y_nonneg, dan z_nonneg dengan term bukti yang ringkas, sedangkan sum_eq dibuktikan dalam mode taktik menggunakan by.

Dengan parameter \(\lambda\) yang memenuhi \(0 \le \lambda \le 1\), kita dapat mengambil rata-rata berbobot \(\lambda a + (1 - \lambda) b\) dari dua titik \(a\) dan \(b\) dalam 2-simpleks standar. Sebagai tantangan, definisikan fungsi tersebut dengan mencontoh fungsi midpoint di atas.

def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardTwoSimplex) : StandardTwoSimplex :=
  sorry

Struktur dapat bergantung pada parameter. Sebagai contoh, kita dapat menggeneralisasi 2-simpleks standar menjadi \(n\)-simpleks standar untuk sembarang \(n\). Pada tahap ini, Anda tidak perlu mengetahui hal lain tentang tipe Fin n selain bahwa tipe tersebut memiliki \(n\) elemen dan Lean mengetahui cara menjumlahkan seluruh elemennya.

open BigOperators

structure StandardSimplex (n : ℕ) where
  V : Fin n → ℝ
  NonNeg : ∀ i : Fin n, 0 ≤ V i
  sum_eq_one : (∑ i, V i) = 1

namespace StandardSimplex

def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
    where
  V i := (a.V i + b.V i) / 2
  NonNeg := by
    intro i
    apply div_nonneg
    · linarith [a.NonNeg i, b.NonNeg i]
    norm_num
  sum_eq_one := by
    simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib,
      a.sum_eq_one, b.sum_eq_one]
    norm_num

end StandardSimplex

Sebagai latihan, cobalah mendefinisikan rata-rata berbobot dari dua titik dalam \(n\)-simpleks standar. Anda dapat menggunakan Finset.sum_add_distrib dan Finset.mul_sum untuk memanipulasi jumlah-jumlah yang bersangkutan.

Kita telah melihat bahwa struktur dapat digunakan untuk membundel data beserta sifat-sifatnya. Menariknya, struktur juga dapat digunakan untuk membundel sifat tanpa data. Sebagai contoh, struktur berikut, IsLinear, membundel dua komponen linearitas.

structure IsLinear (f : ℝ → ℝ) where
  is_additive : ∀ x y, f (x + y) = f x + f y
  preserves_mul : ∀ x c, f (c * x) = c * f x

section
variable (f : ℝ → ℝ) (linf : IsLinear f)

#check linf.is_additive
#check linf.preserves_mul

end

Perlu ditekankan bahwa struktur bukanlah satu-satunya cara untuk membundel data. Struktur data Point dapat didefinisikan menggunakan tipe hasil kali generik, dan IsLinear dapat didefinisikan dengan sebuah and sederhana.

def Point'' :=
  ℝ × ℝ × ℝ

def IsLinear' (f : ℝ → ℝ) :=
  (∀ x y, f (x + y) = f x + f y) ∧ ∀ x c, f (c * x) = c * f x

Konstruksi tipe generik bahkan dapat menggantikan struktur yang memiliki ketergantungan antarkomponen. Sebagai contoh, konstruksi subtipe menggabungkan sepotong data dengan suatu sifat. Tipe PReal dalam contoh berikut dapat dipandang sebagai tipe bilangan real positif. Setiap x : PReal memiliki dua komponen: nilainya dan sifat bahwa nilai tersebut positif. Komponen-komponen ini dapat diakses sebagai x.val, yang bertipe ℝ, dan x.property, yang merepresentasikan fakta 0 < x.val.

def PReal :=
  { y : ℝ // 0 < y }

section
variable (x : PReal)

#check x.val
#check x.property
#check x.1
#check x.2

end

Kita juga dapat menggunakan subtipe untuk mendefinisikan 2-simpleks standar dan \(n\)-simpleks standar untuk sembarang \(n\).

def StandardTwoSimplex' :=
  { p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 }

def StandardSimplex' (n : ℕ) :=
  { v : Fin n → ℝ // (∀ i : Fin n, 0 ≤ v i) ∧ (∑ i, v i) = 1 }

Demikian pula, tipe Sigma merupakan generalisasi pasangan terurut, di mana tipe komponen kedua bergantung pada nilai komponen pertama.

def StdSimplex := Σ n : ℕ, StandardSimplex n

section
variable (s : StdSimplex)

#check s.fst
#check s.snd

#check s.1
#check s.2

end

Diberikan s : StdSimplex, komponen pertama s.fst adalah bilangan asli, sedangkan komponen kedua merupakan elemen simpleks yang bersesuaian, StandardSimplex s.fst. Perbedaan antara tipe Sigma dan subtipe adalah bahwa komponen kedua tipe Sigma berupa data, bukan proposisi.

Meskipun hasil kali, subtipe, dan tipe Sigma dapat digunakan sebagai pengganti struktur, penggunaan struktur menawarkan sejumlah keuntungan. Mendefinisikan struktur menyembunyikan representasi dasarnya dan menyediakan nama khusus bagi fungsi-fungsi pengakses komponen. Hal ini membuat pembuktian lebih tangguh: pembuktian yang hanya bergantung pada antarmuka struktur umumnya akan tetap berlaku ketika definisinya diubah, selama pengakses lama didefinisikan ulang menggunakan definisi baru. Selain itu, sebagaimana akan segera kita lihat, Lean mendukung perangkaian struktur menjadi hierarki yang kaya dan saling terhubung, beserta pengelolaan interaksi antarstruktur tersebut.

7.2. Struktur Aljabar

Untuk memperjelas apa yang dimaksud dengan struktur aljabar, marilah kita mempertimbangkan beberapa contoh.

1. Sebuah himpunan terurut parsial terdiri atas himpunan \(P\) dan relasi biner \(\le\) pada \(P\) yang transitif, refleksif, dan antisimetris.

2. Sebuah grup terdiri atas himpunan \(G\) dengan operasi biner asosiatif, elemen identitas \(1\), serta fungsi \(g \mapsto g^{-1}\) yang menghasilkan invers bagi setiap \(g\) dalam \(G\). Grup disebut abelian atau komutatif jika operasinya komutatif.

3. Sebuah kisi adalah himpunan terurut parsial yang memiliki infimum dan supremum untuk setiap pasangan elemennya.

4. Sebuah gelanggang terdiri atas grup Abelian (yang ditulis secara aditif) \((R, +, 0, x \mapsto -x)\), beserta operasi perkalian asosiatif \(\cdot\) dan identitas \(1\), sedemikian sehingga perkalian distributif terhadap penjumlahan. Gelanggang disebut komutatif jika perkaliannya komutatif.

5. Sebuah gelanggang terurut \((R, +, 0, -, \cdot, 1, \le)\) terdiri atas gelanggang beserta tatanan parsial pada elemen-elemennya, sedemikian sehingga \(a \le b\) mengakibatkan \(a + c \le b + c\) untuk setiap \(a\), \(b\), dan \(c\) dalam \(R\), sedangkan \(0 \le a\) dan \(0 \le b\) mengakibatkan \(0 \le a b\) untuk setiap \(a\) dan \(b\) dalam \(R\).

6. Sebuah ruang metrik terdiri atas himpunan \(X\) dan fungsi \(d : X \times X \to \mathbb{R}\) yang memenuhi:

   • \(d(x, y) \ge 0\) untuk setiap \(x\) dan \(y\) dalam \(X\).

   • \(d(x, y) = 0\) jika dan hanya jika \(x = y\).

   • \(d(x, y) = d(y, x)\) untuk setiap \(x\) dan \(y\) dalam \(X\).

   • \(d(x, z) \le d(x, y) + d(y, z)\) untuk setiap \(x\), \(y\), dan \(z\) dalam \(X\).

7. Sebuah ruang topologi terdiri atas himpunan \(X\) dan koleksi \(\mathcal T\) yang beranggotakan subhimpunan-subhimpunan \(X\), yang disebut subhimpunan terbuka dari \(X\), serta memenuhi:

   • Himpunan kosong dan \(X\) bersifat terbuka.

   • Irisan dua himpunan terbuka bersifat terbuka.

   • Gabungan sembarang keluarga himpunan terbuka bersifat terbuka.

Dalam setiap contoh tersebut, elemen-elemen struktur termasuk dalam suatu himpunan yang disebut himpunan dasar dan kadang mewakili keseluruhan struktur. Sebagai contoh, ketika kita berkata "misalkan \(G\) sebuah grup", lalu "misalkan \(g \in G\)", kita menggunakan \(G\) untuk mewakili sekaligus struktur dan himpunan dasarnya. Tidak setiap struktur aljabar terkait dengan satu himpunan dasar dengan cara ini. Sebagai contoh, graf bipartit melibatkan relasi antara dua himpunan, demikian pula koneksi Galois. Sebuah kategori juga melibatkan dua kumpulan penting, yang lazim disebut objek dan morfisme.

Contoh-contoh tersebut menunjukkan beberapa hal yang harus dilakukan asisten pembuktian untuk mendukung penalaran aljabar. Pertama, asisten tersebut harus mengenali instans konkret suatu struktur. Sistem bilangan \(\mathbb{Z}\), \(\mathbb{Q}\), dan \(\mathbb{R}\) semuanya merupakan gelanggang terurut, dan kita semestinya dapat menerapkan teorema generik tentang gelanggang terurut pada setiap instans itu. Terkadang sebuah himpunan konkret dapat menjadi instans suatu struktur melalui lebih dari satu cara. Sebagai contoh, selain topologi biasa pada \(\mathbb{R}\) yang menjadi landasan analisis real, kita juga dapat mempertimbangkan topologi diskret pada \(\mathbb{R}\), tempat setiap himpunan bersifat terbuka.

Kedua, asisten pembuktian harus mendukung notasi generik pada struktur. Dalam Lean, notasi * digunakan untuk perkalian pada semua sistem bilangan yang lazim, sekaligus untuk perkalian pada grup dan gelanggang generik. Ketika kita menggunakan ekspresi seperti f x * y, Lean harus menggunakan informasi tentang tipe f, x, dan y untuk menentukan perkalian mana yang dimaksud.

Ketiga, asisten tersebut harus menangani kenyataan bahwa struktur dapat mewarisi definisi, teorema, dan notasi dari struktur lain melalui berbagai cara. Sebagian struktur memperluas struktur lain dengan menambahkan aksioma. Gelanggang komutatif tetaplah sebuah gelanggang. Karena itu, setiap definisi yang bermakna dalam gelanggang juga bermakna dalam gelanggang komutatif, dan setiap teorema yang berlaku dalam gelanggang juga berlaku dalam gelanggang komutatif. Sebagian struktur memperluas struktur lain dengan menambahkan data. Sebagai contoh, bagian aditif setiap gelanggang merupakan grup aditif. Struktur gelanggang menambahkan perkalian dan identitas, beserta aksioma yang mengaturnya dan menghubungkannya dengan bagian aditif. Terkadang kita dapat mendefinisikan satu struktur menggunakan struktur lain. Setiap ruang metrik memiliki topologi kanonis yang terkait dengannya, yaitu topologi ruang metrik, dan berbagai topologi dapat dikaitkan dengan sembarang tatanan linear.

Terakhir, penting untuk diingat bahwa matematika memungkinkan kita menggunakan fungsi dan operasi untuk mendefinisikan struktur, sebagaimana kita menggunakannya untuk mendefinisikan bilangan. Hasil kali dan pangkat grup kembali merupakan grup. Untuk setiap \(n\), bilangan bulat modulo \(n\) membentuk gelanggang, dan untuk setiap \(k > 0\), matriks polinomial berukuran \(k \times k\) dengan koefisien dalam gelanggang tersebut kembali membentuk gelanggang. Jadi, kita dapat menghitung dengan struktur semudah menghitung dengan elemennya. Artinya, struktur aljabar menjalani dua peran dalam matematika: sebagai wadah kumpulan objek dan sebagai objek tersendiri. Asisten pembuktian harus dapat mengakomodasi kedua peran ini.

Ketika menangani elemen suatu tipe yang terkait dengan struktur aljabar, asisten pembuktian harus mengenali struktur tersebut dan menemukan definisi, teorema, serta notasi yang sesuai. Semua ini terdengar seperti pekerjaan yang sangat banyak, dan memang demikian. Namun, Lean menggunakan sekumpulan kecil mekanisme mendasar untuk melaksanakan tugas-tugas tersebut. Tujuan bagian ini adalah menjelaskan mekanisme itu dan menunjukkan cara menggunakannya.

Unsur pertama nyaris terlalu jelas untuk disebutkan: secara formal, struktur aljabar merupakan struktur dalam pengertian Bab 7.1. Struktur aljabar adalah spesifikasi bundel data yang memenuhi sejumlah hipotesis aksiomatik, dan dalam Bab 7.1 kita telah melihat bahwa perintah structure memang dirancang tepat untuk keperluan ini. Keduanya benar-benar berjodoh!

Diberikan tipe data α, kita dapat mendefinisikan struktur grup pada α sebagai berikut.

structure Group₁ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  inv_mul_cancel : ∀ x : α, mul (inv x) x = one

Perhatikan bahwa tipe α merupakan parameter dalam definisi Group₁. Jadi, objek struc : Group₁ α sebaiknya dipandang sebagai struktur grup pada α. Dalam Bab 2.2 kita telah melihat bahwa pasangan mul_inv_cancel bagi inv_mul_cancel mengikuti aksioma grup lainnya, sehingga tidak perlu ditambahkan ke definisi.

Definisi grup ini serupa dengan definisi Group dalam Mathlib, dan kita memilih nama Group₁ untuk membedakan versi kita. Jika Anda menulis #check Group lalu melakukan Ctrl-klik pada definisinya, Anda akan melihat bahwa versi Group dalam Mathlib didefinisikan dengan memperluas struktur lain; cara melakukannya akan dijelaskan nanti. Jika Anda mengetik #print Group, Anda juga akan melihat bahwa versi Group dalam Mathlib memiliki sejumlah field tambahan. Karena alasan yang akan dijelaskan nanti, terkadang berguna untuk menambahkan informasi redundan pada struktur, sehingga tersedia field tambahan untuk objek dan fungsi yang sebenarnya dapat didefinisikan dari data inti. Hal itu belum perlu dikhawatirkan sekarang. Pada hakikatnya, versi sederhana Group₁ kita sama dengan definisi grup yang digunakan Mathlib.

Terkadang berguna untuk membundel tipe bersama strukturnya. Mathlib juga memuat definisi struktur Grp yang ekuivalen dengan berikut ini:

structure Grp₁ where
  α : Type*
  str : Group₁ α

Versi Mathlib berada dalam Mathlib.Algebra.Category.Grp.Basic. Anda dapat memeriksanya dengan #check jika modul tersebut ditambahkan ke impor di awal berkas contoh.

Karena alasan yang akan semakin jelas di bawah, biasanya lebih berguna memisahkan tipe α dari struktur Group α. Kedua objek itu secara bersama-sama disebut struktur terbundel sebagian karena representasinya menggabungkan sebagian besar, tetapi tidak semua, komponen ke dalam satu struktur. Dalam Mathlib, huruf Latin kapital seperti G lazim digunakan untuk tipe yang menjadi tipe dasar sebuah grup.

Mari membangun grup dengan mendefinisikan elemen dari tipe Group₁. Untuk setiap pasangan tipe α dan β, Mathlib mendefinisikan tipe Equiv α β yang berisi ekuivalensi antara α dan β. Mathlib juga mendefinisikan notasi sugestif α ≃ β untuk tipe ini. Sebuah elemen f : α ≃ β adalah bijeksi antara α dan β yang direpresentasikan oleh empat komponen: fungsi f.toFun dari α ke β, fungsi invers f.invFun dari β ke α, serta dua sifat yang menyatakan bahwa kedua fungsi tersebut memang saling invers.

variable (α β γ : Type*)
variable (f : α ≃ β) (g : β ≃ γ)

#check Equiv α β
#check (f.toFun : α → β)
#check (f.invFun : β → α)
#check (f.right_inv : ∀ x : β, f (f.invFun x) = x)
#check (f.left_inv : ∀ x : α, f.invFun (f x) = x)
#check (Equiv.refl α : α ≃ α)
#check (f.symm : β ≃ α)
#check (f.trans g : α ≃ γ)

Perhatikan penamaan kreatif bagi tiga konstruksi terakhir. Kita memandang fungsi identitas Equiv.refl, operasi invers Equiv.symm, dan operasi komposisi Equiv.trans sebagai bukti eksplisit bahwa hubungan melalui korespondensi bijektif merupakan relasi ekuivalensi.

Perhatikan pula bahwa f.trans g mengharuskan fungsi maju dikomposisikan dalam urutan terbalik. Mathlib telah mendeklarasikan koersi dari Equiv α β ke tipe fungsi α → β, sehingga kita dapat menghilangkan .toFun dan membiarkan Lean menyisipkannya.

example (x : α) : (f.trans g).toFun x = g.toFun (f.toFun x) :=
  rfl

example (x : α) : (f.trans g) x = g (f x) :=
  rfl

example : (f.trans g : α → γ) = g ∘ f :=
  rfl

Mathlib juga mendefinisikan tipe Equiv.Perm α yang berisi ekuivalensi antara α dan dirinya sendiri.

example (α : Type*) : Equiv.Perm α = (α ≃ α) :=
  rfl

Jelas bahwa Equiv.Perm α membentuk grup di bawah komposisi ekuivalensi. Kita memilih orientasi sehingga mul f g sama dengan g.trans f, yang fungsi majunya adalah f ∘ g. Dengan kata lain, perkalian merupakan operasi yang biasanya kita pahami sebagai komposisi bijeksi. Berikut definisi grup tersebut:

def permGroup {α : Type*} : Group₁ (Equiv.Perm α)
    where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc h g f).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

Faktanya, Mathlib mendefinisikan struktur Group yang persis seperti ini pada Equiv.Perm α dalam berkas Algebra.Group.End. Seperti biasa, Anda dapat mengarahkan penunjuk ke teorema-teorema dalam definisi permGroup untuk melihat pernyataannya, lalu melompat ke definisinya dalam berkas asal guna mempelajari implementasinya.

Dalam matematika biasa, kita umumnya memandang notasi sebagai sesuatu yang tidak bergantung pada struktur. Sebagai contoh, kita dapat mempertimbangkan grup \((G_1, \cdot, 1, \cdot^{-1})\), \((G_2, \circ, e, i(\cdot))\), dan \((G_3, +, 0, -)\). Pada kasus pertama, kita menulis operasi biner sebagai \(\cdot\), identitas sebagai \(1\), dan fungsi invers sebagai \(x \mapsto x^{-1}\). Pada kasus kedua dan ketiga, kita menggunakan alternatif notasi yang ditampilkan. Namun, ketika gagasan grup diformalkan dalam Lean, notasi terikat lebih erat dengan struktur. Dalam Lean, komponen setiap Group bernama mul, one, dan inv. Sebentar lagi kita akan melihat cara menyiapkan notasi multiplikatif agar mengacu pada komponen-komponen tersebut. Jika ingin menggunakan notasi aditif, kita memakai struktur isomorfik AddGroup, yaitu struktur yang mendasari grup aditif. Komponennya bernama add, zero, dan neg, dengan notasi terkait sebagaimana yang dapat Anda duga.

Ingat tipe Point yang kita definisikan dalam Bab 7.1 beserta fungsi penjumlahannya. Definisi-definisi ini disalin kembali dalam berkas contoh yang menyertai bagian ini. Sebagai latihan, definisikan struktur AddGroup₁ yang serupa dengan Group₁ di atas, tetapi menggunakan skema penamaan aditif yang baru dijelaskan. Definisikan negasi dan nol pada tipe data Point, lalu definisikan struktur AddGroup₁ pada Point.

structure AddGroup₁ (α : Type*) where
  (add : α → α → α)
  -- lengkapi bagian lainnya
@[ext]
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ

namespace Point

def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def neg (a : Point) : Point := sorry

def zero : Point := sorry

def addGroupPoint : AddGroup₁ Point := sorry

end Point

Kita sudah membuat kemajuan. Kini kita mengetahui cara mendefinisikan struktur aljabar dalam Lean dan cara mendefinisikan instans struktur tersebut. Namun, kita juga ingin mengaitkan notasi dengan struktur agar dapat menggunakannya pada setiap instans. Lebih jauh, kita ingin dapat mendefinisikan operasi pada suatu struktur dan menggunakannya pada sembarang instans, serta membuktikan teorema tentang struktur dan menggunakannya pada sembarang instans.

Faktanya, Mathlib sudah disiapkan untuk menggunakan notasi, definisi, dan teorema grup generik bagi Equiv.Perm α.

variable {α : Type*} (f g : Equiv.Perm α) (n : ℕ)

#check f * g
#check mul_assoc f g g⁻¹

-- pangkat grup, didefinisikan untuk setiap grup
#check g ^ n

example : f * g * g⁻¹ = f := by rw [mul_assoc, mul_inv_cancel, mul_one]

example : f * g * g⁻¹ = f :=
  mul_inv_cancel_right f g

example {α : Type*} (f g : Equiv.Perm α) : g.symm.trans (g.trans f) = f :=
  mul_inv_cancel_right f g

Anda dapat memeriksa bahwa kemudahan ini belum berlaku pada struktur grup aditif Point yang diminta untuk Anda definisikan di atas. Tugas kita sekarang adalah memahami keajaiban yang berlangsung di balik layar sehingga contoh-contoh Equiv.Perm α bekerja seperti itu.

Persoalannya adalah Lean harus dapat menemukan notasi yang sesuai dan struktur grup implisit dengan menggunakan informasi dalam ekspresi yang kita tulis. Demikian pula, ketika kita menulis x + y dengan ekspresi x dan y bertipe ℝ, Lean harus menafsirkan simbol + sebagai fungsi penjumlahan yang sesuai pada bilangan real. Lean juga harus mengenali tipe ℝ sebagai instans gelanggang komutatif agar semua definisi dan teorema tentang gelanggang komutatif tersedia. Sebagai contoh lain, kekontinuan dalam Lean didefinisikan relatif terhadap sembarang dua ruang topologi. Ketika kita memiliki f : ℝ → ℂ dan menulis Continuous f, Lean harus menemukan topologi yang sesuai pada ℝ dan ℂ.

Keajaiban tersebut tercapai melalui gabungan tiga hal.

1. Logika. Definisi yang harus dapat ditafsirkan dalam sembarang grup menerima tipe grup dan struktur grup sebagai argumen. Demikian pula, teorema tentang elemen sembarang grup diawali kuantor universal atas tipe grup dan struktur grup tersebut.

2. Argumen implisit. Argumen tipe dan struktur umumnya dibiarkan implisit agar kita tidak perlu menuliskannya atau melihatnya dalam jendela informasi Lean. Lean mengisi informasi itu untuk kita tanpa terlihat.

3. Inferensi kelas tipe. Mekanisme ini, yang juga dikenal sebagai inferensi kelas, sederhana tetapi kuat dan memungkinkan kita mendaftarkan informasi agar dapat digunakan Lean kemudian. Ketika Lean diminta mengisi argumen implisit bagi definisi, teorema, atau suatu notasi, Lean dapat memanfaatkan informasi yang telah didaftarkan.

Anotasi (grp : Group G) memberi tahu Lean bahwa argumen tersebut akan diberikan secara eksplisit, sedangkan anotasi {grp : Group G} memberi tahu Lean agar mencoba menyimpulkannya dari petunjuk kontekstual dalam ekspresi. Anotasi [grp : Group G] memberi tahu Lean agar menyintesis argumen terkait menggunakan inferensi kelas tipe. Karena tujuan penggunaan argumen semacam ini adalah agar kita umumnya tidak perlu merujuknya secara eksplisit, Lean mengizinkan kita menulis [Group G] tanpa memberi nama pada argumen tersebut. Anda mungkin telah memperhatikan bahwa Lean otomatis memilih nama seperti _inst_1. Ketika anotasi kurung siku anonim digunakan bersama perintah variable, selama variabelnya masih berada dalam cakupan, Lean otomatis menambahkan argumen [Group G] pada setiap definisi atau teorema yang menyebut G.

Bagaimana kita mendaftarkan informasi yang perlu digunakan Lean untuk melakukan pencarian? Kembali ke contoh grup, kita hanya perlu membuat dua perubahan. Pertama, alih-alih memakai perintah structure untuk mendefinisikan struktur grup, kita memakai kata kunci class untuk menandainya sebagai kandidat inferensi kelas. Kedua, alih-alih mendefinisikan instans tertentu dengan def, kita memakai kata kunci instance untuk mendaftarkannya pada Lean. Seperti nama variabel kelas, nama definisi instans boleh dibiarkan anonim karena pada umumnya kita ingin Lean menemukannya dan menggunakannya tanpa membebani kita dengan rinciannya.

class Group₂ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  inv_mul_cancel : ∀ x : α, mul (inv x) x = one

instance {α : Type*} : Group₂ (Equiv.Perm α) where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc h g f).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

Contoh berikut mengilustrasikan penggunaannya.

#check Group₂.mul

def mySquare {α : Type*} [Group₂ α] (x : α) :=
  Group₂.mul x x

#check mySquare

section
variable {β : Type*} (f g : Equiv.Perm β)

example : Group₂.mul f g = g.trans f :=
  rfl

example : mySquare f = f.trans f :=
  rfl

end

Perintah #check menunjukkan bahwa Group₂.mul memiliki argumen implisit [Group₂ α] yang diharapkan ditemukan melalui inferensi kelas, dengan α sebagai tipe argumen bagi Group₂.mul. Dengan kata lain, {α : Type*} adalah argumen implisit untuk tipe elemen grup, sedangkan [Group₂ α] adalah argumen implisit untuk struktur grup pada α. Demikian pula, ketika mendefinisikan fungsi penguadratan generik mySquare untuk Group₂, kita menggunakan argumen implisit {α : Type*} untuk tipe elemennya dan argumen implisit [Group₂ α] untuk struktur Group₂.

Dalam contoh pertama, ketika kita menulis Group₂.mul f g, tipe f dan g memberi tahu Lean bahwa argumen α bagi Group₂.mul harus diinstansiasi menjadi Equiv.Perm β. Artinya, Lean harus menemukan elemen Group₂ (Equiv.Perm β). Deklarasi instance sebelumnya memberi tahu Lean dengan tepat cara melakukannya. Masalah terselesaikan!

Mekanisme sederhana untuk mendaftarkan informasi agar dapat ditemukan Lean saat diperlukan ini sangat berguna. Berikut salah satu penerapannya. Dalam landasan Lean, tipe data α boleh saja kosong. Namun, dalam sejumlah penerapan, kita perlu mengetahui bahwa suatu tipe memiliki sekurang-kurangnya satu elemen. Sebagai contoh, fungsi List.headI yang mengembalikan elemen pertama suatu daftar dapat mengembalikan nilai baku ketika daftar tersebut kosong. Agar hal itu dapat dilakukan, pustaka Lean mendefinisikan kelas Inhabited α yang hanya menyimpan sebuah nilai baku. Kita dapat menunjukkan bahwa tipe Point merupakan sebuah instans:

instance : Inhabited Point where default := ⟨0, 0, 0⟩

#check (default : Point)

example : ([] : List Point).headI = default :=
  rfl

Mekanisme inferensi kelas juga digunakan untuk notasi generik. Ekspresi x + y merupakan singkatan bagi Add.add x y. Seperti yang mungkin telah Anda duga, Add α adalah kelas yang menyimpan fungsi biner pada α. Menulis x + y memberi tahu Lean agar menemukan instans terdaftar [Add α] dan menggunakan fungsi yang bersesuaian. Di bawah ini kita mendaftarkan fungsi penjumlahan bagi Point.

instance : Add Point where add := Point.add

section
variable (x y : Point)

#check x + y

example : x + y = Point.add x y :=
  rfl

end

Dengan cara ini, kita juga dapat menetapkan notasi + pada operasi biner pada tipe lain.

Namun, kita dapat melangkah lebih jauh. Kita telah melihat bahwa * dapat digunakan dalam setiap grup, + dalam setiap grup aditif, dan keduanya dalam setiap gelanggang. Ketika mendefinisikan instans gelanggang baru dalam Lean, kita tidak perlu mendefinisikan + dan * bagi instans tersebut karena Lean mengetahui bahwa keduanya didefinisikan untuk setiap gelanggang. Kita dapat memakai metode ini untuk menentukan notasi bagi kelas Group₂:

instance {α : Type*} [Group₂ α] : Mul α :=
  ⟨Group₂.mul⟩

instance {α : Type*} [Group₂ α] : One α :=
  ⟨Group₂.one⟩

instance {α : Type*} [Group₂ α] : Inv α :=
  ⟨Group₂.inv⟩

section
variable {α : Type*} (f g : Equiv.Perm α)

#check f * 1 * g⁻¹

def foo : f * 1 * g⁻¹ = g.symm.trans ((Equiv.refl α).trans f) :=
  rfl

end

Pendekatan ini berhasil karena Lean melakukan pencarian rekursif. Berdasarkan instans yang telah kita deklarasikan, Lean dapat menemukan instans Mul (Equiv.Perm α) dengan mencari instans Group₂ (Equiv.Perm α), dan instans Group₂ (Equiv.Perm α) dapat ditemukan karena kita telah menyediakannya. Lean mampu menemukan kedua fakta ini dan merangkaikannya.

Contoh yang baru kita berikan berbahaya karena pustaka Lean juga memiliki instans Group (Equiv.Perm α), sedangkan perkalian didefinisikan pada setiap grup. Akibatnya, instans mana yang akan ditemukan menjadi ambigu. Faktanya, Lean mengutamakan deklarasi yang lebih baru kecuali Anda secara eksplisit menentukan prioritas berbeda. Ada pula cara lain untuk memberi tahu Lean bahwa satu struktur merupakan instans struktur lain, yaitu menggunakan kata kunci extends. Dengan cara inilah Mathlib menetapkan, misalnya, bahwa setiap gelanggang komutatif merupakan gelanggang. Informasi lebih lanjut tersedia dalam Bab 8 dan bagian tentang inferensi kelas dalam Theorem Proving in Lean.

Secara umum, menetapkan nilai * bagi instans struktur aljabar yang notasinya sudah didefinisikan merupakan gagasan buruk. Pendefinisian ulang gagasan Group dalam Lean adalah contoh buatan. Namun, pada kasus ini kedua penafsiran notasi grup sama-sama dapat dikembangkan menjadi Equiv.trans, Equiv.refl, dan Equiv.symm dengan cara yang sama.

Sebagai latihan buatan serupa, definisikan kelas AddGroup₂ dengan mencontoh Group₂. Definisikan notasi biasa untuk penjumlahan, negasi, dan nol pada sembarang AddGroup₂ menggunakan kelas Add, Neg, dan Zero. Kemudian tunjukkan bahwa Point merupakan instans AddGroup₂. Ujilah definisi Anda dan pastikan notasi grup aditif bekerja pada elemen Point.

class AddGroup₂ (α : Type*) where
  add : α → α → α
  -- lengkapi bagian lainnya

Tidak menjadi masalah besar bahwa sebelumnya kita telah mendeklarasikan instans Add, Neg, dan Zero bagi Point. Sekali lagi, kedua cara menyintesis notasi tersebut semestinya menghasilkan jawaban yang sama.

Inferensi kelas bersifat halus dan harus digunakan dengan hati-hati karena mekanisme ini mengatur otomatisasi yang secara tidak terlihat menentukan penafsiran ekspresi yang kita tulis. Namun, jika digunakan dengan bijak, inferensi kelas merupakan alat yang kuat. Mekanisme inilah yang memungkinkan penalaran aljabar dalam Lean.

7.3. Membangun Bilangan Bulat Gauss

Sekarang kita akan mengilustrasikan penggunaan hierarki aljabar dalam Lean dengan membangun sebuah objek matematika penting, yaitu bilangan bulat Gauss, dan menunjukkan bahwa objek tersebut merupakan domain Euklides. Dengan istilah yang selama ini kita gunakan, kita akan mendefinisikan bilangan bulat Gauss dan menunjukkan bahwa tipe tersebut merupakan instans struktur domain Euklides.

Dalam istilah matematika biasa, himpunan bilangan bulat Gauss \(\Bbb{Z}[i]\) adalah himpunan bilangan kompleks \(\{ a + b i \mid a, b \in \Bbb{Z}\}\). Namun, alih-alih mendefinisikannya sebagai subhimpunan bilangan kompleks, tujuan kita di sini adalah mendefinisikannya sebagai tipe data tersendiri. Caranya adalah merepresentasikan bilangan bulat Gauss sebagai pasangan bilangan bulat yang kita pandang sebagai bagian real dan imajiner.

@[ext]
structure GaussInt where
  re : ℤ
  im : ℤ

Pertama-tama kita menunjukkan bahwa bilangan bulat Gauss memiliki struktur gelanggang, dengan 0 didefinisikan sebagai ⟨0, 0⟩, 1 sebagai ⟨1, 0⟩, dan penjumlahan didefinisikan per komponen. Untuk menentukan definisi perkalian, ingat bahwa kita menginginkan elemen \(i\) yang direpresentasikan oleh ⟨0, 1⟩ menjadi akar kuadrat dari \(-1\). Karena itu, kita menginginkan

\[\begin{split}(a + bi) (c + di) & = ac + bci + adi + bd i^2 \\ & = (ac - bd) + (bc + ad)i.\end{split}\]

Penghitungan ini menjelaskan definisi Mul di bawah.

instance : Zero GaussInt :=
  ⟨⟨0, 0⟩⟩

instance : One GaussInt :=
  ⟨⟨1, 0⟩⟩

instance : Add GaussInt :=
  ⟨fun x y ↦ ⟨x.re + y.re, x.im + y.im⟩⟩

instance : Neg GaussInt :=
  ⟨fun x ↦ ⟨-x.re, -x.im⟩⟩

instance : Mul GaussInt :=
  ⟨fun x y ↦ ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩

Seperti dicatat dalam Bab 7.1, semua definisi yang berkaitan dengan suatu tipe data sebaiknya ditempatkan dalam namespace dengan nama yang sama. Karena itu, dalam berkas Lean yang terkait dengan bab ini, definisi-definisi tersebut dibuat dalam namespace GaussInt.

Perhatikan bahwa di sini kita langsung mendefinisikan penafsiran notasi 0, 1, +, -, dan *, bukan memberi nama seperti GaussInt.zero lalu menetapkan notasi tersebut kepadanya. Sering kali berguna untuk memiliki nama eksplisit bagi definisi, misalnya agar dapat digunakan bersama simp dan rw.

theorem zero_def : (0 : GaussInt) = ⟨0, 0⟩ :=
  rfl

theorem one_def : (1 : GaussInt) = ⟨1, 0⟩ :=
  rfl

theorem add_def (x y : GaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ :=
  rfl

theorem neg_def (x : GaussInt) : -x = ⟨-x.re, -x.im⟩ :=
  rfl

theorem mul_def (x y : GaussInt) :
    x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ :=
  rfl

Kita juga sebaiknya memberi nama pada kaidah yang menghitung bagian real dan imajiner, lalu mendaftarkannya pada penyederhana.

@[simp]
theorem zero_re : (0 : GaussInt).re = 0 :=
  rfl

@[simp]
theorem zero_im : (0 : GaussInt).im = 0 :=
  rfl

@[simp]
theorem one_re : (1 : GaussInt).re = 1 :=
  rfl

@[simp]
theorem one_im : (1 : GaussInt).im = 0 :=
  rfl

@[simp]
theorem add_re (x y : GaussInt) : (x + y).re = x.re + y.re :=
  rfl

@[simp]
theorem add_im (x y : GaussInt) : (x + y).im = x.im + y.im :=
  rfl

@[simp]
theorem neg_re (x : GaussInt) : (-x).re = -x.re :=
  rfl

@[simp]
theorem neg_im (x : GaussInt) : (-x).im = -x.im :=
  rfl

@[simp]
theorem mul_re (x y : GaussInt) : (x * y).re = x.re * y.re - x.im * y.im :=
  rfl

@[simp]
theorem mul_im (x y : GaussInt) : (x * y).im = x.re * y.im + x.im * y.re :=
  rfl

Sekarang ternyata sangat mudah menunjukkan bahwa bilangan bulat Gauss merupakan instans gelanggang komutatif. Di sinilah gagasan struktur sangat berguna. Setiap bilangan bulat Gauss tertentu merupakan instans struktur GaussInt, sedangkan tipe GaussInt itu sendiri, beserta operasi-operasi terkait, merupakan instans struktur CommRing. Selanjutnya, struktur CommRing memperluas struktur notasi Zero, One, Add, Neg, dan Mul.

Jika Anda mengetik instance : CommRing GaussInt := _, mengeklik ikon lampu yang muncul dalam VS Code, lalu meminta Lean mengisi kerangka definisi struktur, Anda akan melihat jumlah entri yang cukup menakutkan. Namun, jika Anda melompat ke definisi strukturnya, terlihat bahwa banyak field memiliki definisi baku yang akan diisi Lean secara otomatis. Field-field esensial muncul dalam definisi di bawah. Dua kasus khusus adalah nsmul dan zsmul; abaikan keduanya untuk sekarang karena akan dijelaskan dalam bab berikutnya. Pada setiap kasus, identitas terkait dibuktikan dengan membuka definisi, menggunakan taktik ext untuk mereduksi identitas menjadi komponen real dan imajinernya, menyederhanakan, lalu jika perlu melakukan penghitungan gelanggang yang sesuai pada bilangan bulat. Perhatikan bahwa kita dapat dengan mudah menghindari pengulangan seluruh kode ini, tetapi hal tersebut bukan topik pembahasan sekarang.

instance instCommRing : CommRing GaussInt where
  zero := 0
  one := 1
  add := (· + ·)
  neg x := -x
  mul := (· * ·)
  nsmul := nsmulRec
  zsmul := zsmulRec
  add_assoc := by
    intros
    ext <;> simp <;> ring
  zero_add := by
    intro
    ext <;> simp
  add_zero := by
    intro
    ext <;> simp
  neg_add_cancel := by
    intro
    ext <;> simp
  add_comm := by
    intros
    ext <;> simp <;> ring
  mul_assoc := by
    intros
    ext <;> simp <;> ring
  one_mul := by
    intro
    ext <;> simp
  mul_one := by
    intro
    ext <;> simp
  left_distrib := by
    intros
    ext <;> simp <;> ring
  right_distrib := by
    intros
    ext <;> simp <;> ring
  mul_comm := by
    intros
    ext <;> simp <;> ring
  zero_mul := by
    intros
    ext <;> simp
  mul_zero := by
    intros
    ext <;> simp

Pustaka Lean mendefinisikan kelas tipe tak trivial sebagai tipe yang memiliki sekurang-kurangnya dua elemen berbeda. Dalam konteks gelanggang, hal ini ekuivalen dengan menyatakan bahwa nol tidak sama dengan satu. Karena beberapa teorema umum bergantung pada fakta tersebut, sebaiknya kita membuktikannya sekarang.

instance : Nontrivial GaussInt := by
  use 0, 1
  rw [Ne, GaussInt.ext_iff]
  simp

Sekarang kita akan menunjukkan bahwa bilangan bulat Gauss memiliki satu sifat tambahan yang penting. Sebuah domain Euklides adalah gelanggang \(R\) yang dilengkapi fungsi norma \(N : R \to \mathbb{N}\) dengan dua sifat berikut:

• Untuk setiap \(a\) dan \(b \ne 0\) di \(R\), terdapat \(q\) dan \(r\) di \(R\) sedemikian sehingga \(a = bq + r\), dan berlaku \(r = 0\) atau \(N(r) < N(b)\).

• Untuk setiap \(a\) dan \(b \ne 0\), berlaku \(N(a) \le N(ab)\).

Gelanggang bilangan bulat \(\Bbb{Z}\) dengan \(N(a) = |a|\) merupakan contoh prototipikal sebuah domain Euklides. Dalam kasus itu, kita dapat mengambil \(q\) sebagai hasil pembagian bulat \(a\) oleh \(b\) dan \(r\) sebagai sisanya. Perhatikan bahwa ketika a dan b adalah bilangan bulat, a / b menyatakan pembagian bulat di Lean, sedangkan a % b menyatakan sisanya. Keduanya didefinisikan agar memenuhi sifat-sifat berikut:

example (a b : ℤ) : a = b * (a / b) + a % b :=
  Eq.symm (Int.mul_ediv_add_emod a b)

example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b :=
  Int.emod_nonneg a

example (a b : ℤ) : b ≠ 0 → a % b < |b| :=
  Int.emod_lt_abs a

Dalam gelanggang sebarang, suatu elemen \(a\) disebut unit jika membagi \(1\). Suatu elemen tak nol \(a\) disebut tak tereduksi jika tidak dapat ditulis dalam bentuk \(a = bc\) dengan \(b\) dan \(c\) keduanya bukan unit. Pada bilangan bulat, setiap elemen tak tereduksi \(a\) bersifat prima. Artinya, setiap kali \(a\) membagi hasil kali \(bc\), elemen tersebut membagi \(b\) atau \(c\). Namun, dalam gelanggang lain sifat ini dapat gagal. Dalam gelanggang \(\Bbb{Z}[\sqrt{-5}]\), kita mempunyai

\[6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),\]

dan elemen-elemen \(2\), \(3\), \(1 + \sqrt{-5}\), serta \(1 - \sqrt{-5}\) semuanya tak tereduksi, tetapi tidak prima. Sebagai contoh, \(2\) membagi hasil kali \((1 + \sqrt{-5})(1 - \sqrt{-5})\), tetapi tidak membagi satu pun dari kedua faktornya. Secara khusus, faktorisasi tidak lagi unik: bilangan \(6\) dapat difaktorkan menjadi elemen-elemen tak tereduksi dengan lebih dari satu cara.

Sebaliknya, setiap domain Euklides merupakan domain faktorisasi unik; akibatnya, setiap elemen tak tereduksi bersifat prima. Aksioma-aksioma domain Euklides menyiratkan bahwa setiap elemen tak nol dapat ditulis sebagai hasil kali hingga elemen-elemen tak tereduksi. Aksioma tersebut juga menyiratkan bahwa kita dapat menggunakan algoritma Euklides untuk mencari pembagi persekutuan terbesar dari sembarang dua elemen tak nol a dan b, yakni suatu elemen yang habis dibagi oleh setiap pembagi persekutuan lainnya. Hal ini pada gilirannya menyiratkan bahwa faktorisasi menjadi elemen-elemen tak tereduksi bersifat unik hingga perkalian dengan unit.

Sekarang kita akan menunjukkan bahwa bilangan bulat Gauss merupakan domain Euklides dengan norma yang didefinisikan oleh \(N(a + bi) = (a + bi)(a - bi) = a^2 + b^2\). Bilangan bulat Gauss \(a - bi\) disebut konjugat dari \(a + bi\). Mudah diperiksa bahwa untuk sembarang bilangan kompleks \(x\) dan \(y\), berlaku \(N(xy) = N(x)N(y)\).

Untuk melihat bahwa definisi norma ini menjadikan bilangan bulat Gauss sebuah domain Euklides, hanya sifat pertama yang menantang. Misalkan kita ingin menulis \(a + bi = (c + di) q + r\) untuk \(q\) dan \(r\) yang sesuai. Dengan memperlakukan \(a + bi\) dan \(c + di\) sebagai bilangan kompleks, lakukan pembagian

\[\frac{a + bi}{c + di} = \frac{(a + bi)(c - di)}{(c + di)(c-di)} = \frac{ac + bd}{c^2 + d^2} + \frac{bc -ad}{c^2+d^2} i.\]

Bagian real dan imajinernya mungkin bukan bilangan bulat, tetapi kita dapat membulatkannya ke bilangan bulat terdekat \(u\) dan \(v\). Selanjutnya, kita dapat menyatakan ruas kanan sebagai \((u + vi) + (u' + v'i)\), dengan \(u' + v'i\) sebagai bagian yang tersisa. Perhatikan bahwa \(|u'| \le 1/2\) dan \(|v'| \le 1/2\), sehingga

\[N(u' + v' i) = (u')^2 + (v')^2 \le 1/4 + 1/4 \le 1/2.\]

Dengan mengalikan kedua ruas dengan \(c + di\), kita memperoleh

\[a + bi = (c + di) (u + vi) + (c + di) (u' + v'i).\]

Dengan menetapkan \(q = u + vi\) dan \(r = (c + di) (u' + v'i)\), kita memperoleh \(a + bi = (c + di) q + r\); selanjutnya kita hanya perlu memberi batas pada \(N(r)\):

\[N(r) = N(c + di)N(u' + v'i) \le N(c + di) \cdot 1/2 < N(c + di).\]

Argumen yang baru saja kita lakukan mengharuskan kita memandang bilangan bulat Gauss sebagai subhimpunan bilangan kompleks. Karena itu, salah satu cara memformalkannya di Lean adalah dengan menyematkan bilangan bulat Gauss ke dalam bilangan kompleks, menyematkan bilangan bulat ke dalam bilangan bulat Gauss, mendefinisikan fungsi pembulatan dari bilangan real ke bilangan bulat, dan dengan cermat berpindah di antara sistem-sistem bilangan tersebut. Sebenarnya, inilah tepatnya pendekatan yang digunakan di Mathlib, tempat bilangan bulat Gauss dikonstruksi sebagai kasus khusus gelanggang bilangan bulat kuadratik. Lihat berkas GaussianInt.lean.

Di sini, kita justru akan menjalankan argumen yang seluruhnya berlangsung pada bilangan bulat. Hal ini menggambarkan pilihan yang lazim dihadapi ketika memformalkan matematika. Jika suatu argumen memerlukan konsep atau perangkat yang belum tersedia di pustaka, ada dua pilihan: memformalkan konsep dan perangkat yang diperlukan, atau menyesuaikan argumen agar menggunakan konsep dan perangkat yang sudah tersedia. Pilihan pertama umumnya merupakan investasi waktu yang baik apabila hasilnya dapat digunakan dalam konteks lain. Namun, dari sudut pandang praktis, kadang kala mencari bukti yang lebih elementer lebih efisien.

Teorema hasil-bagi-dan-sisa yang biasa untuk bilangan bulat menyatakan bahwa untuk setiap \(a\) dan \(b\) tak nol, terdapat \(q\) dan \(r\) sedemikian sehingga \(a = b q + r\) dan \(0 \le r < |b|\). Di sini kita akan menggunakan variasi berikut, yang menyatakan bahwa terdapat \(q'\) dan \(r'\) sedemikian sehingga \(a = b q' + r'\) dan \(|r'| \le |b|/2\). Anda dapat memeriksa bahwa jika nilai \(r\) dalam pernyataan pertama memenuhi \(r \le |b|/2\), kita dapat mengambil \(q' = q\) dan \(r' = r\). Jika tidak, kita dapat mengambil \(q' = q + 1\) dan \(r' = r - b\) (untuk \(b\) positif; jika tidak, lakukan perubahan yang semestinya). Kami berterima kasih kepada Heather Macbeth yang menyarankan pendekatan berikut, yang lebih elegan dan menghindari definisi berdasarkan kasus. Kita cukup menambahkan b / 2 pada a sebelum melakukan pembagian, kemudian mengurangkannya dari sisa.

def div' (a b : ℤ) :=
  (a + b / 2) / b

def mod' (a b : ℤ) :=
  (a + b / 2) % b - b / 2

theorem div'_add_mod' (a b : ℤ) : b * div' a b + mod' a b = a := by
  rw [div', mod']
  linarith [Int.mul_ediv_add_emod (a + b / 2) b]

theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by
  rw [mod', abs_le]
  constructor
  · linarith [Int.emod_nonneg (a + b / 2) h.ne']
  have := Int.emod_lt_of_pos (a + b / 2) h
  have := Int.mul_ediv_add_emod b 2
  have := Int.emod_lt_of_pos b zero_lt_two
  linarith

Perhatikan penggunaan kawan lama kita, linarith. Kita juga perlu menyatakan mod' dengan menggunakan div'.

theorem mod'_eq (a b : ℤ) : mod' a b = a - b * div' a b := by linarith [div'_add_mod' a b]

Kita akan menggunakan fakta bahwa \(x^2 + y^2\) sama dengan nol jika dan hanya jika \(x\) dan \(y\) keduanya nol. Sebagai latihan, Anda diminta membuktikan bahwa hal ini berlaku dalam setiap gelanggang terurut.

theorem sq_add_sq_eq_zero {α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α]
    (x y : α) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
  sorry

Semua definisi dan teorema yang tersisa dalam bagian ini akan kita tempatkan di namespace GaussInt. Pertama, kita mendefinisikan fungsi norm dan meminta Anda membuktikan beberapa sifatnya. Semua buktinya singkat.

def norm (x : GaussInt) :=
  x.re ^ 2 + x.im ^ 2

@[simp]
theorem norm_nonneg (x : GaussInt) : 0 ≤ norm x := by
  sorry
theorem norm_eq_zero (x : GaussInt) : norm x = 0 ↔ x = 0 := by
  sorry
theorem norm_pos (x : GaussInt) : 0 < norm x ↔ x ≠ 0 := by
  sorry
theorem norm_mul (x y : GaussInt) : norm (x * y) = norm x * norm y := by
  sorry

Selanjutnya kita mendefinisikan fungsi konjugat:

def conj (x : GaussInt) : GaussInt :=
  ⟨x.re, -x.im⟩

@[simp]
theorem conj_re (x : GaussInt) : (conj x).re = x.re :=
  rfl

@[simp]
theorem conj_im (x : GaussInt) : (conj x).im = -x.im :=
  rfl

theorem norm_conj (x : GaussInt) : norm (conj x) = norm x := by simp [norm]

Terakhir, kita mendefinisikan pembagian pada bilangan bulat Gauss dengan notasi x / y. Operasi ini membulatkan hasil bagi kompleks ke bilangan bulat Gauss terdekat. Untuk itu, kita menggunakan Int.div' yang dirancang khusus. Seperti yang telah kita hitung di atas, jika x adalah \(a + bi\) dan y adalah \(c + di\), bagian real dan imajiner dari x / y masing-masing adalah bilangan bulat terdekat dengan

\[\frac{ac + bd}{c^2 + d^2} \quad \text{dan} \quad \frac{bc -ad}{c^2+d^2}.\]

Di sini, pembilangnya merupakan bagian real dan imajiner dari \((a + bi) (c - di)\), sedangkan kedua penyebutnya sama dengan norma \(c + di\).

instance : Div GaussInt :=
  ⟨fun x y ↦ ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩⟩

Setelah mendefinisikan x / y, kita mendefinisikan x % y sebagai sisanya, yaitu x - y * (x / y). Seperti di atas, kita mencatat definisi tersebut dalam teorema div_def dan mod_def agar dapat menggunakannya bersama simp dan rw.

instance : Mod GaussInt :=
  ⟨fun x y ↦ x - y * (x / y)⟩

theorem div_def (x y : GaussInt) :
    x / y = ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩ :=
  rfl

theorem mod_def (x y : GaussInt) : x % y = x - y * (x / y) :=
  rfl

Definisi-definisi ini langsung menghasilkan x = y * (x / y) + x % y untuk setiap x dan y. Jadi, kita hanya perlu menunjukkan bahwa norma x % y lebih kecil daripada norma y apabila y tidak nol.

Kita baru saja mendefinisikan bagian real dan imajiner dari x / y masing-masing sebagai div' (x * conj y).re (norm y) dan div' (x * conj y).im (norm y). Dengan menghitung, kita memperoleh

(x % y) * conj y = (x - x / y * y) * conj y = x * conj y - x / y * (y * conj y)

Bagian real dan imajiner ruas kanan tepat sama dengan mod' (x * conj y).re (norm y) dan mod' (x * conj y).im (norm y). Berdasarkan sifat div' dan mod', nilai mutlak keduanya dijamin kurang dari atau sama dengan norm y / 2. Jadi, kita mempunyai

norm ((x % y) * conj y) ≤ (norm y / 2)^2 + (norm y / 2)^2 ≤ (norm y / 2) * norm y.

Di sisi lain, kita mempunyai

norm ((x % y) * conj y) = norm (x % y) * norm (conj y) = norm (x % y) * norm y.

Dengan membagi kedua ruas oleh norm y, kita memperoleh norm (x % y) ≤ (norm y) / 2 < norm y, seperti yang diperlukan.

Penghitungan yang rumit ini dilaksanakan dalam bukti berikut. Kami menganjurkan Anda menelusuri perinciannya dan mencoba menemukan argumen yang lebih rapi.

theorem norm_mod_lt (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
    (x % y).norm < y.norm := by
  have norm_y_pos : 0 < norm y := by rwa [norm_pos]
  have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
  · ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
  have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
  · calc
      norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
      _ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
          + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
      _ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
      _ = norm y / 2 * (norm y / 2 * 2) := by ring
      _ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
  calc norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right H2 norm_y_pos
    _ < norm y := by
        apply Int.ediv_lt_of_lt_mul
        · norm_num
        · linarith

Kita telah memasuki tahap akhir. Fungsi norm memetakan bilangan bulat Gauss ke bilangan bulat tak negatif. Kita memerlukan fungsi yang memetakan bilangan bulat Gauss ke bilangan asli. Fungsi tersebut diperoleh dengan mengomposisikan norm dengan Int.natAbs, yang memetakan bilangan bulat ke bilangan asli. Lemma pertama dari dua lemma berikut menetapkan bahwa memetakan norma ke bilangan asli lalu kembali ke bilangan bulat tidak mengubah nilainya. Lemma kedua menyatakan kembali fakta bahwa normanya menurun.

theorem coe_natAbs_norm (x : GaussInt) : (x.norm.natAbs : ℤ) = x.norm :=
  Int.natAbs_of_nonneg (norm_nonneg _)

theorem natAbs_norm_mod_lt (x y : GaussInt) (hy : y ≠ 0) :
    (x % y).norm.natAbs < y.norm.natAbs := by
  apply Int.ofNat_lt.1
  simp only [Int.natCast_natAbs, abs_of_nonneg, norm_nonneg]
  exact norm_mod_lt x hy

Kita juga perlu membuktikan sifat kunci kedua dari fungsi norma pada domain Euklides.

theorem not_norm_mul_left_lt_norm (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
    ¬(norm (x * y)).natAbs < (norm x).natAbs := by
  apply not_lt_of_ge
  rw [norm_mul, Int.natAbs_mul]
  apply le_mul_of_one_le_right (Nat.zero_le _)
  apply Int.ofNat_le.1
  rw [coe_natAbs_norm]
  exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)

Sekarang kita dapat merangkai semuanya untuk menunjukkan bahwa bilangan bulat Gauss merupakan instans domain Euklides. Kita menggunakan fungsi hasil bagi dan sisa yang telah didefinisikan. Definisi domain Euklides dalam Mathlib lebih umum daripada definisi di atas, karena memungkinkan kita menunjukkan bahwa sisa menurun terhadap sembarang ukuran berfondasi baik. Membandingkan nilai-nilai fungsi norma yang menghasilkan bilangan asli hanyalah salah satu contoh ukuran semacam itu. Dalam kasus ini, sifat-sifat yang diperlukan diberikan oleh teorema natAbs_norm_mod_lt dan not_norm_mul_left_lt_norm.

instance : EuclideanDomain GaussInt :=
  { GaussInt.instCommRing with
    quotient := (· / ·)
    remainder := (· % ·)
    quotient_mul_add_remainder_eq :=
      fun x y ↦ by rw [mod_def, add_comm] ; ring
    quotient_zero := fun x ↦ by
      simp [div_def, norm, Int.div']
      rfl
    r := (measure (Int.natAbs ∘ norm)).1
    r_wellFounded := (measure (Int.natAbs ∘ norm)).2
    remainder_lt := natAbs_norm_mod_lt
    mul_left_not_lt := not_norm_mul_left_lt_norm }

Salah satu hasil langsungnya adalah bahwa sekarang kita mengetahui bahwa, pada bilangan bulat Gauss, konsep prima dan tak tereduksi berimpit.

example (x : GaussInt) : Irreducible x ↔ Prime x :=
  irreducible_iff_prime