Yet Another Coq Tactic Index (Pre-Alpha)

Inverted Tactic Index #

This section is organized according to a combination of proof state and intention rather than tactic names.

Solving based on the shape of the goal

If you want to solve the goal that is a true equality. I.e., the goal has the form ‹t› = ‹u› and both ‹t› and ‹u› are equal syntactically after some computation... use reflexivity.
If you want to solve or reduce the goal because the goal could be constructed by a constructor... use constructor.

Solving by absurdity

If you want to solve any goal because the context contains a false equality due to mismatched constructors after some computation... use discriminate.

Uncategorized

If you want to solve the goal that existed already in the context after some computation... use assumption.
If you want to solve the goal because the goal is ‹term›... use apply.

Tactic Index #

This section is organized according to tactic names.

reflexivity

Use it when: you want to solve the goal that is a true equality. I.e., the goal has the form ‹t› = ‹u› and both ‹t› and ‹u› are equal syntactically after some computation.
Additional description: The tactic calls intros automatically before the actual solve.

In this example we will apply reflexivity to prove that for every natural number $x$, if $1 = 1$ then $(3 + 2) + x = (2 + 3) + x$.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
Lemma complex_math :
  forall (x : nat),
    1 = 1 ->
    (3 + 2) + x = (2 + 3) + x.
Proof.
  intros.
  reflexivity.
  (* reflexivity alone
     (without intros) also works *)
Qed.
1

1
2
3
4
1 subgoal (ID 5)

  ============================
  forall x : nat, 1 = 1 -> 3 + 2 + x = 2 + 3 + x
1
2
3
4
1 subgoal (ID 5)

  ============================
  forall x : nat, 1 = 1 -> 3 + 2 + x = 2 + 3 + x
1
2
3
4
5
6
1 subgoal (ID 7)

  x : nat
  H : 1 = 1
  ============================
  3 + 2 + x = 2 + 3 + x
1
No more subgoals.
1
2
3
4
No more subgoals.


complex_math is defined

Note that while Coq can compute concrete values, making it possible to reason that both (3 + 2) + x and (2 + 3) + x reduce to 5 + x and therefore are equal, it cannot compute non-concrete values. Hence, reflexivity can’t prove the goal that needs non-trivial reasoning, like commutativity of natural numbers that involves non-concrete values.

1
2
3
4
5
Lemma commutativity_is_not_trivial :
  forall (x : nat), 1 + x = x + 1.
Proof.
  intros.
  reflexivity.
1

1
2
3
4
1 subgoal (ID 3)

  ============================
  forall x : nat, 1 + x = x + 1
1
2
3
4
1 subgoal (ID 3)

  ============================
  forall x : nat, 1 + x = x + 1
1
2
3
4
5
1 subgoal (ID 4)

  x : nat
  ============================
  1 + x = x + 1
1
2
3
4
5
6
Toplevel input, characters 2-13:
>   reflexivity
>   ^^^^^^^^^^^
Error: In environment
x : nat
Unable to unify "x + 1" with "1 + x".

The above lemma can be proven by performing an induction on x, or by applying lemmas like Nat.add_comm.

Relevant tactics:

  • Equivalent to exact eq_refl.
  • Equivalent to apply eq_refl.

assumption

Usage: assumption
Use it when: you want to solve the goal that existed already in the context after some computation.

In this example we will use assumption to prove that if $x = (1 + 2) + y$, then $x = 3 + y$.

1
2
3
4
5
6
7
8
9
Lemma another_complex_math :
  forall (x y : nat),
    x = (1 + 2) + y ->
    x = 3 + y.
Proof.
  intros.
  assumption.
  (* Use "H: x = 1 + 2 + y" *)
Qed.
1

1
2
3
4
1 subgoal (ID 5)

  ============================
  forall x y : nat, x = 1 + 2 + y -> x = 3 + y
1
2
3
4
1 subgoal (ID 5)

  ============================
  forall x y : nat, x = 1 + 2 + y -> x = 3 + y
1
2
3
4
5
6
1 subgoal (ID 8)

  x, y : nat
  H : x = 1 + 2 + y
  ============================
  x = 3 + y
1
No more subgoals.
1
2
3
4
No more subgoals.


another_complex_math is defined

Relevant tactics:

  • Equivalent to exact ‹H›. where ‹H› is a hypothesis in the context that matches the goal.
  • Equivalent to apply ‹H›.

discriminate

Use it when: you want to solve any goal because the context contains a false equality due to mismatched constructors after some computation.
Additional description: The tactic calls intros automatically before the actual solve.

In this example we will use discriminate to prove that for any natural $y$, if $1 = 2 + y$, then any proposition is true. Of course, the premise can’t be true because the lowest possible value of $y$ is $0$, and even then $1 < 2 + 0$.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
Lemma mismatch_proves_anything :
  forall (y : nat) (P : Prop),
    1 = 2 + y -> P.
Proof.
  intros.
  discriminate.
  (* Use "H: 1 = 2 + y" *)
  (* discriminate alone
     (without intros) also works *)
Qed.
1

1
2
3
4
1 subgoal (ID 3)

  ============================
  forall (y : nat) (P : Prop), 1 = 2 + y -> P
