Každý hrdina potřebuje nepřítele
I když perm sehrál zásadní roli v našem předchozím vítězství nad zlovolnou length_sum_perm_of_B, je to pořád pouhý mladý padawan a musí být řádně vycvičen, aby dosáhl svého plného potenciálu. Nejlepším způsobem, jak toho dosáhnout, je pochopitelně představit hrozivého nepřítele:
theorem perm_training_ground
(Bacb : B a c b)
(Bcbe : B c b e)
(Bbed : B b e d)
(h1 : length b a = length d b)
(h2 : length e b + length a c = length d e + length c b)
(h3 : length a c + length d e = length e c) :
length a c = length b c ∧
length b e = length c b ∧
length e b = length e d := by sorry
Jejda. Dokonce i pořadí bodů je znepokojivé. Nenechme se zastrašit a zkusme analyzovat situaci. Cíl mluví pouze o délkách, ale potřebujeme dostat do hry informaci o pořadí bodů na přímkách. Využití length_sum_of_B se vypadá jako slibný začátek:
have accb := length_sum_of_B Bacb
have beed := length_sum_of_B Bbed
have cbbe := length_sum_of_B Bcbe
Rozšiřování působnosti permu
Teď bychom rádi dosadili tyto nové rovnice do původních hypotéz, ale všechny bohužel mají prohozené argumenty. Zní to jako příležitost pro perm zazářit! Ale…aktuálně ovládá jen permutace v cíli, ne v hypotézách. Naštěstí umí conv pracovat i s hypotézami, takže to napravme:
namespace Lean.Elab.Tactic
syntax "perm" ("at " ident)? : tactic
macro_rules
| `(tactic| perm) =>`(tactic|
(try conv in (occs := *) length _ _ => all_goals length_nf))
| `(tactic| perm at $name) =>`(tactic|
(try conv at $name in (occs := *) length _ _ => all_goals length_nf))
end Lean.Elab.Tactic
To bylo relativně snadné – jen jsme nahradili macro za syntax a macro_rules, čímž jsme rozšířili syntaxi pomocí shody vzorů (ident bude odpovídat názvu hypotézy a ? znamená, že "at " ident je nepovinný argument). Příkaz perm; perm at h1; perm at h2; perm at h3 nyní přeskupí všechny argumenty do správného pořadí. Ale zdá se to trochu nešikovné. Je to to nejlepší, co zvládneš, perme?
syntax "perm" ("at " ident)? ("at *")? : tactic
macro_rules
| `(tactic| perm) =>`(tactic|
(try conv in (occs := *) length _ _ => all_goals length_nf))
| `(tactic| perm at $name) =>`(tactic|
(try conv at $name in (occs := *) length _ _ => all_goals length_nf))
elab_rules : tactic
| `(tactic| perm at *) => withMainContext do
evalTactic (← `(tactic| perm))
for ldecl in ← getLCtx do
let name := mkIdent ldecl.userName
if !ldecl.isImplementationDetail then
evalTactic (← `(tactic| perm at $name))
Hned je to lepší! elab_rules nám dovolí jít hlouběji — nejdřív zavoláme perm jen tak, a potom na každou relevantní hypotézu. (Můžete namítnout, že je to trochu plýtvání, ale v praxi to není problém). Všimněte si, že jsme také museli rozšířit syntaxi.
Pokračujme v důkazu (← odkazuje na symetrickou verzi, takže rw [← abbc] at h1 nahradí pravou stranu abbc v h1 levou stranou):
perm at *
rw [← accb] at h1
rw [← beed] at h1
rw [← cbbe] at h3
Infoview je teď zahlceno neaktuálními předpoklady, takže ho pojďme trochu vyčistit taktikou clear: clear Bacb Bcbe Bbed accb beed cbbe. Pak vypadá takto:
i : incidence_geometry
a b c d e: point
h1 : length a b + length b c = length c d + length d e
h2 : length c d + length a b = length d e + length b c
h3 : length a b + length d e = length b c + length c d
⊢ length a b = length b c ∧ length c d = length b c ∧ length c d = length d e
Není ale jasné, jak teď postupovat. Jasně, můžeme využít našeho kámoše splitAll a získat tři dílčí cíle, ale co bude dál?
Svatý grál lineární algebry
Toto je ideální místo na zásek. Mohli bychom zkoušet různé věci – odečítání členů od obou stran rovnice a následné dosazování (možná v režimu výpočtu), využití komutativity,…nebo zkrátka můžeme použít linarith. Není to podvádění? Možná trochu, ale tato mocná zakončující taktika nám hodně usnadní život. Vyřeší cíl, pokud vyplývá z lineárních (ne)rovností v kontextu (nebo selže), což je přesně náš případ. Sledujme to v akci:
theorem perm_training_ground
(Bacb : B a c b)
(Bcbe : B c b e)
(Bbed : B b e d)
(h1 : length b a = length d b)
(h2 : length e b + length a c = length d e + length c b)
(h3 : length a c + length d e = length e c) :
length a c = length b c ∧
length b e = length c b ∧
length e b = length e d := by
have accb := length_sum_of_B Bacb
have beed := length_sum_of_B Bbed
have cbbe := length_sum_of_B Bcbe
perm at *
rw [← accb] at h1
rw [← beed] at h1
rw [← cbbe] at h3
clear Bacb Bcbe Bbed accb beed cbbe
splitAll
repeat linarith
Tadá! Velký zlý záporák byl poražen. A přece… pořád to vypadá, že by důkaz mohl být efektivnější. linarith má příjemnou vychytávku – linarith[H1, H2,...] v podstatě funguje jako have := H1; have := H2; linarith, aniž by zaneřádil infoview. Takže co takhle zkusit linarith[length_sum_of_B Bacb, length_sum_of_B Bbed, length_sum_of_B Bcbe] a zbavit se have a rw? Normálně by to fungovalo dobře, ale v tomto případě by hypotézy přidané uvnitř linarithu měly nesprávné pořadí argumentů, a perm nelze použít, protože se vše děje najednou. Co teď?
Dokonalá kombinace
Někdy se hrdina musí obětovat a stát se součástí většího celku. A co je lepší než perm i linarith? Hádáte správně – jejich fúze, linperm! Potřebujeme jen rozšířit perm at * o [] schopnost linarithu a zakončit vše linarithem. Nejdřív musíme napodobit chování have:
open Lean Meta in
def haveExpr (n:Name) (h:Expr) :=
withMainContext do
let t ← inferType h
liftMetaTactic fun mvarId => do
let mvarIdNew ← Lean.MVarId.assert mvarId n t h
let (_, mvarIdNew) ← Lean.MVarId.intro1P mvarIdNew
return [mvarIdNew]
Nyní můžeme použít haveExpr v rámci pomocné taktiky havePerms, která analyzuje své argumenty v hranatých závorkách, přidá je do kontextu jako this a zavolá na ně perm:
open Parser Tactic Syntax
syntax "havePerms" (" [" term,* "]")? : tactic
elab_rules : tactic
| `(tactic| havePerms $[[$args,*]]?) => withMainContext do
let hyps := (← ((args.map (TSepArray.getElems)).getD {}).mapM
(elabTerm ·.raw none)).toList
for h in hyps do
haveExpr "this" h
evalTactic (← `(tactic| perm at $(mkIdent "this")))
Zbývá znovu rozšířit syntaxi perm nahrazením
syntax "perm"("at " ident)? ("at *")? : tactic
pomocí
syntax "perm" (" [" term,* "]")? ("at " ident)? ("at *")? : tactic
a nechat jej interně volat havePerms:
macro_rules
| `(tactic| perm [$args,*] ) => `(tactic| havePerms [$args,*])
Nakonec definujme linperm spojením všeho dohromady:
syntax "linperm " ("[" term,* "]")? : tactic
macro_rules
| `(tactic| linperm) => `(tactic| perm at *; linarith)
| `(tactic| linperm [$args,*] ) =>
`(tactic| perm at *; havePerms [$args,*]; linarith)
Uf. Po vší té tvrdé práci je čas sklidit její plody a pozorovat linperm ve chvíli jeho triumfu. Ach, jak nám vyrostl!
theorem perm_training_ground'
(Bacb : B a c b)
(Bcbe : B c b e)
(Bbed : B b e d)
(h1 : length b a = length d b)
(h2 : length e b + length a c = length d e + length c b)
(h3 : length a c + length d e = length e c) :
length a c = length b c ∧
length b e = length c b ∧
length e b = length e d := by
splitAll
repeat linperm [length_sum_of_B Bacb, length_sum_of_B Bcbe, length_sum_of_B Bbed]
Pořád je tu spousta dalších způsobů, jak by (lin)perm mohl dál růst; na rozdíl od přímek v euklidovské geometrii ale příběhy mívají konec. Takže vytáhněte kapesníky a rozlučte se s naším přítelem (lin)permem, aspoň prozatím. Doufám, že vás jeho cesta světem psaní taktik inspirovala a budete moci vylepšovat své dovednosti stejným způsobem jako on.
Pokud máte nějaké návrhy na vylepšení tohoto blogového příspěvku, dejte mi vědět.