6. Matematika Diskret

Matematika diskret mempelajari himpunan, objek, dan struktur berhingga. Kita dapat menghitung banyaknya elemen suatu himpunan berhingga, menghitung jumlah atau hasil kali berhingga atas elemen-elemennya, menentukan nilai maksimum dan minimum, dan sebagainya. Kita juga dapat mempelajari objek yang dibangkitkan melalui sejumlah berhingga penerapan fungsi pembangkit tertentu, mendefinisikan fungsi melalui rekursi struktural, dan membuktikan teorema melalui induksi struktural. Bab ini menjelaskan bagian-bagian Mathlib yang mendukung kegiatan tersebut.

6.1. Finset dan Fintype

Menangani himpunan dan tipe berhingga dalam Mathlib dapat membingungkan karena pustaka ini menyediakan beberapa cara untuk menanganinya. Bagian ini membahas cara-cara yang paling umum.

Kita telah menjumpai tipe Finset dalam Bab 5.2 dan Bab 5.3. Sesuai namanya, sebuah elemen bertipe Finset α adalah himpunan berhingga yang elemen-elemennya bertipe α. Kita akan menyebut objek semacam ini "finset". Tipe data Finset dirancang agar memiliki interpretasi komputasional, dan banyak operasi dasar pada Finset α mengasumsikan bahwa kesamaan pada α dapat diputuskan. Hal ini menjamin adanya algoritma untuk menguji apakah a : α merupakan elemen dari suatu finset s.

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

#check a ∈ s
#check s ∩ t

end

Jika deklarasi [DecidableEq α] dihapus, Lean akan mengeluh pada baris #check s ∩ t karena tidak dapat menghitung irisannya. Namun, semua tipe data yang secara wajar diharapkan dapat digunakan dalam komputasi memiliki kesamaan yang dapat diputuskan. Jika Anda bekerja secara klasik dengan membuka namespace Classical dan mendeklarasikan noncomputable section, Anda dapat menalar tentang finset yang beranggotakan elemen dari tipe apa pun.

Finset mendukung sebagian besar operasi teori himpunan yang juga tersedia bagi himpunan biasa:

open Finset

variable (a b c : Finset ℕ)
variable (n : ℕ)

#check a ∩ b
#check a ∪ b
#check a \ b
#check (∅ : Finset ℕ)

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by
  ext x; simp only [mem_inter, mem_union]; tauto

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by rw [inter_union_distrib_left]

Perhatikan bahwa kita telah membuka namespace Finset, tempat teorema-teorema khusus tentang finset berada. Jika Anda menelusuri contoh terakhir di bawah langkah demi langkah, Anda akan melihat bahwa penerapan ext yang diikuti oleh simp mereduksi identitas tersebut menjadi masalah dalam logika proposisional. Sebagai latihan, Anda dapat mencoba membuktikan beberapa identitas himpunan dari Bab 4 yang diadaptasi untuk finset.

Anda telah melihat notasi Finset.range n untuk himpunan berhingga bilangan asli \(\{ 0, 1, \ldots, n-1 \}\). Finset juga memungkinkan Anda mendefinisikan himpunan berhingga dengan mencacah elemen-elemennya:

#check ({0, 2, 5} : Finset Nat)

def example1 : Finset ℕ := {0, 1, 2}

Ada berbagai cara untuk membuat Lean mengenali bahwa urutan elemen dan kemunculan berulang tidak berpengaruh pada himpunan yang disajikan dengan cara ini.

example : ({0, 1, 2} : Finset ℕ) = {1, 2, 0} := by decide

example : ({0, 1, 2} : Finset ℕ) = {0, 1, 1, 2} := by decide

example : ({0, 1} : Finset ℕ) = {1, 0} := by rw [Finset.pair_comm]

example (x : Nat) : ({x, x} : Finset ℕ) = {x} := by simp

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp [or_comm, or_left_comm]

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp; tauto

Anda dapat menggunakan insert untuk menambahkan satu elemen ke sebuah finset dan Finset.erase untuk menghapus satu elemen. Perhatikan bahwa erase berada dalam namespace Finset, sedangkan insert berada dalam namespace akar.

example (s : Finset ℕ) (a : ℕ) (h : a ∉ s) : (insert a s |>.erase a) = s :=
  Finset.erase_insert h

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : insert a (s.erase a) = s :=
  Finset.insert_erase h

Sebenarnya, {0, 1, 2} hanyalah notasi untuk insert 0 (insert 1 (singleton 2)).

set_option pp.notation false in
#check ({0, 1, 2} : Finset ℕ)

