En les taules que segueixen, nom sempre fa referència a un nom que Lean ja coneix
mentre que nom_nou és un nom nou que podem escollir;
expr denota una expressió,
per exemple el nom d'un objecte en el context,
una expressió aritmètica que depèn d'aquests objectes,
una hipòtesi que tenim al context,
o un lema aplicat a qualsevol d'aquests;
proposició és una expressió de l'estil Prop (e.g. 0 < x).
Quan una d'aquestes paraules apareix dues vegades a la mateixa cel·la,
no vol dir que els noms o expressions hagin de ser les mateixes.
| Símbol lògic | Apareix a l'objectiu | Apareix en una hipòtesi |
|---|---|---|
∀ (per tot) |
intro nom_nou |
apply expr o specialize nom expr |
∃ (existeix) |
use expr |
obtain ⟨nom_nou, nom_nou⟩ := expr |
→ (implica) |
intro nom_nou |
apply expr o specialize nom expr |
↔ (si i només si) |
constructor |
rw [expr] o rw [←expr] |
∧ (i) |
constructor |
obtain ⟨nom_nou, nom_nou⟩ := expr |
∨ (o) |
left o right |
cases expr with | inl nom_nou => ... | inr nom_nou => ... |
¬ (no) |
intro nom_nou |
apply expr o specialize nom expr |
A l'esquerra de la taula següent les parts entre parèntesis són opcionals. L'efecte d'aquestes parts també està escrit entre parèntesis.
| Tàctica | Efecte |
|---|---|
exact expr |
demostra que l'objectiu es pot provar amb expr |
refine |
Igual que exact expr, però podem deixar ?_ en algunes dades i crearà nous objectius |
convert expr |
demostra l'objectiu transformant-lo en un fet ja existent expr i crea nous objectius per aquelles proposicions utilitzades en la transformació que no s'hagin demostrat automàticament |
convert_to proposition |
transforma l'objectiu en el nou objectiu proposició i crea nous objectius per aquells proposicions utilitzades en la transformació que no s'hagin demostrat automàticament |
have nom_nou : proposition |
introduceis un nom nom_nou enunciant que la proposició és certa; simultàniament, crea un nou objectiu per demostrar la proposició |
unfold nom (at hyp) |
reescriu la definició de nom a l'objectiu (o a la hipòtesi hyp) |
rw [expr] (at hyp) |
a l'objectiu (o a la hipòtesi hyp), canvia (totes es instàncies de) la part esquerra de la igualtat o equivalència expr per la part dreta |
rw [←expr] (at hyp) |
a l'objectiu (o a la hipòtesi hyp), canvia (totes es instàncies de) la part dreta de la igualtat o equivalència expr per la part esquerra |
rw [expr, expr, ←expr, ←expr, expr] |
fer diverses reescriptures l'una darrera l'altra (es pot fer servir a l'objectiu o a una hipòtesi donada; es pot alternar canvis esquerra-dreta amb dreta-esquerra) |
calc |
comença una demostració per càlcul (i.e. una successió de proposicions que, al combinar-se fent servir transitivitat, demostraran l'objectiu) |
gcongr |
TODO |
by_cases nom_nou : proposició |
trenca la demostració en dues branques segons proposició sigui cert o fals, fent servir nom_nou com el nom de la hipòtesi respecriva en cada branca |
exfalso |
aplica la regla "Fals implica qualsevol cosa", també coneguda com "ex falso quodlibet" (canvia l'objectiu a False) |
by_contra nom_nou |
comença una demostració per reducció a l'absurd, fent servir nom_nou per la hipòtesi que és la negació de l'objectiu |
push_neg (at hyp) |
simplifica les negacions a l'objectiu (o a la hipòtesi hyp),e.g. canvia ¬ ∀ x, proposició to ∃ x, ¬ proposició |
linarith |
demostra l'objectiu fent servir una combinació lineal de les hipòtesis (inclosos arguments basats en la transitivitat) |
ring |
demostra l'objectiu combinant els axiomes d'un (semi)anell commutatiu |
simp (at hyp) |
simplifica l'objectiu (o la hipòtesi hyp) combinant algunes igualtats i equivalències ja apreses |
simp? (at hyp) |
mostra quines igualtats i equivalències es farien servir per simplificar l'objectiu (o la hipòtesi hyp); dona una llista d'expressions que poden utilitzar-se dins de simp only [...] (at hyp) |
exact? |
busca un lema que demostri l'objectiu fent servir hipòtesis del context |
apply? |
busca lemes la conclusió dels quals coincideixi amb l'objectiu; suggereix aquells que es poden fer servir amb apply o refine |
rw? |
TODO |
aesop |
TODO |