Set Implicit Arguments.
  
Record MonadBind : Type :=
  { M : forall (A : Type), Type;
    bind : forall (A B : Type), M A -> (A -> M B) -> M B; 
    ret : forall (A : Type), A -> M A; 
    left_unit : forall (A B : Type) (f : A -> M B) (a : A), 
      bind A B (ret A a) f = f a;
    right_unit : forall (A B : Type) (m : M A), 
      bind A A m (ret A) = m;
    bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B), 
      bind B C (bind A B m f) g = bind A C m (fun x => bind B C (f x) g)
  }.  

Set Implicit Arguments.
Require Import List.

Fixpoint list_bind (A : Type) (B : Type) (l : list A) (f : A -> list B) {struct l} : list B := 
  match l with 
    | nil => nil 
    | h::t => (f h)++(list_bind t f)
  end.

Definition list_ret (A : Type) := fun a : A => a::nil.
  
Lemma list_left_unit : forall (A B : Type) (f : A -> list B) (a : A), 
  list_bind (list_ret a) f = f a. 
Proof. 
  intros. simpl. rewrite app_nil_end. reflexivity.
Defined. 
  
Lemma list_right_unit : forall (A B : Type) (m : list A), 
  list_bind m (list_ret (A:=A)) = m.
Proof. 
  simple induction m. 
    simpl. reflexivity. 
    intros. simpl.
    cut (list_bind l (list_ret (A:=A)) = l).
      intros. rewrite H0. reflexivity.
      exact H.
Defined. 

Lemma list_bind_assoc : 
  forall (A B C : Type) (m : list A) (f : A -> list B) (g : B -> list C) (x : B), 
    list_bind (list_bind m f) g = list_bind m (fun x => list_bind (f x) g).
Proof. 
  simple induction m. 
    intros. simpl. reflexivity.
    intros. simpl. 
    cut (list_bind (list_bind l f) g = list_bind l (fun x0 : A => list_bind (f x0) g)).
      intros. rewrite <- H0.
      induction (f a). 
        simpl. reflexivity.
        simpl. rewrite IHl0. rewrite app_ass. reflexivity.
      apply H. exact x.
Defined.

Definition ListMonad := 
  Build_MonadBind list list_bind list_ret list_left_unit list_right_unit list_bind_assoc.

Require Import Peano.
Require Import List.

Fixpoint downfrom (n : nat) {struct n} : (list nat) := 
  match n with 
    | 0 => n::nil
    | S m => n::(downfrom m)
  end.

Eval compute in (1::2::3::4::nil) >>= downfrom.