Dengan sebuah finset s dan predikat P, kita dapat menggunakan notasi pembentuk himpunan {x ∈ s | P x} untuk mendefinisikan himpunan yang terdiri atas elemen-elemen s yang memenuhi P. Notasi ini berarti Finset.filter P s, yang juga dapat ditulis s.filter P.

example : {m ∈ range n | Even m} = (range n).filter Even := rfl
example : {m ∈ range n | Even m ∧ m ≠ 3} = (range n).filter (fun m ↦ Even m ∧ m ≠ 3) := rfl

example : {m ∈ range 10 | Even m} = {0, 2, 4, 6, 8} := by decide

Mathlib mengetahui bahwa citra sebuah finset di bawah suatu fungsi juga merupakan finset.

#check (range 5).image (fun x ↦ x * 2)

example : (range 5).image (fun x ↦ x * 2) = {x ∈ range 10 | Even x} := by decide

Lean juga mengetahui bahwa hasil kali Kartesius s ×ˢ t dari dua finset merupakan finset dan bahwa himpunan kuasa suatu finset juga merupakan finset. (Perhatikan bahwa notasi s ×ˢ t juga berlaku untuk himpunan.)

#check s ×ˢ t
#check s.powerset

Mendefinisikan operasi pada finset berdasarkan elemen-elemennya tidak mudah karena setiap definisi semacam itu harus tidak bergantung pada urutan penyajian elemen. Tentu saja, Anda selalu dapat mendefinisikan fungsi dengan menyusun operasi yang sudah ada. Cara lain adalah menggunakan Finset.fold untuk melipat suatu operasi biner atas elemen-elemennya, asalkan operasi tersebut asosiatif dan komutatif. Sifat-sifat ini menjamin bahwa hasilnya tidak bergantung pada urutan penerapan operasi. Jumlah, hasil kali, dan gabungan berhingga didefinisikan dengan cara tersebut. Dalam contoh terakhir di bawah, biUnion berarti "gabungan berindeks terbatas". Dalam notasi matematika konvensional, ekspresi itu ditulis \(\bigcup_{i ∈ s} g(i)\).

#check Finset.fold

def f (n : ℕ) : Int := (↑n)^2

#check (range 5).fold (fun x y : Int ↦ x + y) 0 f
#eval (range 5).fold (fun x y : Int ↦ x + y) 0 f

#check ∑ i ∈ range 5, i^2
#check ∏ i ∈ range 5, i + 1

variable (g : Nat → Finset Int)

#check (range 5).biUnion g

Terdapat prinsip induksi alami pada finset: untuk membuktikan bahwa setiap finset memiliki suatu sifat, tunjukkan bahwa himpunan kosong memiliki sifat tersebut dan bahwa sifat itu tetap berlaku ketika kita menambahkan satu elemen baru ke sebuah finset. (Simbol @ dalam @insert diperlukan pada langkah induksi dalam contoh berikut untuk memberi nama pada parameter a dan s karena keduanya ditandai implisit.)

#check Finset.induction

example {α : Type*} [DecidableEq α] (f : α → ℕ)  (s : Finset α) (h : ∀ x ∈ s, f x ≠ 0) :
    ∏ x ∈ s, f x ≠ 0 := by
  induction s using Finset.induction_on with
  | empty => simp
  | @insert a s anins ih =>
    rw [prod_insert anins]
    apply mul_ne_zero
    · apply h; apply mem_insert_self
    apply ih
    intros x xs
    exact h x (mem_insert_of_mem xs)

Jika s adalah sebuah finset, Finset.Nonempty s didefinisikan sebagai ∃ x, x ∈ s. Anda dapat menggunakan pilihan klasik untuk memilih satu elemen dari finset tak kosong. Demikian pula, pustaka mendefinisikan Finset.toList s, yang menggunakan pilihan untuk mengambil elemen-elemen s dalam suatu urutan.

noncomputable example (s : Finset ℕ) (h : s.Nonempty) : ℕ := Classical.choose h

example (s : Finset ℕ) (h : s.Nonempty) : Classical.choose h ∈ s := Classical.choose_spec h

noncomputable example (s : Finset ℕ) : List ℕ := s.toList

example (s : Finset ℕ) (a : ℕ) : a ∈ s.toList ↔ a ∈ s := mem_toList