1
2
3
4
1 subgoal (ID 3)

  ============================
  forall (y : nat) (P : Prop), 1 = 2 + y -> P
1
2
3
4
5
6
7
1 subgoal (ID 6)

  y : nat
  P : Prop
  H : 1 = 2 + y
  ============================
  P
1
No more subgoals.
1
2
3
4
No more subgoals.


mismatch_proves_anything is defined

The reason that discriminate works in the above example is that 1 is a shorthand for S O, and 2 + y is a shorthand for S (S O) + y which computes (by definition of +) to S (S y), and the highlighted constructors are mismatched.

The example below fails because there’s no immediate mismatched constructors.

1
2
3
4
5
6
7
8
Lemma discriminate_does_not_work_here :
  forall (x : nat),
    x = 3 ->
    x = 1 ->
    true = false.
Proof.
  intros.
  discriminate.
1

1
2
3
4
1 subgoal (ID 7)

  ============================
  forall x : nat, x = 3 -> x = 1 -> true = false
1
2
3
4
1 subgoal (ID 7)

  ============================
  forall x : nat, x = 3 -> x = 1 -> true = false
1
2
3
4
5
6
7
1 subgoal (ID 10)

  x : nat
  H : x = 3
  H0 : x = 1
  ============================
  true = false
1
2
3
4
5
Toplevel input, characters 2-14:
>   discriminate
>   ^^^^^^^^^^^^
Error: Ltac call to "discriminate" failed.
       No primitive equality found.

One possible way to prove the above is to rewrite x to 3 in x = 1 so that we have the term 3 = 1. After that, discriminate would now work.

Relevant tactics:

  • Equivalent to inversion ‹H›. where ‹H› is a false equality hypothesis. In general inversion is more powerful than discriminate.
  • Strictly less powerful than congruence..

constructor

Use it when: you want to solve or reduce the goal because the goal could be constructed by a constructor.

In this example we will use constructor to prove that $4$ is even. First we define what exactly is evenness.

  • We define that evenness is a property of a natural number.
  • We define that we can always construct a proof that $0$ is even.
  • Given that we have a proof that $n$ is even, we define that we can also construct a proof that $2 + n$ is even.

This is captured in the following inductive definition of even:

1
2
3
Inductive even : nat -> Prop :=
| even_O : even O
| even_S : forall (n : nat), even n -> even (2 + n).

Now, we can state our proposition and prove it:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
Inductive even : nat -> Prop :=
| even_O : even O
| even_SS : forall (n : nat),
    even n ->
    even (2 + n).

Lemma four_is_even : even 4.
Proof.
  constructor.
  constructor.
  constructor.
Qed.
1

1
2
even is defined
even_ind is defined
1
2
3
4
1 subgoal (ID 1)

  ============================
  even 4
1
2
3
4
1 subgoal (ID 1)

  ============================
  even 4
1
2
3
4
1 subgoal (ID 3)

  ============================
  even 2
1
2
3
4
1 subgoal (ID 5)

  ============================
  even 0
1
No more subgoals.
1
2
3
4
No more subgoals.


four_is_even is defined

When the goal is even 4, the first constructor finds that the goal can be constructed by using even_SS. However, it cannot solve the goal because even_SS requires a proof of even n (which is even 2 in this case) to construct a proof of even (2 + n) (which is even 4 in this case). This constructor thus can only reduce the goal to even 2.

Similarly, when the goal is even 2, the second constructor finds that the goal can be constructed by using even_SS and reduces the goal to even 0.

When the goal is even 0, the last constructor finds that the goal can be constructed by using even_O. As even_O doesn’t require anything to construct even 0, the last constructor solves the goal.

Caveat: When there are multiple constructors that can be used to constructed the goal, constructor will use the first one, which might not be the one that you want. In that event, the goal might be reduced to a proof state that can’t be proven, as we can see below.
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
Inductive foo : Prop :=
| FooA : False -> foo
| FooB : foo.

Lemma foo_is_constructible : foo.
Proof.
  constructor.
  (* Use FooA instead of FooB *)
  (* We get stuck.
     There's no way to prove False! *)
1

1
2
foo is defined
foo_ind is defined
1
2
3
4
1 subgoal (ID 1)

  ============================
  foo
1
2
3
4
1 subgoal (ID 1)

  ============================
  foo
1
2
3
4
1 subgoal (ID 3)

  ============================
  False

The above lemma can be proven by specifying which constructor should be used manually. E.g., by using exact FooB, apply FooB, etc.

Relevant tactics:

  • Equivalent to apply ‹c›. where the goal can be constructed by the constructor ‹c›.
  • Equivalent to exact ‹c›. if constructor. solves the goal.

apply

Usage: apply ‹term›
Use it when: you want to solve the goal because the goal is ‹term›.

Why not jsCoq? #

jsCoq is great! However, it’s unsuitable to this project for several reasons:

  • It’s too slow to load.
  • It can’t step through several scripts independently.
  • The sidebar is too obtrusive and not really configurable.

Acknowledgements #

I would like to thank Joe Redmon, whose Coq Tactics Index is the template for this tactic index.