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