Tactics Reference
Complete & detailed reference: list of tactics
summary
tactic | description |
---|---|
intros | move hypotheses/variables from goal to context |
reflexivity | finish the proof (when the goal looks like e = e) |
apply | prove goal using a hypothesis, lemma, or constructor |
apply... in H | apply a hypothesis, lemma, or constructor to a hypothesis in the context (forward reasoning) |
apply... with... | explicitly specify values for variables that cannot be determined by pattern matching |
simpl | simplify computations in the goal |
simpl in H | ... or a hypothesis |
rewrite | use an equality hypothesis (or lemma) to rewrite the goal |
rewrite ... in H | ... or a hypothesis |
symmetry | changes a goal of the form t=u into u=t |
symmetry in H | changes a hypothesis of the form t=u into u=t |
transitivity y | prove a goal x=z by proving two new subgoals, x=y and y=z |
unfold | replace a defined constant by its right-hand side in the goal |
unfold... in H | ... or a hypothesis |
destruct... as... | case analysis on values of inductively defined types |
destruct... eqn | specify the name of an equation to be added to the context, recording the result of the case analysis |
induction... as... | induction on values of inductively defined types |
injection | reason by injectivity on equalities between values of inductively defined types |
discriminate | reason by disjointness of constructors on equalities between values of inductively defined types |
assert (H | e) (or assert (e) as H) |
generalize dependent x | move the variable x (and anything else that depends on it) from the context back to an explicit hypothesis in the goal formula |
f_equal | change a goal of the form f x = f y into x = y |
exfalso | to change the goal to [False]; short of ex_falso_quodlibet |
apply
apply term
- this tactic applies to any goal
- matches the current goal against the conclusion of the type of term
- term being applied must match the goal exactly
- on successful match it returns as many subgoals as the number of non-dependent premises of the type of term
- on failure to match the goal and the conclusion is an inductive type isomorphic to a tuple type, then each component of the tuple is recursively matched to the goal in the left-to-right order.
1 2 3 4 5 6 7 |
|
apply in
apply X -> Y in H
- applied to a hypothesis
X -> Y
is some conditional statement with such form- matches H against X and, if successful, replaces it with Y.
1 2 3 4 5 6 7 8 9 |
|
discriminate
discriminate term
- two terms beginning with different constructors can never be equal
- discriminate is used on a hypothesis involving an equality between different constructors, and it solves the current goal immediately
1 2 3 4 5 6 7 |
|
injection
injection term
- constructors of inductive types are injective → if \(c\) is a constructor of an inductive type and \(c\) \(t_1\) and \(c\) \(t_2\) are equal then \(t_1\) and \(t_2\) are equal too.
- using injection H without
as
clause turns all equations into hypotheses at the beginning of the goal
1 2 3 4 5 6 |
|
simpl in
simpl in term
- performs simplification on the hypothesis
term
in the context
1 2 3 4 5 6 7 |
|
symmetry
symmetry
- applies to a goal that has the form
t = u
and changes it intou = t
1 2 3 4 5 |
|
transitivity
transitivity term
- applies to a goal that has the form
t=u
and transforms it into the two subgoalst=term
andterm=u
.
1 2 3 4 5 6 7 8 9 |
|
unfold
unfold qualid
- applies to any goal
qualid
must denote a defined transparent constant or local definition- unfold applies the \(δ\) rule to each occurrence of the constant to which
qualid
refers in the current goal and then replaces it with its \(βι\)-normal form
1 2 3 4 5 6 7 8 9 10 11 |
|