Coq Tactics Reference

Coq Tactics Reference

Comprehensive reference for Coq tactics organized by proof situation.

Table of Contents

• Structural Tactics
• Simplification
• Induction and Cases
• Rewriting
• Automation
• Logical Reasoning
• Arithmetic

Structural Tactics

intro / intros

Introduce variables or hypotheses.

intro x.
intros x y H.
intros.  (* introduce all *)

apply <term>

Apply a theorem or hypothesis.

apply H.
apply plus_comm.
apply IHn.

exact <term>

Provide exact proof term.

exact H.

assumption

Solve goal with an existing hypothesis.

assumption.

assert (<name>: <prop>)

Prove intermediate lemma.

assert (H: n + 0 = n).
{ reflexivity. }

pose proof <term> as <name>

Add a fact to context.

pose proof (plus_comm n m) as H.

Simplification

simpl

Simplify by computation.

simpl.
simpl in H.
simpl in *.

unfold <def>

Unfold a definition.

unfold my_func.
unfold my_func in H.

fold <def>

Fold a definition (reverse of unfold).

fold my_func.

cbv / lazy / compute

Reduction strategies.

cbv.      (* call-by-value *)
lazy.     (* lazy evaluation *)
compute.  (* full computation *)

cbn

Call-by-name normalization (recommended over simpl).

cbn.
cbn in H.

Induction and Cases

induction <var>

Proof by induction.

induction n.
- (* Base case: n = 0 *)
  reflexivity.
- (* Inductive case: n = S n' *)
  (* IHn: induction hypothesis *)
  simpl. rewrite IHn. reflexivity.

Variants:

• induction n as [|n' IH] - Name the induction hypothesis
• induction n using custom_ind - Use custom induction principle

destruct <var>

Case analysis.

destruct n.
- (* Case: n = 0 *)
  reflexivity.
- (* Case: n = S n' *)
  simpl. reflexivity.

Variants:

• destruct n as [|n'] - Name the cases
• destruct n eqn:E - Remember the equation
• destruct H - Destruct a hypothesis

case <var>

Similar to destruct but less aggressive.

case n.

elim <var>

Apply elimination principle.

elim n.

Rewriting

rewrite <term>

Rewrite using an equation (left-to-right).

rewrite H.
rewrite plus_comm.
rewrite <- H.  (* right-to-left *)

Variants:

• rewrite H in H2 - Rewrite in hypothesis
• rewrite H in * - Rewrite everywhere
• rewrite H1, H2, H3 - Multiple rewrites

replace <term1> with <term2>

Replace one term with another.

replace (n + 0) with n.
- (* Prove n + 0 = n *)
  apply plus_n_O.
- (* Continue with n *)

subst

Substitute all equations of form x = t.

subst.
subst x.

reflexivity

Prove equality by computation.

reflexivity.

symmetry

Swap sides of equality.

symmetry.
symmetry in H.

transitivity <term>

Prove equality by transitivity.

transitivity (n + m).

Automation

auto

Automatic proof search.

auto.
auto with arith.
auto with *.

trivial

Solve trivial goals.

trivial.

easy

Combination of trivial tactics.

easy.

tauto

Propositional tautology solver.

tauto.

intuition

Propositional reasoning with simplification.

intuition.
intuition auto.

firstorder

First-order reasoning.

firstorder.

congruence

Equality reasoning with congruence closure.

congruence.

lia

Linear integer arithmetic (requires Require Import Lia).

lia.

nia

Non-linear integer arithmetic.

nia.

Logical Reasoning

split

Split conjunction or biconditional.

split.
- (* Prove left part *)
- (* Prove right part *)

left / right

Choose disjunction branch.

left.   (* Prove P in P \/ Q *)
right.  (* Prove Q in P \/ Q *)

exists <term>

Provide witness for existential.

exists 42.
exists (n + m).

constructor

Apply a constructor of an inductive type.

constructor.
constructor 2.  (* Apply second constructor *)

discriminate

Derive contradiction from impossible equality.

discriminate.
discriminate H.

injection

Extract equalities from constructor equality.

injection H.
injection H as H1 H2.

inversion <hyp>

Invert an inductive predicate.

inversion H.
inversion H as [x y H1 H2].
inversion H; subst.

contradiction

Derive contradiction.

contradiction.

exfalso

Prove anything from False.

exfalso.

Arithmetic

lia

Linear integer arithmetic (Require Import Lia).

lia.

nia

Non-linear integer arithmetic (Require Import Lia).

nia.

ring

Ring solver (Require Import Ring).

ring.

field

Field solver (Require Import Field).

field.

omega

Deprecated (use lia instead).

omega.

Common Proof Patterns

Pattern: Conjunction

Goal: P /\ Q

split.
- (* Prove P *)
- (* Prove Q *)

Pattern: Implication

Goal: P -> Q

intro H.
(* Now have H: P, prove Q *)

Pattern: Universal Quantification

Goal: forall x, P x

intro x.
(* Now prove P x for arbitrary x *)

Pattern: Existential Quantification

Goal: exists x, P x

exists witness.
(* Now prove P witness *)

Pattern: Disjunction

Goal: P \/ Q

left.   (* Choose to prove P *)
(* or *)
right.  (* Choose to prove Q *)

Pattern: Negation

Goal: ~ P

intro H.
(* Now have H: P, derive contradiction *)

Pattern: List Induction

Goal: forall l, P l

intro l.
induction l as [|x l' IHl'].
- (* Base case: l = [] *)
  simpl. reflexivity.
- (* Inductive case: l = x :: l' *)
  (* IHl': P l' *)
  simpl. rewrite IHl'. reflexivity.

Pattern: Natural Number Induction

Goal: forall n, P n

intro n.
induction n as [|n' IHn'].
- (* Base case: n = 0 *)
  reflexivity.
- (* Inductive case: n = S n' *)
  (* IHn': P n' *)
  simpl. rewrite IHn'. reflexivity.

Pattern: Case Analysis on Option

Goal: forall o, P o

intro o.
destruct o as [x|].
- (* Case: o = Some x *)
  simpl. reflexivity.
- (* Case: o = None *)
  simpl. reflexivity.

Pattern: Boolean Case Analysis

Goal: forall b, P b

intro b.
destruct b.
- (* Case: b = true *)
  reflexivity.
- (* Case: b = false *)
  reflexivity.

Tactic Combinators

; (semicolon)

Apply second tactic to all subgoals from first.

split; reflexivity.
induction n; simpl; auto.

try <tactic>

Try tactic, don't fail if it doesn't work.

try reflexivity.

repeat <tactic>

Repeat tactic until it fails.

repeat rewrite H.

<tactic1> || <tactic2>

Try first tactic, if fails try second.

reflexivity || auto.

<tactic>; [<tac1> | <tac2> | ...]

Apply different tactics to different subgoals.

split; [auto | reflexivity].

Advanced Tactics

generalize dependent <var>

Generalize a variable and its dependencies.

generalize dependent n.

remember <term> as <name>

Remember a complex term.

remember (n + m) as k.

clear <hyp>

Remove hypothesis from context.

clear H.
clear H1 H2.

revert <var>

Move variable back to goal (opposite of intro).

revert n.

specialize (<hyp> <args>)

Specialize a hypothesis with arguments.

specialize (H n).

f_equal

Prove equality by proving arguments equal.

f_equal.

eapply <term>

Apply with existential variables.

eapply H.

eauto

Auto with existential variables.

eauto.