Coq cheatsheet and gotchas

Coq resources

For help on standard Coq tactics, consult Coq's reference manual, starting from the indices. The manual can be overwhelming, so it's best used for looking up fine details.

Useful commands

Coq comes with many predefined types, functions, and theorems (“objects”). The most important commands to help you discover them are Check, About, Print, Search, and Compute. Try the following examples:

Check gives the type of any term, even with holes:

Check (1 + _).1 + ?m
     : nat
where
?m : [ |- nat]
Check (fun b => match b with true => 0 | false => 1 end).fun b : bool => if b then 0 else 1
     : bool -> nat

About gives general information about an object:

About bool.bool : Set

bool is not universe polymorphic
Expands to: Inductive Coq.Init.Datatypes.bool
About nat.nat : Set

nat is not universe polymorphic
Expands to: Inductive Coq.Init.Datatypes.nat

Print displays the definition of an object:

Print bool.Inductive bool : Set :=  true : bool | false : bool.
Print Nat.add.Nat.add =
fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end
     : nat -> nat -> nat

Arguments Nat.add (n m)%nat_scope

Search finds objects. Its syntax is very flexible:

Find functions of type nat -> nat -> bool.

Search (nat -> nat -> bool).Nat.testbit: nat -> nat -> bool
Nat.leb: nat -> nat -> bool
Nat.ltb: nat -> nat -> bool
RingMicromega.ge_bool: nat -> nat -> bool
Init.Nat.testbit: nat -> nat -> bool
Init.Nat.ltb: nat -> nat -> bool
Nat.eqb: nat -> nat -> bool
Init.Nat.eqb: nat -> nat -> bool
Init.Nat.leb: nat -> nat -> bool
Nat.testbit_eqf:
  Morphisms.Proper (Morphisms.respectful eq Nat.eqf)
    Nat.testbit
Nat.eqb_compat:
  Morphisms.Proper
    (Morphisms.respectful eq
       (Morphisms.respectful eq eq)) Nat.eqb
Nat.testbit_wd:
  Morphisms.Proper
    (Morphisms.respectful eq
       (Morphisms.respectful eq eq)) Nat.testbit
(use "About" for full details on the implicit
 arguments of Nat.eqb_compat)

Find theorems about || in module Nat.

Search "||" inside Nat.Nat.orb_even_odd:
  forall n : nat,
  (Nat.even n || Nat.odd n)%bool = true
Nat.even_mul:
  forall n m : nat,
  Nat.even (n * m) = (Nat.even n || Nat.even m)%bool
Nat.lor_spec:
  forall a b n : nat,
  Nat.testbit (Nat.lor a b) n =
  (Nat.testbit a n || Nat.testbit b n)%bool
Nat.PrivateImplementsBitwiseSpec.lor_spec:
  forall a b n : nat,
  Nat.testbit (Nat.lor a b) n =
  (Nat.testbit a n || Nat.testbit b n)%bool
Nat.setbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.setbit a n) m =
  ((n =? m) || Nat.testbit a m)%bool
Nat.add3_bits_div2:
  forall a0 b0 c0 : bool,
  (Nat.b2n a0 + Nat.b2n b0 + Nat.b2n c0) / 2 =
  Nat.b2n (a0 && b0 || c0 && (a0 || b0))
Nat.add_carry_div2:
  forall (a b : nat) (c0 : bool),
  (a + b + Nat.b2n c0) / 2 =
  a / 2 + b / 2 +
  Nat.b2n
    (Nat.testbit a 0 && Nat.testbit b 0
     || c0 && (Nat.testbit a 0 || Nat.testbit b 0))

Find theorems about subtraction and equality whose name contains _distr.

Search eq "-" "_distr".Nat.sub_add_distr:
  forall n m p : nat, n - (m + p) = n - m - p
Nat.sub_min_distr_r:
  forall n m p : nat,
  Nat.min (n - p) (m - p) = Nat.min n m - p
Nat.mul_sub_distr_r:
  forall n m p : nat, (n - m) * p = n * p - m * p
Nat.sub_max_distr_r:
  forall n m p : nat,
  Nat.max (n - p) (m - p) = Nat.max n m - p
Nat.mul_sub_distr_l:
  forall n m p : nat, p * (n - m) = p * n - p * m
