プログラミング + アカデミック + 何か面白いこと

  1. Programming
  2. 9 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
    

    What?
    “simpl.” doesn’t work…
    By any chance do I have to prove “a ++ nil = a” ?
    I got it. I’ll do it.

    Lemma nil_app : forall (A : Type)(a : list A),
      a ++ nil = a.
    Proof.
      intros.
      induction a.
      simpl.
      reflexivity.
      simpl.
      rewrite IHa.
      reflexivity.
    Qed.

    It was easy to prove it with induction method.

    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.

    It was also easy to prove with induction method.

    The remaining thing is I’ll beat it!

        rewrite flat_map_app.
        reflexivity.
    Qed.

    Yeah!!
    I did it!

Programming recent post

  1. Install sbt 1.0.0 and run sample template

  2. [Machine Learning]Created docker image includ…

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

  4. [Play][Scala]Develop Request Driven Batch Usi…

  5. [OpenCV][Ruby]Auto check web page design corr…

関連記事

PAGE TOP