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 |