Nat.sub_max_distr_l:
  forall n m p : nat,
  Nat.max (p - n) (p - m) = p - Nat.min n m
Nat.sub_min_distr_l:
  forall n m p : nat,
  Nat.min (p - n) (p - m) = p - Nat.max n m
Nat.sub_sub_distr:
  forall n m p : nat,
  p <= m -> m <= n -> n - (m - p) = n - m + p

Search for a lemma proving the symmetry of =.

Search (?x = ?y -> ?y = ?x).eq_sym: forall [A : Type] [x y : A], x = y -> y = x
EqdepFacts.internal_eq_sym_internal0:
  forall [A : Type] [x y : A], x = y -> y = x
EqdepFacts.internal_eq_sym_internal:
  forall [A : Type] [x y : A], x = y -> y = x

If you are puzzled by a notation, the Locate command can help:

Locate "*".Notation "x * y" := (Init.Nat.mul x y) : nat_scope
  (default interpretation)
Notation "x * y" := (prod x y) : type_scope

To evaluate an expression, use Compute:

Compute (2 * 3, 4 + 4, 0 - 2 + 2, pred (S (S (S 0)))).= (6, 8, 2, 2)
: nat * nat * nat * nat

Syntax recap

To define a function inline, use fun:

Check (fun x => x + 1).fun x : nat => x + 1
     : nat -> nat
Check (fun x: bool => xorb x x).fun x : bool => xorb x x
     : bool -> bool

To perform a case analysis on a value, use match:

Check (fun b (x y: nat) =>
         match b with
         | true => x
         | false => y
         end).fun (b : bool) (x y : nat) => if b then x else y
     : bool -> nat -> nat -> nat

Check (fun (n: nat) =>
         match n with
         | 0 => 1
         | S n => n
         end).fun n : nat => match n with
               | 0 => 1
               | S n0 => n0
               end
     : nat -> nat

In Coq, if is just short for match:

Check (fun (b: bool) (x y: nat) =>
         if b then x else y).fun (b : bool) (x y : nat) => if b then x else y
     : bool -> nat -> nat -> nat

To define a global object, use Definition or Lemma (Theorem is an alias of Lemma):

Definition choose (b: bool) (x y: nat) :=
  if b then x else y.

Compute (choose true 6 512).= 6
: nat

Lemma plus_commutes :
  forall x, x = x + 0 + 0.forall x : nat, x = x + 0 + 0
Proof.forall x : nat, x = x + 0 + 0
  intros.x: nat
x = x + 0 + 0
  Search (_ + 0).Nat.add_0_r: forall n : nat, n + 0 = n
plus_n_O: forall n : nat, n = n + 0
x: nat
x = x + 0 + 0
  rewrite Nat.add_0_r.x: nat
x = x + 0
  rewrite Nat.add_0_r.x: nat
x = x
  reflexivity.
Qed.

Recursive functions use the keyword Fixpoint:

Fixpoint do_n_times
         (ntimes: nat) (step: nat -> nat) (start_from: nat) :=
  match ntimes with
  | 0 => start_from
  | S ntimes' => step (do_n_times ntimes' step start_from)
  end.

Compute (6, do_n_times 12 (fun x => x + 65) 42).= (6, 822)
: nat * nat

You can use bullets or braces to structure your proofs:

Lemma both_zero:
  forall x y z: nat, x + y + z = 0 -> x = 0 /\ y = 0 /\ z = 0.forall x y z : nat,
x + y + z = 0 -> x = 0 /\ y = 0 /\ z = 0
Proof.forall x y z : nat,
x + y + z = 0 -> x = 0 /\ y = 0 /\ z = 0
  destruct x.forall y z : nat,
0 + y + z = 0 -> 0 = 0 /\ y = 0 /\ z = 0
x: nat
forall y z : nat,
S x + y + z = 0 -> S x = 0 /\ y = 0 /\ z = 0
  -forall y z : nat,
