Tactic cheat sheet. #
-- natnumgame tactics
apply,
exact (and assumption)
split
use (use use to make progress with nonempty X)
1) Extracting information from hypotheses #
1a) cases and rcases #
Many objects in Lean are pairs of data. For example, a proof
of P ∧ Q is stored as a pair consisting of a proof of P and
a proof of Q. The hypothesis ∃ n : ℕ, f n = 37 is stored
internally as a pair, namely a natural n and a proof that f n = 37.
Note that "hypothesis" and "proof" mean the same thing.
If h : X is something which is stored as a pair in Lean,
then cases h with a b will destroy h and replace it with
the two pieces of data which made up h, calling them a and b.
1b) specialize #
Say you have a long hypothesis h : ∀ n : ℕ, f n > 37 → n = 23.
This hypothesis is a function. It takes as inputs a natural number n
and a proof that f n > 37, and then it gives as output a proof
that n = 23. You can feed in some inputs and specialize the function.
Say for example you you manage to prove the hypothesis ht : f t > 37 for some natural
number t. Then specialize h t ft would change h to t = 23.
2) Making new hypothesis #
have #
The have tactic makes a new hypothesis. The proof of the current goal
is paused and a new goal is created. Generally one should now put braces
{ } because if there is more than one goal then understanding what the
code is doing can get very difficult.
3) Using hypotheses to change the goal. #
2a) rw #
The generic sub in tactic. If h : X = Y then rw h will change all
X's in the goal to Y's. Also works with h : P ↔ Q if P and Q
are true-false statements.
2b) convert #
convert is in some sense the opposite way of thinking to rw. Instead
of continually rewriting the goal until it becomes one of your assumptions,
why not just tell Lean that the assumption is basically the right answer
modulo a few loose ends, which Lean will then leave for you as new goals.