`intros`

: move hyp/vars from goat to ctx`reflexivity`

: finish proof when`lhs = rhs`

in goal`apply`

: prove goal using hyp, lemma, constr.`simpl`

: simplify.`rewrite`

: use an equality in Hyp to rewrite the goal.`symmetry`

: swaps lhs and rhs`unfold`

: replace const with its rhs in goal`destruct... as...`

: case analysis.`destruct... eqn:...`

records the result of the case analysis and adds it to the context.`induction... as...`

: induction`injection`

: injectivity on equalities`discriminate`

: reason by disjointness of constructors`assert (H: e)`

: introduce a lemma locally`generalize dependent x`

: move x (and all dependencies) from ctx to goal.`apply ... in H`

: forward reasoning by applying to hyp in ctx`simpl in H.`

`rewrite ... in H`

`symmetry in H`

`unfold... in H`

`rewrite (plus_comm x y)`

applies plus_comm with the arguments x, y instantiated.`apply some_lema with (x := 42)`

applies the lemma with x instantiated as 42.

- When proving correctness of the tail recursive rev. Induct on the first list. You’ll need a lemma that generalizes over the accumulator. When trying to prove that lemma, make sure you quantify over all accumulators (So don’t intro it). This is important to be able to apply the IH.

`intros`

: Introduce variables into the context, giving them names.`simpl`

: Simplify the goal.`reflexivity`

: Prove that some expression`x`

is equal to itself.`destruct`

: Consider all possible constructors of an inductive data type, generating subgoals that need to be solved separately.`rewrite`

: Replace one side of an equation by the other.`apply`

: Suppose that the current goal is`Q`

. If`H : Q`

, then`apply H`

solves the goal. If`H : P -> Q`

, then`apply H`

replaces`Q`

by`P`

in the goal. If`H`

has multiple hypotheses,`H : P1 -> P2 -> ... -> Pn -> Q`

, then`apply H`

generates one subgoal for each`Pi`

.`induction`

: Argue by induction. It works as`destruct`

, but additionally giving us an inductive hypothesis in the inductive case.`discriminate`

: Looks for an equation between terms starting with different constructors, and solves the current goal.`revert`

: The opposite of`intros`

; removes variables and hypotheses from the context, putting them back in the goal.`clear`

: Remove hypotheses from the context (ex. needed to simplify the IH).`unfold`

: Calling`unfold foo`

expands the definition of`foo`

in the goal.`trivial`

: solves simple goals through`reflexivity`

and by looking for assumptions in the context that apply directly. If it cannot solve the goal, it does nothing.`;`

: An expression such as`foo; bar`

first calls`foo`

, then calls`bar`

on all generated subgoals. A common idiom is`foo; trivial`

, which solves the trivial subgoals and does nothing on the remaining ones.`try`

: Calling`try foo`

tries to execute`foo`

, doing nothing if`foo`

raises any errors. In particular, if`foo`

is a terminating tactic such as`discriminate`

,`try foo`

attempts to solve the goal, and does nothing if it fails.`destruct ... eqn: ...`

: Do case analysis on an expression while generating an equation.`lia`

: Short for “Linear Integer Arithmetic”; tries to solve goals that involve linear systems of inequalites on integers.`specialize`

: Instantiate a universally quantified hypothesis`assert`

: Introduce a new hypothesis in the context, requiring us to prove that it holds. The curly braces`{}`

allow us to focus on the current subgoal, like`+`

and`-`

.