Anda dapat menggunakan Finset.min dan Finset.max untuk memilih elemen minimum atau maksimum dari finset yang elemennya berada dalam suatu tatanan linear. Demikian pula, Anda dapat menggunakan Finset.inf dan Finset.sup untuk finset yang elemennya berada dalam suatu kisi, tetapi ada satu kendala. Apa yang harus dijadikan elemen minimum dari finset kosong? Anda dapat memeriksa bahwa versi bertanda prima dari fungsi-fungsi di bawah menambahkan prasyarat bahwa finset tersebut tak kosong. Untuk menangani finset kosong, versi tanpa prima Finset.min dan Finset.max menambahkan elemen terbesar atau terkecil, secara berturut-turut, pada tipe keluaran. Versi tanpa prima Finset.inf dan Finset.sup mengasumsikan bahwa kisi tersebut dilengkapi elemen terbesar atau terkecil, secara berturut-turut.

#check Finset.min
#check Finset.min'
#check Finset.max
#check Finset.max'
#check Finset.inf
#check Finset.inf'
#check Finset.sup
#check Finset.sup'

example : Finset.Nonempty {2, 6, 7} := ⟨6, by trivial⟩
example : Finset.min' {2, 6, 7} ⟨6, by trivial⟩ = 2 := by trivial

Setiap finset s memiliki kardinalitas berhingga, Finset.card s, yang dapat ditulis #s ketika namespace Finset terbuka.

#check Finset.card

#eval (range 5).card

example (s : Finset ℕ) : s.card = #s := by rfl

example (s : Finset ℕ) : s.card = ∑ _i ∈ s, 1 := by rw [card_eq_sum_ones]

example (s : Finset ℕ) : s.card = ∑ _i ∈ s, 1 := by simp

Bagian berikutnya sepenuhnya membahas penalaran mengenai kardinalitas.

Ketika memformalkan matematika, kita sering harus menentukan apakah definisi dan teorema akan dinyatakan menggunakan himpunan atau tipe. Penggunaan tipe sering menyederhanakan notasi dan pembuktian, tetapi bekerja dengan subhimpunan dari suatu tipe dapat lebih luwes. Padanan berbasis tipe bagi finset adalah fintype, yakni suatu tipe α yang dilengkapi instans Fintype α. Menurut definisi, sebuah fintype hanyalah tipe data yang dilengkapi finset univ yang memuat seluruh elemennya.

variable {α : Type*} [Fintype α]

example : ∀ x : α, x ∈ Finset.univ := by
  intro x; exact mem_univ x

Fintype.card α sama dengan kardinalitas finset yang bersesuaian.

example : Fintype.card α = (Finset.univ : Finset α).card := rfl

Kita telah melihat contoh prototipikal fintype, yaitu tipe Fin n untuk setiap n. Lean mengenali bahwa kelas fintype tertutup terhadap operasi seperti hasil kali.

example : Fintype.card (Fin 5) = 5 := by simp
example : Fintype.card ((Fin 5) × (Fin 3)) = 15 := by simp

Setiap elemen s dari Finset α dapat dikoersikan menjadi tipe (↑s : Type), yaitu subtipe yang terdiri atas elemen-elemen α yang termuat dalam s. Selain itu, Lean mengetahui bahwa ↑s merupakan fintype.

variable (s : Finset ℕ)

