ExtLib.Data.Monads.ReaderMonadLaws

Require Import RelationClasses.
Require Import Setoid.
Require Import ExtLib.Data.Fun.
Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Structures.MonadLaws.
Require Import ExtLib.Data.Monads.ReaderMonad.

Set Implicit Arguments.
Set Strict Implicit.

(*
Section Laws.
  Variable m : Type -> Type.
  Variable Monad_m : Monad m.
  Variable mtype : forall T, type T -> type (m T).
  Variable mtypeOk : forall T (tT : type T), typeOk tT -> typeOk (mtype tT).
  Variable ML_m : MonadLaws Monad_m mtype.

  Variable S : Type.
  Variable type_S : type S.
  Variable typeOk_S : typeOk type_S.

  Definition readerT_eq T (tT : type T) (a b : readerT S m T) : Prop :=
    equal (runReaderT a) (runReaderT b).

  Global Instance type_readerT (T : Type) (tT : type T) : type (readerT S m T) :=
    type_from_equal (readerT_eq tT).

  Global Instance typeOk_readerT (T : Type) (tT : type T) (tOkT : typeOk tT) 
    : typeOk  (type_readerT tT).
  Proof.
    eapply typeOk_from_equal.
    { simpl. unfold readerT_eq. intros.
      generalize (only_proper _ _ _ H); intros.
      split; do 4 red; intuition. }
    { red. unfold equal; simpl. unfold readerT_eq; simpl.
      unfold Morphisms.respectful; simpl. firstorder. }
    { red. unfold equal; simpl. unfold readerT_eq; simpl.
      unfold Morphisms.respectful; simpl. intros.
      etransitivity. eapply H; eauto.
      destruct (only_proper _ _ _ H1).
      eapply H0. eapply preflexive; eauto with typeclass_instances. }
  Qed.

  Theorem mproper_red : forall (C : Type) (tC : type C) (o : readerT S m C),
    proper o ->
    proper (runReaderT o).
  Proof. clear. intros. apply H. Qed.

  Global Instance proper_runReaderT T (tT : type T) : proper (@runReaderT S m T).
  Proof.
    repeat red; intros.
    apply H in H0. apply H0.
  Qed.

  Global Instance proper_mkReaderT T (tT : type T) : proper (@mkReaderT S m T).
  Proof.
    repeat red; intros.
    apply H in H0. apply H0.
  Qed.

  Ltac unfold_readerT :=
    red; simpl; intros; do 2 (red; simpl); intros.

  Global Instance MonadLaws_readerT : MonadLaws (@Monad_readerT S _ Monad_m) _.
  Proof.
    constructor.
    { (* bind_of_return *)
      unfold_readerT.
      erewrite bind_of_return; eauto with typeclass_instances; type_tac. }
    { (* return_of_bind *)
      unfold_readerT.
      rewrite return_of_bind; intros; eauto with typeclass_instances.
      intros. eapply H0. eassumption. }
    { (* bind_associativity *)
      unfold_readerT.
      rewrite bind_associativity; eauto with typeclass_instances; type_tac. }
    { unfold_readerT. red; intros.
      type_tac. }
    { intros. unfold bind; simpl. red; intros. red; intros. 
      red; simpl. red; simpl; intros. solve_equal. }
  Qed.

(*
  Global Instance MonadTLaws_readerT : @MonadTLaws (readerT S m) (@Monad_readerT S m _)
    r_mleq m Monad_m (@MonadT_readerT _ m).
  Proof.
    constructor; intros; simpl; eapply lower_meq; unfold liftM; simpl; monad_norm;
      reflexivity.
  Qed.
*)

End Laws.
*)