Tactic

Explanation

intros m n

Introduces variables into the context

generalize dependent n

Quantifies over n and anything that depends on it

simpl [in H]

Simplifies the goal, where possible

"in H" simplifies the hypothesis H

"in *" simplifies the goal and all hypotheses

apply H

Matches the hypothesis/lemma H with the goal

rewrite -> H [in H’]

Given a hypothesis H of the form "x=y", replaces x with y.

"<-" reverses the order

destruct x as [m|n] eqn:E

Case analysis on x.

"as.. " names the variables that appear

"Eqn:E" remembers the given case as E

induction x as [m|n IH] eqn:E

Like destruct but adds an inductive hypothesis for the inductive cases.

inversion H x as [m|n IH]

Like destruct but doesn’t throw out information, solves cases that fail to match.

injection (H) [as (H’)]

Removes constructors K from the hypothesis "H : K m = K n"

remember x as y eqn:E

Adds a new variable y into the context, remembering (E:x=y).

assert (H : P)

Adds P as a new subgoal. Once P is proven, adds it as the hypothesis H.

symmetry [in (H)]

Replaces "x = y" with "y = x"

discriminate (H)

If H has the form "J m = K n", where J and K are different constructors, solves the goal

contradict (H)

Replaces the goal with the negation of H (most useful when (H : ~P))

Tactic

shorthand for

apply to

reflexivity

apply eq_refl

x = y

split

apply conj

P /\ Q

left/right

apply or_introl/orintror

P \/ Q

exists x

apply (ex_intro _ x)

exists y, P