ExtLib.Data.Monads.IdentityMonadLaws

Require Import Coq.Classes.RelationClasses.
Require Import Setoid.
Require Import ExtLib.Data.Fun.
Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Structures.MonadLaws.
Require Import ExtLib.Data.Monads.IdentityMonad.

Set Implicit Arguments.
Set Strict Implicit.

(*
Section with_T.
  Context {T : Type} (e : type T).

  Definition equal_ident (a b : ident T) : Prop :=
    equal (unIdent a) (unIdent b).

  Global Instance type_ident : type (ident T) :=
  { equal := equal_ident
  ; proper := fun x => proper (unIdent x)
  }.

  Global Instance typeOk_ident (tT : typeOk e) : typeOk type_ident.
  Proof.
    constructor.
    { unfold equal, proper, type_ident, equal_ident; simpl; intros.
      apply only_proper; auto. }
    { red. destruct x. intros.
      red; simpl. red; simpl.
      eapply preflexive with (wf := proper); eauto with typeclass_instances. }
    { red. simpl. unfold equal_ident. intros.
      symmetry. assumption. }
    { red; simpl. unfold equal_ident. intros.
      etransitivity; eassumption. }
  Qed.

  Global Instance proper_unIdent : proper unIdent.
  Proof. red; simpl; red; simpl. destruct x; compute; auto. Qed.

  Global Instance proper_mkIdent : proper mkIdent.
  Proof. do 7 red. compute; auto. Qed.

End with_T.

(*
Global Instance FunctorOrder_fmleq : FunctorOrder _ (@Identity_leq) _.
Proof.
  constructor; eauto with typeclass_instances.
Qed.
*)

Require Import ExtLib.Tactics.TypeTac.

Global Instance MonadLaws_GFix : MonadLaws Monad_ident (@type_ident).
Proof.
  constructor; eauto with typeclass_instances; try solve  compute; intuition .
  { unfold equal; simpl. intros. red in H2. red; simpl.
    eapply H2. eapply preflexive with (wf := proper); auto.
    eapply equiv_prefl; auto. }
  { unfold proper, equal; simpl. eauto with typeclass_instances. }
  { simpl; intros. red. solve_equal. }
  { unfold bind, Monad_ident. do 6 red; intros. solve_equal. }
Qed.
*)