0 + y + z = 0 -> 0 = 0 /\ y = 0 /\ z = 0 destruct y.forall z : nat,
0 + 0 + z = 0 -> 0 = 0 /\ 0 = 0 /\ z = 0
y: nat
forall z : nat,
0 + S y + z = 0 -> 0 = 0 /\ S y = 0 /\ z = 0
    {forall z : nat,
0 + 0 + z = 0 -> 0 = 0 /\ 0 = 0 /\ z = 0 intros z Heq; simpl in *.z: nat
Heq: z = 0
0 = 0 /\ 0 = 0 /\ z = 0
      rewrite Heq; split.z: nat
Heq: z = 0
0 = 0
z: nat
Heq: z = 0
0 = 0 /\ 0 = 0
      -z: nat
Heq: z = 0
0 = 0 reflexivity.
      -z: nat
Heq: z = 0
0 = 0 /\ 0 = 0 split; reflexivity. }y: nat
forall z : nat,
0 + S y + z = 0 -> 0 = 0 /\ S y = 0 /\ z = 0
    {y: nat
forall z : nat,
0 + S y + z = 0 -> 0 = 0 /\ S y = 0 /\ z = 0 intros z Heq.y, z: nat
Heq: 0 + S y + z = 0
0 = 0 /\ S y = 0 /\ z = 0
      simpl in *.y, z: nat
Heq: S (y + z) = 0
0 = 0 /\ S y = 0 /\ z = 0
      congruence. }
  -x: nat
forall y z : nat,
S x + y + z = 0 -> S x = 0 /\ y = 0 /\ z = 0 intros y z Heq.x, y, z: nat
Heq: S x + y + z = 0
S x = 0 /\ y = 0 /\ z = 0
    simpl in *.x, y, z: nat
Heq: S (x + y + z) = 0
S x = 0 /\ y = 0 /\ z = 0
    congruence.
Qed.

A few gotchas

Natural numbers saturate at 0:

Compute (3 - 5 + 3).= 3
: nat

The order in which you perform induction on variables matters: if x comes before y and you do induction on y, your induction hypothesis will not be general enough.

Lemma add_comm:
  forall x y: nat, x + y = y + x.forall x y : nat, x + y = y + x
Proof.forall x y : nat, x + y = y + x
  induction y.x: nat
x + 0 = 0 + x
x, y: nat
IHy: x + y = y + x
x + S y = S y + x
  -x: nat
x + 0 = 0 + x induction x.0 + 0 = 0 + 0
x: nat
IHx: x + 0 = 0 + x
S x + 0 = 0 + S x
    +0 + 0 = 0 + 0 reflexivity.
    +x: nat
IHx: x + 0 = 0 + x
S x + 0 = 0 + S x simpl in *.x: nat
IHx: x + 0 = x
S (x + 0) = S x
      rewrite IHx.x: nat
IHx: x + 0 = x
S x = S x
      reflexivity.
  -x, y: nat
IHy: x + y = y + x
x + S y = S y + x simpl.x, y: nat
IHy: x + y = y + x
x + S y = S (y + x)

Here, IHy is valid only for one specific y.

   Abort.

   Lemma add_comm:
     forall x y: nat, x + y = y + x.forall x y : nat, x + y = y + x
   Proof.forall x y : nat, x + y = y + x
     induction x.forall y : nat, 0 + y = y + 0
x: nat
IHx: forall y : nat, x + y = y + x
forall y : nat, S x + y = y + S x
     -forall y : nat, 0 + y = y + 0 induction y.0 + 0 = 0 + 0
y: nat
IHy: 0 + y = y + 0
0 + S y = S y + 0
       +0 + 0 = 0 + 0 reflexivity.
       +y: nat
IHy: 0 + y = y + 0
0 + S y = S y + 0 simpl in *.y: nat
IHy: y = y + 0
S y = S (y + 0)
         rewrite <- IHy.y: nat
IHy: y = y + 0
S y = S y
         reflexivity.
     -x: nat
IHx: forall y : nat, x + y = y + x
forall y : nat, S x + y = y + S x intros; simpl.x: nat
IHx: forall y : nat, x + y = y + x
y: nat
S (x + y) = y + S x

Here, IHx starts with forall y.

   Abort.

Here's an example where this subtlety matters:

Fixpoint factorial (n: nat) :=
  match n with
  | O => 1
  | S n' => n * factorial n'
  end.

Fixpoint factorial_acc (n: nat) (acc: nat) :=
  match n with
  | O => acc
  | S n' => factorial_acc n' (n * acc)
  end.

First attempt, but our lemma is too weak:

