Lists of Coq tactics
This page contains a list of Coq tactics you may use during the course.
This list will be updated weekly.
- intros x: move an assumption from the goal
into the context.
- reflexivity: finish the proof in case it is of the
shape x = x.
- symmetry: change a goal of the shape
shape x = y into
shape y = x.
- rewrite H: use the equality hypothesis
H to rewrite the goal.
- simpl: simplify the goal by computation.
- unfold f: unfold a non-fixpoint function
f.
- destruct x: perform case-analysis.
- destruct x eqn:H: perform case-analysis and
record the result of the case-analysis as an equation named
H.
- induction x: perform induction.
- assert (H: X): create a sublemma named
H.
- apply H: prove a goal using a hypothesis,
lemma or constructor named H.
The variant apply H with (x:=y) can be used to
instantiate variables.
- inversion H: reason by injectivity and
distinctness of constructors of a hypothesis 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.
- split: generate a goal for each conjunct of
a conjunction.
- left and right:
prove the left or right variant of a disjunction.
- chear H: delete a hypothesis
H from the context.
- subst x:
substitute away an hypothesis H : x = e or
or e = x and delete it.
- subst:
substitute away the hypotheses H : x = e or
or e = x for any variable
x and delete these.
- rename x into y:
change the name of a hypothesis or variable.
- assumption:
try to find a hypothesis that exactly matches the goal and use it.
- contradiction:
try to find a hypothesis that is logically equivalent to False and solve the
goal using it.
- constructor:
try to apply a constructor from some Inductive definition in the current
environment.
Many of these tactics accept the modifier in H
to operate on a hypothesis rather than the goal.
Lists of Coq tacticals
- tac1 ; tac2: first performs
tac1 and then
tac2 on any subgoal generated by the first
tactic.
- repeat tac: repeatedly performs
tac until the tactic fails.
- try tac: the same as
tac, apart from the case in which
tac fails, then
try tac succesfully does nothing at all.
Lists of Coq command
- Check: prints the type of a term.
- Print: prints the definition of a term.
- Eval compute in: computes the outcome of a term.
- SearchAbout: search for lemmas or definitions.