Require Coq.Setoids.Setoid.

Reserved Notation "x >>= f" (at level 42, left
associativity).

Reserved Notation "m [] n"  (at level 42, left
associativity).

Inductive monad_syn (X : Type) : Type :=
  | ret : X -> monad_syn X
  | mplus : monad_syn X -> monad_syn X -> monad_syn X
  | mzero : monad_syn X
  | bind : forall (Y :Type), monad_syn Y -> (Y -> monad_syn X) -> monad_syn X.

Notation "x >>= f" := (bind _ _ x f).

Notation " m [] n" := (mplus _ m n).

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

Axiom mplus_assoc : forall (X : Type) (m n p : monad_syn X),
  (m [] n)[] p =  m [] (n [] p).

Axiom mzero_left : forall (X: Type) (m : monad_syn X),
  (mzero X) [] m = m.

Axiom mzero_right : forall (X : Type) (m : monad_syn X),
   m [] (mzero X) = m.

Axiom mzero_bind : forall (X Y : Type) (f : X -> monad_syn Y),
  (mzero X) >>= f = mzero Y.

Axiom ret_not_mzero : forall (X :Type) (x :X),
  not (ret X x = mzero X).

Axiom mplus_mzero_both_mzero : forall X (m n : monad_syn X),
   m [] n = mzero X <-> (m = mzero X) /\ (n = mzero X).

Axiom ret_bind : forall (X Y : Type) (x : X) (f : X -> monad_syn Y),
  (ret X x) >>=  f = f x.

Axiom mplus_bind : forall (X Y:Type)(m n:monad_syn X)(f:X->monad_syn Y),
  (m [] n) >>= f = (m >>= f) [] (n >>= f).

Axiom bind_mzero_f_mzero:forall (X Y:Type)(m:monad_syn X)(f:X->monad_syn Y),
  not(m = mzero X) -> 
    (m >>= f = mzero Y) -> f = (fun z => (mzero Y)).

Axiom mzero_or_not_mzero : forall (X: Type) (m : monad_syn X),
  m = mzero X \/ not(m = mzero X).

Axiom mzero_f_bind : forall (X Y : Type) (m : monad_syn X),
   m >>= (fun z => mzero Y) = mzero Y.

Theorem x : forall (X : Type) ( m : monad_syn X),
  m = mzero X \/ (exists (x : X), m = ret X x)\/ 
  exists (n p : monad_syn X),
    (not (n = mzero X)) /\
    (not (p = mzero X)) /\
    m = mplus X n p.
Proof. intros. induction m.
  Case"m = return x".
    right. left. exists x. reflexivity.
  Case"m = m1 [] m2".
    destruct IHm1.
    SCase"m1 = mzero".
      destruct IHm2. rewrite -> H. rewrite -> H0.
      rewrite -> mzero_left. left. reflexivity. destruct H0. destruct H0.
      rewrite -> H. rewrite -> H0. rewrite -> mzero_left. right. left.
      exists x. reflexivity. destruct H0. destruct H0. rewrite -> H.
      destruct H0. destruct H1. rewrite -> mzero_left. right. right. 
      exists x. exists x0.  split.  apply H0. split.  apply H1. apply H2.
      destruct H.
    SCase"m1 = return x".
      destruct IHm2. rewrite -> H0. rewrite -> mzero_right.
      destruct H. rewrite -> H. right. left. exists x.
      reflexivity. destruct H0. right. right. destruct H. destruct H0.
      exists (ret X x). exists (ret X x0). split. apply ret_not_mzero.
      split. apply ret_not_mzero. rewrite -> H. rewrite -> H0. reflexivity.
      destruct H0. destruct H0. destruct H0. destruct H1. rewrite -> H2.
      rewrite <- mplus_assoc. right. right. exists (mplus X m1 x).
      exists x0. split. rewrite -> mplus_mzero_both_mzero. unfold not. 
      intro. destruct H3. contradiction. split. apply H1. reflexivity.
    SCase"m1 = n [] p".
      destruct IHm2. rewrite -> H0. rewrite -> mzero_right. right. right.
      apply H. destruct H0.  destruct H0. destruct H. destruct H.
      destruct H. destruct H1. rewrite -> H2. right. right. 
      exists (mplus X x0 x1). exists m2. split.
      rewrite -> mplus_mzero_both_mzero. unfold not. intro. destruct H3. 
      contradiction. split. rewrite -> H0. apply ret_not_mzero.
      reflexivity. destruct H. destruct H0. destruct H. destruct H0.
      destruct H. destruct H0. destruct H1. destruct H2. right. right.
      exists (mplus X x x1). exists (mplus X x0 x2). split. 
      rewrite -> mplus_mzero_both_mzero. unfold not. intro. 
      destruct H5. contradiction. split. rewrite -> mplus_mzero_both_mzero.
      unfold not. intro. destruct H5. contradiction. rewrite -> H4.
      rewrite -> H3. reflexivity.
  Case"m = mzero".
    left. reflexivity.
  Case"m = n >>= f".
    destruct IHm.
    SCase"n = mzero".
      rewrite -> H0. rewrite -> mzero_bind. left. reflexivity.
    destruct H0.
    SCase"n = return x".
      destruct H0. rewrite -> H0. rewrite -> ret_bind. apply H.
    destruct H0.
    SCase"n = n1 [] n2".
      destruct H0. destruct H0. destruct H1. rewrite -> H2. 
      rewrite -> mplus_bind. 
      assert(H3 : bind _ _ x0 m0 = (mzero X) -> (m0 = (fun x => (mzero X)))).
      SSCase"Proof of Assertion".
        apply bind_mzero_f_mzero. apply H1.
      assert(H4 : bind _ _ x m0 = (mzero X) -> (m0 = (fun x => (mzero X)))).
      SSCase"Proof of Assertion".
        apply bind_mzero_f_mzero. apply H0.
      assert(H5:bind _ _ x m0=(mzero X) \/ not(bind _ _ x m0 = (mzero X))).
      SSCase"Proof of Assertion".
        apply mzero_or_not_mzero.
      assert(H6 : bind _ _ x0 m0=(mzero X) \/ not(bind _ _ x0 m0=(mzero X))).
      SSCase"Proof of Assertion".
        apply mzero_or_not_mzero.
      destruct H5. apply H4 in H5. rewrite -> H5. left. rewrite->mzero_f_bind.
      rewrite -> mzero_left. rewrite -> mzero_f_bind. reflexivity.
      destruct H6. apply H3 in H6. rewrite -> H6.
      left. rewrite -> mzero_f_bind. rewrite -> mzero_left.
      rewrite -> mzero_f_bind. reflexivity. right. right.
      exists (bind X Y x m0). exists (bind X Y x0 m0).
      split. apply H5. split. apply H6. reflexivity. Qed.