simpl |
|
Simplifies the goal |
destruct |
x |
Considers all possible constructors of the term x, generating subgoals that need to be solved separately. |
|
x eqn:eq |
Destructs x, remembers which constructor is being considered in the equality hypothesis eq. |
induction |
x as [ | n1 IH1 | n2 IH2 | ...] | Same as destruct but adds an inductive hypothesis to inductively defined cases. Names the variables and inductive hypotheses generated by induction with the given names. |
rewrite |
H |
Where H is of type e1 = e2, replaces e1 in the goal with e2. |
|
<- H |
Replaces e2 with e1 |
apply |
H |
Uses lemma or hypothesis H to solve the goal. If H has hypotheses, adds them as new goals. |
|
PQ in HP |
Allows us to conclude Q from hypotheses P -> Q and P. (In logic, modus ponens.) |
inversion |
H |
If hypothesis H states that e1 = e2, where e1 and e2 are expressions that start with different constructors, then inversion H completes the current subgoal. If they start with the same constructor, it generates hypotheses relating the subterms. |
assert |
H : P |
Adds a new hypothesis H that P is true to the goal. Adds the new subgoal P as the current goal. |
Tactic |
Effect |
reflexivity |
Solves a goal of the form x = x. |
assumption |
If we have a hypothesis that is equal to the goal, solves the goal. |
discriminate |
If we have a contradictory hypothesis involving an equality, solves the goal. (A special case of the logical ex falso quodlibet.) |
contradiction |
If we have a contradictory hypothesis not involving an equality, solves the goal. (A special case of the logical ex falso quodlibet.) |
trivial |
Checks if the goal is trivially true or equivalent to a hypothesis, solves if so. Otherwise, does nothing (does not fail). |
auto |
Tries a collection of basic tactics to solve the goal. Otherwise, does nothing (does not fail). |
congruence |
A powerful automation technique that subsumes reflexivity, assumption, discriminate and contradiction. |
omega |
Solves arithmetic equations over natural numbers. |
lia |
A more powerful sibling of omega. |
Note that these are often special cases and simplifications. Click through to the Coq documentation for a description of the tactics' general behavior and underlying theory.