Lemma factorial_acc_correct:
  forall n, factorial n = factorial_acc n 1.forall n : nat, factorial n = factorial_acc n 1
Proof.forall n : nat, factorial n = factorial_acc n 1
  induction n.factorial 0 = factorial_acc 0 1
n: nat
IHn: factorial n = factorial_acc n 1
factorial (S n) = factorial_acc (S n) 1
  -factorial 0 = factorial_acc 0 1 simpl.1 = 1
    reflexivity.
  -n: nat
IHn: factorial n = factorial_acc n 1
factorial (S n) = factorial_acc (S n) 1 simpl.n: nat
IHn: factorial n = factorial_acc n 1
factorial n + n * factorial n =
factorial_acc n (S (n * 1))
    Search (_ * 1).Nat.mul_1_r: forall n : nat, n * 1 = n
n: nat
IHn: factorial n = factorial_acc n 1
factorial n + n * factorial n =
factorial_acc n (S (n * 1))
    rewrite Nat.mul_1_r.n: nat
IHn: factorial n = factorial_acc n 1
factorial n + n * factorial n = factorial_acc n (S n)

Stuck! We have no way to simplify factorial_acc n (S n).

Abort.

Second attempt: a generalized lemma, but we put the acc first, so induction will not generalize it.

Lemma factorial_acc_correct:
  forall acc n, factorial n * acc = factorial_acc n acc.forall acc n : nat,
factorial n * acc = factorial_acc n acc
Proof.forall acc n : nat,
factorial n * acc = factorial_acc n acc
  induction n.acc: nat
factorial 0 * acc = factorial_acc 0 acc
acc, n: nat
IHn: factorial n * acc = factorial_acc n acc
factorial (S n) * acc = factorial_acc (S n) acc
  -acc: nat
factorial 0 * acc = factorial_acc 0 acc simpl.acc: nat
acc + 0 = acc
    rewrite Nat.add_0_r.acc: nat
acc = acc
    reflexivity.
  -acc, n: nat
IHn: factorial n * acc = factorial_acc n acc
factorial (S n) * acc = factorial_acc (S n) acc simpl.acc, n: nat
IHn: factorial n * acc = factorial_acc n acc
(factorial n + n * factorial n) * acc =
factorial_acc n (acc + n * acc)
    Fail rewrite <- IHn.The command has indeed failed with message:
Found no subterm matching "factorial_acc n acc"
in the current goal.
acc, n: nat
IHn: factorial n * acc = factorial_acc n acc
(factorial n + n * factorial n) * acc =
factorial_acc n (acc + n * acc)

Stuck! IHn is too weak.

Abort.

Third time's the charm! Note how we ordered n and acc.

Lemma factorial_acc_correct:
  forall n acc, factorial n * acc = factorial_acc n acc.forall n acc : nat,
factorial n * acc = factorial_acc n acc
Proof.forall n acc : nat,
factorial n * acc = factorial_acc n acc
  induction n.forall acc : nat,
factorial 0 * acc = factorial_acc 0 acc
n: nat
IHn: forall acc : nat, factorial n * acc = factorial_acc n acc
forall acc : nat,
factorial (S n) * acc = factorial_acc (S n) acc
  -forall acc : nat,
factorial 0 * acc = factorial_acc 0 acc intros.acc: nat
factorial 0 * acc = factorial_acc 0 acc
    simpl.acc: nat
acc + 0 = acc
    rewrite Nat.add_0_r.acc: nat
acc = acc
    reflexivity.
  -n: nat
IHn: forall acc : nat, factorial n * acc = factorial_acc n acc
forall acc : nat,
factorial (S n) * acc = factorial_acc (S n) acc intros.n: nat
IHn: forall acc : nat, factorial n * acc = factorial_acc n acc
acc: nat
factorial (S n) * acc = factorial_acc (S n) acc
    simpl.n: nat
IHn: forall acc : nat, factorial n * acc = factorial_acc n acc
acc: nat
(factorial n + n * factorial n) * acc =
factorial_acc n (acc + n * acc)

IHn is strong enough now!

    rewrite <- IHn.n: nat
IHn: forall acc : nat, factorial n * acc = factorial_acc n acc
acc: nat
(factorial n + n * factorial n) * acc =
factorial n * (acc + n * acc)
    lia.
Qed.