V následujících tabulkách vždy jmeno označuje jméno, které už Lean zná,
zatímco pojmenovani je nové jméno (právě poskytnuté);
term je libovolný výraz,
například jméno známého termu,
funkce aplikovaná na term,
aritmetický výraz,
předpoklad z lokálního kontextu,
nebo nějaké lemma aplikované na cokoliv z toho;
tvrzeni je term typu Prop (například 0 < x).
Když se některé z těchto slov objeví v jedné buňce vícekrát,
jednotlivé výskyty označují odlišná jména nebo výrazy.
Následující tabulka ukazuje, jak typicky reagujeme na který logický symbol v závislosti na jeho umístění (v čele cíle nebo v čele předpokladu).
| Logický symbol | V cíli | V předpokladu |
|---|---|---|
∀ (pro každé) |
intro pojmenovani |
apply term nebo specialize jmeno term |
∃ (existuje) |
use term |
obtain ⟨pojmenovani, pojmenovani⟩ := term |
→ (implikuje) |
intro pojmenovani |
apply term nebo specialize jmeno term |
↔ (právě tehdy když) |
constructor |
rw [term] nebo rw [←term] |
∧ (AND) |
constructor |
obtain ⟨pojmenovani, pojmenovani⟩ := term |
∨ (OR) |
left nebo right |
cases term with | inl pojmenovani => ... | inr pojmenovani => ... |
¬ (NOT) |
intro pojmenovani |
apply term nebo specialize jmeno term |
Závorky v levém sloupci označují volitelné části. Účinek těchto částí je v pravém sloupci také napsán v závorkách.
| Taktika | Co dělá |
|---|---|
exact term |
cíl je splněn pomocí term |
convert term |
dokaž cíl tím, že ho převedeš na již známý fakt term, a vytvoř pomocné cíle pro ty transformace použité k převodu, které nebyly dokázány automaticky |
convert_to tvrzeni |
dokaž cíl tím, že ho převedeš na jiný cíl tvrzeni, a vytvoř dodatečné cíle pro ty transformace použité k převodu, které nebyly dokázány automaticky |
have pojmenovani : tvrzeni |
přidej do kontextu předpoklad pojmenovani, který tvrdí tvrzeni, a zároveň vytvoř a zaměř nový cíl dokázat tvrzeni |
unfold jmeno (at hyp) |
rozbal definici jmeno v cíli (nebo v předpokladu hyp) |
rw [term] (at hyp) |
v cíli (nebo v předpokladu hyp) nahraď všechny výskyty levé strany rovnosti nebo ekvivalence term za její pravou stranu |
rw [←term] (at hyp) |
v cíli (nebo v předpokladu hyp) nahraď všechny výskyty pravé strany rovnosti nebo ekvivalence term za její levou stranu |
rw [term, term, ←term, ←term, term] |
proveď několik přepisů v řadě za sebou (opět může být použito v cíli i v předpokladu; libovolná podmnožina term může být provedena zprava doleva) |
by_cases pojmenovani : tvrzeni |
rozlož důkaz na dvě větve podle toho, jestli tvrzeni je splněn nebo ne, kde pojmenovani označuje kýženou hypotézu v obou větvích |
exfalso |
použij pravidlo "ze sporu plyne cokoliv" neboli "ex falso quodlibet" (nahradí současný cíl za False) |
by_contra pojmenovani |
zahaj důkaz sporem, kde pojmenovani bude jméno pro předpoklad, který je negací cíle |
push_neg (at hyp) |
posuň negace směrem „dovnitř“ v cíli (nebo v předpokladu hyp),například změň ¬ ∀ x, tvrzeni na ∃ x, ¬ tvrzeni |
linarith |
dokaž cíl pomocí lineární kombinace předpokladů (zahrnuje argumenty z tranzitivity (ne)rovností) |
ring |
dokaž cíl pomocí vlastností sčítání, odčítání, násobení a mocnin |
simp (at hyp) |
zjednoduš cíl (nebo předpoklad hyp) pomocí nějaké kombinace známých rovností a ekvivalencí |
simp? (at hyp) |
ukaž, které rovnosti a ekvivalence by mohly být použity ke zjednodušení cíle (nebo předpokladu hyp); dej seznam výrazů, které mohou být použity uvnitř simp only [...] (at hyp) |
exact? |
najdi v knihovně (navíc s využitím lokálního kontextu) lemma, které uzavře cíl |