Set Implicit Arguments.

Require Import List.
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.
(* Notations *)
Reserved Notation "x >>= f" (at level 42, left
associativity).

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

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

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

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

Reserved Notation "m <<= n"   (at level 42, left
associativity).

Class Monad (M : Type -> Type) := {
  bind : forall A B,
    M A -> (A -> M B) -> M B;
  unit : forall A , A -> M A;
  bind_assoc :
    forall A B C
    (m : M A)
    (f : A -> M B) (g : B -> M C),
    bind (bind m f) g = bind m (fun i => bind (f i) g);
  right_unit : forall A (m : M A),
    bind m (@unit A) = m;
  left_unit : forall A B (x : A) (f : A -> M B),
    bind (unit x) f = f x
}.

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

Definition join (M : Type -> Type) `{Monad M} (X : Type) (m : M (M X)): M X :=
  m >>= id.

Definition map (M:Type->Type)(X Y:Type)(f:X->Y)`{Monad M}(m:M X):M Y :=
  m >>= (fun x => unit (f x)).

Notation "x >>- f" := (map f x).


Class E_Monad (M : Type -> Type) :=   
{
 emonad_monad :> Monad M;
 epsilon : forall X, X -> M X -> Prop;
 epsilon_unit : forall X (x y : X), epsilon x (unit y) <-> x = y;
 epsilon_bind : forall X Y 
                (m : M X)
                (f : X -> M Y)
                (y : Y),
                epsilon y (m >>= f) <-> 
                exists (x : X), and (epsilon x m) (epsilon y (f x)) 
 }.


Theorem epsilon_join:forall X (M:Type->Type)`{E_Monad M}(m:M(M X))(x:X),
  ( exists (y : M X), ((epsilon y m) /\ (epsilon x y) ) )
   <->
  (epsilon  x (join _ m)).
Proof. intros. split.
 Case "->".
   intros. apply epsilon_bind in H0. unfold join. apply H0.
 Case "<-".
   intros. apply epsilon_bind. unfold join in H0. apply H0. Qed.

Theorem epsilon_map:forall X Y (M:Type->Type)`{E_Monad M}(m:M X)(f:X->Y)(y:Y),
  ( epsilon  y  ( m>>-f ) ) <->
   exists (x : X), (y = f x) /\ (epsilon x m).
Proof. intros. split.
  Case"->".
    intros. unfold map in H0. apply epsilon_bind in H0.
    destruct H0. exists x. destruct H0. split. apply epsilon_unit in H1.
    rewrite -> H1. reflexivity. apply H0.
  Case"<-".
    intros. destruct H0. unfold map. apply epsilon_bind. exists x.
    destruct H0. split. apply H1. apply epsilon_unit. apply H0. Qed.

