3. Logika

Pada bab sebelumnya, kita membahas persamaan, pertidaksamaan, dan pernyataan matematika dasar seperti "\(x\) membagi \(y\)." Pernyataan matematika yang kompleks dibangun dari pernyataan-pernyataan sederhana semacam ini dengan menggunakan istilah logis seperti "dan", "atau", "tidak", "jika ... maka", "setiap", dan "ada". Dalam bab ini, kami menunjukkan cara bekerja dengan pernyataan yang dibangun dengan cara tersebut.

3.1. Implikasi dan Kuantor Universal

Perhatikan pernyataan setelah #check berikut:

#check ∀ x : ℝ, 0 ≤ x → |x| = x

Dengan kata-kata, kita akan mengatakan, "untuk setiap bilangan real x, jika 0 ≤ x, maka nilai mutlak x sama dengan x". Kita juga dapat memiliki pernyataan yang lebih rumit seperti:

#check ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε

Dengan kata-kata, kita akan mengatakan, "untuk setiap x, y, dan ε, jika 0 < ε ≤ 1, nilai mutlak x kurang dari ε, dan nilai mutlak y kurang dari ε, maka nilai mutlak x * y kurang dari ε." Di Lean, dalam suatu rangkaian implikasi terdapat tanda kurung implisit yang dikelompokkan ke kanan. Jadi, ekspresi di atas berarti "jika 0 < ε, maka jika ε ≤ 1, maka jika |x| < ε ..." Dengan demikian, ekspresi tersebut menyatakan bahwa semua asumsi secara bersama-sama mengimplikasikan kesimpulannya.

Anda telah melihat bahwa meskipun kuantor universal dalam pernyataan ini menjangkau objek-objek dan tanda panah implikasi memperkenalkan hipotesis, Lean memperlakukan keduanya dengan cara yang sangat mirip. Secara khusus, jika Anda telah membuktikan teorema berbentuk demikian, Anda dapat menerapkannya pada objek dan hipotesis dengan cara yang sama. Sebagai contoh, kita akan menggunakan pernyataan berikut, yang nanti akan kami bantu Anda buktikan:

theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
  sorry

section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)

#check my_lemma a b δ
#check my_lemma a b δ h₀ h₁
#check my_lemma a b δ h₀ h₁ ha hb

end

Anda juga telah melihat bahwa di Lean lazim digunakan kurung kurawal untuk menjadikan variabel terkuantifikasi bersifat implisit ketika variabel tersebut dapat disimpulkan dari hipotesis-hipotesis berikutnya. Dengan demikian, kita cukup menerapkan lema pada hipotesis tanpa menyebutkan objeknya.

theorem my_lemma2 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
  sorry

section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)

#check my_lemma2 h₀ h₁ ha hb

end

Pada tahap ini, Anda juga telah mengetahui bahwa jika Anda menggunakan taktik apply untuk menerapkan my_lemma pada sasaran berbentuk |a * b| < δ, Anda akan memperoleh sasaran-sasaran baru yang mengharuskan Anda membuktikan setiap hipotesis.

Untuk membuktikan pernyataan seperti ini, gunakan taktik intro. Perhatikan apa yang dilakukannya dalam contoh berikut:

theorem my_lemma3 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  sorry

Kita dapat memakai nama apa pun untuk variabel yang dikuantifikasi secara universal; namanya tidak harus x, y, dan ε. Perhatikan bahwa kita tetap harus memperkenalkan variabel tersebut meskipun ditandai sebagai implisit: menjadikannya implisit berarti kita tidak menuliskannya ketika menulis ekspresi yang menggunakan my_lemma, tetapi variabel itu tetap merupakan bagian penting dari pernyataan yang sedang kita buktikan. Setelah perintah intro, sasarannya sama dengan sasaran yang akan muncul sejak awal seandainya kita mencantumkan semua variabel dan hipotesis sebelum titik dua, seperti yang kita lakukan pada seksi terakhir. Sebentar lagi kita akan melihat mengapa kadang-kadang variabel dan hipotesis perlu diperkenalkan setelah pembuktian dimulai.

Untuk membantu Anda membuktikan lema tersebut, kami berikan awalnya:

theorem my_lemma4 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  calc
    |x * y| = |x| * |y| := sorry
    _ ≤ |x| * ε := sorry
    _ < 1 * ε := sorry
    _ = ε := sorry

Selesaikan pembuktian menggunakan teorema abs_mul, mul_le_mul, abs_nonneg, mul_lt_mul_of_pos_right, dan one_mul. Ingat bahwa Anda dapat menemukan teorema-teorema seperti ini dengan pelengkapan Ctrl-spasi (atau Cmd-spasi pada Mac). Ingat pula bahwa Anda dapat menggunakan .mp dan .mpr atau .1 dan .2 untuk mengambil kedua arah dari suatu pernyataan jika-dan-hanya-jika.

Kuantor universal sering tersembunyi di dalam definisi, dan Lean akan menguraikan definisi untuk menampakkannya bila diperlukan. Sebagai contoh, mari kita definisikan dua predikat, FnUb f a dan FnLb f a, dengan f sebagai fungsi dari bilangan real ke bilangan real dan a sebagai bilangan real. Predikat pertama menyatakan bahwa a adalah batas atas bagi nilai-nilai f, sedangkan predikat kedua menyatakan bahwa a adalah batas bawah bagi nilai-nilai f.

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

Dalam contoh berikut, fun x ↦ f x + g x adalah fungsi yang memetakan x ke f x + g x. Dalam teori tipe, proses beralih dari ekspresi f x + g x ke fungsi ini disebut abstraksi lambda.

example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by
  intro x
  dsimp
  apply add_le_add
  apply hfa
  apply hgb

Menerapkan intro pada sasaran FnUb (fun x ↦ f x + g x) (a + b) memaksa Lean menguraikan definisi FnUb dan memperkenalkan x untuk kuantor universal. Sasarannya kemudian menjadi (fun (x : ℝ) ↦ f x + g x) x ≤ a + b. Namun, penerapan (fun x ↦ f x + g x) pada x semestinya menghasilkan f x + g x, dan perintah dsimp melakukan penyederhanaan tersebut. (Huruf "d" merupakan singkatan dari "definitional" atau "definisional".) Anda dapat menghapus perintah itu dan pembuktiannya tetap berfungsi; Lean memang harus melakukan kontraksi tersebut agar dapat memahami perintah apply berikutnya. Perintah dsimp sekadar membuat sasaran lebih mudah dibaca dan membantu kita menentukan langkah selanjutnya. Pilihan lain ialah menggunakan taktik change dengan menulis change f x + g x ≤ a + b. Ini membantu membuat pembuktian lebih mudah dibaca dan memberi Anda kendali lebih besar atas cara sasaran ditransformasikan.

Bagian pembuktian selanjutnya bersifat rutin. Dua perintah apply terakhir memaksa Lean menguraikan definisi FnUb dalam hipotesis. Cobalah menyusun pembuktian serupa untuk pernyataan berikut:

example (hfa : FnLb f a) (hgb : FnLb g b) : FnLb (fun x ↦ f x + g x) (a + b) :=
  sorry

example (nnf : FnLb f 0) (nng : FnLb g 0) : FnLb (fun x ↦ f x * g x) 0 :=
  sorry

example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
    FnUb (fun x ↦ f x * g x) (a * b) :=
  sorry

Meskipun kita telah mendefinisikan FnUb dan FnLb untuk fungsi dari bilangan real ke bilangan real, Anda perlu menyadari bahwa definisi dan pembuktian tersebut jauh lebih umum. Definisi itu masuk akal bagi fungsi di antara dua tipe apa pun yang kodomainnya memiliki suatu pengertian tentang tatanan. Pemeriksaan tipe teorema add_le_add menunjukkan bahwa teorema tersebut berlaku bagi setiap struktur monoid yang menghormati tatanan terkait; rincian maknanya belum penting untuk saat ini, tetapi perlu diketahui bahwa bilangan asli, bulat, rasional, dan real semuanya merupakan instansnya. Jadi, jika kita membuktikan teorema fnUb_add pada tingkat keumuman itu, teorema tersebut akan berlaku pada semua instans ini.

variable {α : Type*} {R : Type*} [AddCommMonoid R] [PartialOrder R] [IsOrderedCancelAddMonoid R]

#check add_le_add

def FnUb' (f : α → R) (a : R) : Prop :=
  ∀ x, f x ≤ a

theorem fnUb_add {f g : α → R} {a b : R} (hfa : FnUb' f a) (hgb : FnUb' g b) :
    FnUb' (fun x ↦ f x + g x) (a + b) := fun x ↦ add_le_add (hfa x) (hgb x)

Anda telah melihat kurung siku seperti ini dalam Seksi Bab 2.2, meskipun kita masih belum menjelaskan maknanya. Agar konkret, kita akan tetap menggunakan bilangan real dalam sebagian besar contoh, tetapi perlu diketahui bahwa Mathlib memuat definisi dan teorema yang bekerja pada tingkat keumuman tinggi.

