Lean série 03: Taktiky

Automatizace nízkoúrovňových částí

Ani triky z předchozího dílu nestačily na důkaz length_sum_perm_of_B. I když bychom mohli konjunkce manuálně rozdělit a dokázat každou část zvlášť, nebylo by to dobré využití našeho času. Místo toho si můžeme všimnout, že po použití axiomu

(length_symm : ∀ (a b : point), length a b = length b a)

na správných místech tvrzení snadno plyne z lemmatu len_pos_of_neq a axiomu length_sum_of_B. Jak ale poznáme, kdy na výraz použít length_symm a kdy ho nechat být?

Metaprogramování na scénu

Místo nutnosti zadat explicitní výrazy tvořící důkaz nám Lean umožňuje použít taktiky. Ty mají různé účely, ale obecně nám umožňují částečně automatizovat proces dokazování a neřešit „samozřejmé“ části, takže můžeme přemýšlet na vyšší úrovni. Ve skutečnosti jsme již viděli několik taktik minule, konkrétně have, constructor, exact, rw a sorry. Taktiky lze řetězit i rozšířit jejich definice; také si můžeme vytvořit vlastní – na což se přesně chystáme!

Pokud chceme pouze spojit několik taktik do jedné, stačí nám makra — to je ta jednodušší varianta. Ale když opravdu potřebujeme sáhnout na vnitřní stav, musíme si zašpinit ruce a použít elabs (zkratka pro elaborations). Držte si klobouky! (A stejně jako minule si vše můžete zkoušet online.)

Normální forma pro length

Začněme jednodušším cílem – upravit jediný výraz length do normálního tvaru. Jinými slovy, length a b i length b a by měly po použití taktiky vést ke stejnému výstupu. Lexikografické řazení argumentů je jednou z přirozených možností.

namespace Lean.Elab.Tactic

def getNthArgName (tgt : Expr) (n : Nat) : MetaM Name :=
  do
    let some id := Lean.Expr.fvarId? (Lean.Expr.getArg! tgt n) | throwError "argument {n} is not a free variable"
    id.getUserName

elab "length_nf" : conv => withMainContext do
  let tgt ← instantiateMVars (← Conv.getLhs)
  let n1 ← getNthArgName tgt 1
  let n2 ← getNthArgName tgt 2
  if n2.lt n1 then
    evalTactic (← `(tactic| rw [@length_symm _ _] ))

end Lean.Elab.Tactic

Vskutku, tohle funguje! Právě jsme definovali novou taktiku length_nf použitelnou v conv režimu. Přistupuje k uživatelským jménům argumentů a pak je vymění, pokud je ten druhý lexikograficky menší, než ten první. Všimněme si použití _ _ – správné argumenty jsou automaticky dosazeny. Taktika žije uvnitř jmenného prostoru Lean.Elab.Tactic a je slušné do něj (tj. před řádek end) umístit i všechny následující taktiky.

(Tyto řádky možná nevypadají jako raketová věda, ale bez tutoriálu jako je tento, mi trvalo několik týdnů na ně přijít. Naštěstí jsem vytrval, protože jsem neměl ponětí, do čeho jdu…)

Rozšíření na všechny výrazy

Nyní potřebujeme použít length_nf na všechny výskyty length v daném výrazu, bez ohledu na to, jak hluboko jsou vnořené. Zní to náročně, ale conv režim zachraňuje situaci, protože nám umožní zacílit výrazy s chirurgickou přesností! Můžeme ho zkombinovat s taktikou all_goals, která se snaží zabít všechny mouchy jednou následující ranou, a try, která zajišťuje, že následující taktika nikdy neselže. Když ještě přidáme shodu vzorů, zcela nová taktika perm je na světě:

macro "perm" : tactic =>
  `(tactic| try conv in (occs := *) length _ _ => all_goals length_nf)

Volání perm v taktickém režimu nyní normalizuje všechny výrazy length v cíli. Zkuste si to! Na tom, jak si proměnné v infoview mění místa, je něco nesmírně uspokojivého. (V původním projektu je perm ještě výkonnější, protože normalizuje všechna symetrická primitiva. Pro length máme pouze dvě možnosti (zaměnit nebo ne), ale pro trojúhelníky nám perm ušetří ruční výběr ze 3! možností. Trojúhelníky jsou prostě láska.)

Rozdělení konjunkcí

Ale ještě jsme neskončili. K rozdělení konjunkcí v length_sum_perm_of_B jsme mohli třináctkrát zavolat constructor (vždy následovaný taktikou pro dílčí cíl), ale teď už jsme moudřejší! Existuje taktika repeat, která opakovaně aplikuje danou taktiku, dokud neselže. Bohužel repeat constructor nepomáhá, protože po první aplikaci už nebude první nový cíl dále dělitelný. Ovšem blízký příbuzný repeat' se rekurzivně aplikuje na všechny nově vzniklé podcíle, což přesně potřebujeme. Rozdělování velkých cílů zní užitečně (i v každodenním životě), takže v rámci tréninku můžeme rovnou vytvořit vlastní taktiku splitAll:

macro "splitAll" : tactic => `(tactic | repeat' constructor)

(Všimněme si použití ; — dovolí nám řetězit taktiky v rámci jednoho řádku. Mimochodem, taky bychom mohli použít Mathlib taktiku split_ands s velmi podobným účinkem.)

Vše do sebe zapadá

Nyní se občerstvěte nějakou zdravou alternativu k popcornu a hleďte:

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
  perm
  splitAll
  all_goals
  try exact len_pos_of_neq $ ne_12_of_B Babc
  try exact len_pos_of_neq $ ne_23_of_B Babc
  try exact len_pos_of_neq $ ne_13_of_B Babc
  try exact length_sum_of_B Babc

Dost příjemný pocit, ne?

Ukazuje se ale, že tato verze perm stále není dost silná pro mnoho praktických účelů. Takže ji v příštím díle nakrmíme steroidy…

Pokud máte nějaké návrhy na vylepšení tohoto blogového příspěvku, dejte mi vědět.

Zpět