# Coq and The Monad Laws: The Third

## The Third Monad Law

The previous two articles introduced Coq and the first two Monad Laws. I am discussing the third one separately because it will take longer to prove.

The proof for the third law will proceed at first like the others, induction and some simplification.

```
Theorem third_law :
forall (A B C : Set) (m : list A)
(f : A -> list B) (g : B -> list C),
bind B C (bind A B m f) g =
bind A C m (fun x => bind B C (f x) g).
Proof.
induction m.
(* base case *)
simpl.
trivial.
(* inductive case *)
intros f g.
simpl.
unfold bind.
unfold bind in IHm.
```

Which brings us to this state in the interactive theorem prover.

```
1 subgoal
A : Set
B : Set
C : Set
a : A
m : list A
IHm : forall (f : A -> list B) (g : B -> list C),
flat_map g (flat_map f m) =
flat_map (fun x : A => flat_map g (f x)) m
f : A -> list B
g : B -> list C
============================
flat_map g (f a ++ flat_map f m) =
flat_map g (f a) ++ flat_map (fun x : A => flat_map g (f x)) m
```

At this point, if we could rewrite
`flat_map g (f a ++ flat_map f m)`

into
`flat_map g (f a) ++ flat_map g (flat_map f m))`

then we would be able to apply the Inductive Hypothesis and
be home free.

The "cut" tactic allows you to make an assumption, and then later come back and prove your assumption correct. Using "cut",

```
cut (flat_map g (f a ++ flat_map f m) =
flat_map g (f a) ++ flat_map g (flat_map f m)).
intro Distrib.
rewrite Distrib.
rewrite IHm.
reflexivity.
```

the original goal is easily solved. But Coq has generated an additional subgoal: we must now prove that this cut is correct.

```
1 subgoal
A : Set
B : Set
C : Set
a : A
m : list A
IHm : forall (f : A -> list B) (g : B -> list C),
flat_map g (flat_map f m) =
flat_map (fun x : A => flat_map g (f x)) m
f : A -> list B
g : B -> list C
============================
flat_map g (f a ++ flat_map f m) =
flat_map g (f a) ++ flat_map g (flat_map f m)
```

We'll proceed by induction on `f a`

which
has inductive type `list B`

.

```
induction (f a).
(* base case *)
simpl.
reflexivity.
(* inductive case *)
simpl.
rewrite IHl.
rewrite app_ass.
reflexivity.
Qed.
End ListMonad.
```

All done. We only needed the association property of list append,
which I found by querying `SearchAbout app.`

## Summary

Here is a much shorter proof which takes advantage of some of Coq's automated tactics.

```
Theorem third_law' :
forall (A B C : Set) (m : list A)
(f : A -> list B) (g : B -> list C),
bind B C (bind A B m f) g =
bind A C m (fun x => bind B C (f x) g).
Proof.
induction m; simpl; intuition.
replace (bind B C (f a ++ bind A B m f) g)
with (bind B C (f a) g ++ bind B C (bind A B m f) g);
[ rewrite IHm
| induction (f a); simpl; auto;
rewrite app_ass; rewrite IHl
]; auto.
Qed.
```

On a final note, Coq has the ability to extract code into several different languages.

```
Extraction Language Haskell.
Recursive Extraction bind ret.
```

results in

```
module Main where
import qualified Prelude
data List a = Nil | Cons a (List a)
app l m = case l of
Nil -> m
Cons a l1 -> Cons a (app l1 m)
flat_map f l = case l of
Nil -> Nil
Cons x t -> app (f x) (flat_map f t)
ret :: a1 -> List a1
ret a = Cons a Nil
bind :: (List a1) -> (a1 -> List a2) -> List a2
bind m f = flat_map f m
```

- mrd's blog
- Login to post comments