example : (↑s : Type) = {x : ℕ // x ∈ s} := rfl
example : Fintype.card ↑s = s.card := by simp

Lean dan Mathlib menggunakan inferensi kelas tipe untuk melacak struktur tambahan pada fintype, yakni finset universal yang memuat seluruh elemen. Dengan kata lain, Anda dapat memandang fintype sebagai struktur aljabar yang dilengkapi data tambahan tersebut. Bab 7 menjelaskan cara kerjanya.

6.2. Argumen Pencacahan

Kemahiran mencacah berbagai objek merupakan bagian utama kombinatorika. Mathlib memuat beberapa identitas dasar untuk menghitung elemen finset:

open Finset

variable {α β : Type*} [DecidableEq α] [DecidableEq β] (s t : Finset α) (f : α → β)

example : #(s ×ˢ t) = #s * #t := by rw [card_product]
example : #(s ×ˢ t) = #s * #t := by simp

example : #(s ∪ t) = #s + #t - #(s ∩ t) := by rw [card_union]

example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by rw [card_union_of_disjoint h]
example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by simp [h]

example (h : Function.Injective f) : #(s.image f) = #s := by rw [card_image_of_injective _ h]

example (h : Set.InjOn f s) : #(s.image f) = #s := by rw [card_image_of_injOn h]

Dengan membuka namespace Finset, kita dapat menggunakan notasi #s untuk s.card serta nama-nama ringkas seperti card_union dan seterusnya.

Mathlib juga dapat menghitung elemen fintype:

open Fintype

variable {α β : Type*} [Fintype α] [Fintype β]

example : card (α × β) = card α * card β := by simp

example : card (α ⊕ β) = card α + card β := by simp

example (n : ℕ) : card (Fin n → α) = (card α)^n := by simp

variable {n : ℕ} {γ : Fin n → Type*} [∀ i, Fintype (γ i)]

example : card ((i : Fin n) → γ i) = ∏ i, card (γ i) := by simp

example : card (Σ i, γ i) = ∑ i, card (γ i) := by simp

Ketika namespace Fintype tidak terbuka, kita harus menggunakan Fintype.card, bukan card.

Berikut adalah contoh penghitungan kardinalitas suatu finset, yaitu gabungan range n dengan salinan range n yang digeser sekurang-kurangnya sejauh n. Penghitungan tersebut mengharuskan kita menunjukkan bahwa kedua himpunan dalam gabungan itu saling lepas. Baris pertama pembuktian menghasilkan syarat samping Disjoint (range n) (image (fun i ↦ m + i) (range n)), yang dibuktikan pada akhir pembuktian. Predikat Disjoint terlalu umum untuk langsung berguna bagi kita, tetapi teorema disjoint_iff_ne mengubahnya ke bentuk yang dapat kita gunakan.

#check Disjoint

example (m n : ℕ) (h : m ≥ n) :
    card (range n ∪ (range n).image (fun i ↦ m + i)) = 2 * n := by
  rw [card_union_of_disjoint, card_range, card_image_of_injective, card_range]; omega
  . apply add_right_injective
  . simp [disjoint_iff_ne]; omega

Sepanjang bagian ini, omega akan menjadi alat andalan kita untuk menangani penghitungan aritmetika dan pertidaksamaan.

Berikut contoh yang lebih menarik. Pertimbangkan subhimpunan dari \(\{0, \ldots, n\} \times \{0, \ldots, n\}\) yang terdiri atas pasangan \((i, j)\) dengan \(i < j\). Jika pasangan-pasangan ini dipandang sebagai titik kisi pada bidang koordinat, semuanya membentuk segitiga atas dari persegi yang bersudut \((0, 0)\) dan \((n, n)\), tanpa menyertakan diagonalnya. Kardinalitas persegi penuh adalah \((n + 1)^2\). Setelah ukuran diagonal dikurangkan dan hasilnya dibagi dua, diperoleh kardinalitas segitiga \(n (n + 1) / 2\).

Sebagai cara lain, perhatikan bahwa baris-baris segitiga tersebut berukuran \(0, 1, \ldots, n\), sehingga kardinalitasnya adalah jumlah \(n\) bilangan bulat positif pertama. Pernyataan have pertama dalam pembuktian di bawah menggambarkan segitiga sebagai gabungan baris-barisnya; baris \(j\) terdiri atas bilangan \(0, 1, ..., j - 1\) yang masing-masing dipasangkan dengan \(j\). Dalam pembuktian di bawah, notasi (., j) menyingkat fungsi fun i ↦ (i, j). Selebihnya hanyalah penghitungan kardinalitas finset.

def triangle (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range (n+1) ×ˢ range (n+1) | p.1 < p.2}

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n = (range (n+1)).biUnion (fun j ↦ (range j).image (., j)) := by
    ext p
    simp only [triangle, mem_filter, mem_product, mem_range, mem_biUnion, mem_image]
    constructor
    . rintro ⟨⟨hp1, hp2⟩, hp3⟩
      use p.2, hp2, p.1, hp3
    . rintro ⟨p1, hp1, p2, hp2, rfl⟩
      omega
  rw [this, card_biUnion]; swap
  · -- tangani dahulu sifat saling lepas
    intro x _ y _ xney
    simp [disjoint_iff_ne, xney]
  -- lanjutkan penghitungan
  transitivity (∑ i ∈ range (n + 1), i)
  · congr; ext i
    rw [card_image_of_injective, card_range]
    intros i1 i2; simp
  rw [sum_range_id]; rfl

Variasi pembuktian berikut melakukan penghitungan dengan fintype, bukan finset. Tipe α ≃ β adalah tipe ekuivalensi antara α dan β. Sebuah ekuivalensi terdiri atas pemetaan maju, pemetaan balik, serta bukti bahwa keduanya saling invers. Pernyataan have pertama dalam pembuktian menunjukkan bahwa triangle n ekuivalen dengan gabungan saling lepas dari Fin i ketika i berkisar pada Fin (n + 1). Menariknya, fungsi maju dan fungsi balik dibangun dengan taktik, bukan ditulis secara eksplisit. Karena kedua fungsi tersebut hanya memindahkan data dan informasi, rfl membuktikan bahwa keduanya saling invers.

Setelah itu, rw [←Fintype.card_coe] menulis ulang #(triangle n) sebagai kardinalitas subtipe { x // x ∈ triangle n }, dan selebihnya merupakan penghitungan.

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n ≃ Σ i : Fin (n + 1), Fin i.val :=
    { toFun := by
        rintro ⟨⟨i, j⟩, hp⟩
        have : (i ≤ n ∧ j ≤ n) ∧ i < j := by simpa [triangle] using hp
        exact ⟨⟨j, by linarith⟩, ⟨i, by linarith⟩⟩
      invFun := by
        rintro ⟨i, j⟩
        use ⟨j, i⟩
        suffices j ≤ n ∧ i ≤ n by simpa [triangle]
        constructor <;> linarith [i.2, j.2]
      left_inv := by intro i; rfl
      right_inv := by intro i; rfl }
  rw [←Fintype.card_coe]
  trans; apply (Fintype.card_congr this)
  rw [Fintype.card_sigma, sum_fin_eq_sum_range]
  convert Finset.sum_range_id (n + 1)
  simp_all

Berikut pendekatan lain lagi. Baris pertama pembuktian di bawah mereduksi masalah menjadi pembuktian 2 * #(triangle n) = (n + 1) * n. Kita dapat melakukannya dengan menunjukkan bahwa dua salinan segitiga tersebut tepat mengisi persegi panjang range n ×ˢ range (n + 1). Sebagai latihan, cobalah melengkapi langkah-langkah penghitungan tersebut. Dalam solusi, kita banyak mengandalkan omega pada langkah kedua dari belakang, tetapi tetap perlu mengerjakan cukup banyak bagian secara manual.

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  apply Nat.eq_div_of_mul_eq_right (by norm_num)
  let turn (p : ℕ × ℕ) : ℕ × ℕ := (n - 1 - p.1, n - p.2)
  calc 2 * #(triangle n)
      = #(triangle n) + #(triangle n) := by
          sorry
    _ = #(triangle n) + #(triangle n |>.image turn) := by
          sorry
    _ = #(range n ×ˢ range (n + 1)) := by
          sorry
    _ = (n + 1) * n := by
          sorry

Anda dapat meyakinkan diri bahwa kita memperoleh segitiga yang sama, hanya digeser ke bawah, jika dalam definisi triangle kedua kemunculan range (n + 1) diganti dengan range n dan < diganti dengan ≤. Latihan di bawah meminta Anda menggunakan fakta ini untuk menunjukkan bahwa kedua segitiga tersebut berukuran sama.

def triangle' (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range n ×ˢ range n | p.1 ≤ p.2}

example (n : ℕ) : #(triangle' n) = #(triangle n) := by sorry

Mari menutup bagian ini dengan sebuah contoh dan latihan dari tutorial tentang kombinatorika yang disampaikan Bhavik Mehta dalam Lean for the Curious Mathematician pada tahun 2023. Misalkan kita memiliki graf bipartit dengan himpunan simpul s dan t. Untuk setiap a dalam s, sekurang-kurangnya tiga sisi keluar dari a, sedangkan untuk setiap b dalam t, paling banyak satu sisi masuk ke b. Dengan demikian, jumlah sisi dalam graf sekurang-kurangnya tiga kali kardinalitas s dan paling banyak kardinalitas t. Akibatnya, tiga kali kardinalitas s tidak lebih besar daripada kardinalitas t. Teorema berikut menerapkan argumen ini dengan relasi r sebagai representasi sisi-sisi graf. Pembuktiannya merupakan penghitungan yang elegan.

open Classical
variable (s t : Finset ℕ) (a b : ℕ)

theorem doubleCounting {α β : Type*} (s : Finset α) (t : Finset β)
    (r : α → β → Prop)
    (h_left : ∀ a ∈ s, 3 ≤ #{b ∈ t | r a b})
    (h_right : ∀ b ∈ t, #{a ∈ s | r a b} ≤ 1) :
    3 * #(s) ≤ #(t) := by
  calc 3 * #(s)
      = ∑ a ∈ s, 3                               := by simp [mul_comm]
    _ ≤ ∑ a ∈ s, #({b ∈ t | r a b})              := sum_le_sum h_left
    _ = ∑ a ∈ s, ∑ b ∈ t, if r a b then 1 else 0 := by simp
    _ = ∑ b ∈ t, ∑ a ∈ s, if r a b then 1 else 0 := sum_comm
    _ = ∑ b ∈ t, #({a ∈ s | r a b})              := by simp
    _ ≤ ∑ b ∈ t, 1                               := sum_le_sum h_right
    _ ≤ #(t)                                     := by simp

Latihan berikut juga diambil dari tutorial Mehta. Misalkan A merupakan subhimpunan dari range (2 * n) dengan n + 1 elemen. Mudah dilihat bahwa A pasti memuat dua bilangan bulat berurutan, sehingga memuat dua elemen yang saling prima. Jika Anda menonton tutorial tersebut, Anda akan melihat bahwa cukup banyak usaha dihabiskan untuk membuktikan fakta berikut, yang kini dibuktikan secara otomatis oleh omega.

example (m k : ℕ) (h : m ≠ k) (h' : m / 2 = k / 2) : m = k + 1 ∨ k = m + 1 := by omega

Solusi latihan Mehta menggunakan prinsip rumah merpati, dalam bentuk exists_lt_card_fiber_of_mul_lt_card_of_maps_to, untuk menunjukkan bahwa terdapat dua elemen berbeda m dan k dalam A sedemikian sehingga m / 2 = k / 2. Cobalah melengkapi pembenaran fakta tersebut, lalu gunakan hasilnya untuk menyelesaikan pembuktian.

example {n : ℕ} (A : Finset ℕ)
    (hA : #(A) = n + 1)
    (hA' : A ⊆ range (2 * n)) :
    ∃ m ∈ A, ∃ k ∈ A, Nat.Coprime m k := by
  have : ∃ t ∈ range n, 1 < #({u ∈ A | u / 2 = t}) := by
    apply exists_lt_card_fiber_of_mul_lt_card_of_maps_to
    · sorry
    · sorry
  rcases this with ⟨t, ht, ht'⟩
  simp only [one_lt_card, mem_filter] at ht'
  sorry

6.3. Tipe yang Didefinisikan secara Induktif

Landasan Lean memungkinkan kita mendefinisikan tipe induktif, yaitu tipe data yang instansnya dibangkitkan dari bawah ke atas. Sebagai contoh, tipe data List α yang berisi daftar elemen-elemen α dibangkitkan dengan memulai dari daftar kosong, nil, lalu menambahkan elemen satu demi satu ke bagian depan daftar. Di bawah ini kita akan mendefinisikan tipe pohon biner BinTree. Elemen-elemennya dibangkitkan dengan memulai dari pohon kosong, lalu membangun pohon baru dengan menautkan sebuah simpul baru pada dua pohon yang sudah ada.

Dalam Lean, kita dapat mendefinisikan tipe induktif yang objeknya tak berhingga, seperti pohon berfondasi baik dengan percabangan terhitung. Namun, definisi induktif berhingga lazim digunakan dalam matematika diskret, terutama dalam cabang-cabang yang berkaitan dengan ilmu komputer. Lean tidak hanya menyediakan sarana untuk mendefinisikan tipe semacam itu, tetapi juga prinsip induksi dan pendefinisian melalui rekursi. Sebagai contoh, tipe data List α didefinisikan secara induktif:

namespace MyListSpace

inductive List (α : Type*) where
  | nil  : List α
  | cons : α → List α → List α

end MyListSpace

Definisi induktif tersebut menyatakan bahwa setiap elemen List α adalah nil, yaitu daftar kosong, atau cons a as, dengan a sebuah elemen α dan as sebuah daftar elemen-elemen α. Nama lengkap konstruktornya adalah List.nil dan List.cons, tetapi Anda dapat menggunakan notasi yang lebih pendek ketika namespace List terbuka. Ketika namespace List tidak terbuka, Anda dapat menulis .nil dan .cons a as di mana pun Lean mengharapkan sebuah daftar; Lean akan menyisipkan kualifikasi List secara otomatis. Sepanjang bagian ini, kita akan menempatkan definisi sementara dalam namespace terpisah seperti MyListSpace agar tidak berbenturan dengan pustaka standar. Di luar namespace sementara tersebut, kita kembali menggunakan definisi pustaka standar.

Lean mendefinisikan notasi [] untuk nil dan :: untuk cons. Anda juga dapat menulis [a, b, c] untuk a :: b :: c :: []. Fungsi penambahan dan pemetaan didefinisikan secara rekursif sebagai berikut:

def append {α : Type*} : List α → List α → List α
  | [],      bs => bs
  | a :: as, bs => a :: append as bs

def map {α β : Type*} (f : α → β) : List α → List β
  | []      => []
  | a :: as => f a :: map f as

#eval append [1, 2, 3] [4, 5, 6]
#eval map (fun n => n^2) [1, 2, 3, 4, 5]

Perhatikan bahwa terdapat kasus dasar dan kasus rekursif. Pada masing-masing kasus, kedua klausa pendefinisi berlaku secara definisional:

theorem nil_append {α : Type*} (as : List α) : append [] as = as := rfl

theorem cons_append {α : Type*} (a : α) (as : List α) (bs : List α) :
    append (a :: as) bs = a :: append as bs := rfl

theorem map_nil {α β : Type*} (f : α → β) : map f [] = [] := rfl

theorem map_cons {α β : Type*} (f : α → β) (a : α) (as : List α) :
    map f (a :: as) = f a :: map f as := rfl

Fungsi append dan map telah didefinisikan dalam pustaka standar, dan append as bs dapat ditulis sebagai as ++ bs.

Lean memungkinkan Anda menulis pembuktian dengan induksi yang mengikuti struktur definisi.

variable {α β γ : Type*}
variable (as bs cs : List α)
variable (a b c : α)

open List

theorem append_nil : ∀ as : List α, as ++ [] = as
  | [] => rfl
  | a :: as => by rw [cons_append, append_nil as]

theorem map_map (f : α → β) (g : β → γ) :
    ∀ as : List α, map g (map f as) = map (g ∘ f) as
  | [] => rfl
  | a :: as => by rw [map_cons, map_cons, map_cons, map_map f g as]; rfl

Anda juga dapat menggunakan taktik induction'.

Tentu saja, teorema-teorema ini sudah tersedia dalam pustaka standar. Sebagai latihan, cobalah mendefinisikan fungsi reverse dalam namespace MyListSpace3 (agar tidak berbenturan dengan List.reverse dari pustaka standar) yang membalik urutan sebuah daftar. Anda dapat mengujinya dengan #eval reverse [1, 2, 3, 4, 5]. Definisi reverse yang paling langsung memerlukan waktu kuadratik, tetapi hal itu tidak perlu dikhawatirkan di sini. Anda dapat melompat ke definisi List.reverse dalam pustaka standar untuk melihat implementasi yang berjalan dalam waktu linear. Cobalah membuktikan reverse (as ++ bs) = reverse bs ++ reverse as dan reverse (reverse as) = as. Anda dapat menggunakan cons_append dan append_assoc, tetapi mungkin perlu merumuskan dan membuktikan beberapa lema bantu.

def reverse : List α → List α := sorry

theorem reverse_append (as bs : List α) : reverse (as ++ bs) = reverse bs ++ reverse as := by
  sorry

theorem reverse_reverse (as : List α) : reverse (reverse as) = as := by sorry

Sebagai contoh lain, perhatikan definisi induktif pohon biner berikut beserta fungsi untuk menghitung ukuran dan kedalaman suatu pohon biner.

inductive BinTree where
  | empty : BinTree
  | node  : BinTree → BinTree → BinTree

namespace BinTree

def size : BinTree → ℕ
  | empty    => 0
  | node l r => size l + size r + 1

def depth : BinTree → ℕ
  | empty    => 0
  | node l r => max (depth l) (depth r) + 1

Kita akan menghitung pohon biner kosong sebagai pohon biner berukuran 0 dan berkedalaman 0, karena konvensi ini memudahkan pembahasan. Dalam literatur, objek-objek dari tipe data ini kadang disebut pohon biner diperluas. Dengan menyertakan pohon kosong, misalnya, kita dapat mendefinisikan pohon node empty (node empty empty) yang terdiri atas sebuah simpul akar, subpohon kiri kosong, dan subpohon kanan yang hanya terdiri atas satu simpul.

Berikut sebuah pertidaksamaan penting yang menghubungkan ukuran dan kedalaman:

theorem size_le : ∀ t : BinTree, size t ≤ 2^depth t - 1
  | empty    => Nat.zero_le _
  | node l r => by
    simp only [depth, size]
    calc l.size + r.size + 1
      ≤ (2^l.depth - 1) + (2^r.depth - 1) + 1 := by
          gcongr <;> apply size_le
    _ ≤ (2 ^ max l.depth r.depth - 1) + (2 ^ max l.depth r.depth - 1) + 1 := by
          gcongr <;> simp
    _ ≤ 2 ^ (max l.depth r.depth + 1) - 1 := by
          have : 0 < 2 ^ max l.depth r.depth := by simp
          omega

Cobalah membuktikan pertidaksamaan berikut, yang sedikit lebih mudah. Ingat, jika Anda melakukan pembuktian dengan induksi seperti pada teorema sebelumnya, Anda harus menghapus := by.

theorem depth_le_size : ∀ t : BinTree, depth t ≤ size t := by sorry

Definisikan pula operasi flip pada pohon biner, yang secara rekursif menukar subpohon kiri dan kanan.

def flip : BinTree → BinTree := sorry

Jika definisi Anda benar, pembuktian berikut semestinya cukup dengan rfl.

example: flip  (node (node empty (node empty empty)) (node empty empty)) =
    node (node empty empty) (node (node empty empty) empty) := sorry

Buktikan pernyataan berikut:

theorem size_flip : ∀ t, size (flip t) = size t := by sorry

Kita menutup bagian ini dengan sedikit logika formal. Berikut adalah definisi induktif formula proposisional.

inductive PropForm : Type where
  | var (n : ℕ)           : PropForm
  | fls                   : PropForm
  | conj (A B : PropForm) : PropForm
  | disj (A B : PropForm) : PropForm
  | impl (A B : PropForm) : PropForm

Setiap formula proposisional merupakan variabel var n, konstanta salah fls, atau formula majemuk berbentuk conj A B, disj A B, atau impl A B. Dalam notasi matematika biasa, semuanya lazim ditulis secara berturut-turut sebagai \(p_n\), \(\bot\), \(A \wedge B\), \(A \vee B\), dan \(A \to B\). Konektif proposisional lain dapat didefinisikan menggunakan konektif-konektif ini. Sebagai contoh, kita dapat mendefinisikan \(\neg A\) sebagai \(A \to \bot\) dan \(A \leftrightarrow B\) sebagai \((A \to B) \wedge (B \to A)\).

Setelah mendefinisikan tipe data formula proposisional, kita mendefinisikan arti mengevaluasi sebuah formula proposisional terhadap penetapan nilai kebenaran Boolean v pada variabel-variabelnya.

def eval : PropForm → (ℕ → Bool) → Bool
  | var n,    v => v n
  | fls,      _ => false
  | conj A B, v => A.eval v && B.eval v
  | disj A B, v => A.eval v || B.eval v
  | impl A B, v => ! A.eval v || B.eval v

Definisi berikut menentukan himpunan variabel yang muncul dalam suatu formula. Teorema sesudahnya menunjukkan bahwa mengevaluasi formula pada dua penetapan nilai kebenaran yang bersepakat pada variabel-variabel formula tersebut menghasilkan nilai yang sama.

def vars : PropForm → Finset ℕ
  | var n    => {n}
  | fls      => ∅
  | conj A B => A.vars ∪ B.vars
  | disj A B => A.vars ∪ B.vars
  | impl A B => A.vars ∪ B.vars

theorem eval_eq_eval : ∀ (A : PropForm) (v1 v2 : ℕ → Bool),
    (∀ n ∈ A.vars, v1 n = v2 n) → A.eval v1 = A.eval v2
  | var n, v1, v2, h    => by simp_all [vars, eval]
  | fls, v1, v2, h      => by simp_all [eval]
  | conj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | disj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | impl A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]

Dengan memperhatikan pengulangan tersebut, kita dapat memanfaatkan otomatisasi secara lebih cerdik.

theorem eval_eq_eval' (A : PropForm) (v1 v2 : ℕ → Bool) (h : ∀ n ∈ A.vars, v1 n = v2 n) :
    A.eval v1 = A.eval v2 := by
  cases A <;> simp_all [eval, vars, fun A => eval_eq_eval' A v1 v2]

Fungsi subst A m C menyatakan hasil penggantian setiap kemunculan variabel var m dalam formula A dengan formula C.

def subst : PropForm → ℕ → PropForm → PropForm
  | var n,    m, C => if n = m then C else var n
  | fls,      _, _ => fls
  | conj A B, m, C => conj (A.subst m C) (B.subst m C)
  | disj A B, m, C => disj (A.subst m C) (B.subst m C)
  | impl A B, m, C => impl (A.subst m C) (B.subst m C)

Sebagai contoh, tunjukkan bahwa mengganti variabel yang tidak muncul dalam suatu formula tidak mengubah formula tersebut:

theorem subst_eq_of_not_mem_vars :
    ∀ (A : PropForm) (n : ℕ) (C : PropForm), n ∉ A.vars → A.subst n C = A := sorry

Teorema berikut menyatakan sesuatu yang lebih halus dan menarik: mengevaluasi A.subst n C pada penetapan nilai kebenaran v sama dengan mengevaluasi A pada penetapan yang memberikan nilai C kepada var n. Cobalah membuktikannya.

theorem subst_eval_eq : ∀ (A : PropForm) (n : ℕ) (C : PropForm) (v : ℕ → Bool),
  (A.subst n C).eval v = A.eval (fun m => if m = n then C.eval v else v m) := sorry