Induction with Coq

To get ourselves introduced to the induction tactic, we’ll start by showing that 0 is a right identity for the naturals under addition, i.e. $\forall n \in \mathbb{N}, n + 0 = n$ .

The definition of addition is: $n = 0 + n, S(m) + n = S(m + n)$ .

Mathematically, we start with induction on n.

We have $0 + 0 = 0$ for the base case, which is true (based on definition of add).
For the inductive step, we assume that $n + 0 = n$ , and try to prove that $S n + 0 = S n$ .
We can rewrite our goal by using the definition of add, where we have $S n + 0 = S (n + 0)$ .
Now using the hypothesis we have $S (n + 0) = S n$ , which is what we needed to show.

Programmatically, we have:

Compute 2+3. (* Test to see what's 2 plus 3 *)

Theorem zero_identity_on_addition : (forall n:nat, n + 0 = n).
Proof.
  intros n.
  induction n.     (* Use induction on n *)
  (* Base case *)
    simpl.         (* Simplify 0 + 0 = 0 to 0 = 0 *)
    exact eq_refl. (* Which is exactly reflexivity *)
  (* Inductive step *)
  simpl.           (* At this point we have S n + 0 = S n, in other words n + 1 + 0 = n + 1 *)
                   (* Simplify to get (n + 0) + 1 = n + 1 *)
  rewrite IHn.     (* Use the hypothesis to rewrite (n + 0) to n *)
  exact eq_refl.   (* n + 1 = n + 1 is proven by reflexivity *)
Qed.

Neat, right?

Our second example is more complex. We will:
1. Define a recursive function, fact.
2. Prove that $fact(3) = 6$ .
3. Introduce and prove a lemma to be used for our proof.
4. Prove that $fact(n) > 0$ .

Mathematically:

$fact(n) = \left\{ \begin{array}{ll} 1 & \mbox{if } n = 0 \\ n * fact(n - 1) & \mbox otherwise \end{array} \right.$
To show what fact(3) is, we go by definitions: $3 * fact(2) = 3 * 2 * fact(1) = 3 * 2 * 1 * fact(0) = 6$ .
To prove $x > 0 \implies x + y > 0$ , which is the lemma we’ll use in our Coq proof, note we have as givens $x > 0, y \ge 0$ (since $y \in \mathbb{N}$ ).

From here, we have two cases:
$\begin{cases} y = 0: x + y = x + 0 = x > 0 \\ y > 0: x + y > 0 + x = x > 0 \end{cases}$

By transitivity on $(>, \mathbb{N})$ for the second case, combined with the first case, we can conclude that $x + y > 0$ .
To prove that $fact(n) > 0$ for $n \ge 0$ , we use induction on n.

Base case: $n = 0: fact(0) = 1 > 0$ , which is true.
Inductive step: Assume $fact(k) > 0$ for some $n = k$ . Note that $n \ge 0 \implies k + 1 > 0$ , so we’re good to multiply with a positive number.

Multiply both sides by k + 1 to get $(k + 1) * fact(k) = fact(k + 1) > 0$ , which is what we needed to show.

Thus $fact(n) > 0$ in general.

Now for the programming part.

The recursive definition:

(* If we try to use Definition, we get fact is not defined *)
(* Coq provides a special syntax Fixpoint for recursion *)
Fixpoint fact (n:nat) : nat :=
  match n with
    | S n => S n * fact n
    | 0 => 1
end.

Evaluate and prove $fact(3) = 6$

Compute (fact 3).
 
Theorem fact_3_eq_6 : (fact 3 = 6).
Proof.
  simpl.           (* Evaluate fact 3 = 6 *)
  exact eq_refl.   (* 6 = 6 is exactly reflexivity *)
Qed.

We start our lemma as follows:

Require Import Coq.Arith.Plus.

Lemma x_plus_y_gt_0 : (forall x y : nat, x > 0 -> x + y > 0).
Proof.
  intros x y.
  intros x_gt_0.
  unfold gt.           (* Convert x + y > 0 to 0 < x + y *) 
  unfold gt in x_gt_0. (* Convert x_gt_0 : x > 0 to x_gt_0 : 0 < x *)
  (* We have that Theorem lt_plus_trans n m p : n < m -> n < m + p *)
  (* So we feed 0, x, y to match the arguments, and additionally pass x_gt_0 to match the n < m part *)
  exact (lt_plus_trans 0 x y x_gt_0).
Qed.

Nothing new going on here. But, we can try to be smart, and try to rewrite the lemma as:

Require Import Omega.

Lemma x_plus_y_gt_0 : (forall x y : nat, x > 0 -> x + y > 0).
Proof.
  intros x y.
  omega.
Qed.

The new thing we can notice here is the usage of the omega tactic.

This tactic is an automatic decision procedure for Presburger arithmetic, i.e. it will solve any arithmetic-based proof goal that it understands (and that is true). But note e.g. that it doesn’t understand multiplication.

The actual proof

Theorem fact_gt_0 : (forall n : nat, fact n > 0).
Proof.
  intros n.
  induction n.
  (* Base case *)
    simpl.          (* At this point we have fact 0 > 0, simplify to get 1 > 0 *)
    exact (le_n 1). (* This is exactly 1 > 0 *)
  (* Inductive step *)
    simpl.          (* Simplify to convert fact(n + 1) > 0 to fact n + n * fact n > 0 *)
                    (* Which is exactly our lemma defined above *)
                    (* We also have IHn : fact n > 0 *)
    (* Feed (fact n), (n * fact n) into x_plus_y_gt_0, and IHn as well for the x > 0 part *)
    exact (x_plus_y_gt_0 (fact n) (n * fact n) IHn).
Qed.

Thus, the complete program:

Require Import Omega.

(* If we try to use Definition, we get fact is not defined *)
(* Coq provides a special syntax Fixpoint for recursion *)
Fixpoint fact (n:nat) : nat :=
  match n with
    | S n => S n * fact n
    | 0 => 1
end.

Compute (fact 3).

Theorem fact_3_eq_6 : (fact 3 = 6).
Proof.
  simpl.           (* Evaluate fact 3 = 6 *)
  exact eq_refl.   (* 6 = 6 is exactly reflexivity *)
Qed.

Lemma x_plus_y_gt_0 : (forall x y : nat, x > 0 -> x + y > 0).
Proof.
  intros x y.
  omega.
Qed.

Theorem fact_gt_0 : (forall n : nat, fact n > 0).
Proof.
  intros n.
  induction n.
  (* Base case *)
    simpl.          (* At this point we have fact 0 > 0, simplify to get 1 > 0 *)
    exact (le_n 1). (* This is exactly 1 > 0 *)
  (* Inductive step *)
    simpl.          (* Simplify to convert fact(n + 1) > 0 to fact n + n * fact n > 0 *)
                    (* Which is exactly our lemma defined above *)
                    (* We also have IHn : fact n > 0 *)
    (* Feed (fact n), (n * fact n) into x_plus_y_gt_0, and IHn as well for the x > 0 part *)
    exact (x_plus_y_gt_0 (fact n) (n * fact n) IHn).
Qed.

As a conclusion from the examples above, we can say that Coq with its type mechanism provides a neat way for us to reason about properties of our programs.