TraversableFunctor.v

From Tealeaves Require Export
  Classes.Categorical.TraversableFunctor
  Functors.Early.Reader.

Import Functor.Notations.

#[local] Generalizable Variable X Y T U G ϕ A B.
#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.
#[local] Arguments pure F%function_scope {Pure}
  {A}%type_scope _.
#[local] Arguments mult F%function_scope {Mult}
  {A B}%type_scope _.

(** * Traversable Instance for Certain Functors *)
(**********************************************************************)

(** ** Traversable Instance for <<(E ×)>> *)
(**********************************************************************)
Section TraversableFunctor_prod.

  Generalizable All Variables.

  Context
    (E: Type).

  #[global] Instance Dist_prod: ApplicativeDist (prod E) :=
    fun F Fmap mlt pur A '(x, a) => map F (pair x) a.

  Lemma dist_natural_prod: forall `{Applicative G} `(f: A -> B),
      map (G ∘ prod E) f ∘ dist (prod E) G =
        dist (prod E) G ∘ map (prod E ∘ G) f.E: Type
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B),
map (G ∘ prod E) f ∘ dist (prod E) G =
dist (prod E) G ∘ map (prod E ∘ G) f
  Proof.E: Type
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B),
map (G ∘ prod E) f ∘ dist (prod E) G =
dist (prod E) G ∘ map (prod E ∘ G) f
    intros.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (G ∘ prod E) f ∘ dist (prod E) G =
dist (prod E) G ∘ map (prod E ∘ G) f ext [x a]; cbn.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
x: E
a: G A
(map (G ∘ prod E) f ∘ dist (prod E) G) (x, a) =
map G (pair (id x)) (map G f a)
    unfold compose; cbn.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
x: E
a: G A
map (G ○ prod E) f (map G (pair x) a) =
map G (pair (id x)) (map G f a)
    unfold_ops @Map_compose.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
x: E
a: G A
map G (map (prod E) f) (map G (pair x) a) =
map G (pair (id x)) (map G f a)
    compose near a.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
x: E
a: G A
(map G (map (prod E) f) ∘ map G (pair x)) a =
(map G (pair (id x)) ∘ map G f) a
    do 2 rewrite fun_map_map.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
x: E
a: G A
map G (map (prod E) f ∘ pair x) a =
map G (pair (id x) ∘ f) a
    reflexivity.
  Qed.

  Instance dist_natural_prod_:
    forall `{Applicative G}, Natural (@dist (prod E) _ G _ _ _).E: Type
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
Natural
  (@dist (prod E) Dist_prod G Map_G Pure_G Mult_G)
  Proof.E: Type
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
Natural
  (@dist (prod E) Dist_prod G Map_G Pure_G Mult_G)
    constructor; try typeclasses eauto.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> B),
map (G ○ prod E) f ∘ dist (prod E) G =
dist (prod E) G ∘ map (prod E ○ G) f
    intros.E: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (G ○ prod E) f ∘ dist (prod E) G =
dist (prod E) G ∘ map (prod E ○ G) f eapply (dist_natural_prod f).
  Qed.

  Lemma dist_morph_prod: forall `{ApplicativeMorphism G1 G2 ϕ} A,
      dist (prod E) G2 ∘ map (prod E) (ϕ A) =
        ϕ (E * A) ∘ dist (prod E) G1.E: Type
forall (G1 G2 : Type -> Type) (H : Map G1)
  (H0 : Mult G1) (H1 : Pure G1) (H2 : Map G2)
  (H3 : Mult G2) (H4 : Pure G2) (ϕ : G1 ⇒ G2),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist (prod E) G2 ∘ map (prod E) (ϕ A) =
ϕ (E * A) ∘ dist (prod E) G1
  Proof.E: Type
forall (G1 G2 : Type -> Type) (H : Map G1)
  (H0 : Mult G1) (H1 : Pure G1) (H2 : Map G2)
  (H3 : Mult G2) (H4 : Pure G2) (ϕ : G1 ⇒ G2),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist (prod E) G2 ∘ map (prod E) (ϕ A) =
ϕ (E * A) ∘ dist (prod E) G1
    intros; unfold compose; cbn.E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
dist (prod E) G2 ○ map (prod E) (ϕ A) =
ϕ (E * A) ○ dist (prod E) G1 ext [x a]; cbn.E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
x: E
a: G1 A
map G2 (pair (id x)) (ϕ A a) =
ϕ (E * A) (map G1 (pair x) a)
    now rewrite appmor_natural.
  Qed.

  Lemma dist_unit_prod: forall (A: Type),
      dist (prod E) (fun A => A) = @id (prod E A).E: Type
forall A : Type,
dist (prod E) (fun A0 : Type => A0) = id
  Proof.E: Type
forall A : Type,
dist (prod E) (fun A0 : Type => A0) = id
    intros; unfold compose; cbn.E, A: Type
dist (prod E) (fun A : Type => A) = id ext [x a]; now cbn.
  Qed.

  Lemma dist_linear_prod:
    forall `{Applicative G1} `{Applicative G2} (A: Type),
      dist (prod E) (G1 ∘ G2) =
        map G1 (dist (prod E) G2) ∘ dist (prod E) G1 (A := G2 A).E: Type
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall A : Type,
dist (prod E) (G1 ∘ G2) =
map G1 (dist (prod E) G2) ∘ dist (prod E) G1
  Proof.E: Type
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall A : Type,
dist (prod E) (G1 ∘ G2) =
map G1 (dist (prod E) G2) ∘ dist (prod E) G1
    intros; unfold compose; cbn.E: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
