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.

- 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.

- 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.