Sebagai contoh lain kuantor universal yang tersembunyi, Mathlib mendefinisikan predikat Monotone, yang menyatakan bahwa suatu fungsi tak menurun terhadap argumennya:

example (f : ℝ → ℝ) (h : Monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b :=
  @h

Sifat Monotone f didefinisikan persis sebagai ekspresi setelah titik dua. Kita perlu meletakkan simbol @ sebelum h karena, jika tidak, Lean akan mengembangkan argumen implisit untuk h dan menyisipkan tempat kosong.

Membuktikan pernyataan tentang kemonotonan melibatkan penggunaan intro untuk memperkenalkan dua variabel, misalnya a dan b, serta hipotesis a ≤ b. Untuk menggunakan hipotesis kemonotonan, Anda dapat menerapkannya pada argumen dan hipotesis yang sesuai, lalu menerapkan ekspresi yang dihasilkan pada sasaran. Atau, Anda dapat menerapkannya pada sasaran dan membiarkan Lean membantu Anda bekerja mundur dengan menampilkan hipotesis yang masih diperlukan sebagai subsasaran baru.

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := by
  intro a b aleb
  apply add_le_add
  apply mf aleb
  apply mg aleb

Jika suatu pembuktian sesingkat ini, sering kali lebih mudah memberikan suku bukti sebagai gantinya. Untuk mendeskripsikan pembuktian yang untuk sementara memperkenalkan objek a dan b serta hipotesis aleb, Lean menggunakan notasi fun a b aleb ↦ .... Ini serupa dengan cara ekspresi seperti fun x ↦ x^2 mendeskripsikan suatu fungsi dengan memberi nama sementara pada objek x, lalu menggunakannya untuk mendeskripsikan suatu nilai. Jadi, perintah intro dalam pembuktian sebelumnya berkorespondensi dengan abstraksi lambda dalam suku bukti berikutnya. Perintah-perintah apply kemudian berkorespondensi dengan penyusunan penerapan teorema pada argumen-argumennya.

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x :=
  fun _a _b aleb ↦ add_le_add (mf aleb) (mg aleb)

Berikut sebuah trik yang berguna: jika Anda mulai menulis suku bukti fun a b aleb ↦ _ dengan memakai garis bawah pada tempat yang seharusnya berisi sisa ekspresi, Lean akan menandai kesalahan untuk menunjukkan bahwa ia tidak dapat menebak nilai ekspresi tersebut. Jika Anda memeriksa jendela Lean InfoView di VS Code atau mengarahkan penunjuk ke penanda kesalahan bergelombang, Lean akan menunjukkan sasaran yang harus diselesaikan oleh ekspresi yang tersisa.

Anda akan melihat Lean mencetak peringatan tentang pembuktian di atas, yang menyatakan bahwa a dan b tidak digunakan dalam badan fungsi. Ini merupakan mekanisme umum yang, misalnya, berguna untuk menghindari asumsi yang tidak diperlukan dalam suatu teorema. Dalam contoh ini, peringatan tersebut tidak benar-benar memberi informasi yang berguna. Kita dapat menonaktifkannya sampai akhir seksi saat ini dengan menulis set_option linter.unusedVariables false, atau hanya untuk contoh tersebut dengan menulis set_option linter.unusedVariables false in di atas contoh.

Kita juga dapat mengganti a dan b dengan garis bawah untuk memberi tahu Lean bahwa kita tidak ingin menamainya. Lean kemudian akan memakai nama tak terakses yang dibuat secara otomatis, seperti x✝. Sebagai alternatif, kita dapat mengawali nama dengan garis bawah untuk memberi tahu Lean bahwa kita tidak bermaksud menggunakannya.

Cobalah membuktikan contoh-contoh berikut, baik dengan taktik maupun suku bukti:

example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=
  sorry

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) :=
  sorry

Berikut beberapa contoh lainnya. Suatu fungsi \(f\) dari \(\Bbb R\) ke \(\Bbb R\) disebut genap jika \(f(-x) = f(x)\) untuk setiap \(x\), dan disebut ganjil jika \(f(-x) = -f(x)\) untuk setiap \(x\). Contoh berikut mendefinisikan kedua gagasan tersebut secara formal dan membuktikan satu fakta mengenainya. Anda dapat melengkapi pembuktian fakta-fakta lainnya.