dist (prod E) (G1 ○ G2) =
map G1 (dist (prod E) G2) ○ dist (prod E) G1 ext [x a].E: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
x: E
a: G1 (G2 A)
dist (prod E) (G1 ○ G2) (x, a) =
map G1 (dist (prod E) G2) (dist (prod E) G1 (x, a))
    unfold_ops @Dist_prod @Map_compose.E: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
x: E
a: G1 (G2 A)
map G1 (map G2 (pair x)) a =
map G1 (fun '(x, a) => map G2 (pair x) a)
  (map G1 (pair x) a)
    compose near a on right.E: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
x: E
a: G1 (G2 A)
map G1 (map G2 (pair x)) a =
(map G1 (fun '(x, a) => map G2 (pair x) a)
 ∘ map G1 (pair x)) a
    now rewrite fun_map_map.
  Qed.

  #[global] Instance Traversable_prod:
    Classes.Categorical.TraversableFunctor.TraversableFunctor (prod E) :=
    {| dist_natural := @dist_natural_prod_;
       dist_morph := @dist_morph_prod;
       dist_unit := @dist_unit_prod;
       dist_linear := @dist_linear_prod;
    |}.

End TraversableFunctor_prod.

(** * Distribution over Certain Applicative Functors *)
(**********************************************************************)

(** ** Constant Applicative Functors *)
(** To distributive over constant applicative functors, i.e. to fold
    over monoidal values, we can use the <<Const>> applicative
    functor. This tends to clutter operations with <<unconst>>
    operations which get in the way of convenient rewriting. We
    provide a lighter-weight alternative in this section and some
    specifications proving equivalence with the <<Const>> versions. *)
(**********************************************************************)
From Tealeaves Require Import Classes.Monoid Functors.Constant.

Section TraversableFunctor_const.

  #[local] Generalizable Variable M.

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

  (** *** Distribution over <<const>> is agnostic about the tag. *)
  (** Distribution over a constant applicative functor is agnostic
      about the type argument ("tag") to the constant functor. On
      paper it is easy to ignore this, but in Coq this must be
      proved. Observe this equality is ill-typed if [Const] is used
      instead. *)
  (********************************************************************)
  Lemma dist_const1: forall (X: Type) `{Monoid M},
      (@dist T _ (const M)
         Map_const Pure_const Mult_const X)
      =
        (@dist T _ (const M)
           Map_const Pure_const Mult_const False).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
forall (X M : Type) (op : Monoid_op M)
  (unit0 : Monoid_unit M),
Monoid M -> dist T (const M) = dist T (const M)
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
forall (X M : Type) (op : Monoid_op M)
  (unit0 : Monoid_unit M),
Monoid M -> dist T (const M) = dist T (const M)
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) = dist T (const M) symmetry.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) = dist T (const M) change (?f = ?g) with (f = g ∘ (@id (T M))).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) = dist T (const M) ∘ id
    rewrite <- fun_map_id.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) = dist T (const M) ∘ map T id
    change (@id M) with
      (map (A := False) (B:=X) (const M) exfalso).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) =
dist T (const M) ∘ map T (map (const M) exfalso)
    change (map T (map (const M) ?f))
      with (map (T ∘ const M) f).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) =
dist T (const M) ∘ map (T ∘ const M) exfalso
    rewrite <- (natural
                 (ϕ := @dist T _ (const M) _ _ _) (B := X) (A := False)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) =
map (const M ○ T) exfalso ∘ dist T (const M)
    reflexivity.
  Qed.

  Lemma dist_const2: forall (X Y: Type) `{Monoid M},
      (@dist T _ (const M)
         Map_const Pure_const Mult_const X)
      =
        (@dist T _ (const M)
           Map_const Pure_const Mult_const Y).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
forall (X Y M : Type) (op : Monoid_op M)
  (unit0 : Monoid_unit M),
Monoid M -> dist T (const M) = dist T (const M)
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
forall (X Y M : Type) (op : Monoid_op M)
  (unit0 : Monoid_unit M),
Monoid M -> dist T (const M) = dist T (const M)
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
X, Y, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (const M) = dist T (const M) now rewrite (dist_const1 X), (dist_const1 Y).
  Qed.

  (** *** Distribution over [Const] vs <<const>> *)
  (********************************************************************)
  Theorem traversable_const_spec (tag: Type) `{Monoid M}:
    unconst ∘ @dist T _ (Const M)
      Map_Const
      Pure_Const
      Mult_Const tag ∘ map T mkConst
    = @dist T _ (const M)
        Map_const
        Pure_const
        Mult_const tag.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
tag, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
unconst ∘ dist T (Const M) ∘ map T mkConst =
dist T (const M)
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
tag, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
unconst ∘ dist T (Const M) ∘ map T mkConst =
dist T (const M)
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
tag, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
unconst ∘ dist T (Const M) ∘ map T mkConst =
dist T (const M) rewrite <- (dist_morph (ϕ := @unconst _)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
tag, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (fun _ : Type => M) ∘ map T unconst
∘ map T mkConst = dist T (const M)
    reassociate -> on left.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
tag, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (fun _ : Type => M)
∘ (map T unconst ∘ map T mkConst) = dist T (const M) rewrite fun_map_map.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
tag, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (fun _ : Type => M) ∘ map T (unconst ∘ mkConst) =
dist T (const M)
    change (unconst ∘ mkConst) with (@id M).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
tag, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
dist T (fun _ : Type => M) ∘ map T id =
dist T (const M)
    now rewrite fun_map_id.
  Qed.

End TraversableFunctor_const.