Skip to content

Latest commit

 

History

History
51 lines (47 loc) · 10.1 KB

README-CAT.md

File metadata and controls

51 lines (47 loc) · 10.1 KB

Tàctiques Lean 4 per principiants

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