Theorem all_pairs:forall X Y (M:Type->Type)`{E_Monad M}(l:M X)(m:M Y),
  exists (n : M  (prod X Y)),
  forall (z : X * Y),
      ( epsilon z n ) <-> ( epsilon (fst z) l) /\ (epsilon (snd z) m ).
Proof. intros. 
  exists ( l >>= (fun x => (m >>= (fun y => (unit (x , y)))))).
  intros. split.
  Case"->". 
    intros. split. apply epsilon_bind with (y :=z) in H0.
    destruct H0. destruct H0. apply epsilon_bind in H1. destruct H1.
    destruct H1. apply epsilon_unit in H2. rewrite -> H2. simpl.
    apply H0. apply epsilon_bind in H0. destruct H0. destruct H0.
    apply epsilon_bind in H1. destruct H1. destruct H1.
    apply epsilon_unit in H2. rewrite -> H2. simpl. apply H1.
  Case"<-".
    intros. destruct H0. apply epsilon_bind. exists (fst z).
    split. apply H0. apply epsilon_bind. exists (snd z). split.
    apply H1. assert(H2 : z = (fst z , snd z)). 
    apply surjective_pairing. rewrite <- H2. apply epsilon_unit. reflexivity.
  Qed.


Class Monad_Plus (M:Type->Type) :=   
{ 
  monad_plus_monad :> Monad M;
  mzero : forall X, M X;
  mplus : forall X, M X -> M X -> M X;
  mzero_bind : forall X Y (f : X -> M Y), (mzero X)>>= f = mzero Y;
  mzero_mplus_left : forall X (m : M X), mplus (mzero X) m = m;
  mzero_mplus_right : forall X (m : M X), mplus m (mzero X) = m;
  mplus_assoc : forall X (m n p : M X),
                  mplus m (mplus n p) = mplus (mplus m n) p ;
  mplus_bind : forall X Y (m n : M X) (f : X -> M Y),
                 (mplus m n) >>= f = mplus (m >>= f) ( n >>= f)
}.

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

Class E_Monad_Plus (M:Type->Type) :=   
{ 
  e_monad_plus_monad_plus :> Monad_Plus M;
  e_monad_plus_e_monad :> E_Monad M;
  mplus_epsilon : forall X (x : X)(m n : M X), 
                    epsilon x (mplus _ m  n) <->
                   ((epsilon x m) \/ (epsilon x n));
  mzero_epsilon :forall X (m : M X), 
                 (m = mzero X) <-> 
                 (forall (x : X), not (epsilon x m))
}.
Theorem mplus_mzero_both_mzero : 
  forall (X:Type) (M:Type->Type)`{E_Monad_Plus M}(m n:M X),
     m[]n = mzero X <-> (m = mzero X) /\ (n = mzero X).
Proof. intros. split.
  Case"->".
    intro. split. apply mzero_epsilon. intros.
    unfold not. intros. 
    assert(H2 : epsilon x (m[]n)).
    SCase"Proof of Assertion". 
      apply mplus_epsilon. left. apply H1.
    rewrite -> H0 in H2. apply mzero_epsilon in H2. apply H2.
    reflexivity. apply mzero_epsilon. intros. unfold not. intro.
    assert(H2 : epsilon x (m[]n)).
    SCase"Proof of Assertion".
      apply mplus_epsilon. right. apply H1.
    rewrite -> H0 in H2. apply mzero_epsilon in H2. apply H2. reflexivity.
  Case"<-".
    intro. destruct H0. rewrite -> H0. rewrite -> H1.
    apply mzero_mplus_left. Qed.

Theorem mplus_dist_join : forall X (M:Type->Type)`{Monad_Plus M}(m n:M(M X)), 
  join _ (m [] n) = (join _ m) [] (join _ n).
Proof. intros. unfold join. apply mplus_bind. Qed.

Theorem mplus_dist_map:
  forall X Y (M:Type->Type)`{Monad_Plus M}(m n:M X)(f:X->M Y),
    (m [] n) >>- f = (m >>-f) [] (n >>- f).
Proof. intros. unfold map. apply mplus_bind. Qed.

Class Monad_Plus_WF (M : Type -> Type) :=   
{ 
  monad_plus_wf_monad_plus :> Monad_Plus M;
  rel : forall X, M X -> M X -> Prop;
  well_found : forall X, well_founded (@rel X);
  mzero_min : forall X (m : M X), rel (mzero X) m;
  left_plus : forall X (m n: M X),
    not(n = mzero X) -> rel m (m [] n);
  right_plus : forall X (m n: M X), 
    not(m = mzero X) -> rel n (m[]n)
 }.

Class Fold_Monad (M : Type -> Type) :=   
{
 foldmonad_monad :> Monad M;
 fold : forall X Y,(X->Y->Y)->Y->(M X)->Y 
 }.

Class Fold_Monad_Plus (M : Type -> Type) :=
{
  fmonadplus_fmonad :> Fold_Monad M;
  fmonadplus_monadplus :> Monad_Plus M;
  fold_prop : forall X (m : M X),
    fold (fun x=>fun y=>((unit x)[]y))
         (mzero X)
          m = m
}.

