# Coq and The Monad Laws: The First and Second

Submitted by mrd on Wed, 08/15/2007 - 4:14pm.

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.

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. ```

The first is the base case for `nil`, and the second is the inductive case for `cons`.

``` 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.