Tech Tips

1. Uncategorized
2. 36 view

[Coq]Try to define Monad of list

It needs following characters.
• f(return(A),g) = g(A)
• f(A,return) = A
• f(f(A, g),h) = f(A, (x -> f(g(B), h)))

Also it needs following function.
• return
• f(a,b) = b(a)
Monad’s definition is following with the characters and functions.
```Class MyMonad (M: Type -&amp;amp;gt; Type) := {
myreturn : forall {A}, A -&amp;amp;gt; M A
; mybind : forall {A B}, M A -&amp;amp;gt; (A -&amp;amp;gt; M B) -&amp;amp;gt; M B
; myleft_identify : forall A B (a: A) (f: A -&amp;amp;gt; M B), mybind (myreturn a) f = f a
; myright_identify : forall A (m: M A), mybind m myreturn = m
; myassociativity : forall A B C (m:M A) (f: A -&amp;amp;gt; M B) (g: B -&amp;amp;gt; M C), mybind (mybind m f) g = mybind m (fun x =&amp;amp;gt; mybind(f x) g)
}.```
```Instance MList: MyMonad list := {
myreturn A x := x :: nil
; mybind A B m f := mymap A B f m
}.```
I could define them.
But I can’t prove it…
Maybe it needs like concat function in Haskell.

Proof

I couldn’t prove that list monad satisfy the monad law. I googled any way to solve the problem and found flat_map function.
```Class MyMonad (M: Type -&amp;amp;gt; Type) := {
myreturn : forall {A}, A -&amp;amp;gt; M A
; mybind : forall {A B}, M A -&amp;amp;gt; (A -&amp;amp;gt; M B) -&amp;amp;gt; M B
; myleft_identify : forall A B (a: A) (f: A -&amp;amp;gt; M B), mybind (myreturn a) f = f a
; myright_identify : forall A (m: M A), mybind m myreturn = m
; myassociativity : forall A B C (m:M A) (f: A -&amp;amp;gt; M B) (g: B -&amp;amp;gt; M C), mybind (mybind m f) g = mybind m (fun x =&amp;amp;gt; mybind(f x) g)
}.

Instance MList: MyMonad list := {
myreturn A x := x :: nil
; mybind A B m f := flat_map f m
}.```
Game on!
```Proof.
intros A B a f.
simpl.

------------------------------------
3 subgoal
A : Type
B : Type
a : A
f : A -&amp;amp;gt; list B
______________________________________(1/3)
f a ++ nil = f a
______________________________________(2/3)
forall (A : Type) (m : list A), flat_map (fun x : A =&amp;amp;gt; x :: nil) m = m
______________________________________(3/3)
forall (A B C : Type) (m : list A) (f : A -&amp;amp;gt; list B) (g : B -&amp;amp;gt; list C),
flat_map g (flat_map f m) = flat_map (fun x : A =&amp;amp;gt; flat_map g (f x)) m
```
```Lemma nil_app : forall (A : Type)(a : list A),
a ++ nil = a.
Proof.
intros.
induction a.
simpl.
reflexivity.
simpl.
rewrite IHa.
reflexivity.
Qed.```
Let’s get back.
```  rewrite nil_app.
reflexivity.

intros.
induction m.
simpl.
reflexivity.
simpl.
rewrite IHm.
reflexivity.

intros.
induction m.
simpl.
reflexivity.
simpl.
rewrite &amp;amp;lt;- IHm.

---------------------------------

1 subgoals
A : Type
B : Type
C : Type
a : A
m : list A
f : A -&amp;amp;gt; list B
g : B -&amp;amp;gt; list C
IHm : flat_map g (flat_map f m) = flat_map (fun x : A =&amp;amp;gt; flat_map g (f x)) m
______________________________________(1/1)
flat_map g (f a ++ flat_map f m) =
flat_map g (f a) ++ flat_map g (flat_map f m)
```
Not again.
I got it. Let’s prove “flat_map f (a ++ b) = flat_map f(a) ++ flat_map f (b)”!
```Lemma flat_map_app : forall (A B : Type)(l l' : list A)(f : A -&amp;amp;gt; list B),
flat_map f (l++l') = flat_map f l ++ flat_map f l'.
Proof.
induction l.
simpl.
intros.
reflexivity.

intros.
simpl.
rewrite IHl.
rewrite app_ass.
reflexivity.
Qed.```
The remaining thing is I’ll beat it!
```    rewrite flat_map_app.
reflexivity.
Qed.```
Yeah!!
I did it!