Code checklist

Here is a checklist of some of the most important stuff (in my opinion) that should be ran through any code change, regardless of a programming language:

Does what it’s supposed to do
- Process it mentally (proof of correctness)
- Automated tests
- Manual tests
Can’t be further broken into smaller pieces
Is written in a generalized way (re-usage)
Has no repeating parts
My future-self and coworkers can understand it
- Is documented
- Is readable
Conforms to (any) coding standards for consistency
Separation of concerns

With experience, one doesn’t need to think about these, since they occur naturally.

There might be a couple of more that I missed, but these should be a good base.

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.

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.

My first proofs in Coq

Lately I’ve been spending some time working on Mike Nahas’s tutorial, for the Coq theorem prover.

Here’s a quick summary of what I’ve learned:

Coq is structured into 3 languages:
– Vernacular language – manages definitions, e.g. commands “Theorem”, “Proof”, “Qed”.
– Tactics language – the commands we use to do the proofs themselves, e.g. intros, pose, destruct, exact, etc.
– Gallina language – where we specify what we want to prove, e.g. (forall A B : Prop, A /\ B -> B).

Here’s the first proof I’ve managed to do myself:

Theorem my_first_proof : (forall A B : Prop, A /\ B -> B).
Proof.
  intros A B.     (* These are the Props *)
  intros A_and_B. (* This is A and B from the Gallina definition above *)
  destruct A_and_B as [proof_A proof_B].
  (* At this point we've destructed A_and_B innto proof_A : A and proof_B : B *)
  exact proof_B.  (* This is exactly proof_B *)
Qed.

And here’s how that looks in CoqIDE:

Here’s my second proof, which uses the pose tactic to do a rename:

Theorem my_second_proof : (forall A B : Prop, A -> (A -> B) -> B).
Proof.
  intros A B.     (* These are the Props *)
  intros proof_A. (* This is the proof of A *)
  intros A_imp_B. (* This is A -> B)
  pose (proof_B := A_imp_B proof_A).
  (* At this point, proof_B is actually the combination of A -> B and A, which is B *)
  exact proof_B.  (* And is exactly what we needed. We could've also just do  exact (A_imp_B proof_A). instead *)
Qed.

Proving conditionals:

Theorem my_third_proof : (forall A B : Prop, A -> A \/ B).
Proof.
  intros A B.
  intros proof_A.
  pose (proof_A_or_B := or_introl proof_A : A \/ B).
  exact proof_A_or_B.
Qed.

We had to use the built-in or_introl proof for the type “or”. Note that “Inductive” allows us to create a new type. In addition, we had to explicitly set the type of the proof_A_or_B.

Finally, let’s define our week days, have a function that calculates the next day and prove that after Monday comes Tuesday:

Inductive Day : Set :=
  | Mon : Day
  | Tue : Day
  | Wed : Day
  | Thu : Day
  | Fri : Day
  | Sat : Day
  | Sun : Day.

Definition Next (day : Day) : Day :=
  match day with
    | Mon => Tue
    | Tue => Wed
    | Wed => Thu
    | Thu => Fri
    | Fri => Sat
    | Sat => Sun
    | Sun => Mon
  end.

Eval compute in Next Mon.

Theorem after_monday_simple : ((Next Mon) = Tue).
Proof.
  simpl.         (* Evaluate (Next Mon) which is Tue as we've seen above *)
  exact eq_refl. (* This is exactly reflexivity on equality. *)

  (* Could also just use reflexivity here, but note that reflexivity does simpl implicitly *)
  (* reflexivity. (* Tue = Tue is proven by reflexivity *) *)
Qed.

Theorem after_monday : (forall A : Day, A = Mon -> Next A = Tue).
Proof.
  intros A.
  intros A_eq_Mon.
  rewrite A_eq_Mon. (* Instead of trying to prove Next A = Tue, try to prove Next Mon = Tue *)
  simpl.
  constructor.      (* Since reflexivity does simpl implicitly, it makes more sense to use this instead *)
Qed.

And some interesting discussion on #coq @ freenode:

 <bor0> how many tactic commands are there like in total? 😀
 <johnw> 191 in Coq 8.5
 <bor0> wow, that's a lot. and I've only got introduced to about 10 or so
 <johnw> you don't need to know all of them, by any means
 <johnw> some are the more basic tactics from which other tactics are built up
 <johnw> think of it like a standard tactic library
 <johnw> that's the beauty of all this: almost everything is just about types and finding inhabitants of types

Fun stuff, right? 🙂

Recursive and iterative processes and procedures

During my js ⊂ lisp talk at beerjs, I noticed there were a few questions about recursion and tail call recursion, so with this post I hope to address that.

To start with, let’s define the following methods for creating a pair and getting its values:

function cons( $a, $b ) {
return function( $second ) use ( $a, $b ) {
return $second ? $b : $a;
};
}

function car( $pair ) {
return $pair( false );
}

function cdr( $pair ) {
return $pair( true );
}

An iterative process is characterized by a process whose state is captured with variables and rules how to transform them to the next state.

A recursive process is characterized by a chain of deferred evaluations. Note that a recursive procedure need not always generate a recursive process.

An iterative procedure is a procedure that does not have any references to itself.

A recursive procedure is a procedure that has references to itself.

With this, we see that there are recursive processes, and there are recursive procedures. Combining those, we get the following table:

Process / Procedure	Iterative	Recursive
Iterative	1	2
Recursive	3	4

Now that we’ve classified the combinations, we can discuss their properties and characteristics by examples:

An iterative process with iterative procedure. No recursion is involved, and there is no need for deferred evaluations (since the process is iterative). It can be further optimized using other looping constructs than goto, but we will write it this way to show the similarity with 3.
```
// Iterative process, iteration (for languages that don't support tail call optimization)
function lengthiter_i( $pair, $acc = 0 ) {
begin:
if ( null === $pair ) {
return $acc;
}        $pair = cdr( $pair );
$acc  = 1 + $acc;
goto begin;
}
```

A recursive process with iterative procedure. Recursion is involved, but since the procedure is iterative, we will implement it with the help of a list (stack), e.g. to allow for deferred evaluations in some cases:

// Recursive process, iteration
function lengthrec_i( $pair ) {
$stack = [];
$acc = 0;        while ( null !== $pair ) {
array_push( $stack, 1 );
$pair = cdr( $pair );
}while ( ! empty( $stack ) ) {
$acc += array_pop( $stack );
}

return $acc;
}

An iterative process with recursive procedure. Similar to the iterative process with iterative procedure, although differently implemented. May fail on languages that don’t have tail call optimization. Compare this code to 1 to see the similarity (additionally we map the arguments $pair => cdr( $pair ) and $acc => 1 + $acc).
```
// Iterative process, recursion
function lengthiter_r( $pair, $acc = 0 ) {
if ( null === $pair ) {
return $acc;
}        return lengthiter_r( cdr( $pair ), 1 + $acc );
}
```
A recursive process with recursive procedure. Similar to the recursive process with iterative procedure, although differently implemented in the way that the stack is implicit by calling the function multiple times, so we don’t need to handle it ourselves. For example:
```
// Recursive process, recursion
function lengthrec_r( $pair ) {
if ( null === $pair ) {
return 0;
}        return 1 + lengthrec_r( cdr( $pair ) );
}
```