This post explain basic and common tactics in Coq and their underlying logic.

Make use of lemmas - The apply Tactic

The rewrite tactic is to apply equalities If you have $H: x = y$ and the goal is $P~x$, using rewrite H to change the goal to $P~y$.

On the other hand, the apply tactic is to apply lemmas. If you have $L: P \to Q$ and the goal is $Q$, using apply L to change the goal to $P$.

Example - use of apply - (exercise silly_ex):

Theorem silly_ex : forall p,
  (forall n, even n = true -> even (S n) = false) ->
  (forall n, even n = false -> odd n = true) ->
  even p = true ->
  odd (S p) = true.
Proof.
  intros p eq1 eq2 eq3.
  apply eq2. apply eq1. apply eq3.
  Qed.

When we use apply H, the statement H will begin with a ∀ that introduces some universally quantified variables. Note that to use the apply tactic, the conclusion of the applied-by theorem must be exactly identical to the goal. Therefore, sometimes it is necessary to modified goal to accommodate the theorem. One most simple modification is symmetry tactic, which switches the left and right sides of an equality in the goal.

Example - use of symmetry - (exercise apply_exercise1)

Theorem rev_exercise1 : forall (l l' : list nat),
  l = rev l' ->
  l' = rev l.
Proof.
  intros l l' eq1.
  rewrite eq1.
  symmetry.
  (* [ rev_involutive : forall (X : Type) (l : list X), rev (rev l) = l ] *)
  apply rev_involutive. 
  Qed.

Transitive Relations - The transitivity Tactic

Transitivity: If P a b and P b c both holds and P is a transitive property, we can conclude that P a c.

For example, if we know 6 > 4 and 4 > 2 and > is a transitive relation, we are justified to conclude that 6 > 2.

Coq also has a built-in tactic transitivity that accomplishes the same purpose.

Example - use of transitivity - exercise trans_eq_exercise

Example trans_eq_exercise : forall (n m o p : nat),
     m = (minustwo o) ->
     (n + p) = m ->
     (n + p) = (minustwo o).
Proof.
  intros n m o p H1 H2.
  transitivity m.
  apply H2.
  apply H1.
  Qed.

But Coq does not required the proof of transitivity before using the transitivity tactic. It just assumes the transitivity holds. Thus for custom or less standard relations, ensuring and proving their properties, including transitivity, is an important part of constructing correct and meaningful proofs.

One-to-one Relations - The injection Tactic

A One-to-one relation - or more formally, an injective relation says that a property of map $f:A\to B$ holds if

\[f(x) = f(y)\]

Then it must be

\[x = y\]

This property is true in all inductively defined type in Coq. So this technique is able to be generalize to every constructor. The corresponding tactic is injection, which generates all possible equations from a hypothesis.

Example - use of injection - exercise injection_ex3

Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  j = z :: l ->
  x = y.
Proof.
  intros X x y z l j H0 H1.
  injection H0.
  intros H0a H0b.
  assert ( H2: y::l=z::l ). { rewrite H0a. rewrite H1. reflexivity.  }
  injection H2 as H2i.
  rewrite H2i. rewrite H0b.
  reflexivity.
  Qed.

We can also make use of injective relations directedly on functions in the goal. Coq provides f_equal tactic to perform simplification based on assumption that the relation is injective.

Example - eq_implies_succ_equal

Theorem eq_implies_succ_equal' : forall (n m : nat),
  n = m -> S n = S m.
Proof. intros n m H. f_equal. apply H. Qed.

It is observed that S n = S m is immediately be simplified to n = m after using the f_equal tactic.

Principle of Explosion - The discriminate tactic

The principle of explosion is also known as ex falso - in Latin “from falsehood, anything (follows)” - which is the law according to which any statement can be proven from a contradiction in logic systems.

In Coq, every inductively defined type has $disjoint$ constructors. For example, the nat type has two disjoint constructors: S nat and O, in which any two terms with different constructors can never be equal. In the context that we assume such two terms are equal, we are justified to prove anything we want.

The quote is from the software foundations, which explains the reason why we can do this, which I can’t really find a better explanation that it.

If you find the principle of explosion confusing, remember that these proofs are not showing that the conclusion of the statement holds. Rather, they are showing that, if the nonsensical situation described by the premise did somehow hold, then the nonsensical conclusion would also follow, because we’d be living in an inconsistent universe where every statement is true.

The discriminate tactic can be use when the goal is a contradiction that wants us to prove two terms with different constructors are the same.

Example - use of discriminate - exercise injection_ex3

Example discriminate_ex3 :
  forall (X : Type) (x y z : X) (l j : list X),
    x :: y :: l = [] ->
    x = z.
Proof.
  intros X x t z l j contrast.
  discriminate contrast. Qed.

This example is trivial - a theorem built on a contradiction is not practically useful - but it shows that we can develop any bullshit given a nonsensical premise. It is more useful in branches produced by destruct of induction of some proof, in which we can just use discriminate to say “This branch is impossible to stand so we can skip it”.

Forward and Backward Reasoning

Forward reasoning starts from what we know and iteratively push forward until the goal is reached. Informal proofs seen in math and CS classes are often presented in this style. Conversely, backward reasoning begins from the goal that we want to proof, iteratively transform it to what we already know. This is the default style in Coq.

It is not necessarily to say one way is better than the other, and we are able to combine them as our tools to draw a reasonable and intuitive conclusion. To employ forward reasoning, we can use the in clause:

Theorem S_inj : forall (n m : nat) (b : bool),
  ((S n) =? (S m)) = b  ->
  (n =? m) = b.
Proof.
  intros n m b H. simpl in H. apply H.  Qed.

The line simpl in H. transform H from

(S n =? S m) = b

to

(n =? m) = b

By the definition of =? (eqb) operator.

Similarly, it is also acceptable to use other tactics on hypothesis such as symmetry in H, apply lemma1 in H and more. Just follow the same rule as what we have done on the goal.

Specializing Hypothesis - The specialize Tactic

Hypothesis with $\forall$ quantifiers can be specialize to what we want it to be.

Example trans_eq_example''' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
  (* trans_eq: forall X (n m o : X), n = m -> m = o -> n = o *)
  specialize trans_eq with (m:=[c;d]) as H.
  apply H.
  apply eq1. apply eq2. 
Qed.

We explicitly specialize a general lemma trans_eq to a specific lemma that accommodates the goal with the name H:

H: forall n o, n = [c; d] -> [c; d] = o -> n = o

The example shows specialization form a global theorem. Note that we can specialize local hypothesis as well.

Generalize Induction Hypothesis

Sometimes it is important to control the form of the induction hypothesis. To be more specific, when there are multiple variables, it is not necessary to introduce all variables from the goal to the context. Instead, we may find it convenient to let them stay in the context so that the hypothesis can be more general.

Example - general induction - exercise eqb_true

Theorem eqb_true : forall n m,
  n =? m = true -> n = m.
Proof.
  intros n. induction n as [| n' IHn].
  - intros m eq. destruct m.
    + reflexivity.
    + discriminate. 
  - intros m eq. destruct m as [| m'].
    + discriminate.
    + apply eq_implies_succ_equal. apply IHn. apply eq. 
Qed.

In this example, it is only n in the context the induction, so that we get a hypothesis:

IHn: forall m : nat, (n' =? m) = true -> n' = m

Not that the m in IHn is a general variable with a $\forall$ quantifier, which is not the same with m in the theorem declaration. In practice, m can be specialized to any other nat. i.e. S m

Another useful example to illustrate this idea:

Example - exercise plus_n_n_injective

Theorem plus_n_n_injective : forall n m,
  n + n = m + m ->
  n = m.
Proof.
  intros n. induction n.
  - simpl. intros m H. destruct m.
    + reflexivity.
    + discriminate.
  - intros m H. destruct m as [| m'].
    + discriminate.
    + simpl in H. 
      rewrite <- plus_n_Sm in H.
      rewrite <- plus_n_Sm in H.
      injection H as H'.
      apply IHn in H'.
      f_equal.
      apply H'.
  Qed.

Sometimes the order of variables in the theorem declaration cannot achieve what we want just like the example above - keep m in the goal while introduce n to the context - we can use generalize tactic to re-generalize some variables.

Example - use of generalize - exercise gen_dep_practice.

Lemma length_0_empty: forall (X: Type) (l: list X), 
	length l = 0 -> l = nil.
Proof.
  intros. destruct l. reflexivity. discriminate. 
Qed.

Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X),
  length l = n ->
  nth_error l n = None.
Proof.
  intros n X l. generalize n.
  induction l as [| x l' IHl].
  - simpl. reflexivity.
  - intros n' eq. destruct n'.
    + apply length_0_empty in eq. rewrite eq. reflexivity.
    + simpl. apply IHl. simpl in eq. injection eq as eq1. apply eq1.
Qed.

Delve into Expressions - The unfold Tactic

The unfold tactic tells Coq to replace the expression by their definition. It is a rather straightforward tactic that “evaluates” an expression.

Sometime simpl will also perform an unfolding if the function is not too complicated. In this case, we need to use unfold to encourage Coq to do so.

Example:

Definition bar x :=
  match x with
  | O => 5
  | S _ => 5
  end.

Fact silly_fact_2' : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  unfold bar.
  destruct m eqn:E.
  - reflexivity.
  - reflexivity.
Qed.

Destruct on Compound Expressions

When we are reasoning a function, especially after unfolding, sometime it is needed to perform case analysis as well. Especially there is no existing lemmas can be employ. In this case, we might need to look at the if..else branches one-by-one. To do that, we can use destruct on expressions.

Example

Definition sillyfun (n : nat) : bool :=
  if n =? 3 then false
  else if n =? 5 then false
  else false.

Theorem sillyfun_false : forall (n : nat),
  sillyfun n = false.
Proof.
  intros n. unfold sillyfun.
  destruct (n =? 3) eqn:E1.
    - (* n =? 3 = true *) reflexivity.
    - (* n =? 3 = false *) destruct (n =? 5) eqn:E2.
      + (* n =? 5 = true *) reflexivity.
      + (* n =? 5 = false *) reflexivity.  Qed.

The sillyfun_false theorem declares a property which tells the function sillyfun always returns false. It looks at every branches by destruct the predicate expression.

A more meaningful example is from the exercise: Example - exercise combine_split:

Fixpoint split {X Y : Type} (l : list (X*Y))
               : (list X) * (list Y) :=
  match l with
  | [] => ([], [])
  | (x, y) :: t =>
      match split t with
      | (lx, ly) => (x :: lx, y :: ly)
      end
  end.

(** Prove that [split] and [combine] are inverses in the following
    sense: *)

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros X Y l.
  induction l. 
  - simpl. intros. 
    injection H as H1 H2. 
    rewrite <- H1. rewrite <- H2. 
    reflexivity.
  - destruct x as [x1 x2]. simpl. destruct (split l) as [lx ly].
    intros. injection H as H1 H2. 
    rewrite <- H1.
    rewrite <- H2.
    simpl. rewrite IHl. reflexivity. reflexivity.
Qed.

In this example, the destruct only produce one subgoal since the split l pattern match in the definition of split only has one branch. But it moves forward from

match split l with
| (lx, ly) => (x1 :: lx, x2 :: ly) = (l1 l2)
end

to

(x1 :: lx, x2 :: ly) = (l1, l2)

which is still a meaningful step in the proof.