Lean 4 ‘te: Temeller #15

Herkese merhaba, önceki yazımda giriş yaptığım “Mathematics in Lean” kitabına bu yazımda yine bir örnekle devam edeceğim.

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

Bu linkten ulaşabilirsiniz: https://github.com/fizikzedenin-kodlari/LeanOnMath/blob/main/example%2315.lean

Yine aşama aşama örneği inceleyelim. İlk satır, Mathlib kütüphanesinden komutları kullanabilmemiz içindi, o yüzden ikinci satırdan başlıyorum:

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

Bu satırı parça parça inceleyelim:

(a b c d e f : ℝ)

a, b, c, d, e ve f, reel sayı olmak üzere.

(h : a * b = c * d)  (h' : e = f)

Burada gördüğünüz h ve h' ifadelerine bakalım. Öncelikle bu isimlendirme kısmı örneği yazan kişiye kalmış. Siz buna başka isimler de verebilirsiniz ama standart olarak hipotezin ilk harfi olmasından dolayı kitap boyunca sıklıkla h ve ikinci bir hipotez için de h' tercih edilmiş. Buradaki ' ifadesi herhangi bir matematiksel ifadeyi temsil etmiyor. h2 gibi bir şey de yazabilirdiniz.

Burada asıl amaç, elimizde bazı eşitlikler var mesela a * b = c * d Bu eşitliği biz kullanacağız ve her seferinde bunu uzun uzun yazmak istemiyoruz. Bunu kısaltmak istediğimiz için ona en kısa olacak şekilde bir isim verdik. Bu ismi verdiğimizi Lean’in anlama yolu ise o isimden sonra : koymak. Bu anlattığım şey aynen h' için geçerli.

a * (b * e) = c * (d * f)

Bizim ispatlamak istediğimiz kısım burası. Elimizde olan şey a * (b * e) . Biz bunun eşitliğin sağ tarafına, yani c * (d * f) ‘e eşit olduğunu göstermek istiyoruz. Bunu göstermek için örnekte verilen h ve h' eşitliklerini kullanacağız.

:= by

İspata başlayacağımızı belirten kod parçası.

Şimdi gelelim ispatın ilk satırına:

rw [h']

Burada, yaptığımız şey Lean’e “ h' ‘ü uygula” demek aslında. Yani, e yerine f koy.

İspatın ikinci satırı:

rw [ ← mul_assoc]

Burada Mathlib kütüphanesinden mul_assoc komutunu alıyoruz fakat bize ters yönü lazım olduğu için başına ters yönlü ok ← koyuyoruz. Bunu açıklayayım:

#check mul_assoc yazdığınızda “expected type” kısmında karşınıza şu açıklama çıkar:

⊢ ∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)

En sağda yer alan şu ifadeye bakacak olursak:

a * b * c = a * (b * c)

Burada sol tarafta hiç parantez yokken, sağ tarafta sağdan iki ifadenin parantez içine alındığını görüyoruz.

Şimdi ispatlamak istediğimiz şeye dönelim:

a * (b * e) = c * (d * f)

Eşitliğin sol tarafı, sağdan parantezli. Bu Mathlib kütüphanesinden kullanmak istediğimiz mul_assoc komutunun zıt yönü aslında. Biz bu parantezleri kaldırıp işimize devam etmek istiyoruz. Yani hedefimiz şu:

a * (b * e) = a * b * e

İspatın ilk satırında, h' ‘ü uyguladığımız için e ‘yi f ile değiştirmiştik. Dolayısıyla aslında amacımız şuna dönüştü:

a * (b * f) = a * b * f

Bunun içindir ki

rw [ ← mul_assoc]

kullandık.

İspatın 3.satırına gelelim:

rw [h]

Burada, soruda verilen h yi uygulamak istiyoruz. Yani a * b yerine c * d yazacağız. Dolayısıyla elde ettiğimiz şey şuna dönüşecek:

a * b * f = c * d * f

Şimdi ispatın son adımına gelelim:

rw [mul_assoc]

Bu sefer, örnekte ulaşmak istediğimiz yer c * (d * f) olduğu için, sağdaki çarpımı parantez içine almamız lazım. O yüzden bu işe yarayan mul_assoc komutunu kullandık.

Böylelikle ispatlamak istediğimiz şeye soruda verilen h ve h' hipotezlerini kullanarak varmış olduk.

Kodlamayla kalın!

Yeni yazılardan anında haberdar olmak için Whatsapp kanal linki: https://whatsapp.com/channel/0029Vb8vtRsCRs1m7Qjexq0H