More proofs and tactics with Coq

If you look at the Tactics index, you will find many useful tactics to use in attempt to prove what you’re trying to prove.

One interesting example I’ve found is the auto tactic.

This tactic implements a Prolog-like resolution procedure to solve the current goal. So let’s try it and see how we can use it:

Goal (5 > 4).
  auto.       (* This magical command tries to prove stuff automatically *)
  Show Proof. (* And show us how it did it *)
Qed.

It’s proven 5 > 4 very easily, and with Show Proof we can additionally see how it did that. We see it used le_n 5, so now we can rewrite our proof:

Goal (5 > 4).
  exact (le_n 5).
Qed.

We could also dig into le_n to see what it actually does.

In our next example we’ll have a look at the case tactic (we’ve already used destruct before):

Require Import Bool.

Notation "x && y" := (andb x y).

Theorem x_and_true : (forall x : bool, x && true = x).
Proof.
  intros x.
  case x. (* Case analysis on x *)
  (* Handle the case where x is true *)
    simpl.       (* Simplify true && true *)
    reflexivity. (* true = true is proven by reflexivity *)
  (* Handle the case where x is false *)
    simpl.       (* Simplify false && true *)
    reflexivity. (* false = false is proven by reflexivity *)
Qed.

As you can see we’re relying on the Bool package and its function andb, but for simplicity we wrote an alias for it (&&) to use as infix operator.

We can check how Bool is defined, and if we do that we’ll see it has 2 options (true, false) and we’re ready to use case.

When we say case on something of type bool, it will go through the cases in order, so it starts with true, and once we prove that case it will proceed with false.

Our last (and most complex) example is where we introduce ourselves to the unfold tactic, and also rely on external proofs:

Require Import PeanoNat.

Theorem x_gte_5_x_gt_4 : (forall x : nat, x = 5 \/ x > 5 -> x > 4).
Proof.
  intros x.
  intros x_gte_5.
  case x_gte_5.
  (* Handle case x = 5 *)
    intros x_eq_5.  (* At this point we have x = 5 and x > 4 *)
    rewrite x_eq_5. (* Rewrite x > 4 with x = 5 to get 5 > 4 *)
    exact (le_n 5). (* Check le_n in Coq library, 5 > 4 is exactly that *)
  (* Handle case x > 5 *)
    (* Coq's ">" (gt) is defined in terms of "<" (lt), so we unfold to convert *)
    unfold gt.      (* At this point we have 5 < x -> 4 < x *)
    (* Check lt_succ_l in Coq library, 5 < m -> 4 < m is exactly that (which is why we used unfold) *)
    exact (Nat.lt_succ_l 4 x).
Qed.

In our next post we’ll be looking at the induction tactic, as well as some examples for it.