1 Introduction

This cheatsheet provides a quick reference to various tools and tactics in Coq, accompanied by examples to illustrate their usage in solving goals.

2 Basic Tactics

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

2.2 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 and in the proof.

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

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

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

After introducing this hypothesis, P_holds (stating that P is true) into the context, we can use assumption to complete the proof:

Lemma p_implies_p : forall P : Prop,
    P -> P.
Proof.
    intros P P_holds.
    assumption.
Qed.

3 Logical Tactics

3.1 split

Usage: Split a conjunction into two separate goals.
Example:

split.

3.2 left / right

Usage: Prove a disjunction by proving one of its parts.
Example:

left.

3.3 exists

Usage: Provide a witness for an existential quantifier.
Example:

exists x.

4 Advanced Tactics

4.1 induction

Usage: Apply induction on a variable.
Example:

induction n.

4.2 inversion

Usage: Derive information from equality of inductive types.
Example:

inversion H.

4.3 destruct

Usage: Case analysis on a variable or hypothesis.
Example:

destruct n.

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