Theorem fold_mplus:forall X (M:Type->Type)
            `{Fold_Monad_Plus M}(m n:M X),
            fold (fun x=>fun y=>((unit x)[]y)) 
                 (mzero X) (m[]n) =
            (fold (fun x=>fun y=>((unit x)[]y))
                  (mzero X) m) []
            (fold (fun x=>fun y=>((unit x)[]y))
                  (mzero X) n).
Proof. intros. repeat (rewrite -> fold_prop).
  reflexivity. Qed.

Section lists.
Theorem flat_map_app : forall (X Y:Type)(l:list X)(l':list X)(f:X->list Y),
     flat_map f (l ++ l') = (flat_map f l) ++ (flat_map f l').
Proof. intros. induction l as [| h t].
  Case"Base Case".
    auto.
  Case"Induction Step".
    simpl. rewrite -> IHt. apply app_assoc. Qed. 

Definition my_flat_map (A B : Type):=
 fun (a: list A) => fun (b:A->list B) => flat_map b a.

Theorem list_bind_assoc : 
   forall X Y Z
         (l : list X)
         (f : X -> list Y)
         (g : Y -> list Z),
    my_flat_map (my_flat_map l f) g=my_flat_map l (fun i=> my_flat_map (f i) g).
Proof. intros. induction l as [| h t].
   Case"Base Case".
     auto.
   Case"Induction Step".
     simpl. rewrite <- IHt. apply flat_map_app. Qed.

Theorem list_bind_unit : forall X Y  (x : X) (f : X -> list Y),
   my_flat_map  (x::nil) f = f x. 
Proof. intros. simpl. apply app_nil_r. Qed.

Theorem list_unit_bind : forall X (l : list X),
   my_flat_map l (fun x => x::nil) = l.
Proof. intros. induction l as [| h t].
  Case"Base Case".
    simpl. reflexivity.
  Case"Induction Step".
    simpl. rewrite -> IHt. reflexivity. Qed.

Instance list_Monad : Monad list :=
{
bind := my_flat_map;
unit := fun X => fun x => x::nil;
bind_assoc := list_bind_assoc;
left_unit := list_bind_unit;
right_unit := list_unit_bind
}. 

Theorem list_epsilon_unit : forall X (x y : X),
  In x (y::nil) <-> x = y.
Proof. intros. simpl. split.
  Case"->".
    intro. destruct H. rewrite -> H.
    reflexivity. inversion H.
  Case"<-".
    intros. left. rewrite -> H. reflexivity. Qed.

Theorem list_epsilon_bind : 
 forall X Y (m : list X)(f : X -> list Y) (y : Y),
     In y (my_flat_map m f) <-> exists (x : X),
                                (In x m) /\ (In y (f x)).
Proof. intros. split.
  Case"->".
    intro. induction m as [| h t].
    SCase"Base Case".
      inversion H.
    SCase"Induction Step".
      simpl in H. apply in_app_or in H. destruct H.
      exists h. split. apply in_eq. apply H. apply IHt in H.
      destruct H. destruct H. exists x. split. apply in_cons.
      apply H. apply H0.
  Case"<-".
    intro. induction m as [| h t].
    SCase"Base Case".
      inversion H. destruct H0. inversion H0.
    SCase"Induction Step".
      simpl. destruct H. destruct H. apply in_or_app. simpl in H.
      destruct H. left. rewrite -> H. apply H0. right. apply IHt.
      exists x. split. apply H. apply H0. Qed.

Instance list_emonad : E_Monad list :={
 emonad_monad := list_Monad;
 epsilon := In;
 epsilon_bind := list_epsilon_bind;
 epsilon_unit := list_epsilon_unit
}.

Theorem list_mzero_bind : forall X Y  (f : X -> list Y),
  nil >>= f = nil.
Proof. intros. reflexivity. Qed.

Theorem list_mplus_epsilon : forall X (x : X) (m n:list X),
  epsilon x (m ++ n) <-> 
  epsilon x m \/ epsilon x n.
Proof. intros. split. apply in_app_or. apply in_or_app. Qed.

Theorem list_mzero_epsilon : forall X (x : X), not (epsilon x nil).
Proof. auto. Qed.

Instance list_monad_plus : Monad_Plus list := {
  monad_plus_monad := list_Monad;
  mzero := fun X => nil;
  mplus := app;
  mzero_bind := list_mzero_bind;
  mzero_mplus_left := app_nil_l;
  mzero_mplus_right := app_nil_r;
  mplus_assoc := app_assoc;
  mplus_bind := flat_map_app
}.
End lists.

Section Trees.


Inductive Tree (A: Type): Type :=
  | Leaf : A -> Tree A
  | Branch : Tree A -> Tree A -> Tree A.

Definition tree_unit (A : Type) (a : A) : Tree A := Leaf a.

Fixpoint tree_bind (A B: Type) (m : Tree A) (f:A->Tree B) : Tree B :=
  match m with
  | Leaf x => f x
  | Branch l r => Branch (tree_bind l f) (tree_bind r f)
  end.

Theorem tree_bind_unit : forall X Y (x : X) (f : X -> Tree Y),
   tree_bind (Leaf x) f = f x.
Proof. intros. reflexivity. Qed.

Theorem tree_unit_bind : forall X (t : Tree X),
   tree_bind t (fun x => (Leaf x)) = t.
Proof. intros.  induction t as [| l r].
  Case"Base Case".
    reflexivity.
  Case"Induction Step".
    simpl. rewrite -> IHt1. rewrite -> r. reflexivity. Qed.

Theorem tree_bind_assoc : 
   forall X Y Z
         (t : Tree X)
         (f : X -> Tree Y)
         (g : Y -> Tree Z),
    tree_bind (tree_bind t f) g = tree_bind t (fun i=> tree_bind (f i) g).
Proof. intros. induction t as [| l r].
   Case"Base Case".
     auto.
   Case"Induction Step".
     simpl. rewrite <- IHt1. rewrite -> r. reflexivity. Qed.

Fixpoint in_tree (A : Type)(a : A)(t : Tree A) : Prop :=
  match t with
  | Leaf x => (x=a)
  | Branch l r => or (in_tree a l) (in_tree a r)
  end.

Theorem tree_epsilon_unit : forall X (x y : X),
  in_tree x (Leaf y) <-> x = y.
Proof. intros. split.
  Case"->".
    intro. simpl in H. rewrite -> H. reflexivity.
  Case"<-".
    intro. rewrite H. reflexivity. Qed.

Lemma in_branch_or : forall (A : Type)(a : A)(l r : Tree A),
  ( (in_tree a l) \/ (in_tree a r)) -> in_tree a (Branch l r).
Proof. intros. simpl. apply H. Qed.

Theorem tree_epsilon_bind : 
 forall X Y (t : Tree X)(f : X -> Tree Y) (y : Y),
     in_tree y (tree_bind t f) <-> 
     exists (x : X), (in_tree x t) /\ (in_tree y (f x)).
Proof. intros. split.
  Case "->".
    induction t as [| l r].
    SCase"Base Case".
      intros. simpl in H. exists a. split. reflexivity. apply H.
    SCase"Induction Step".
      intros. simpl in H. destruct H. apply r in H.
      destruct H as [z z_prop]. exists z. split. simpl. 
      left. apply z_prop. apply z_prop.
      apply IHt1 in H. destruct H as [z z_prop]. exists z.
      split. simpl. right. destruct z_prop. apply H.
      destruct z_prop. apply H0.
  Case"<-".
    intros. induction t as [| l r].
    SCase"Base Case".
      simpl. destruct H as [x x_prop]. destruct x_prop. simpl in H.
      rewrite -> H. apply H0.
    SCase"Induction Step". 
      simpl. destruct H as [x x_prop]. destruct x_prop. simpl in H.
      destruct H. left. apply r. exists x. split. apply H. apply H0.
      right. apply IHt1. exists x. split. apply H. apply H0. Qed.

Instance tree_Monad : Monad Tree :=
{
  bind := tree_bind;
  unit := tree_unit;
  bind_assoc := tree_bind_assoc;
  left_unit := tree_bind_unit;
  right_unit := tree_unit_bind
}.

Instance tree_Emonad : E_Monad Tree:={
  emonad_monad := tree_Monad;
  epsilon := in_tree;
  epsilon_bind := tree_epsilon_bind;
  epsilon_unit := tree_epsilon_unit
}.

End Trees.