From Tealeaves Require Import
  Classes.Categorical.Monad
  Classes.Categorical.Applicative
  Adapters.CategoricalToKleisli.Monad
  Misc.Product.

Import Misc.Product.Notations.

(** * Monadic Applicative Functors *)
(**********************************************************************)
Section Applicative_Monad.

  #[local] Generalizable Variable T.

  Import Applicative.Notations.

  Context
    `{Categorical.Monad.Monad T}.

  Import Kleisli.Monad.
  Import CategoricalToKleisli.Monad.DerivedOperations.
  Import CategoricalToKleisli.Monad.DerivedInstances.

  (** ** Derived Operations *)
  (********************************************************************)
  #[global] Instance Pure_Monad: Pure T := @ret T _.

  #[global] Instance Mult_Monad: Mult T :=
    fun A B (p: T A * T B) =>
      match p with (ta, tb) =>
                     bind (fun a => strength (a, tb)) ta
      end.

  (** ** Derived Laws *)
  (********************************************************************)
  Theorem app_pure_natural_Monad:
    forall (A B: Type) (f: A -> B) (x: A),
      map f (pure x) = pure (f x).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
x: A
map f (pure x) = pure (f x) unfold_ops @Pure_Monad.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
x: A
map f (ret x) = ret (f x)
    compose near x.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
f: A -> B
x: A
(map f ∘ ret) x = (ret ∘ f) x now rewrite (natural (ϕ := @ret T _)).
  Qed.

  Theorem app_mult_natural_Monad:
    forall (A B C D: Type) (f: A -> C) (g: B -> D) (x: T A) (y: T B),
      map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : T A) (y : T B),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : T A) (y : T B),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y) unfold_ops @Mult_Monad.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
bind (fun a : C => strength (a, map g y)) (map f x) =
map (map_tensor f g)
  (bind (fun a : A => strength (a, y)) x)
    compose near x.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
(bind (fun a : C => strength (a, map g y)) ∘ map f) x =
(map (map_tensor f g)
 ∘ bind (fun a : A => strength (a, y))) x
    rewrite bind_map.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
bind ((fun a : C => strength (a, map g y)) ∘ f) x =
(map (map_tensor f g)
 ∘ bind (fun a : A => strength (a, y))) x
    rewrite map_bind.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
bind ((fun a : C => strength (a, map g y)) ∘ f) x =
bind
  (map (map_tensor f g)
   ∘ (fun a : A => strength (a, y))) x
    fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
(fun a : C => strength (a, map g y)) ∘ f =
map (map_tensor f g) ∘ (fun a : A => strength (a, y)) ext c; unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
c: A
map (pair (f c)) (map g y) =
map (map_tensor f g) (map (pair c) y) compose near y.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C, D: Type
f: A -> C
g: B -> D
x: T A
y: T B
c: A
(map (pair (f c)) ∘ map g) y =
(map (map_tensor f g) ∘ map (pair c)) y
    now rewrite 2(fun_map_map (F := T)).
  Qed.

  Theorem app_assoc_Monad:
    forall (A B C: Type) (x: T A) (y: T B) (z: T C),
      map α ((x ⊗ y) ⊗ z) = x ⊗ (y ⊗ z).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B C : Type) (x : T A) (y : T B) (z : T C),
map α (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B C : Type) (x : T A) (y : T B) (z : T C),
map α (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
map α (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z) unfold_ops @Mult_Monad.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
map α
  (bind (fun a : A * B => strength (a, z))
     (bind (fun a : A => strength (a, y)) x)) =
bind
  (fun a : A =>
   strength
     (a, bind (fun a0 : B => strength (a0, z)) y)) x
    compose near x on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
map α
  ((bind (fun a : A * B => strength (a, z))
    ∘ bind (fun a : A => strength (a, y))) x) =
bind
  (fun a : A =>
   strength
     (a, bind (fun a0 : B => strength (a0, z)) y)) x
    rewrite (kmon_bind2 (T := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
map α
  (bind
     (kc (fun a : A * B => strength (a, z))
        (fun a : A => strength (a, y))) x) =
bind
  (fun a : A =>
   strength
     (a, bind (fun a0 : B => strength (a0, z)) y)) x
    compose near x on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
(map α
 ∘ bind
     (kc (fun a : A * B => strength (a, z))
        (fun a : A => strength (a, y)))) x =
bind
  (fun a : A =>
   strength
     (a, bind (fun a0 : B => strength (a0, z)) y)) x
    rewrite (map_bind).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
bind
  (map α
   ∘ kc (fun a : A * B => strength (a, z))
       (fun a : A => strength (a, y))) x =
bind
  (fun a : A =>
   strength
     (a, bind (fun a0 : B => strength (a0, z)) y)) x
    fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
map α
∘ kc (fun a : A * B => strength (a, z))
    (fun a : A => strength (a, y)) =
(fun a : A =>
 strength (a, bind (fun a0 : B => strength (a0, z)) y)) ext a; unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  (kc (fun a : A * B => map (pair a) z)
     (fun a : A => map (pair a) y) a) =
map (pair a) (bind (fun a : B => map (pair a) z) y)
    compose near y on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  (kc (fun a : A * B => map (pair a) z)
     (fun a : A => map (pair a) y) a) =
(map (pair a) ∘ bind (fun a : B => map (pair a) z)) y rewrite (map_bind).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  (kc (fun a : A * B => map (pair a) z)
     (fun a : A => map (pair a) y) a) =
bind (map (pair a) ∘ (fun a : B => map (pair a) z)) y
    unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  (kc (fun a : A * B => map (pair a) z)
     (fun a : A => map (pair a) y) a) =
bind (fun a0 : B => map (pair a) (map (pair a0) z)) y compose near z on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  (kc (fun a : A * B => map (pair a) z)
     (fun a : A => map (pair a) y) a) =
bind (fun a0 : B => (map (pair a) ∘ map (pair a0)) z)
  y
    unfold kc.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  ((bind (fun a : A * B => map (pair a) z)
    ∘ (fun a : A => map (pair a) y)) a) =
bind (fun a0 : B => (map (pair a) ∘ map (pair a0)) z)
  y unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  (bind (fun a : A * B => map (pair a) z)
     (map (pair a) y)) =
bind (fun a0 : B => map (pair a) (map (pair a0) z)) y
    compose near y on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  ((bind (fun a : A * B => map (pair a) z)
    ∘ map (pair a)) y) =
bind (fun a0 : B => map (pair a) (map (pair a0) z)) y
    rewrite (bind_map).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α
  (bind ((fun a : A * B => map (pair a) z) ∘ pair a) y) =
bind (fun a0 : B => map (pair a) (map (pair a0) z)) y compose near y on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
(map α
 ∘ bind ((fun a : A * B => map (pair a) z) ∘ pair a))
  y =
bind (fun a0 : B => map (pair a) (map (pair a0) z)) y
    rewrite (map_bind).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
bind
  (map α
   ∘ ((fun a : A * B => map (pair a) z) ∘ pair a)) y =
bind (fun a0 : B => map (pair a) (map (pair a0) z)) y fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
map α ∘ ((fun a : A * B => map (pair a) z) ∘ pair a) =
(fun a0 : B => map (pair a) (map (pair a0) z)) ext b.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
b: B
(map α ∘ ((fun a : A * B => map (pair a) z) ∘ pair a))
  b = map (pair a) (map (pair b) z) unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
b: B
map α (map (pair (a, b)) z) =
map (pair a) (map (pair b) z)
    compose near z.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B, C: Type
x: T A
y: T B
z: T C
a: A
b: B
(map α ∘ map (pair (a, b))) z =
(map (pair a) ∘ map (pair b)) z
    now do 2 (rewrite (fun_map_map (F := T))).
  Qed.

  Theorem app_unital_l_Monad: forall (A: Type) (x: T A),
      map left_unitor (pure tt ⊗ x) = x.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A : Type) (x : T A),
map left_unitor (pure tt ⊗ x) = x
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A : Type) (x : T A),
map left_unitor (pure tt ⊗ x) = x
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map left_unitor (pure tt ⊗ x) = x unfold_ops @Mult_Monad @Pure_Monad.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map left_unitor
  (bind (fun a : unit => strength (a, x)) (ret tt)) =
x
    compose near tt.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map left_unitor
  ((bind (fun a : unit => strength (a, x)) ∘ ret) tt) =
x rewrite mon_bind_comp_ret.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map left_unitor (strength (tt, x)) = x
    unfold strength.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map left_unitor (map (pair tt) x) = x compose near x.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
(map left_unitor ∘ map (pair tt)) x = x
    rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map (left_unitor ∘ pair tt) x = x change (left_unitor ∘ pair tt) with (@id A).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map id x = x
    now rewrite (fun_map_id (F := T)).
  Qed.

  Theorem app_unital_r_Monad: forall (A: Type) (x: T A),
      map right_unitor (x ⊗ pure tt) = x.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A : Type) (x : T A),
map right_unitor (x ⊗ pure tt) = x
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A : Type) (x : T A),
map right_unitor (x ⊗ pure tt) = x
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map right_unitor (x ⊗ pure tt) = x unfold_ops @Mult_Monad @Pure_Monad.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
map right_unitor
  (bind (fun a : A => strength (a, ret tt)) x) = x
    compose near x.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
(map right_unitor
 ∘ bind (fun a : A => strength (a, ret tt))) x = x rewrite (map_bind).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
bind
  (map right_unitor
   ∘ (fun a : A => strength (a, ret tt))) x = x
    replace (map right_unitor ∘ (fun a: A => strength (a, ret tt)))
      with (ret (T := T) (A := A)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
bind ret x = x
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
ret =
map right_unitor ∘ (fun a : A => strength (a, ret tt))
    now rewrite mon_bind_id.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
ret =
map right_unitor ∘ (fun a : A => strength (a, ret tt))
    ext a; unfold compose; cbn.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
a: A
ret a = map right_unitor (map (pair a) (ret tt)) compose near (ret tt).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
a: A
ret a = (map right_unitor ∘ map (pair a)) (ret tt)
    rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
a: A
ret a = map (right_unitor ∘ pair a) (ret tt) compose near tt.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
a: A
ret a = (map (right_unitor ∘ pair a) ∘ ret) tt
    rewrite (natural (ϕ := @ret T _ )).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A: Type
x: T A
a: A
ret a = (ret ∘ map (right_unitor ∘ pair a)) tt now unfold compose; cbn.
  Qed.

  Theorem app_mult_pure_Monad: forall (A B: Type) (a: A) (b: B),
      pure a ⊗ pure b = pure (a, b).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b)
  Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
forall (A B : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b)
    intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
a: A
b: B
pure a ⊗ pure b = pure (a, b) intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
a: A
b: B
pure a ⊗ pure b = pure (a, b) unfold_ops @Mult_Monad @Pure_Monad.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
a: A
b: B
bind (fun a : A => strength (a, ret b)) (ret a) =
ret (a, b)
    compose near a.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
a: A
b: B
(bind (fun a : A => strength (a, ret b)) ∘ ret) a =
ret (a, b) rewrite mon_bind_comp_ret.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: Categorical.Monad.Monad T
A, B: Type
a: A
b: B
strength (a, ret b) = ret (a, b)
    now rewrite strength_return.
  Qed.

  (** ** Typeclass Instance *)
  (********************************************************************)
  #[global] Instance Applicative_Monad: Applicative T :=
    { app_mult_pure := app_mult_pure_Monad;
      app_pure_natural := app_pure_natural_Monad;
      app_mult_natural := app_mult_natural_Monad;
      app_assoc := app_assoc_Monad;
      app_unital_l := app_unital_l_Monad;
      app_unital_r := app_unital_r_Monad;
    }.

End Applicative_Monad.