From Tealeaves Require Export
  Functors.Early.Writer
  Functors.Reader
  Misc.Product
  Classes.Monoid.

#[local] Generalizable Variables W T F A M.

From Tealeaves Require Import
  Classes.Categorical.Bimonad
  Classes.Categorical.RightModule.

Import Strength.Notations.
Import Monad.Notations.
Import Monoid.Notations.
Import Product.Notations.

#[local] Arguments ret (T)%function_scope {Return}
  (A)%type_scope _.
#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.
#[local] Arguments extract (W)%function_scope {Extract}
  (A)%type_scope _.
#[local] Arguments cojoin W%function_scope {Cojoin}
  {A}%type_scope _.


(** * <<T ∘ (W ×)>> is a monad *)
(* TODO: This can get moved to Categories/DecoratedFunctor.v *)
(**********************************************************************)
Section strength_as_writer_distributive_law.

  Context
    `{Monoid W}.

  Lemma strength_ret_l `{Functor F}: forall A: Type,
      σ ∘ ret (W ×) (F A) =
        map F (ret (W ×) A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type,
σ ∘ ret (prod W) (F A) = map F (ret (prod W) A)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type,
σ ∘ ret (prod W) (F A) = map F (ret (prod W) A)
    reflexivity.
  Qed.

  Lemma strength_join_l `{Functor F}: forall A: Type,
      σ ∘ join (T := (W ×)) (A := F A) =
        map F (join (T := (W ×)) (A := A)) ∘ σ ∘ map (W ×) σ.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type,
σ ∘ join = map F join ∘ σ ∘ map (prod W) (σ)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
forall A : Type,
σ ∘ join = map F join ∘ σ ∘ map (prod W) (σ)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
σ ∘ join = map F join ∘ σ ∘ map (prod W) (σ) ext [w1 [w2 t]].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(σ ∘ join) (w1, (w2, t)) =
(map F join ∘ σ ∘ map (prod W) (σ)) (w1, (w2, t)) unfold compose; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
map F (pair (w1 ● w2)) (id t) =
map F join (map F (pair (id w1)) (map F (pair w2) t))
    compose near t.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map F (pair (w1 ● w2)) ∘ id) t =
map F join
  ((map F (pair (id w1)) ∘ map F (pair w2)) t) rewrite fun_map_map.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map F (pair (w1 ● w2)) ∘ id) t =
map F join (map F (pair (id w1) ∘ pair w2) t)
    compose near t on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map F (pair (w1 ● w2)) ∘ id) t =
(map F join ∘ map F (pair (id w1) ∘ pair w2)) t rewrite fun_map_map.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
A: Type
w1, w2: W
t: F A
(map F (pair (w1 ● w2)) ∘ id) t =
map F (join ∘ (pair (id w1) ∘ pair w2)) t
    reflexivity.
  Qed.

  Context
    `{Monad T}.

  #[export, program] Instance BeckDistributiveLaw_strength:
    BeckDistributiveLaw (W ×) T :=
    {| bdist_join_r := strength_join T W;
       bdist_unit_r := strength_ret T W;
       bdist_join_l := strength_join_l;
       bdist_unit_l := strength_ret_l;
    |}.

  #[export] Instance: Monad (T ∘ (W ×)) := Monad_Beck.

End strength_as_writer_distributive_law.

(** * Miscellaneous Properties *)
(**********************************************************************)
Section Writer_miscellaneous.

  Context
    `{Monoid W}.

  Import Categorical.Monad.Notations.

  (* This rewrite is useful when proving decoration-traversal
     compatibility in the binder case. *)
  Theorem strength_shift1:
    forall (F: Type -> Type) `{Functor F} (w: W) (A: Type),
      σ ∘ μ (T := (W ×)) ∘ pair w =
        map F (μ (T := (W ×)) ∘ pair w) ∘ strength (F := F) (B := A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (F : Type -> Type) (Map_F : Map F),
Functor F ->
forall (w : W) (A : Type),
σ ∘ μ ∘ pair w = map F (μ ∘ pair w) ∘ σ
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (F : Type -> Type) (Map_F : Map F),
Functor F ->
forall (w : W) (A : Type),
σ ∘ μ ∘ pair w = map F (μ ∘ pair w) ∘ σ
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
w: W
A: Type
σ ∘ μ ∘ pair w = map F (μ ∘ pair w) ∘ σ ext [w' x].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
w: W
A: Type
w': W
x: F A
(σ ∘ μ ∘ pair w) (w', x) =
(map F (μ ∘ pair w) ∘ σ) (w', x) unfold compose; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
w: W
A: Type
w': W
x: F A
map F (pair (w ● w')) (id x) =
map F (μ ○ pair w) (map F (pair w') x)
    compose near x.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
F: Type -> Type
Map_F: Map F
H0: Functor F
w: W
A: Type
w': W
x: F A
(map F (pair (w ● w')) ∘ id) x =
(map F (μ ○ pair w) ∘ map F (pair w')) x now rewrite fun_map_map.
  Qed.

  Lemma pair_incr_zero: forall (w: W) (A: Type),
      incr (A := A) w ∘ pair Ƶ = pair w.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (w : W) (A : Type), incr w ∘ pair Ƶ = pair w
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (w : W) (A : Type), incr w ∘ pair Ƶ = pair w
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
w: W
A: Type
incr w ∘ pair Ƶ = pair w
    ext p.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
w: W
A: Type
p: A
(incr w ∘ pair Ƶ) p = (w, p) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
w: W
A: Type
p: A
(w ● Ƶ, p) = (w, p)
    rewrite monoid_id_r.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
w: W
A: Type
p: A
(w, p) = (w, p)
    reflexivity.
  Qed.

End Writer_miscellaneous.