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

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

- mrd's blog
- Login to post comments