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 .