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