From Tealeaves Require Import
  Classes.Categorical.Monad
  Classes.Categorical.RightModule
  Classes.Kleisli.Monad.

Import Kleisli.Monad.Notations.

#[local] Generalizable Variables T A B C.

(** * Categorical Monad to Kleisli Monad *)
(**********************************************************************)

(** ** Derived <<bind>> Operation *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Bind_Categorical (T: Type -> Type)
    `{map_T: Map T}
    `{join_T: Join T}: Bind T T :=
  fun {A B} (f: A -> T B) => join ∘ map (F := T) f.

End DerivedOperations.

(** ** Derived <<bind>> is Compatible with Original <map>> *)
(**********************************************************************)
#[export] Instance Compat_Map_Bind_Derived
  `{Categorical.Monad.Monad T}:
  Compat_Map_Bind T T
    (Bind_TU := DerivedOperations.Bind_Categorical T).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
Compat_Map_Bind T T
Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
Compat_Map_Bind T T
  hnf.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
H = DerivedOperations.Map_Bind T T ext A B f.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
H A B f = DerivedOperations.Map_Bind T T A B f
  change_left (map f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = DerivedOperations.Map_Bind T T A B f
  unfold DerivedOperations.Map_Bind.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = bind (ret ∘ f)
  unfold bind, DerivedOperations.Bind_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = join ∘ map (ret ∘ f)
  rewrite <- fun_map_map.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = join ∘ (map ret ∘ map f)
  reassociate <- on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = join ∘ map ret ∘ map f
  rewrite mon_join_map_ret.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = id ∘ map f
  reflexivity.
Qed.



Module DerivedInstances.

  (* Alectryon doesn't like this
     Import CategoricalToKleisli.Monad.DerivedOperations.
   *)
  Import DerivedOperations.

  Section with_monad.

    Context
      `{Categorical.Monad.Monad T}.

    (** ** <<join>> as <<id ⋆ id>> *)
    (******************************************************************)
    Lemma join_to_kc `{Categorical.Monad.Monad T}: forall (A: Type),
        join (T := T) (A := A) = id ⋆ id.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
H3: Map T
H4: Return T
H5: Join T
H6: Categorical.Monad.Monad T
forall A : Type, join = id ⋆ id
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
H3: Map T
H4: Return T
H5: Join T
H6: Categorical.Monad.Monad T
forall A : Type, join = id ⋆ id
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
H3: Map T
H4: Return T
H5: Join T
H6: Categorical.Monad.Monad T
A: Type
join = id ⋆ id unfold kc, bind, Bind_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
H3: Map T
H4: Return T
H5: Join T
H6: Categorical.Monad.Monad T
A: Type
join = join ∘ map id ∘ id
      rewrite fun_map_id.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
H3: Map T
H4: Return T
H5: Join T
H6: Categorical.Monad.Monad T
A: Type
join = join ∘ id ∘ id
      reflexivity.
    Qed.

    (** ** Derived Kleisli Monad Laws *)
    (******************************************************************)

    (** *** Identity law *)
    (******************************************************************)
    Lemma mon_bind_id:
      forall (A: Type),
        bind (ret (T := T) (A := A)) = @id (T A).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall A : Type, bind ret = id
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall A : Type, bind ret = id
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
bind ret = id
      unfold_ops @Bind_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
join ∘ map ret = id
      rewrite (mon_join_map_ret (T := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
id = id
      reflexivity.
    Qed.

    (** *** Composition law *)
    (******************************************************************)
    Lemma mon_bind_bind:
      forall (A B C: Type) (g: B -> T C) (f: A -> T B),
        bind g ∘ bind f = bind (g ⋆ f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B C : Type) (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B C : Type) (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
      introv.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
bind g ∘ bind f = bind (g ⋆ f)
      unfold kc.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
bind g ∘ bind f = bind (bind g ∘ f)
      unfold_ops @Bind_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ map (join ∘ map g ∘ f)
      rewrite <- 2(fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ (map join ∘ map (map g) ∘ map f)
      reassociate <- on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ (map join ∘ map (map g)) ∘ map f
      reassociate <- on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ map join ∘ map (map g) ∘ map f
      unfold_compose_in_compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ map join ∘ map (map g) ∘ map f
      rewrite <- (mon_join_join (T := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ join ∘ map (map g) ∘ map f
      change (map (F := T) (map g)) with (map (F := T ∘ T) g).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ join ∘ map g ∘ map f
      reassociate -> near (map (F := T ∘ T) g).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ (join ∘ map g) ∘ map f
      rewrite <- (natural (ϕ := @join T _)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
g: B -> T C
f: A -> T B
join ∘ map g ∘ (join ∘ map f) =
join ∘ (map g ∘ join) ∘ map f
      reflexivity.
    Qed.

    (** *** Unit law *)
    (******************************************************************)
    Lemma mon_bind_comp_ret: forall (A B: Type) (f: A -> T B),
        bind f ∘ ret = f.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B : Type) (f : A -> T B), bind f ∘ ret = f
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B : Type) (f : A -> T B), bind f ∘ ret = f
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> T B
bind f ∘ ret = f unfold_ops @Bind_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> T B
join ∘ map f ∘ ret = f
      reassociate -> on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> T B
join ∘ (map f ∘ ret) = f
      unfold_compose_in_compose; (* these rewrites are not visible *)
        change (@compose A) with (@compose ((fun A => A) A)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> T B
join ∘ (map f ∘ ret) = f
      rewrite natural.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> T B
join ∘ (ret ∘ map f) = f
      reassociate <- on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> T B
join ∘ ret ∘ map f = f
      now rewrite (mon_join_ret (T := T)).
    Qed.

    #[export] Instance KleisliPreModule_CategoricalPreModule:
      Kleisli.Monad.RightPreModule T T :=
      {| kmod_bind1 := @mon_bind_id;
         kmod_bind2 := @mon_bind_bind;
      |}.
    #[export] Instance KleisliMonad_CategoricalMonad:
      Kleisli.Monad.Monad T :=
      {| kmon_bind0 := @mon_bind_comp_ret;
      |}.

  End with_monad.

End DerivedInstances.

(*
  (** ** Derived laws *)
  (********************************************************************)
  Section ToKleisli_laws.

  Context
  (T: Type -> Type)
  `{Categorical.Monad.Monad T}.

  Generalizable All Variables.
  Import Kleisli.Monad.Notations.
  Import ToKleisli.

  Lemma map_to_bind: forall `(f: A -> B),
  map T f = bind (ret T B ∘ f).
  Proof.
  intros. unfold_ops @Bind_Categorical.
  rewrite <- (fun_map_map (F := T)).
  reassociate <-.
  rewrite (mon_join_map_ret (T := T)).
  reflexivity.
  Qed.

  Corollary bind_map: forall `(g: B -> T C) `(f: A -> B),
  bind g ∘ map T f = bind (g ∘ f).
  Proof.
  intros. unfold transparent tcs.
  now rewrite <- (fun_map_map (F := T)).
  Qed.

  Corollary map_bind: forall `(g: B -> C) `(f: A -> T B),
  map T g ∘ bind f = bind (map T g ∘ f).
  Proof.
  intros. unfold transparent tcs.
  reassociate <- on left.
  rewrite (natural). unfold_ops @Map_compose.
  now rewrite <- (fun_map_map (F := T)).
  Qed.

  (** ** Left identity law *)
  Theorem kleisli_id_l: forall `(f: A -> T B),
  (@ret T _ B) ⋆1 f = f.
  Proof.
  intros. unfold kc1. now rewrite (kmon_bind1 (T := T)).
  Qed.

  (** ** Right identity law *)
  Theorem kleisli_id_r: forall `(g: B -> T C),
  g ⋆1 (@ret T _ B) = g.
  Proof.
  intros. unfold kc1. now rewrite (kmon_bind0 (T := T)).
  Qed.

  (** ** Associativity law *)
  Theorem kleisli_assoc:
  forall `(h: C -> T D) `(g: B -> T C) `(f: A -> T B),
  h ⋆1 (g ⋆1 f) = (h ⋆1 g) ⋆1 f.
  Proof.
  intros. unfold kc1 at 3. now rewrite <- (kmon_bind2 (T := T)).
  Qed.

  End ToKleisli_laws.
 *)


