proving monad laws for something.

IOtt.v

(**
   IOtt functor from
   Swierstra, Wouter, and Thorsten Altenkirch. "Beauty in the Beast."
   In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop.
   Haskell '07. ACM, 2007. http://doi.acm.org/10.1145/1291201.1291206.
**)

Require Import Logic.FunctionalExtensionality.

Inductive IOtt (a: Set) : Set :=
  | GetChar: (nat -> IOtt a) -> IOtt a
  | PutChar: nat -> IOtt a -> IOtt a
  | Return: a -> IOtt a
.

Definition IOtt_rtn := Return.
Fixpoint IOtt_bind (a b: Set) (x: IOtt a) (g: a -> IOtt b) :=
  match x with
    | Return a' => g a'
    | GetChar f => GetChar _ (fun c => IOtt_bind _ _ (f c) g)
    | PutChar c a' => PutChar _ c (IOtt_bind _ _ a' g)
  end.

(** Monad Laws **)

Definition MonadLaws (F: Set -> Set)
  (rtn: forall a: Set, a -> F a)
  (bind: forall a b, F a -> (a -> F b) -> F b)
  : Prop :=
  (forall a b x k,
    bind a b (rtn a x) k = k x)
  /\
  (forall a m,
    bind a _ m (rtn _) = m)
  /\
  (forall (a b c: Set) (m: F a) (k: a -> F b) (h: b -> F c),
    bind a c m (fun x => bind b c (k x) h) = bind b c (bind a b m k) h).

Lemma monadIOtt : MonadLaws IOtt IOtt_rtn IOtt_bind.
  unfold MonadLaws.
  split.
    intros a b x k.
    unfold IOtt_rtn.
    unfold IOtt_bind.
    reflexivity.

  split.
    intros a m.
    induction m; simpl; f_equal.
      apply functional_extensionality.
      assumption.

      assumption.

      unfold IOtt_rtn.
      reflexivity.

    intros a b c m k h.
    induction m; simpl; f_equal.
      apply functional_extensionality.
      assumption.

      assumption.
Qed.