From Tealeaves Require Export
  Classes.Multisorted.DecoratedTraversableMonad
  Functors.Multisorted.Batch.

Import Product.Notations.
Import TypeFamily.Notations.
Import Multisorted.Batch.Notations.

#[local] Generalizable Variables A B C F G W U T K.

(** * Iterating over a DTM *)
(******************************************************************************)
Section batchm_operation.

  Context
    `{Index}
    (U : Type -> Type)
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}.

  Definition batchm {A : Type} (B : Type) : forall (k : K), W * A -> @BatchM _ T W A B (T k B) :=
    fun k '(w, a) => Go (@id (T k B)) ⧆ (w, a).

  Definition toBatchM {A : Type} (B : Type) : U A -> @BatchM _ T W A B (U B) :=
    mbinddt U (@BatchM _ T W A B) (batchm B).

End batchm_operation.

(** ** Representing <<mbinddt>> with <<runBatch>> *)
(******************************************************************************)
Section toBatchM.

  Context
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}.

  Theorem mbinddt_to_runBatchM :
    forall `{Applicative F} (A B : Type) (t : U A)
      (f : forall k, W * A -> F (T k B)),
      mbinddt U F f t = runBatchM f (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (t : U A)
  (f : forall k : K, W * A -> F (T k B)),
mbinddt U F f t = runBatchM f (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (t : U A)
  (f : forall k : K, W * A -> F (T k B)),
mbinddt U F f t = runBatchM f (toBatchM U B t)
    intros.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, W * A -> F (T k B)
mbinddt U F f t = runBatchM f (toBatchM U B t) unfold toBatchM.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, W * A -> F (T k B)
mbinddt U F f t =
runBatchM f (mbinddt U BatchM (batchm B) t)
    compose near t on right.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, W * A -> F (T k B)
mbinddt U F f t =
(runBatchM f ∘ mbinddt U BatchM (batchm B)) t
    rewrite (dtp_mbinddt_morphism W T U BatchM F).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, W * A -> F (T k B)
mbinddt U F f t =
mbinddt U F ((fun k : K => runBatchM f) ◻ batchm B) t
    fequal.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, W * A -> F (T k B)
f = (fun k : K => runBatchM f) ◻ batchm B ext k [w a].
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, W * A -> F (T k B)
k: K
w: W
a: A
f k (w, a) =
((fun k : K => runBatchM f) ◻ batchm B) k (w, a) cbn.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, W * A -> F (T k B)
k: K
w: W
a: A
f k (w, a) = ap F (pure id) (f k (w, a))
    now rewrite ap1.
  Qed.

  Corollary mbindd_to_runBatchM :
    forall (A B : Type) (t : U A)
      (f : forall k, W * A -> T k B),
      mbindd U f t = runBatchM (F := fun A => A) f (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B),
mbindd U f t = runBatchM f (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B),
mbindd U f t = runBatchM f (toBatchM U B t)
    intros.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
mbindd U f t = runBatchM f (toBatchM U B t) rewrite mbindd_to_mbinddt.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
mbinddt U (fun A : Type => A) f t =
runBatchM f (toBatchM U B t) now rewrite mbinddt_to_runBatchM.
  Qed.

  Corollary mbindt_to_runBatchM :
    forall `{Applicative F} (A B : Type) (t : U A)
      (f : forall k, A -> F (T k B)),
      mbindt U F f t = runBatchM (f ◻ allK extract) (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (t : U A)
  (f : forall k : K, A -> F (T k B)),
mbindt U F f t =
runBatchM (f ◻ allK extract) (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (t : U A)
  (f : forall k : K, A -> F (T k B)),
mbindt U F f t =
runBatchM (f ◻ allK extract) (toBatchM U B t)
    intros.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, A -> F (T k B)
mbindt U F f t =
runBatchM (f ◻ allK extract) (toBatchM U B t) rewrite mbindt_to_mbinddt.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: forall k : K, A -> F (T k B)
mbinddt U F (f ◻ allK extract) t =
runBatchM (f ◻ allK extract) (toBatchM U B t) now rewrite mbinddt_to_runBatchM.
  Qed.

  Corollary mmapdt_to_runBatchM  :
    forall `{Applicative F} (A B : Type) (t : U A)
      `(f : K -> W * A -> F B),
      mmapdt U F f t = runBatchM (fun k => map (F := F) (mret T k) ∘ f k) (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (t : U A) (f : K -> W * A -> F B),
mmapdt U F f t =
runBatchM (fun k : K => map (mret T k) ∘ f k)
  (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (F : Type -> Type) (Map_G : Map F)
  (Pure_G : Pure F) (Mult_G : Mult F),
Applicative F ->
forall (A B : Type) (t : U A) (f : K -> W * A -> F B),
mmapdt U F f t =
runBatchM (fun k : K => map (mret T k) ∘ f k)
  (toBatchM U B t)
    intros.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: K -> W * A -> F B
mmapdt U F f t =
runBatchM (fun k : K => map (mret T k) ∘ f k)
  (toBatchM U B t)
    rewrite mmapdt_to_mbinddt.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: K -> W * A -> F B
mbinddt U F (mapMret ◻ f) t =
runBatchM (fun k : K => map (mret T k) ∘ f k)
  (toBatchM U B t)
    rewrite mbinddt_to_runBatchM.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
t: U A
f: K -> W * A -> F B
runBatchM (mapMret ◻ f) (toBatchM U B t) =
runBatchM (fun k : K => map (mret T k) ∘ f k)
  (toBatchM U B t)
    reflexivity.
  Qed.

  Corollary mbind_to_runBatchM :
    forall (A B : Type) (t : U A)
      (f : forall k, A -> T k B),
      mbind U f t = runBatchM (F := fun A => A) (f ◻ allK extract) (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : A ~k~> T B),
mbind U f t =
runBatchM (f ◻ allK extract) (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : A ~k~> T B),
mbind U f t =
runBatchM (f ◻ allK extract) (toBatchM U B t)
    intros.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
mbind U f t =
runBatchM (f ◻ allK extract) (toBatchM U B t)
    rewrite mbind_to_mbinddt.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
mbinddt U (fun A : Type => A) (f ◻ allK extract) t =
runBatchM (f ◻ allK extract) (toBatchM U B t)
    rewrite mbinddt_to_runBatchM.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
runBatchM (f ◻ allK extract) (toBatchM U B t) =
runBatchM (f ◻ allK extract) (toBatchM U B t)
    reflexivity.
  Qed.

  Corollary mmapd_to_runBatchM `(f : K -> W * A -> B) (t : U A) :
    mmapd U f t = runBatchM (F := fun A => A) (mret T ◻ f) (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> W * A -> B
t: U A
mmapd U f t = runBatchM (mret T ◻ f) (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> W * A -> B
t: U A
mmapd U f t = runBatchM (mret T ◻ f) (toBatchM U B t)
    rewrite mmapd_to_mbinddt.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> W * A -> B
t: U A
mbinddt U (fun A : Type => A) (mret T ◻ f) t =
runBatchM (mret T ◻ f) (toBatchM U B t)
    rewrite mbinddt_to_runBatchM.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> W * A -> B
t: U A
runBatchM (mret T ◻ f) (toBatchM U B t) =
runBatchM (mret T ◻ f) (toBatchM U B t)
    reflexivity.
  Qed.

  Corollary mmapt_to_runBatchM `{Applicative F} `(f : K -> A -> F B) (t : U A) :
    mmapt U F f t = runBatchM (fun k => map (F := F) (mret T k) ∘ f k ∘ extract (W := (W ×))) (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
f: K -> A -> F B
t: U A
mmapt U F f t =
runBatchM
  (fun k : K => map (mret T k) ∘ f k ∘ extract)
  (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
f: K -> A -> F B
t: U A
mmapt U F f t =
runBatchM
  (fun k : K => map (mret T k) ∘ f k ∘ extract)
  (toBatchM U B t)
    rewrite mmapt_to_mbinddt.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
f: K -> A -> F B
t: U A
mbinddt U F ((mapMret ◻ f) ◻ allK extract) t =
runBatchM
  (fun k : K => map (mret T k) ∘ f k ∘ extract)
  (toBatchM U B t)
    rewrite mbinddt_to_runBatchM.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H1: Applicative F
A, B: Type
f: K -> A -> F B
t: U A
runBatchM ((mapMret ◻ f) ◻ allK extract)
  (toBatchM U B t) =
runBatchM
  (fun k : K => map (mret T k) ∘ f k ∘ extract)
  (toBatchM U B t)
    reflexivity.
  Qed.

  Corollary mmap_to_runBatchM `(f : K -> A -> B) (t : U A) :
    mmap U f t = runBatchM (F := fun A => A) (mret T ◻ f ◻ allK extract) (toBatchM U B t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> A -> B
t: U A
mmap U f t =
runBatchM ((mret T ◻ f) ◻ allK extract)
  (toBatchM U B t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> A -> B
t: U A
mmap U f t =
runBatchM ((mret T ◻ f) ◻ allK extract)
  (toBatchM U B t)
    rewrite mmap_to_mbinddt.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> A -> B
t: U A
mbinddt U (fun A : Type => A)
  ((mret T ◻ f) ◻ allK extract) t =
runBatchM ((mret T ◻ f) ◻ allK extract)
  (toBatchM U B t)
    rewrite mbinddt_to_runBatchM.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
f: K -> A -> B
t: U A
runBatchM ((mret T ◻ f) ◻ allK extract)
  (toBatchM U B t) =
runBatchM ((mret T ◻ f) ◻ allK extract)
  (toBatchM U B t)
    reflexivity.
  Qed.

  Lemma id_to_runBatchM `(t : U A) :
    t = runBatchM (F := fun A => A) (mret T ◻ allK extract) (toBatchM U A t).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
t = runBatchM (mret T ◻ allK extract) (toBatchM U A t)
  Proof.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
t = runBatchM (mret T ◻ allK extract) (toBatchM U A t)
    change t with (id t) at 1.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
id t =
runBatchM (mret T ◻ allK extract) (toBatchM U A t)
    rewrite <- (dtp_mbinddt_mret W T U).
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
mbinddt U (fun a : Type => a) (mret T ◻ allK extract)
  t =
runBatchM (mret T ◻ allK extract) (toBatchM U A t)
    rewrite mbinddt_to_runBatchM.
ix: Index
W: Type
T: K -> Type -> Type
U: Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
runBatchM (mret T ◻ allK extract) (toBatchM U A t) =
runBatchM (mret T ◻ allK extract) (toBatchM U A t)
    reflexivity.
  Qed.

End toBatchM.