Syntetická euklidovská geometrie
Dle slibu v úvodu si teď ukážeme konkrétní příklady. Tedy aspoň tak konkrétní, jak to jen v syntetické euklidovské geometrii jde – zapomeňte na souřadnice bodů a vaše oblíbené analytické výpočty. Následují zjednodušené úryvky z dizertace mého kamaráda Andrého, která formalizuje Euklidovy Základy (mimochodem, takhle jsem se poprvé dostal k Leanu a zpětně mi to připadá jako docela přístupná cesta).
(Poznámka: budeme pracovat v Leanu 4, takže neváhejte si vše zkusit online nebo lokálně. A nezapomeňte, že po umístění kurzoru do kódu můžete vidět aktuální stav v infoview!)
import Mathlib.Data.Real.Basic
universe u1 u2 u3
class incidence_geometry :=
(point : Type u1)
(line : Type u2)
(circle : Type u3)
(length : point → point → ℝ)
(B : point → point → point → Prop) -- Betweenness
(length_nonneg : ∀ (a b : point), 0 ≤ length a b)
(length_symm : ∀ (a b : point), length a b = length b a)
(length_eq_zero_iff : ∀ {a b : point}, length a b = 0 ↔ a = b)
(length_sum_of_B : ∀ {a b c : point},
B a b c → length a b + length b c = length a c)
(ne_12_of_B : ∀ {a b c : point}, B a b c → a ≠ b )
(ne_13_of_B : ∀ {a b c : point}, B a b c → a ≠ c )
(ne_23_of_B : ∀ {a b c : point}, B a b c → b ≠ c )
variable [i : incidence_geometry]
open incidence_geometry
Toto je minimální příprava, s detaily si teď moc nelamme hlavu. V podstatě deklarujeme, že budeme pracovat s body, přímkami a kružnicemi, přičemž budeme mít funkci, která měří délku dvou bodů a predikát, který říká, zda tři body leží na jedné přímce v daném pořadí. (Všimli jste si, že nikde neříkáme, co tyto objekty jsou? To je právě ten syntetický přístup.) Máme také pár axiomů o těchto funkcích – ne úplně ty, které navrhl Euclid, ale zatím budou stačit.
Pojďme se nyní podívat na první lemma!
lemma len_pos_of_neq (ab : a ≠ b) : 0 < length a b := by sorry
Závorky za názvem lemmatu obsahují pojmenované vstupní předpoklady, zatímco tvrzení za dvojtečkou je přesně to, co se snažíme dokázat (říkejme mu cíl; můžeme ho také vidět v infoview za symbolem ⊢). (Pokud chcete, můžete si lemmata a věty představit jako funkce se vstupy a výstupy oddělenými dvojtečkou.)
Po := by měl následovat důkaz; klíčové slovo by nás přepne do taktického režimu (o něm více později) a sorry znamená, že se nám důkaz zatím nepodařilo dokončit důkaz a prosíme kompilátor o trpělivost. (sorry ve skutečnosti zavádí další axiom, takže bychom ho měli používat jen v nedokončených projektech; jinak riskujeme, že v naší teorii dojdeme ke sporu.) Pojďme to napravit:
lemma len_pos_of_neq (ab : a ≠ b) : 0 < length a b :=
Ne.lt_of_le' (length_eq_zero_iff.not.mpr ab) (length_nonneg a b)
Vyrazilo vám toto tvrzení dech? No…asi ne, je to jen prostý důsledek axiomů o délce. Důkaz možná také nevypadá příliš poučně, ale tím se nenechme nezpomalit.
Modulární design
Teď jste možná trochu zmatení a/nebo demotivovaní. Neměli jsme náhodou dělat opravdovou matematiku? Jde o to, že většina lemmat jsou jen malé stavební kameny, jejichž hodnota se ukáže až ve větším kontextu (trochu to připomíná modulární filozofii Linuxu – každá funkce by měla dělat jen jednu věc, zato pořádně). Jinak řečeno:
Lemma 1 (Euclid-Hernández-Espiet) Každý důkaz se stane zvládnutelným, pokud na něj zaútočíte pomocí dlouhé řady lemmat fungujících jako API – bez ohledu na to, jak malá nebo triviální se zdají.
Lemma 2 ↑Kluci mají pravdu.
Lemma 3 V tom případě…Lemma 1 implikuje Lemma 2.
Lemma 4 Ve skutečnosti jsou ekvivalentní.
Asi netřeba pokračovat. Důkazy takových tvrzení však nemusí být vůbec jednoduché a jejich výstižné zachycení je umění samo o sobě. Zvažme následující příklad:
theorem length_sum_perm_of_B' (Babc : B a b c) :
0 < length a b ∧ 0 < length b a := by
have ab : a ≠ b := ne_12_of_B Babc
have ab_pos : 0 < length a b := len_pos_of_neq ab
constructor
exact ab_pos
rw [length_symm] at ab_pos
exact ab_pos
Snad aspoň zhruba vidíte, co se tu děje (mrkněte na infoview). Stručně:
- klíčové slovo
havezavádí do našeho kontextu další hypotézu na základě těch předchozích, constructorrozděluje konjunkci v cíli na dva samostatné cíle,exactuzavírá aktuální cíl pomocí předpokladu, který už máme k dispozici,rwpřepisuje rovnost vycházející z dřívějšího lemmatu uvnitř tvrzení v našem kontextu.
Zde je ekvivalentní jednořádkový důkaz (za pomocí |> pro řetězení, ▸ pro konverzi typu a ⟨⟩ pro tvorbu složených výrazů):
theorem length_sum_perm_of_B'' (Babc : B a b c) :
0 < length a b ∧ 0 < length b a :=
⟨ ne_12_of_B Babc |> len_pos_of_neq,
ne_12_of_B Babc |> length_symm a b ▸ len_pos_of_neq⟩
A ještě kratší verze, pomocí mocného zjednodušovače simp:
theorem length_sum_perm_of_B''' (Babc : B a b c) :
0 < length a b ∧ 0 < length b a := by
simp [length_symm b, Babc.length_pos]
První důkaz nabízí detaily čitelné pro člověka a druhý sestrojuje důkazové členy přímo, ale ten poslední je v mnoha kontextech preferovaný pro svou jednoduchost, protože můžeme nízkoúrovňové detaily ignorovat. Ale ani to nemusí stačit – co když je tvrzení věty mnohem delší?
theorem length_sum_perm_of_B (Babc : B a b c) :
0 < length a b ∧ 0 < length b a ∧ 0 < length b c ∧
0 < length c b ∧ 0 < length a c ∧ 0 < length c a ∧
length a b + length b c = length a c ∧
length b a + length b c = length a c ∧
length b a + length c b = length a c ∧
length b a + length b c = length c a ∧
length b a + length c b = length c a ∧
length a b + length c b = length a c ∧
length a b + length b c = length c a ∧
length a b + length c b = length c a
:= by sorry
(Pokud se vám to nezdá – nejedná se o vymyšlený příklad, ale o skutečný problém, který bylo třeba v projektu vyřešit.)
I když tu není žádný skutečný matematický obsah, napsat důkaz pouze pomocí dosud zmíněných metod by bylo velmi zdlouhavé. (Oprava: pomocí simp to vlastně jde celkem snadno, zkuste si to jako cvičení.). Raději použijeme mocné taktiky – přístup Leanu k automatizaci. Více o tom, jak je vytvořit, v příštím díle!
Pokud máte nějaké návrhy na vylepšení tohoto blogového příspěvku, dejte mi prosím vědět.