Production Level Knowledge & Tips

  1. 未分類
  2. 5 view

[Coq]Try to define Monad of list

Definition of List Monad

Try to define Monad of Haskell.
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 -> Type) := {
    myreturn : forall {A}, A -> M A
  ; mybind : forall {A B}, M A -> (A -> M B) -> M B
  ; myleft_identify : forall A B (a: A) (f: A -> 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 -> M B) (g: B -> M C), mybind (mybind m f) g = mybind m (fun x => mybind(f x) g)
}.
Next is list monad instance.
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.
I’ll try to prove list monad satisfy the monad law. At first I’ll show monad law and list monad.
Class MyMonad (M: Type -> Type) := {
    myreturn : forall {A}, A -> M A
  ; mybind : forall {A B}, M A -> (A -> M B) -> M B
  ; myleft_identify : forall A B (a: A) (f: A -> 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 -> M B) (g: B -> M C), mybind (mybind m f) g = mybind m (fun x => 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 -> list B
______________________________________(1/3)
f a ++ nil = f a
______________________________________(2/3)
forall (A : Type) (m : list A), flat_map (fun x : A => x :: nil) m = m
______________________________________(3/3)
forall (A B C : Type) (m : list A) (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
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 <- IHm.

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

1 subgoals
A : Type
B : Type
C : Type
a : A
m : list A
f : A -> list B
g : B -> list C
IHm : flat_map g (flat_map f m) = flat_map (fun x : A => 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 -> 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!

未分類 recent post

  1. Install sbt 1.0.0 and run sample template

  2. Visualization of Neural Network and its Train…

  3. [Machine Learning]Created docker image includ…

  4. [Node.js]How to write batch script with Node.…

  5. [Hive]Get top n items for each category

関連記事

PAGE TOP