Coq Tactics

These are a set of Coq tactics that I’ve learned while completing the various courses and solving the software foundation book.

  • intros : This is the first tactic that is used to introduce the working variables the in the current environement.

  • simpl : This simplifies the current expression, breaks down the complex defitions to simplest terms

  • unfold : This unfolds a definition previously defined for the current state in the the current expression term.

  • rewrite : Rewrites the expression using a previous definition or a hypotheses.

  • inversion : Reproduces the hypotheses’s forming condition and hence helping to solve the current expression state.

  • assumption : Solves the program state using a hypothesis or a definition available in that programming environment.

  • reflexivity : Uses mathematical reflexivity property to show equality

  • auto : Solves some easy proofs.

  • exact : Solves a goal the exact proof term that proves the goal is known.

  • contradiction : Solves any goal if the context contains False or contradictory hypotheses in current proof environment.

  • left/right : replaces the goal of disjunction with either one.

  • split : produces 2 subgoals of a conjuction term.

  • destruct : Generates a subgoal for every constructor of an inductive type.

  • induction : It generates a subgoal for every constructor of an inductive type and provides an induction hypothesis for recursively defined constructors.

Lastly, you can define your own tactic using the Ltac .