(** * Right modules *)
(**********************************************************************)
Module ToKleisliRightModule.

  Import DerivedOperations.
  Import DerivedInstances.

  #[export] Instance Bind_RightAction
    (T U: Type -> Type)
    `{Map_T: Map U}
    `{RightAction_TU: RightAction U T}:
    Bind T U :=
    fun A B (f: A -> T B) => right_action U ∘ map (F := U) f.

  Section Monad_kleisli_laws.

    Context
      (T F: Type -> Type)
      `{Categorical.RightModule.RightModule F T}.

    (** *** Identity law *)
    Lemma bind_id:
      `(bind (ret (T := T) (A := A)) = @id (F A)).
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
forall A : Type, bind ret = id
    Proof.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
forall A : Type, bind ret = id
      intros.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A: Type
bind ret = id unfold transparent tcs.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A: Type
right_action F ∘ map ret = id
      now rewrite (mod_action_map_ret).
    Qed.

    (** *** Composition law *)
    Lemma bind_bind: forall (A B C: Type) (g: B -> T C) (f: A -> T B),
        bind g ∘ bind f = bind (g ⋆ f).
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
forall (A B C : Type) (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
    Proof.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
forall (A B C : Type) (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
      introv.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
bind g ∘ bind f = bind (g ⋆ f) unfold kc.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
bind g ∘ bind f = bind (bind g ∘ f)
      unfold_ops @Bind_Categorical.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
bind g ∘ bind f = bind (join ∘ map g ∘ f)
      unfold_ops @Bind_RightAction.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
right_action F ∘ map g ∘ (right_action F ∘ map f) =
right_action F ∘ map (join ∘ map g ∘ f)
      rewrite <- 2(fun_map_map (F := F)).
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
right_action F ∘ map g ∘ (right_action F ∘ map f) =
right_action F ∘ (map join ∘ map (map g) ∘ map f)
      reassociate <- on right.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
right_action F ∘ map g ∘ (right_action F ∘ map f) =
right_action F ∘ (map join ∘ map (map g)) ∘ map f
      change (map (F := F) (map (F := T) g)) with (map (F := F ∘ T) g).
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
right_action F ∘ map g ∘ (right_action F ∘ map f) =
right_action F ∘ (map join ∘ map g) ∘ map f
      reassociate <- on right.
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
right_action F ∘ map g ∘ (right_action F ∘ map f) =
right_action F ∘ map join ∘ map g ∘ map f
      rewrite <- (mod_action_action (U := T) (T := F)).
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
right_action F ∘ map g ∘ (right_action F ∘ map f) =
right_action F ∘ right_action F ∘ map g ∘ map f
      reassociate -> near (map (F := F ∘ T) g).
T, F: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Map F
H3: RightAction F T
H4: RightModule.RightModule F T
A, B, C: Type
g: B -> T C
f: A -> T B
right_action F ∘ map g ∘ (right_action F ∘ map f) =
right_action F ∘ (right_action F ∘ map g) ∘ map f
      now rewrite <- (natural (ϕ := @right_action F T _)).
    Qed.

  End Monad_kleisli_laws.

  #[local] Instance Kleisli_RightModule {F T}
    `{Categorical.RightModule.RightModule F T}
: Kleisli.Monad.RightPreModule T F :=
    {| kmod_bind1 := @bind_id T F _ _ _ _ _ _;
       kmod_bind2 := @bind_bind T F _ _ _ _ _ _;
    |}.

  (** ** Specification for <<map>>  *)
  (********************************************************************)
  Section Monad_suboperations.

    Context
      (T: Type -> Type)
      `{Categorical.Monad.Monad T}.

    (** *** [map] as a special case of [bind]. *)
    Lemma map_to_bind {A B}: forall `(f: A -> B),
        map f = bind (ret ∘ f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
forall f : A -> B, map f = bind (ret ∘ f)
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
forall f : A -> B, map f = bind (ret ∘ f)
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = bind (ret ∘ f) unfold transparent tcs.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = join ∘ map (ret ∘ f)
      rewrite <- (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = join ∘ (map ret ∘ map f)
      reassociate <- on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
map f = join ∘ map ret ∘ map f
      now rewrite (mon_join_map_ret (T := T)).
    Qed.

  End Monad_suboperations.

End ToKleisliRightModule.