def FnEven (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

def FnOdd (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = -f (-x)

example (ef : FnEven f) (eg : FnEven g) : FnEven fun x ↦ f x + g x := by
  intro x
  calc
    (fun x ↦ f x + g x) x = f x + g x := rfl
    _ = f (-x) + g (-x) := by rw [ef, eg]


example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnOdd fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by
  sorry

Pembuktian pertama dapat dipersingkat dengan menggunakan dsimp atau change untuk menghilangkan abstraksi lambda. Namun, Anda dapat memeriksa bahwa rw berikutnya tidak akan berfungsi kecuali kita menghilangkan abstraksi lambda secara eksplisit, karena jika tidak, ia tidak dapat menemukan pola f x dan g x dalam ekspresi. Berbeda dengan beberapa taktik lain, rw bekerja pada tingkat sintaksis; ia tidak akan menguraikan definisi atau menerapkan reduksi untuk Anda (terdapat varian bernama erw yang berusaha sedikit lebih keras ke arah ini, tetapi tidak jauh lebih keras).

Kuantor universal implisit dapat ditemukan di mana-mana setelah Anda mengetahui cara mengenalinya.

Mathlib memuat pustaka yang baik untuk memanipulasi himpunan. Ingat bahwa Lean tidak memakai landasan yang berbasis teori himpunan; jadi, kata himpunan di sini memiliki makna biasa sebagai kumpulan objek matematika dari suatu tipe α. Jika x bertipe α dan s bertipe Set α, maka x ∈ s adalah proposisi yang menyatakan bahwa x merupakan anggota s. Jika y memiliki tipe lain β, maka ekspresi y ∈ s tidak bermakna. Di sini, "tidak bermakna" berarti "tidak memiliki tipe sehingga Lean tidak menerimanya sebagai pernyataan yang terbentuk dengan baik". Hal ini berbeda, misalnya, dari teori himpunan Zermelo--Fraenkel, tempat a ∈ b merupakan pernyataan yang terbentuk dengan baik untuk sembarang dua objek matematika a dan b. Sebagai contoh, sin ∈ cos merupakan pernyataan yang terbentuk dengan baik dalam ZF. Kelemahan landasan teori himpunan ini menjadi salah satu alasan penting untuk tidak memakainya dalam asisten pembuktian yang dimaksudkan untuk membantu kita mendeteksi ekspresi tanpa makna. Di Lean, sin bertipe ℝ → ℝ dan cos bertipe ℝ → ℝ, yang tidak sama dengan Set (ℝ → ℝ) bahkan setelah definisi diuraikan; karena itu, pernyataan sin ∈ cos tidak bermakna. Lean juga dapat digunakan untuk mengerjakan teori himpunan itu sendiri. Sebagai contoh, independensi hipotesis kontinuum dari aksioma Zermelo--Fraenkel telah diformalkan di Lean. Namun, metateori teori himpunan semacam itu sepenuhnya berada di luar ruang lingkup buku ini.

Jika s dan t bertipe Set α, maka relasi himpunan bagian s ⊆ t didefinisikan sebagai ∀ {x : α}, x ∈ s → x ∈ t. Variabel dalam kuantor ditandai implisit sehingga, dengan h : s ⊆ t dan h' : x ∈ s, kita dapat menulis h h' sebagai pembenaran untuk x ∈ t. Contoh berikut memberikan pembuktian taktik dan suku bukti yang membenarkan refleksivitas relasi himpunan bagian, lalu meminta Anda melakukan hal yang sama untuk transitivitas.

variable {α : Type*} (r s t : Set α)

example : s ⊆ s := by
  intro x xs
  exact xs

theorem Subset.refl : s ⊆ s := fun _x xs ↦ xs

theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
  sorry

Sebagaimana kita mendefinisikan FnUb untuk fungsi, kita dapat mendefinisikan SetUb s a untuk menyatakan bahwa a adalah batas atas himpunan s, dengan asumsi bahwa s merupakan himpunan elemen dari suatu tipe yang dilengkapi tatanan. Dalam contoh berikut, Anda diminta membuktikan bahwa jika a merupakan batas bagi s dan a ≤ b, maka b juga merupakan batas bagi s.

variable {α : Type*} [PartialOrder α]
variable (s : Set α) (a b : α)

def SetUb (s : Set α) (a : α) :=
  ∀ x, x ∈ s → x ≤ a

example (h : SetUb s a) (h' : a ≤ b) : SetUb s b :=
  sorry

Kita menutup seksi ini dengan satu contoh penting terakhir. Suatu fungsi \(f\) disebut injektif jika, untuk setiap \(x_1\) dan \(x_2\), jika \(f(x_1) = f(x_2)\), maka \(x_1 = x_2\). Mathlib mendefinisikan Function.Injective f dengan x₁ dan x₂ sebagai variabel implisit. Contoh berikut menunjukkan bahwa, pada bilangan real, setiap fungsi yang menambahkan suatu konstanta bersifat injektif. Kemudian Anda diminta menunjukkan bahwa perkalian dengan konstanta tak nol juga bersifat injektif, dengan menggunakan nama lema dalam contoh sebagai sumber inspirasi. Ingatlah untuk memakai pelengkapan Ctrl-spasi setelah menebak awal nama lema.

open Function

example (c : ℝ) : Injective fun x ↦ x + c := by
  intro x₁ x₂ h'
  exact (add_left_inj c).mp h'

example {c : ℝ} (h : c ≠ 0) : Injective fun x ↦ c * x := by
  sorry

Terakhir, tunjukkan bahwa komposisi dua fungsi injektif juga bersifat injektif:

variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}

example (injg : Injective g) (injf : Injective f) : Injective fun x ↦ g (f x) := by
  sorry

3.2. Kuantor Eksistensial

Kuantor eksistensial, yang dapat dimasukkan sebagai \ex di VS Code, digunakan untuk menyatakan frasa "terdapat". Ekspresi formal ∃ x : ℝ, 2 < x ∧ x < 3 di Lean menyatakan bahwa terdapat bilangan real di antara 2 dan 3. (Kita akan membahas simbol konjungsi, ∧, dalam Bab 3.4.) Cara baku untuk membuktikan pernyataan seperti itu ialah menunjukkan suatu bilangan real dan membuktikan bahwa bilangan tersebut memiliki sifat yang dinyatakan. Bilangan 2,5, yang dapat kita masukkan sebagai 5 / 2 atau (5 : ℝ) / 2 ketika Lean tidak dapat menyimpulkan dari konteks bahwa yang kita maksud adalah bilangan real, memiliki sifat yang diperlukan, dan taktik norm_num dapat membuktikan bahwa bilangan itu memenuhi deskripsinya.

Ada beberapa cara untuk merangkai informasi tersebut. Jika diberikan sasaran yang diawali kuantor eksistensial, taktik use digunakan untuk memberikan objeknya, sehingga tersisa sasaran untuk membuktikan sifatnya.

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  use 5 / 2
  norm_num

Taktik use dapat menerima bukti sekaligus data:

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h1 : 2 < (5 : ℝ) / 2 := by norm_num
  have h2 : (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2, h1, h2

Sebenarnya, taktik use juga secara otomatis mencoba memakai asumsi yang tersedia.

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2

Sebagai alternatif, kita dapat memakai notasi konstruktor anonim Lean untuk menyusun bukti bagi suatu pernyataan berkuantor eksistensial.

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
  ⟨5 / 2, h⟩

Perhatikan bahwa tidak ada by; di sini kita memberikan suku bukti eksplisit. Kurung sudut kiri dan kanan, yang masing-masing dapat dimasukkan sebagai \< dan \>, meminta Lean merangkai data yang diberikan dengan konstruksi apa pun yang sesuai untuk sasaran saat ini. Kita dapat memakai notasi ini tanpa terlebih dahulu memasuki mode taktik:

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
  ⟨5 / 2, by norm_num⟩

Sekarang kita mengetahui cara membuktikan pernyataan eksistensial. Namun, bagaimana cara menggunakannya? Jika kita mengetahui bahwa terdapat objek dengan suatu sifat tertentu, kita semestinya dapat memberi nama pada sembarang objek tersebut dan menalar mengenainya. Sebagai contoh, ingat kembali predikat FnUb f a dan FnLb f a dari seksi sebelumnya, yang masing-masing menyatakan bahwa a adalah batas atas atau batas bawah bagi f. Kita dapat memakai kuantor eksistensial untuk menyatakan bahwa "f terbatas" tanpa menentukan batasnya:

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

def FnHasUb (f : ℝ → ℝ) :=
  ∃ a, FnUb f a

def FnHasLb (f : ℝ → ℝ) :=
  ∃ a, FnLb f a

Kita dapat memakai teorema fnUb_add dari seksi sebelumnya untuk membuktikan bahwa jika f dan g memiliki batas atas, maka fun x ↦ f x + g x juga memilikinya.

variable {f g : ℝ → ℝ}

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  rcases ubf with ⟨a, ubfa⟩
  rcases ubg with ⟨b, ubgb⟩
  use a + b
  apply fnUb_add ubfa ubgb

Taktik rcases menguraikan informasi dalam kuantor eksistensial. Anotasi seperti ⟨a, ubfa⟩, yang ditulis dengan kurung sudut yang sama seperti konstruktor anonim, disebut pola dan mendeskripsikan informasi yang kita harapkan ketika menguraikan argumen utama. Jika diberikan hipotesis ubf bahwa terdapat batas atas bagi f, rcases ubf with ⟨a, ubfa⟩ menambahkan variabel baru a sebagai suatu batas atas ke dalam konteks, bersama hipotesis ubfa bahwa batas tersebut memiliki sifat yang dinyatakan. Sasaran tidak berubah; yang berubah ialah kini kita dapat memakai objek baru dan hipotesis baru tersebut untuk membuktikan sasaran. Ini merupakan cara penalaran yang umum dalam matematika: kita menguraikan objek yang keberadaannya dinyatakan atau diimplikasikan oleh suatu hipotesis, lalu memakainya untuk membuktikan keberadaan sesuatu yang lain.

Cobalah memakai cara ini untuk membuktikan pernyataan berikut. Mungkin akan berguna jika beberapa contoh dari seksi sebelumnya diubah menjadi teorema bernama, seperti yang kita lakukan dengan fnUb_add, atau Anda dapat memasukkan argumennya secara langsung ke dalam pembuktian.

example (lbf : FnHasLb f) (lbg : FnHasLb g) : FnHasLb fun x ↦ f x + g x := by
  sorry

example {c : ℝ} (ubf : FnHasUb f) (h : c ≥ 0) : FnHasUb fun x ↦ c * f x := by
  sorry

Huruf "r" dalam rcases merupakan singkatan dari "recursive" atau "rekursif", karena taktik ini memungkinkan kita memakai pola serumit apa pun untuk menguraikan data bersarang. Taktik rintro merupakan gabungan intro dan rcases:

example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
  rintro ⟨a, ubfa⟩ ⟨b, ubgb⟩
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

Lean juga mendukung fungsi dengan pencocokan pola dalam ekspresi dan suku bukti:

example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x :=
  fun ⟨a, ubfa⟩ ⟨b, ubgb⟩ ↦ ⟨a + b, fnUb_add ubfa ubgb⟩

Tugas menguraikan informasi dalam suatu hipotesis begitu penting sehingga Lean dan Mathlib menyediakan sejumlah cara untuk melakukannya. Sebagai contoh, taktik obtain menyediakan sintaks yang jelas:

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  obtain ⟨a, ubfa⟩ := ubf
  obtain ⟨b, ubgb⟩ := ubg
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

Anggap instruksi obtain pertama mencocokkan "isi" ubf dengan pola yang diberikan, lalu menetapkan setiap komponennya kepada variabel bernama. rcases dan obtain dikatakan melakukan destruct pada argumennya.

Lean juga mendukung sintaks yang serupa dengan sintaks dalam bahasa pemrograman fungsional lain:

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  cases ubf
  case intro a ubfa =>
    cases ubg
    case intro b ubgb =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  cases ubf
  next a ubfa =>
    cases ubg
    next b ubgb =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  match ubf, ubg with
    | ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x :=
  match ubf, ubg with
    | ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
      ⟨a + b, fnUb_add ubfa ubgb⟩

Dalam contoh pertama, jika Anda meletakkan kursor setelah cases ubf, Anda akan melihat bahwa taktik tersebut menghasilkan satu sasaran yang diberi label intro oleh Lean. (Nama khusus ini berasal dari nama internal bagi primitif aksiomatik yang menyusun bukti pernyataan eksistensial.) Taktik case kemudian memberi nama pada komponen-komponennya. Contoh kedua serupa, hanya saja penggunaan next alih-alih case membuat Anda tidak perlu menyebutkan intro. Kata match dalam dua contoh terakhir menegaskan bahwa yang kita lakukan di sini adalah apa yang oleh ilmuwan komputer disebut "pencocokan pola". Perhatikan bahwa pembuktian ketiga diawali dengan by; setelah itu, versi taktik dari match mengharapkan bukti taktis di sebelah kanan tanda panah. Contoh terakhir merupakan suku bukti: tidak ada taktik yang digunakan.

Dalam bagian selanjutnya dari buku ini, kita akan tetap memakai rcases, rintro, dan obtain sebagai cara yang diutamakan untuk menggunakan kuantor eksistensial. Namun, tidak ada salahnya melihat sintaks alternatif, terutama jika kelak Anda berada di antara para ilmuwan komputer.

Untuk menggambarkan salah satu cara menggunakan rcases, kita membuktikan suatu fakta matematika klasik: jika dua bilangan bulat x dan y masing-masing dapat ditulis sebagai jumlah dua kuadrat, maka hasil kalinya, x * y, juga dapat ditulis demikian. Sebenarnya, pernyataan ini berlaku bagi setiap gelanggang komutatif, bukan hanya bilangan bulat. Dalam contoh berikut, rcases menguraikan dua kuantor eksistensial sekaligus. Kemudian kita memberikan nilai-nilai khusus yang diperlukan untuk menyatakan x * y sebagai jumlah kuadrat dalam bentuk daftar argumen bagi pernyataan use, lalu menggunakan ring untuk memverifikasi bahwa nilai tersebut berfungsi.

variable {α : Type*} [CommRing α]

def SumOfSquares (x : α) :=
  ∃ a b, x = a ^ 2 + b ^ 2

theorem sumOfSquares_mul {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
    SumOfSquares (x * y) := by
  rcases sosx with ⟨a, b, xeq⟩
  rcases sosy with ⟨c, d, yeq⟩
  rw [xeq, yeq]
  use a * c - b * d, a * d + b * c
  ring

Pembuktian ini tidak memberikan banyak wawasan, tetapi berikut salah satu cara untuk memotivasinya. Suatu bilangan bulat Gaussian adalah bilangan berbentuk \(a + bi\), dengan \(a\) dan \(b\) bilangan bulat serta \(i = \sqrt{-1}\). Menurut definisi, norma bilangan bulat Gaussian \(a + bi\) adalah \(a^2 + b^2\). Jadi, norma suatu bilangan bulat Gaussian merupakan jumlah kuadrat, dan setiap jumlah kuadrat dapat dinyatakan dengan cara ini. Teorema di atas mencerminkan fakta bahwa norma hasil kali bilangan bulat Gaussian sama dengan hasil kali norma-normanya: jika \(x\) adalah norma \(a + bi\) dan \(y\) adalah norma \(c + di\), maka \(xy\) adalah norma \((a + bi) (c + di)\). Pembuktian kita yang sukar dipahami menggambarkan bahwa pembuktian yang paling mudah diformalkan tidak selalu merupakan pembuktian yang paling mudah dipahami. Dalam Bab 7.3, kami akan membekali Anda dengan sarana untuk mendefinisikan bilangan bulat Gaussian dan menggunakannya guna memberikan pembuktian alternatif.

Penguraian suatu persamaan di dalam kuantor eksistensial, lalu pemakaiannya untuk menulis ulang ekspresi dalam sasaran, merupakan pola yang sering muncul. Karena itu, taktik rcases menyediakan suatu singkatan: jika Anda memakai kata kunci rfl sebagai pengganti pengidentifikasi baru, rcases melakukan penulisan ulang secara otomatis (trik ini tidak berfungsi dengan lambda pencocokan pola).

theorem sumOfSquares_mul' {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
    SumOfSquares (x * y) := by
  rcases sosx with ⟨a, b, rfl⟩
  rcases sosy with ⟨c, d, rfl⟩
  use a * c - b * d, a * d + b * c
  ring

Seperti kuantor universal, kuantor eksistensial dapat ditemukan tersembunyi di mana-mana jika Anda mengetahui cara mengenalinya. Sebagai contoh, keterbagian secara implisit merupakan pernyataan "terdapat".

example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
  rcases divab with ⟨d, beq⟩
  rcases divbc with ⟨e, ceq⟩
  rw [ceq, beq]
  use d * e; ring

Sekali lagi, ini menyediakan konteks yang baik untuk memakai rcases bersama rfl. Cobalah dalam pembuktian di atas. Hasilnya terasa memuaskan!

Kemudian, cobalah membuktikan pernyataan berikut:

example (divab : a ∣ b) (divac : a ∣ c) : a ∣ b + c := by
  sorry

Sebagai contoh penting lainnya, suatu fungsi \(f : \alpha \to \beta\) disebut surjektif jika untuk setiap \(y\) dalam kodomain \(\beta\), terdapat \(x\) dalam domain \(\alpha\) sedemikian sehingga \(f(x) = y\). Perhatikan bahwa pernyataan ini memuat kuantor universal sekaligus kuantor eksistensial; hal ini menjelaskan mengapa contoh berikut memakai intro dan use.

example {c : ℝ} : Surjective fun x ↦ x + c := by
  intro y
  use y - c
  dsimp; ring

Cobalah sendiri contoh ini dengan memakai teorema mul_div_cancel₀:

example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
  sorry

Pada titik ini, perlu disebutkan bahwa terdapat taktik field_simp yang sering kali dapat menghilangkan penyebut dengan cara yang berguna. Taktik tersebut dapat digunakan bersama taktik ring.

example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by
  field_simp [h]
  ring

Contoh berikut menggunakan hipotesis surjektivitas dengan menerapkannya pada nilai yang sesuai. Perhatikan bahwa Anda dapat memakai rcases pada ekspresi apa pun, bukan hanya pada hipotesis.

example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
  rcases h 2 with ⟨x, hx⟩
  use x
  rw [hx]
  norm_num

Lihat apakah Anda dapat memakai cara-cara ini untuk menunjukkan bahwa komposisi fungsi-fungsi surjektif juga bersifat surjektif.

variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}

example (surjg : Surjective g) (surjf : Surjective f) : Surjective fun x ↦ g (f x) := by
  sorry

3.3. Negasi

Simbol ¬ dimaksudkan untuk menyatakan negasi; jadi, ¬ x < y menyatakan bahwa x tidak kurang dari y, ¬ x = y (atau, secara ekuivalen, x ≠ y) menyatakan bahwa x tidak sama dengan y, dan ¬ ∃ z, x < z ∧ z < y menyatakan bahwa tidak terdapat z yang berada secara ketat di antara x dan y. Di Lean, notasi ¬ A menyingkat A → False, yang dapat dipahami sebagai pernyataan bahwa A mengimplikasikan kontradiksi. Secara praktis, ini berarti Anda sudah mengetahui sebagian cara bekerja dengan negasi: Anda dapat membuktikan ¬ A dengan memperkenalkan hipotesis h : A dan membuktikan False; dan jika Anda memiliki h : ¬ A serta h' : A, menerapkan h pada h' menghasilkan False.

Sebagai ilustrasi, perhatikan prinsip irrefleksivitas lt_irrefl untuk suatu tatanan ketat, yang menyatakan bahwa ¬ a < a berlaku untuk setiap a. Prinsip asimetri lt_asymm menyatakan bahwa a < b → ¬ b < a. Mari kita tunjukkan bahwa lt_asymm mengikuti dari lt_irrefl.

example (h : a < b) : ¬b < a := by
  intro h'
  have : a < a := lt_trans h h'
  apply lt_irrefl a this

Contoh ini memperkenalkan beberapa trik baru. Pertama, ketika Anda memakai have tanpa memberikan label, Lean memakai nama this, yang menyediakan cara mudah untuk merujuknya kembali. Karena pembuktiannya sangat singkat, kita memberikan suku bukti eksplisit. Namun, hal yang benar-benar perlu Anda perhatikan dalam pembuktian ini adalah hasil taktik intro, yang menyisakan sasaran False, serta fakta bahwa pada akhirnya kita membuktikan False dengan menerapkan lt_irrefl pada bukti a < a.

Berikut contoh lain yang memakai predikat FnHasUb yang didefinisikan dalam seksi sebelumnya, yang menyatakan bahwa suatu fungsi memiliki batas atas.

example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
  intro fnub
  rcases fnub with ⟨a, fnuba⟩
  rcases h a with ⟨x, hx⟩
  have : f x ≤ a := fnuba x
  linarith

Ingat bahwa sering kali akan mudah memakai linarith ketika suatu sasaran mengikuti dari persamaan dan pertidaksamaan linear yang terdapat dalam konteks.

Lihat apakah Anda dapat membuktikan pernyataan berikut dengan cara serupa:

example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f :=
  sorry

example : ¬FnHasUb fun x ↦ x :=
  sorry

Mathlib menyediakan sejumlah teorema yang berguna untuk menghubungkan tatanan dan negasi:

#check (not_le_of_gt : a > b → ¬a ≤ b)
#check (not_lt_of_ge : a ≥ b → ¬a < b)
#check (lt_of_not_ge : ¬a ≥ b → a < b)
#check (le_of_not_gt : ¬a > b → a ≤ b)

Ingat kembali predikat Monotone f, yang menyatakan bahwa f tak menurun. Gunakan beberapa teorema yang baru saja dicantumkan untuk membuktikan berikut ini:

example (h : Monotone f) (h' : f a < f b) : a < b := by
  sorry

example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
  sorry

Kita dapat menunjukkan bahwa contoh pertama dalam cuplikan terakhir tidak dapat dibuktikan jika < diganti dengan ≤. Perhatikan bahwa kita dapat membuktikan negasi suatu pernyataan berkuantor universal dengan memberikan contoh tandingan. Lengkapi pembuktiannya.

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  let f := fun x : ℝ ↦ (0 : ℝ)
  have monof : Monotone f := by sorry
  have h' : f 1 ≤ f 0 := le_refl _
  sorry

Contoh ini memperkenalkan taktik let, yang menambahkan suatu definisi lokal ke dalam konteks. Jika Anda meletakkan kursor setelah perintah let, di jendela sasaran akan terlihat bahwa definisi f : ℝ → ℝ := fun x ↦ 0 telah ditambahkan ke dalam konteks. Lean akan mengembangkan definisi f bila diperlukan. Secara khusus, ketika kita membuktikan f 1 ≤ f 0 dengan le_refl, Lean mereduksi f 1 dan f 0 menjadi 0.

Gunakan le_of_not_gt untuk membuktikan berikut ini:

example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
  sorry

Banyak pembuktian yang baru saja kita lakukan menggunakan secara implisit fakta berikut. Untuk sembarang sifat P, menyatakan bahwa tidak ada objek yang memiliki sifat P sama artinya dengan menyatakan bahwa setiap objek tidak memiliki sifat P. Demikian pula, menyatakan bahwa tidak setiap objek memiliki sifat P ekuivalen dengan menyatakan bahwa terdapat objek yang tidak memiliki sifat P. Dengan kata lain, keempat implikasi berikut valid (tetapi salah satunya tidak dapat dibuktikan dengan apa yang telah kita jelaskan sejauh ini):

variable {α : Type*} (P : α → Prop) (Q : Prop)

example (h : ¬∃ x, P x) : ∀ x, ¬P x := by
  sorry

example (h : ∀ x, ¬P x) : ¬∃ x, P x := by
  sorry

example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
  sorry

example (h : ∃ x, ¬P x) : ¬∀ x, P x := by
  sorry

Implikasi pertama, kedua, dan keempat mudah dibuktikan dengan cara yang telah Anda lihat. Kami menganjurkan Anda untuk mencobanya. Namun, implikasi ketiga lebih sulit karena menyimpulkan keberadaan suatu objek dari fakta bahwa ketiadaan objek tersebut menghasilkan kontradiksi. Ini merupakan contoh penalaran matematika klasik. Kita dapat memakai pembuktian dengan kontradiksi untuk membuktikan implikasi ketiga sebagai berikut.

example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
  by_contra h'
  apply h
  intro x
  show P x
  by_contra h''
  exact h' ⟨x, h''⟩

Pastikan Anda memahami cara kerjanya. Taktik by_contra memungkinkan kita membuktikan sasaran Q dengan mengasumsikan ¬ Q dan menurunkan kontradiksi. Sebenarnya, ini ekuivalen dengan menggunakan ekuivalensi not_not : ¬ ¬ Q ↔ Q. Pastikan bahwa Anda dapat membuktikan arah maju ekuivalensi ini dengan by_contra, sedangkan arah baliknya mengikuti aturan biasa untuk negasi.

example (h : ¬¬Q) : Q := by
  sorry

example (h : Q) : ¬¬Q := by
  sorry

Gunakan pembuktian dengan kontradiksi untuk membuktikan berikut ini, yang merupakan konvers dari salah satu implikasi yang kita buktikan di atas. (Petunjuk: gunakan intro terlebih dahulu.)

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  sorry

Bekerja dengan pernyataan majemuk yang didahului negasi sering kali melelahkan, dan mengganti pernyataan seperti itu dengan bentuk ekuivalen yang negasinya telah didorong ke dalam merupakan pola matematika yang umum. Untuk memudahkannya, Mathlib menyediakan taktik push_neg, yang menyatakan ulang sasaran dengan cara tersebut (termasuk menyederhanakan ¬ ¬A menjadi A). Perintah push_neg at h menyatakan ulang hipotesis h.

example (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by
  push_neg at h
  exact h

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  dsimp only [FnHasUb, FnUb] at h
  push_neg at h
  exact h

Dalam contoh kedua, kita memakai dsimp untuk mengembangkan definisi FnHasUb dan FnUb. (Kita perlu memakai dsimp, bukan rw, untuk mengembangkan FnUb karena definisi tersebut muncul dalam cakupan suatu kuantor.) Anda dapat memverifikasi bahwa dalam contoh di atas dengan ¬∃ x, P x dan ¬∀ x, P x, taktik push_neg melakukan hal yang diharapkan. Bahkan tanpa mengetahui cara memakai simbol konjungsi, Anda semestinya dapat memakai push_neg untuk membuktikan berikut ini:

example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
  sorry

Mathlib juga memiliki taktik contrapose, yang mentransformasikan sasaran A → B menjadi ¬B → ¬A. Serupa dengan itu, jika diberikan sasaran untuk membuktikan B dari hipotesis h : A, contrapose h menyisakan sasaran untuk membuktikan ¬A dari hipotesis ¬B. Menggunakan contrapose! sebagai pengganti contrapose juga menerapkan push_neg pada sasaran dan hipotesis yang relevan.

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  contrapose! h
  exact h

example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by
  contrapose! h
  use x / 2
  constructor <;> linarith

Kita belum menjelaskan perintah constructor atau penggunaan titik koma setelahnya, tetapi kita akan melakukannya dalam seksi berikutnya.

Kita menutup seksi ini dengan prinsip ex falso, yang menyatakan bahwa dari kontradiksi dapat disimpulkan pernyataan apa pun. Di Lean, prinsip ini direpresentasikan oleh False.elim, yang membuktikan False → P untuk sembarang proposisi P. Prinsip ini mungkin tampak aneh, tetapi cukup sering muncul. Kita sering membuktikan teorema dengan memisahkannya menjadi beberapa kasus, dan kadang-kadang dapat menunjukkan bahwa salah satu kasus bersifat kontradiktif. Dalam keadaan itu, kita perlu menyatakan bahwa kontradiksi tersebut membuktikan sasaran agar dapat beralih ke kasus berikutnya. (Kita akan melihat contoh penalaran berdasarkan kasus dalam Bab 3.5.)

Lean menyediakan sejumlah cara untuk menutup suatu sasaran setelah kontradiksi diperoleh.

example (h : 0 < 0) : a > 37 := by
  exfalso
  apply lt_irrefl 0 h

example (h : 0 < 0) : a > 37 :=
  absurd h (lt_irrefl 0)

example (h : 0 < 0) : a > 37 := by
  have h' : ¬0 < 0 := lt_irrefl 0
  contradiction

Taktik exfalso mengganti sasaran saat ini dengan sasaran untuk membuktikan False. Jika diberikan h : P dan h' : ¬ P, suku absurd h h' membuktikan proposisi apa pun. Terakhir, taktik contradiction mencoba menutup sasaran dengan menemukan kontradiksi dalam hipotesis, misalnya pasangan berbentuk h : P dan h' : ¬ P. Tentu saja, dalam contoh ini, linarith juga berfungsi.

3.4. Konjungsi dan Jika-dan-Hanya-Jika

Anda telah melihat bahwa simbol konjungsi, ∧, digunakan untuk menyatakan "dan". Taktik constructor memungkinkan Anda membuktikan pernyataan berbentuk A ∧ B dengan membuktikan A, lalu membuktikan B.

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by
  constructor
  · assumption
  intro h
  apply h₁
  rw [h]

Dalam contoh ini, taktik assumption meminta Lean menemukan asumsi yang akan menyelesaikan sasaran. Perhatikan bahwa rw terakhir menyelesaikan sasaran dengan menerapkan refleksivitas ≤. Berikut beberapa cara alternatif untuk menyusun contoh sebelumnya dengan memakai kurung sudut untuk konstruktor anonim. Yang pertama adalah versi suku bukti yang ringkas dari pembuktian sebelumnya, yang memasuki mode taktik pada kata kunci by.

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
  ⟨h₀, fun h ↦ h₁ (by rw [h])⟩

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
  have h : x ≠ y := by
    contrapose! h₁
    rw [h₁]
  ⟨h₀, h⟩

Menggunakan konjungsi, alih-alih membuktikannya, mengharuskan kita menguraikan bukti bagi kedua bagiannya. Untuk itu, Anda dapat memakai taktik rcases, serta rintro atau fun dengan pencocokan pola, semuanya dengan cara yang serupa dengan penggunaannya pada kuantor eksistensial.

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  rcases h with ⟨h₀, h₁⟩
  contrapose! h₁
  exact le_antisymm h₀ h₁

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x := by
  rintro ⟨h₀, h₁⟩ h'
  exact h₁ (le_antisymm h₀ h')

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x :=
  fun ⟨h₀, h₁⟩ h' ↦ h₁ (le_antisymm h₀ h')

Sebagai analogi bagi taktik obtain, terdapat pula have dengan pencocokan pola:

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  have ⟨h₀, h₁⟩ := h
  contrapose! h₁
  exact le_antisymm h₀ h₁

Berbeda dengan rcases, di sini taktik have membiarkan h tetap berada dalam konteks. Meskipun kita tidak akan menggunakannya, sekali lagi tersedia sintaks pencocokan pola yang lazim bagi ilmuwan komputer:

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  cases h
  case intro h₀ h₁ =>
    contrapose! h₁
    exact le_antisymm h₀ h₁

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  cases h
  next h₀ h₁ =>
    contrapose! h₁
    exact le_antisymm h₀ h₁

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  match h with
    | ⟨h₀, h₁⟩ =>
        contrapose! h₁
        exact le_antisymm h₀ h₁

Berbeda dengan penggunaan kuantor eksistensial, Anda juga dapat mengambil bukti bagi kedua komponen hipotesis h : A ∧ B dengan menulis h.left dan h.right, atau, secara ekuivalen, h.1 dan h.2.

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  intro h'
  apply h.right
  exact le_antisymm h.left h'

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x :=
  fun h' ↦ h.right (le_antisymm h.left h')

Cobalah memakai teknik-teknik ini untuk mencari berbagai cara untuk membuktikan pernyataan berikut ini:

example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m :=
  sorry

Anda dapat menyarangkan penggunaan ∃ dan ∧ dengan konstruktor anonim, rintro, dan rcases.

example : ∃ x : ℝ, 2 < x ∧ x < 4 :=
  ⟨5 / 2, by norm_num, by norm_num⟩

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
  rintro ⟨z, xltz, zlty⟩
  exact lt_trans xltz zlty

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y :=
  fun ⟨_z, xltz, zlty⟩ ↦ lt_trans xltz zlty

Ingat bahwa mengawali z dengan garis bawah memberi tahu Lean bahwa kita tidak bermaksud memakai z. Jika tidak, Lean akan menampilkan peringatan bahwa z tidak digunakan.

Anda juga dapat memakai taktik use:

example : ∃ x : ℝ, 2 < x ∧ x < 4 := by
  use 5 / 2
  constructor <;> norm_num

example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
  use 5
  use 7
  norm_num

example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
  rintro ⟨h₀, h₁⟩
  use h₀
  exact fun h' ↦ h₁ (le_antisymm h₀ h')

Dalam contoh pertama, <;> setelah perintah constructor meminta Lean memakai taktik norm_num pada kedua sasaran yang dihasilkan.

Di Lean, A ↔ B tidak didefinisikan sebagai (A → B) ∧ (B → A), meskipun dapat saja didefinisikan demikian, dan perilakunya kurang lebih sama. Anda telah melihat bahwa h.mp dan h.mpr atau h.1 dan h.2 dapat dipakai untuk kedua arah h : A ↔ B. Anda juga dapat memakai cases dan taktik terkait. Untuk membuktikan pernyataan jika-dan-hanya-jika, Anda dapat memakai constructor atau kurung sudut, seperti ketika membuktikan suatu konjungsi.

example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
  constructor
  · contrapose!
    rintro rfl
    rfl
  contrapose!
  exact le_antisymm h

example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y :=
  ⟨fun h₀ h₁ ↦ h₀ (by rw [h₁]), fun h₀ h₁ ↦ h₀ (le_antisymm h h₁)⟩

Suku bukti terakhir sukar dibaca. Ingat bahwa Anda dapat memakai garis bawah ketika menulis ekspresi seperti itu untuk melihat apa yang diharapkan Lean.

Cobalah berbagai teknik dan sarana yang baru saja Anda lihat untuk membuktikan berikut ini:

example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y :=
  sorry

Untuk latihan yang lebih menarik, tunjukkan bahwa untuk sembarang bilangan real x dan y, x^2 + y^2 = 0 jika dan hanya jika x = 0 dan y = 0. Kami menyarankan agar Anda membuktikan sebuah lema bantu dengan memakai linarith, pow_two_nonneg, dan eq_zero_of_pow_eq_zero.

theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
  have h' : x ^ 2 = 0 := by sorry
  eq_zero_of_pow_eq_zero h'

example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 :=
  sorry

Di Lean, biimplikasi memiliki dua peran. Anda dapat memperlakukannya seperti konjungsi dan menggunakan kedua bagiannya secara terpisah. Namun, Lean juga mengetahui bahwa biimplikasi merupakan relasi refleksif, simetris, dan transitif di antara proposisi, dan Anda juga dapat memakainya bersama calc dan rw. Sering kali akan mudah menulis ulang suatu pernyataan menjadi pernyataan yang ekuivalen. Dalam contoh berikut, kita memakai abs_lt untuk mengganti ekspresi berbentuk |x| < y dengan ekspresi ekuivalen - y < x ∧ x < y; dalam contoh setelahnya, kita memakai Nat.dvd_gcd_iff untuk mengganti ekspresi berbentuk m ∣ Nat.gcd n k dengan ekspresi ekuivalen m ∣ n ∧ m ∣ k.

example (x : ℝ) : |x + 3| < 5 → -8 < x ∧ x < 2 := by
  rw [abs_lt]
  intro h
  constructor <;> linarith

example : 3 ∣ Nat.gcd 6 15 := by
  rw [Nat.dvd_gcd_iff]
  constructor <;> norm_num

Lihat apakah Anda dapat memakai rw bersama teorema di bawah ini untuk memberikan pembuktian singkat bahwa negasi bukanlah fungsi tak menurun. (Perhatikan bahwa push_neg tidak akan menguraikan definisi untuk Anda, sehingga rw [Monotone] diperlukan dalam pembuktian teorema tersebut.)

theorem not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
  rw [Monotone]
  push_neg
  rfl

example : ¬Monotone fun x : ℝ ↦ -x := by
  sorry

Latihan yang tersisa dalam seksi ini dirancang untuk memberi Anda lebih banyak latihan dengan konjungsi dan biimplikasi. Ingat bahwa tatanan parsial adalah relasi biner yang transitif, refleksif, dan antisimetris. Kadang-kadang muncul gagasan yang bahkan lebih lemah: suatu pratatanan hanyalah relasi refleksif dan transitif. Untuk sembarang pratatanan ≤, Lean menetapkan melalui aksioma bahwa pratatanan ketat yang terkait memenuhi a < b ↔ a ≤ b ∧ ¬ b ≤ a. Tunjukkan bahwa jika ≤ merupakan tatanan parsial, maka a < b ekuivalen dengan a ≤ b ∧ a ≠ b:

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

example : a < b ↔ a ≤ b ∧ a ≠ b := by
  rw [lt_iff_le_not_ge]
  sorry

Di luar operasi logis, Anda tidak memerlukan apa pun selain le_refl, le_trans, dan le_antisymm. Tunjukkan bahwa bahkan ketika ≤ hanya diasumsikan sebagai pratatanan, kita dapat membuktikan bahwa tatanan ketatnya bersifat irrefleksif dan transitif. Dalam contoh kedua, demi kemudahan, kita memakai penyederhana alih-alih rw untuk menyatakan < dalam kerangka ≤ dan ¬. Kita akan kembali membahas penyederhana nanti, tetapi di sini kita hanya mengandalkan fakta bahwa ia akan memakai lema yang ditunjukkan secara berulang, bahkan jika lema itu perlu diinstansiasi dengan nilai yang berbeda.

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

example : ¬a < a := by
  rw [lt_iff_le_not_ge]
  sorry

example : a < b → b < c → a < c := by
  simp only [lt_iff_le_not_ge]
  sorry

3.5. Disjungsi

Cara kanonik untuk membuktikan disjungsi A ∨ B adalah dengan membuktikan A atau membuktikan B. Taktik left memilih A, sedangkan taktik right memilih B.

variable {x y : ℝ}

example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
  left
  linarith [pow_two_nonneg x]

example (h : -y > x ^ 2 + 1) : y > 0 ∨ y < -1 := by
  right
  linarith [pow_two_nonneg x]

Kita tidak dapat memakai konstruktor anonim untuk menyusun bukti bagi pernyataan "atau", karena Lean harus menebak komponen disjungsi mana yang hendak kita buktikan. Ketika menulis term bukti, sebagai gantinya kita dapat memakai Or.inl dan Or.inr untuk menyatakan pilihan tersebut secara eksplisit. Di sini, inl dan inr masing-masing menyingkat introduksi sisi kiri dan introduksi sisi kanan.

example (h : y > 0) : y > 0 ∨ y < -1 :=
  Or.inl h

example (h : y < -1) : y > 0 ∨ y < -1 :=
  Or.inr h

Mungkin tampak aneh bahwa kita membuktikan suatu disjungsi dengan membuktikan salah satu sisinya. Dalam praktiknya, kasus mana yang berlaku biasanya bergantung pada pemisahan kasus yang tersirat atau tersurat dalam asumsi dan data. Taktik rcases memungkinkan kita memanfaatkan hipotesis berbentuk A ∨ B. Berbeda dengan penggunaan rcases pada konjungsi atau kuantor eksistensial, di sini taktik rcases menghasilkan dua sasaran. Keduanya memiliki kesimpulan yang sama, tetapi pada kasus pertama A diasumsikan benar, sedangkan pada kasus kedua B diasumsikan benar. Dengan kata lain, sesuai namanya, taktik rcases menjalankan pembuktian berdasarkan kasus. Seperti biasa, kita dapat memberi tahu Lean nama yang hendak dipakai untuk hipotesis. Dalam contoh berikutnya, kita meminta Lean memakai nama h pada setiap cabang.

example : x < |y| → x < y ∨ x < -y := by
  rcases le_or_gt 0 y with h | h
  · rw [abs_of_nonneg h]
    intro h; left; exact h
  · rw [abs_of_neg h]
    intro h; right; exact h

Perhatikan bahwa pola ⟨h₀, h₁⟩ untuk konjungsi berubah menjadi h₀ | h₁ untuk disjungsi. Bayangkan pola pertama mencocokkan data yang memuat sekaligus h₀ dan h₁, sedangkan pola kedua, dengan garis tegak, mencocokkan data yang memuat salah satu: h₀ atau h₁. Dalam contoh ini, karena kedua sasaran terpisah, kita memilih nama yang sama, h, pada setiap kasus.

Fungsi nilai mutlak didefinisikan sedemikian rupa sehingga kita dapat langsung membuktikan bahwa x ≥ 0 mengimplikasikan |x| = x (inilah teorema abs_of_nonneg), sedangkan x < 0 mengimplikasikan |x| = -x (inilah abs_of_neg). Ekspresi le_or_gt 0 x membuktikan 0 ≤ x ∨ x < 0, sehingga kita dapat memisahkan kedua kasus tersebut.

Lean juga mendukung sintaks pencocokan pola ala ilmu komputer untuk disjungsi. Di sini taktik cases menjadi lebih menarik, karena memungkinkan kita menamai setiap case dan memberi nama pada hipotesis yang diintroduksi, dekat dengan tempat hipotesis itu digunakan.

example : x < |y| → x < y ∨ x < -y := by
  cases le_or_gt 0 y
  case inl h =>
    rw [abs_of_nonneg h]
    intro h; left; exact h
  case inr h =>
    rw [abs_of_neg h]
    intro h; right; exact h

Nama inl dan inr masing-masing menyingkat introduksi kiri dan introduksi kanan. Penggunaan case memiliki kelebihan karena Anda dapat membuktikan kasus-kasus itu dalam urutan mana pun; Lean memakai labelnya untuk menemukan sasaran yang sesuai. Jika urutannya tidak penting, Anda dapat memakai next atau match, bahkan have dengan pencocokan pola.

example : x < |y| → x < y ∨ x < -y := by
  cases le_or_gt 0 y
  next h =>
    rw [abs_of_nonneg h]
    intro h; left; exact h
  next h =>
    rw [abs_of_neg h]
    intro h; right; exact h

example : x < |y| → x < y ∨ x < -y := by
  match le_or_gt 0 y with
    | Or.inl h =>
      rw [abs_of_nonneg h]
      intro h; left; exact h
    | Or.inr h =>
      rw [abs_of_neg h]
      intro h; right; exact h

Dalam penggunaan match, kita perlu memakai nama lengkap kedua cara kanonik untuk membuktikan disjungsi, yakni Or.inl dan Or.inr. Dalam buku ini, kita biasanya akan memakai rcases untuk memisahkan kasus-kasus suatu disjungsi.

Cobalah membuktikan ketaksamaan segitiga dengan memakai dua teorema pertama dalam cuplikan berikutnya. Keduanya diberi nama yang sama seperti di Mathlib.

namespace MyAbs

theorem le_abs_self (x : ℝ) : x ≤ |x| := by
  sorry

theorem neg_le_abs (x : ℝ) : -x ≤ |x| := by
  sorry

theorem abs_add_le (x y : ℝ) : |x + y| ≤ |x| + |y| := by
  sorry

Jika Anda menikmati kasus-kasus ini (permainan kata memang disengaja) dan ingin lebih banyak berlatih dengan disjungsi, cobalah soal-soal berikut.

theorem lt_abs : x < |y| ↔ x < y ∨ x < -y := by
  sorry

theorem abs_lt : |x| < y ↔ -y < x ∧ x < y := by
  sorry

Anda juga dapat memakai rcases dan rintro pada disjungsi bersarang. Ketika pemakaiannya menghasilkan pemisahan kasus yang sesungguhnya dengan beberapa sasaran, pola untuk setiap sasaran baru dipisahkan oleh garis tegak.

example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
  rcases lt_trichotomy x 0 with xlt | xeq | xgt
  · left
    exact xlt
  · contradiction
  · right; exact xgt

Anda tetap dapat menyarangkan pola dan memakai kata kunci rfl untuk melakukan substitusi berdasarkan persamaan:

example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by
  rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
  · rw [mul_assoc]
    apply dvd_mul_right
  · rw [mul_comm, mul_assoc]
    apply dvd_mul_right

Cobalah membuktikan pernyataan berikut dengan satu baris (panjang). Gunakan rcases untuk mengurai hipotesis dan memisahkan kasus, lalu gunakan <;> linarith untuk menyelesaikan setiap cabang.

example {z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ∨ z = x ^ 2 + y ^ 2 + 1) : z ≥ 0 := by
  sorry

Pada bilangan real, persamaan x * y = 0 menyatakan bahwa x = 0 atau y = 0. Di Mathlib, fakta ini dikenal sebagai eq_zero_or_eq_zero_of_mul_eq_zero dan merupakan contoh menarik lainnya tentang bagaimana disjungsi dapat muncul. Cobalah memakainya untuk membuktikan pernyataan berikut:

example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
  sorry

example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
  sorry

Ingatlah bahwa Anda dapat memakai taktik ring untuk membantu perhitungan.

Dalam sembarang gelanggang \(R\), elemen \(x\) sedemikian sehingga \(x y = 0\) untuk suatu \(y\) yang tidak nol disebut pembagi nol kiri; elemen \(x\) sedemikian sehingga \(y x = 0\) untuk suatu \(y\) yang tidak nol disebut pembagi nol kanan; dan elemen yang merupakan pembagi nol kiri atau kanan disebut singkatnya pembagi nol. Teorema eq_zero_or_eq_zero_of_mul_eq_zero menyatakan bahwa bilangan real tidak memiliki pembagi nol nontrivial. Gelanggang komutatif dengan sifat ini disebut daerah integral. Bukti Anda untuk kedua teorema di atas juga seharusnya berlaku dalam setiap daerah integral:

variable {R : Type*} [CommRing R] [IsDomain R]
variable (x y : R)

example (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
  sorry

example (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
  sorry

Sebenarnya, jika Anda cermat, teorema pertama dapat dibuktikan tanpa memakai sifat komutatif perkalian. Dalam hal itu, cukup diasumsikan bahwa R merupakan Ring, bukan CommRing.

Kadang-kadang dalam suatu bukti kita ingin memisahkan kasus menurut benar atau tidaknya sebuah pernyataan. Untuk sembarang proposisi P, kita dapat memakai em P : P ∨ ¬ P. Nama em menyingkat sebutan bahasa Inggris untuk hukum tiada jalan tengah.

example (P : Prop) : ¬¬P → P := by
  intro h
  cases em P
  · assumption
  · contradiction

Sebagai alternatif, Anda dapat memakai taktik by_cases.

example (P : Prop) : ¬¬P → P := by
  intro h
  by_cases h' : P
  · assumption
  contradiction

Perhatikan bahwa taktik by_cases memungkinkan Anda menentukan label bagi hipotesis yang diintroduksi pada setiap cabang, dalam contoh ini h' : P pada satu cabang dan h' : ¬ P pada cabang lainnya. Jika label tersebut dihilangkan, Lean memakai h secara baku. Cobalah membuktikan ekuivalensi berikut dengan memakai by_cases untuk membuktikan salah satu arahnya.

example (P Q : Prop) : P → Q ↔ ¬P ∨ Q := by
  sorry

3.6. Barisan dan Konvergensi

Kini kita telah menguasai cukup banyak keterampilan untuk mulai mengerjakan matematika yang sesungguhnya. Di Lean, kita dapat merepresentasikan barisan bilangan real \(s_0, s_1, s_2, \ldots\) sebagai fungsi s : ℕ → ℝ. Barisan semacam ini dikatakan konvergen ke bilangan \(a\) jika untuk setiap \(\varepsilon > 0\) terdapat suatu indeks sehingga, setelah indeks itu, barisan tetap berjarak kurang dari \(\varepsilon\) dari \(a\). Dengan kata lain, terdapat bilangan \(N\) sehingga untuk setiap \(n \ge N\), berlaku \(| s_n - a | < \varepsilon\). Di Lean, kita dapat merumuskannya sebagai berikut:

def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

Notasi ∀ ε > 0, ... merupakan singkatan yang praktis untuk ∀ ε, ε > 0 → .... Demikian pula, ∀ n ≥ N, ... menyingkat ∀ n, n ≥ N → .... Ingat pula bahwa ε > 0 didefinisikan sebagai 0 < ε, sedangkan n ≥ N didefinisikan sebagai N ≤ n.

Dalam seksi ini, kita akan membuktikan beberapa sifat konvergensi. Namun, pertama-tama kita akan membahas tiga taktik yang berguna untuk menangani kesamaan. Taktik pertama, ext, memberi kita cara untuk membuktikan bahwa dua fungsi adalah sama. Misalkan \(f(x) = x + 1\) dan \(g(x) = 1 + x\) merupakan fungsi dari bilangan real ke bilangan real. Tentu saja \(f = g\), karena keduanya menghasilkan nilai yang sama untuk setiap \(x\). Taktik ext memungkinkan kita membuktikan persamaan antara dua fungsi dengan membuktikan bahwa nilainya sama pada setiap nilai argumennya.

example : (fun x y : ℝ ↦ (x + y) ^ 2) = fun x y : ℝ ↦ x ^ 2 + 2 * x * y + y ^ 2 := by
  ext
  ring

Nanti kita akan melihat bahwa ext sebenarnya berlaku lebih umum dan bahwa nama variabel yang muncul juga dapat ditentukan. Sebagai contoh, Anda dapat mencoba mengganti ext dengan ext u v dalam bukti di atas. Taktik kedua, congr, memungkinkan kita membuktikan persamaan antara dua ekspresi dengan menangani bagian-bagian yang berbeda:

example (a b : ℝ) : |a| = |a - b + b| := by
  congr
  ring

Di sini taktik congr mengupas penerapan abs pada kedua sisi, sehingga kita tinggal membuktikan a = a - b + b.

Terakhir, taktik convert dipakai untuk menerapkan teorema ketika kesimpulan teorema tersebut tidak persis cocok dengan sasaran. Sebagai contoh, misalkan kita ingin membuktikan a < a * a dari 1 < a. Sebuah teorema dalam pustaka, mul_lt_mul_iff_left₀, memungkinkan kita membuktikan 1 * a < a * a. Salah satu pilihan ialah bekerja mundur dan menulis ulang sasaran agar memiliki bentuk tersebut. Sebagai gantinya, taktik convert memungkinkan kita menerapkan teorema dalam bentuknya semula, lalu menyisakan tugas membuktikan persamaan-persamaan yang diperlukan agar sasaran menjadi cocok.

example {a : ℝ} (h : 1 < a) : a < a * a := by
  convert (mul_lt_mul_iff_left₀ _).2 h
  · rw [one_mul]
  exact lt_trans zero_lt_one h

Contoh ini memperlihatkan kiat berguna lainnya: ketika kita menerapkan ekspresi yang memuat garis bawah dan Lean tidak dapat mengisinya secara otomatis, Lean membiarkannya untuk kita selesaikan sebagai sasaran lain.

Pernyataan berikut menunjukkan bahwa setiap barisan konstan \(a, a, a, \ldots\) bersifat konvergen.

theorem convergesTo_const (a : ℝ) : ConvergesTo (fun _x : ℕ ↦ a) a := by
  intro ε εpos
  use 0
  intro n nge
  rw [sub_self, abs_zero]
  apply εpos

Lean memiliki taktik simp yang sering menghemat pekerjaan Anda dalam menjalankan langkah seperti rw [sub_self, abs_zero] secara manual. Kita akan segera menjelaskannya lebih lanjut.

Untuk teorema yang lebih menarik, mari kita tunjukkan bahwa jika s konvergen ke a dan t konvergen ke b, maka fun n ↦ s n + t n konvergen ke a + b. Sebelum mulai menulis bukti formal, sebaiknya kita memiliki gambaran yang jelas tentang bukti di atas kertas. Untuk ε yang lebih besar dari 0, gagasannya ialah memakai hipotesis untuk memperoleh Ns sedemikian sehingga, mulai indeks tersebut, s berjarak kurang dari ε / 2 dari a, serta memperoleh Nt sedemikian sehingga, mulai indeks tersebut, t berjarak kurang dari ε / 2 dari b. Kemudian, setiap kali n lebih besar dari atau sama dengan maksimum Ns dan Nt, barisan fun n ↦ s n + t n seharusnya berjarak kurang dari ε dari a + b. Contoh berikut mulai menerapkan strategi ini. Cobalah menuntaskan buktinya.

theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ}
      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
    ConvergesTo (fun n ↦ s n + t n) (a + b) := by
  intro ε εpos
  dsimp -- baris ini tidak diperlukan, tetapi sedikit merapikan sasaran.
  have ε2pos : 0 < ε / 2 := by linarith
  rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
  rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
  use max Ns Nt
  sorry

Sebagai petunjuk, Anda dapat memakai le_of_max_le_left dan le_of_max_le_right, sedangkan norm_num dapat membuktikan ε / 2 + ε / 2 = ε. Taktik congr juga berguna untuk menunjukkan bahwa |s n + t n - (a + b)| sama dengan |(s n - a) + (t n - b)|, karena setelah itu Anda dapat memakai ketaksamaan segitiga. Perhatikan bahwa semua variabel s, t, a, dan b kita tandai sebagai implisit karena dapat disimpulkan dari hipotesis.

Membuktikan teorema yang sama dengan perkalian menggantikan penjumlahan cukup rumit. Kita akan mencapainya dengan terlebih dahulu membuktikan beberapa pernyataan bantu. Cobalah menuntaskan pula bukti berikut, yang menunjukkan bahwa jika s konvergen ke a, maka fun n ↦ c * s n konvergen ke c * a. Sebaiknya kita memisahkan kasus berdasarkan apakah c sama dengan nol atau tidak. Kasus nol telah ditangani, dan Anda diminta membuktikan hasilnya dengan asumsi tambahan bahwa c tidak nol.

theorem convergesTo_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : ConvergesTo s a) :
    ConvergesTo (fun n ↦ c * s n) (c * a) := by
  by_cases h : c = 0
  · convert convergesTo_const 0
    · rw [h]
      ring
    rw [h]
    ring
  have acpos : 0 < |c| := abs_pos.mpr h
  sorry

Teorema berikut juga menarik secara tersendiri: teorema ini menunjukkan bahwa nilai mutlak suku-suku suatu barisan konvergen terbatas mulai indeks tertentu. Kita telah memulai buktinya; cobalah menuntaskannya.

theorem exists_abs_le_of_convergesTo {s : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) :
    ∃ N b, ∀ n, N ≤ n → |s n| < b := by
  rcases cs 1 zero_lt_one with ⟨N, h⟩
  use N, |a| + 1
  sorry

Sebenarnya, teorema tersebut dapat diperkuat dengan menyatakan bahwa terdapat batas b yang berlaku untuk semua nilai n. Namun, versi ini sudah cukup kuat untuk keperluan kita, dan pada akhir seksi ini kita akan melihat bahwa teorema tersebut berlaku secara lebih umum.

Lema bantu berikut membuktikan bahwa jika s konvergen ke a dan t konvergen ke 0, maka fun n ↦ s n * t n konvergen ke 0. Untuk membuktikannya, kita memakai teorema sebelumnya guna memperoleh batas B bagi s setelah suatu indeks N₀. Cobalah memahami strategi yang telah kita uraikan dan tuntaskan buktinya.

theorem aux {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t 0) :
    ConvergesTo (fun n ↦ s n * t n) 0 := by
  intro ε εpos
  dsimp
  rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
  have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
  have pos₀ : ε / B > 0 := div_pos εpos Bpos
  rcases ct _ pos₀ with ⟨N₁, h₁⟩
  sorry

Jika Anda telah sampai sejauh ini, selamat! Kini teorema kita tinggal selangkah lagi. Bukti berikut menuntaskannya.

theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ}
      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
    ConvergesTo (fun n ↦ s n * t n) (a * b) := by
  have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
    apply aux cs
    convert convergesTo_add ct (convergesTo_const (-b))
    ring
  have := convergesTo_add h₁ (convergesTo_mul_const b cs)
  convert convergesTo_add h₁ (convergesTo_mul_const b cs) using 1
  · ext; ring
  ring

Untuk latihan menantang lainnya, cobalah melengkapi kerangka bukti berikut untuk menunjukkan bahwa limit bersifat tunggal. (Jika ingin mengambil tantangan lebih besar, Anda dapat menghapus kerangka tersebut dan mencoba membuktikannya dari awal.)

theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ}
      (sa : ConvergesTo s a) (sb : ConvergesTo s b) :
    a = b := by
  by_contra abne
  have : |a - b| > 0 := by sorry
  let ε := |a - b| / 2
  have εpos : ε > 0 := by
    change |a - b| / 2 > 0
    linarith
  rcases sa ε εpos with ⟨Na, hNa⟩
  rcases sb ε εpos with ⟨Nb, hNb⟩
  let N := max Na Nb
  have absa : |s N - a| < ε := by sorry
  have absb : |s N - b| < ε := by sorry
  have : |a - b| < |a - b| := by sorry
  exact lt_irrefl _ this

Kita menutup seksi ini dengan mengamati bahwa bukti-bukti kita dapat diperumum. Sebagai contoh, satu-satunya sifat bilangan asli yang telah kita gunakan adalah bahwa strukturnya memiliki tatanan parsial dengan min dan max. Anda dapat memeriksa bahwa semuanya tetap berlaku jika setiap kemunculan ℕ diganti dengan sembarang tatanan linear α:

variable {α : Type*} [LinearOrder α]

def ConvergesTo' (s : α → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

Dalam Bab 11.1, kita akan melihat bahwa Mathlib memiliki mekanisme untuk menangani konvergensi dalam kerangka yang jauh lebih umum, bukan hanya dengan mengabstraksikan ciri-ciri khusus domain dan kodomain, melainkan juga dengan mengabstraksikan berbagai jenis konvergensi.