Coq and The Monad Laws: The First and Second

The First Monad Law

In the previous article, I gave a brief introduction to Coq and the List Monad. I listed three Theorems but did not prove them. Now I will show how to prove the first two Theorems.

Here is the context of our code:

Section ListMonad. Require Import List. Definition ret (A : Set) (a : A) := a :: nil. Definition bind (A B : Set) (m : list A) (f : A -> list B) := flat_map f m.

The first Theorem, restated:

Theorem first_law : forall (A B : Set) (a : A) (f : A -> list B), bind A B (ret A a) f = f a.

At this point, Coq will enter an interactive proof mode. In coqtop, the prompt will change accordingly. In ProofGeneral Emacs, a new window will pop up. In either case, you will be presented with a view of the current assumptions and goals that looks like this:

1 subgoal ============================ forall (A B : Set) (a : A) (f : A -> list B), bind A B (ret A a) f = f a

There are no assumptions, and one goal to prove.

Proof. intros A B a f.

Coq proofs can proceed with "tactics" which instruct the proof engine to perform a certain operation, or series of operations. In this case, we are introducing assumptions named A,B,a,f drawn from the antecedents of the goal. Now the proof view looks like this:

1 subgoal A : Set B : Set a : A f : A -> list B ============================ bind A B (ret A a) f = f a

The "unfold" tactic takes the definition of the given argument and tries to substitute it directly into the goal.

unfold bind. unfold ret. unfold flat_map.

Now we have a vastly simplified goal.

1 subgoal A : Set B : Set a : A f : A -> list B ============================ f a ++ nil = f a

Everyone knows that appending nil to a list returns the same list. But how do we explain this to Coq? Search and find out if Coq already knows about this fact.

SearchRewrite (_ ++ nil).

SearchRewrite is used to search for theorems of the form a = b which can be used to rewrite portions of your goal. I use the wildcard _ to indicate that I want to find any theorem involving appending nil to anything. Coq finds:

app_nil_end: forall (A : Set) (l : list A), l = l ++ nil

We can use this with the "rewrite" tactic. We want to rewrite our code which looks like l ++ nil into l. That is a right-to-left rewrite, which is specified like so:

rewrite <- app_nil_end.

And finally we have a goal f a = f a which Coq can trivially solve with

reflexivity.

Or any of the more automated tactics, like "trivial" or "auto".

Qed.

The first monad law is discharged and proven. You can run Check first_law. to see the new theorem.

The Second Monad Law

This second proof will proceed by induction on the structure of the list parameter m. The "induction" tactic causes Coq to try a proof by induction. The proof will be split into two parts, based on case breakdown of the list type.

Theorem second_law : forall (A : Set) (m : list A), bind A A m (ret A) = m. Proof. induction m.

2 subgoals A : Set ============================ bind A A nil (ret A) = nil subgoal 2 is: bind A A (a :: m) (ret A) = a :: m

The base case is easy, the "simpl" tactic can take care of the unfolding and simplification.

simpl. reflexivity.

The inductive case is also straightforward, because after the "simpl" step, the Inductive Hypothesis is already applicable. The appropriate IHm assumption is provided by the "induction" tactic.

simpl. rewrite IHm. reflexivity. Qed.

Summary

The full proofs, minus the commentary:

Theorem first_law : forall (A B : Set) (a : A) (f : A -> list B), bind A B (ret A a) f = f a. Proof. intros A B a f. unfold bind. unfold ret. unfold flat_map. rewrite <- app_nil_end. reflexivity. Qed. Theorem second_law : forall (A : Set) (m : list A), bind A A m (ret A) = m. Proof. induction m. (* base case *) simpl. reflexivity. (* inductive case *) simpl. rewrite IHm. reflexivity. Qed.

Next time, the Third Monad Law, and a more complicated proof.