Coq Cheatsheet: Tools and Tactics for Goal Solving
Introduction
This cheatsheet provides a quick reference to various tools and tactics in Coq, accompanied by examples to illustrate their usage in solving goals.
Basic Tactics
intros
Usage: Introduce hypotheses and variables into the context.
Example: Proving symmetry in equality.
Theorem symmetry_eq : forall a b : nat, a = b -> b = a. Proof. intros a b H. apply H. Qed.
This theorem states that if (a = b), then (b = a). The intros tactic introduces variables a, b, and hypothesis H into the proof context.
apply
Usage: Apply a theorem, lemma, or hypothesis.
Example: Using transitivity of equality.
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.
Here, apply is used to use the hypotheses H1 and H2 in the proof.
rewrite
Usage: Rewrite a goal using a hypothesis or theorem.
Example: Demonstrating rewriting.
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 rewrites a in the goal with b, using hypothesis H.
## reflexivity
Usage: Prove a goal of the form a = a.
Example:
Lemma use_reflexivity:
(* Simple theorem, x always equals x *)
forall x: Set, x = x.
Proof.
(* Introduce variables/hypotheses *)
intro.
reflexivity.
Qed.
assumption
Usage: When the goal is already in the context, you can use assumption to prove it.
Example:
Lemma p_implies_p : forall P : Prop,
(* P implies P is always true *)
P -> P.
Proof.
(* We can specify names for introduced variables/hypotheses *)
intros P P_holds.
assumption.
Qed.
After introducing the hypothesis P_holds (stating that P is true) into the context, we can use assumption to complete the proof.
Logical Tactics
split
Usage: Split a conjunction into two separate goals.
Example:
split.
left / right
Usage: Prove a disjunction by proving one of its parts.
Example:
left.
exists
Usage: Provide a witness for an existential quantifier.
Example:
exists x.
Advanced Tactics
induction
Usage: Apply induction on a variable.
Example:
induction n.
inversion
Usage: Derive information from equality of inductive types.
Example:
inversion H.
destruct
Usage: Case analysis on a variable or hypothesis.
Example:
destruct n.
Conclusion
This cheatsheet offers a glimpse into the powerful tactics at your disposal in Coq. Experimenting with these tactics will deepen your understanding and proficiency in proof construction.