Coq Cheatsheet: Tools and Tactics for Goal Solving
Interactive reference
A quick, clickable reference to common Coq tactics. Pick a group below, then expand any card for a worked example and explanation. Tactics run from everyday building blocks to heavier proof automation.
Tactic reference
The everyday moves: get hypotheses into scope, apply what you know, and rewrite toward the goal.
introsIntroduce hypotheses and variables into the context
Theorem symmetry_eq : forall a b : nat, a = b -> b = a.
Proof. intros a b H. apply H. Qed.
Introduces variables a, b, and hypothesis H into the proof context.
applyApply a theorem, lemma, or hypothesis
Theorem trans_eq : forall a b c : nat, (a = b) -> (b = c) -> (a = c).
Proof. intros a b c H1 H2. apply H1. apply H2. Qed.
apply uses the hypotheses H1 and H2 to discharge the goal.
rewriteRewrite a goal using a hypothesis or theorem
Theorem rewrite_example : forall a b c : nat, (a = b) -> (a + c = b + c).
Proof. intros a b c H. rewrite -> H. reflexivity. Qed.
rewrite -> H replaces a in the goal with b using hypothesis H.
reflexivityProve a goal of the form a = a
Lemma use_reflexivity : forall x : Set, x = x.
Proof. intro. reflexivity. Qed.Closes any goal where both sides are definitionally equal.
assumptionClose a goal that already appears in the context
Lemma p_implies_p : forall P : Prop, P -> P.
Proof. intros P P_holds. assumption. Qed.
Once P_holds is in context, assumption finds it and closes the goal.
Tactics that mirror the shape of logical connectives — conjunction, disjunction, and existentials.
splitSplit a conjunction into two separate goals
split.
Turns a goal A /\ B into two subgoals, A and B.
left / rightProve a disjunction by choosing one side
left. (* prove the A in A \/ B *)
right. (* prove the B in A \/ B *)
Commits the proof of A \/ B to one disjunct.
existsProvide a witness for an existential quantifier
exists x.
Supplies a concrete witness x for a goal of the form exists y, P y.
Heavier machinery for reasoning about inductive structure and case analysis.
inductionApply induction on a variable
induction n.
Generates a base case and an inductive step, with an induction hypothesis for n.
inversionDerive information from equality of inductive types
inversion H.
Extracts the constraints that must hold for H to be well-typed, discharging impossible cases.
destructCase analysis on a variable or hypothesis
destruct n.
Splits the proof into one subgoal per constructor of n.
Where to go next
This is a starting point, not the whole story. The real fluency comes from
combining these tactics — chaining with ;, automating with auto and
lia, and reading the proof state after each step. Fire up a Coq session and
experiment: the proof state is the best teacher.