TraversableFunctor.v

From Tealeaves Require Export
  Classes.Kleisli.TraversableFunctor
  Classes.Categorical.ContainerFunctor
  Classes.Categorical.ShapelyFunctor
  Classes.Categorical.Monad (Return, ret)
  Functors.Backwards
  Functors.Constant
  Functors.Identity
  Functors.Early.List
  Functors.ProductFunctor
  Misc.Prop.

From Tealeaves Require Import
  Classes.Categorical.ApplicativeCommutativeIdempotent.

From Tealeaves Require
  Classes.Coalgebraic.TraversableFunctor
  Adapters.KleisliToCoalgebraic.TraversableFunctor.

From Coq Require Import Logic.Decidable.

Import Kleisli.TraversableFunctor.Notations.
Import ContainerFunctor.Notations.
Import Monoid.Notations.
Import Subset.Notations.
Import Categorical.Applicative.Notations.
Import ProductFunctor.Notations. (* ◻ *)

#[local] Generalizable Variable T G M ϕ A B C.

(** * Miscellaneous Properties of Traversable Functors *)
(**********************************************************************)

(** ** Traversing in the Idempotent Center stays in the Idempotent Center *)
(**********************************************************************)
Section traverse_comm_idem.

  Context
    `{TraversableFunctor T}
    `{Applicative G}.


  Context `{f: A -> G B}
    (Hyp: forall a, IdempotentCenter G B (f a)).

  Lemma traverse_idem_center: forall (t: T A),
      IdempotentCenter G (T B) (traverse (G := G) f t).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
Hyp: forall a : A, IdempotentCenter G B (f a)
forall t : T A,
IdempotentCenter G (T B) (traverse f t)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
Hyp: forall a : A, IdempotentCenter G B (f a)
forall t : T A,
IdempotentCenter G (T B) (traverse f t)
    (* Actually, this requires the representation theorem *)
  Abort.

End traverse_comm_idem.

(** ** Interaction between <<traverse>> and <<pure>> *)
(**********************************************************************)
Section traversable_purity.

  Context
    `{TraversableFunctor T}.

  Theorem traverse_purity1:
    forall `{Applicative G},
      `(traverse (G := G) pure = @pure G _ (T A)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G -> forall A : Type, traverse pure = pure
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G -> forall A : Type, traverse pure = pure
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A: Type
traverse pure = pure
    change (@pure G _ A) with (@pure G _ A ∘ id).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A: Type
traverse (pure ∘ id) = pure
    rewrite <- (trf_traverse_morphism (G1 := fun A => A) (G2 := G)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A: Type
pure ∘ traverse id = pure
    rewrite trf_traverse_id.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A: Type
pure ∘ id = pure
    reflexivity.
  Qed.

  Lemma traverse_purity2:
    forall `{Applicative G2}
      `{Applicative G1}
      `(f: A -> G1 B),
      traverse (G := G2 ∘ G1) (pure (F := G2) ∘ f) =
        pure (F := G2) ∘ traverse f.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G2 : Type -> Type) (Map_G : Map G2)
  (Pure_G : Pure G2) (Mult_G : Mult G2),
Applicative G2 ->
forall (G1 : Type -> Type) (Map_G0 : Map G1)
  (Pure_G0 : Pure G1) (Mult_G0 : Mult G1),
Applicative G1 ->
forall (A B : Type) (f : A -> G1 B),
traverse (pure ∘ f) = pure ∘ traverse f
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G2 : Type -> Type) (Map_G : Map G2)
  (Pure_G : Pure G2) (Mult_G : Mult G2),
Applicative G2 ->
forall (G1 : Type -> Type) (Map_G0 : Map G1)
  (Pure_G0 : Pure G1) (Mult_G0 : Mult G1),
Applicative G1 ->
forall (A B : Type) (f : A -> G1 B),
traverse (pure ∘ f) = pure ∘ traverse f
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
A, B: Type
f: A -> G1 B
traverse (pure ∘ f) = pure ∘ traverse f
    rewrite <- (trf_traverse_morphism (G1 := G1) (G2 := G2 ∘ G1)
                 (ϕ := fun A => @pure G2 _ (G1 A))).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
A, B: Type
f: A -> G1 B
pure ∘ traverse f = pure ∘ traverse f
    reflexivity.
  Qed.

  Context
    `{Map T}
    `{! Compat_Map_Traverse T}.

  Lemma traverse_purity3:
    forall `{Applicative G2}
      `(f: A -> B),
      traverse (T := T) (G := G2) (pure (F := G2) ∘ f) =
        pure (F := G2) ∘ map f.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall (G2 : Type -> Type) (Map_G : Map G2)
  (Pure_G : Pure G2) (Mult_G : Mult G2),
Applicative G2 ->
forall (A B : Type) (f : A -> B),
traverse (pure ∘ f) = pure ∘ map f
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall (G2 : Type -> Type) (Map_G : Map G2)
  (Pure_G : Pure G2) (Mult_G : Mult G2),
Applicative G2 ->
forall (A B : Type) (f : A -> B),
traverse (pure ∘ f) = pure ∘ map f
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H1: Applicative G2
A, B: Type
f: A -> B
traverse (pure ∘ f) = pure ∘ map f
    rewrite <- (trf_traverse_morphism (G1 := fun A => A) (G2 := G2)
                 (ϕ := fun A => @pure G2 _ (A))).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H1: Applicative G2
A, B: Type
f: A -> B
pure ∘ traverse f = pure ∘ map f
    rewrite map_to_traverse.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H1: Applicative G2
A, B: Type
f: A -> B
pure ∘ traverse f = pure ∘ traverse f
    reflexivity.
  Qed.

End traversable_purity.

(** * Factorizing Operations through <<runBatch>> *)
(**********************************************************************)
Section factorize_operations.

  Import Coalgebraic.TraversableFunctor.
  Import Adapters.KleisliToCoalgebraic.TraversableFunctor.

  Context
    `{Map T}
    `{ToBatch T}
    `{Traverse T}
    `{! Kleisli.TraversableFunctor.TraversableFunctor T}
    `{! Compat_Map_Traverse T}
    `{! Compat_ToBatch_Traverse T}.

  (** ** Factoring operations through <<toBatch>> *)
  (********************************************************************)
  Lemma traverse_through_runBatch
    `{Applicative G} `(f: A -> G B):
    traverse f = runBatch f ∘ toBatch.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A, B: Type
f: A -> G B
traverse f = runBatch f ∘ toBatch
  Proof.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A, B: Type
f: A -> G B
traverse f = runBatch f ∘ toBatch
    rewrite toBatch_to_traverse.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A, B: Type
f: A -> G B
traverse f = runBatch f ∘ traverse (batch A B)
    rewrite trf_traverse_morphism.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A, B: Type
f: A -> G B
traverse f = traverse (runBatch f ∘ batch A B)
    rewrite (runBatch_batch G).T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H3: Applicative G
A, B: Type
f: A -> G B
traverse f = traverse f
    reflexivity.
  Qed.

  Corollary map_through_runBatch {A B: Type} (f: A -> B):
    map f = runBatch (G := fun A => A) f ∘ toBatch.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B: Type
f: A -> B
map f = runBatch f ∘ toBatch
  Proof.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B: Type
f: A -> B
map f = runBatch f ∘ toBatch
    rewrite map_to_traverse.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B: Type
f: A -> B
traverse f = runBatch f ∘ toBatch
    rewrite traverse_through_runBatch.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B: Type
f: A -> B
runBatch f ∘ toBatch = runBatch f ∘ toBatch
    reflexivity.
  Qed.

  Corollary id_through_runBatch: forall (A: Type),
      id = runBatch (G := fun A => A) id ∘ toBatch (T := T) (A' := A).T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A : Type, id = runBatch id ∘ toBatch
  Proof.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A : Type, id = runBatch id ∘ toBatch
    intros.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
id = runBatch id ∘ toBatch
    rewrite <- trf_traverse_id.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
traverse id = runBatch id ∘ toBatch
    rewrite (traverse_through_runBatch (G := fun A => A)).T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
runBatch id ∘ toBatch = runBatch id ∘ toBatch
    reflexivity.
  Qed.

  (** ** Naturality of <<toBatch>> *)
  (********************************************************************)
  Lemma toBatch_mapfst: forall (A B A': Type) (f: A -> B),
      toBatch (A := B) (A' := A') ∘ map f =
        mapfst_Batch f ∘ toBatch (A := A) (A' := A').T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall (A B A' : Type) (f : A -> B),
toBatch ∘ map f = mapfst_Batch f ∘ toBatch
  Proof.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall (A B A' : Type) (f : A -> B),
toBatch ∘ map f = mapfst_Batch f ∘ toBatch
    intros.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, A': Type
f: A -> B
toBatch ∘ map f = mapfst_Batch f ∘ toBatch
    rewrite toBatch_to_traverse.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, A': Type
f: A -> B
traverse (batch B A') ∘ map f =
mapfst_Batch f ∘ toBatch
    rewrite traverse_map.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, A': Type
f: A -> B
traverse (batch B A' ∘ f) = mapfst_Batch f ∘ toBatch
    rewrite toBatch_to_traverse.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, A': Type
f: A -> B
traverse (batch B A' ∘ f) =
mapfst_Batch f ∘ traverse (batch A A')
    rewrite (trf_traverse_morphism
               (morphism := ApplicativeMorphism_mapfst_Batch f)).T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, A': Type
f: A -> B
traverse (batch B A' ∘ f) =
traverse (mapfst_Batch f ∘ batch A A')
    rewrite ret_natural.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, A': Type
f: A -> B
traverse (batch B A' ∘ f) = traverse (batch B A' ∘ f)
    reflexivity.
  Qed.

  Lemma toBatch_mapsnd: forall (X A A': Type) (f: A -> A'),
      mapsnd_Batch f ∘ toBatch =
        map (map f) ∘ toBatch (A := X) (A' := A).T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall (X A A' : Type) (f : A -> A'),
mapsnd_Batch f ∘ toBatch = map (map f) ∘ toBatch
  Proof.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall (X A A' : Type) (f : A -> A'),
mapsnd_Batch f ∘ toBatch = map (map f) ∘ toBatch
    intros.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
X, A, A': Type
f: A -> A'
mapsnd_Batch f ∘ toBatch = map (map f) ∘ toBatch
    rewrite toBatch_to_traverse.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
X, A, A': Type
f: A -> A'
mapsnd_Batch f ∘ traverse (batch X A') =
map (map f) ∘ toBatch
    rewrite (trf_traverse_morphism
               (morphism := ApplicativeMorphism_mapsnd_Batch f)).T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
X, A, A': Type
f: A -> A'
traverse (mapsnd_Batch f ∘ batch X A') =
map (map f) ∘ toBatch
    rewrite ret_dinatural.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
X, A, A': Type
f: A -> A'
traverse (map f ∘ batch X A) = map (map f) ∘ toBatch
    rewrite toBatch_to_traverse.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
X, A, A': Type
f: A -> A'
traverse (map f ∘ batch X A) =
map (map f) ∘ traverse (batch X A)
    rewrite map_traverse.T: Type -> Type
H: Map T
H0: ToBatch T
H1: Traverse T
H2: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
X, A, A': Type
f: A -> A'
traverse (map f ∘ batch X A) =
traverse (map f ∘ batch X A)
    reflexivity.
  Qed.

End factorize_operations.

(** * Traversals by Particular Applicative Functors *)
(**********************************************************************)

(** ** Product of Two Applicative Functors *)
(**********************************************************************)
Section traverse_applicative_product.

  Definition applicative_arrow_combine {F G A B}
    `(f: A -> F B) `(g: A -> G B): A -> (F ◻ G) B :=
    fun a => product (f a) (g a).

  #[local] Notation "f <◻> g" :=
    (applicative_arrow_combine f g) (at level 60): tealeaves_scope.

  Context
    `{TraversableFunctor T}
    `{Map T}
    `{! Compat_Map_Traverse T}
    `{Applicative G1}
    `{Applicative G2}.

  Variables
    (A B: Type)
    (f: A -> G1 B)
    (g: A -> G2 B).

  Lemma traverse_product1: forall (t: T A),
      pi1 (traverse (f <◻> g) t) = traverse f t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
forall t : T A,
pi1 (traverse (f <◻> g) t) = traverse f t
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
forall t : T A,
pi1 (traverse (f <◻> g) t) = traverse f t
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
pi1 (traverse (f <◻> g) t) = traverse f t
    pose (ApplicativeMorphism_pi1 G1 G2).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
a:= ApplicativeMorphism_pi1 G1 G2: ApplicativeMorphism (G1 ◻ G2) G1 (@pi1 G1 G2)
pi1 (traverse (f <◻> g) t) = traverse f t
    compose near t on left.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
a:= ApplicativeMorphism_pi1 G1 G2: ApplicativeMorphism (G1 ◻ G2) G1 (@pi1 G1 G2)
(pi1 ∘ traverse (f <◻> g)) t = traverse f t
    rewrite trf_traverse_morphism.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
a:= ApplicativeMorphism_pi1 G1 G2: ApplicativeMorphism (G1 ◻ G2) G1 (@pi1 G1 G2)
traverse (pi1 ∘ (f <◻> g)) t = traverse f t
    reflexivity.
  Qed.

  Lemma traverse_product2: forall (t: T A),
      pi2 (traverse (f <◻> g) t) = traverse g t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
forall t : T A,
pi2 (traverse (f <◻> g) t) = traverse g t
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
forall t : T A,
pi2 (traverse (f <◻> g) t) = traverse g t
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
pi2 (traverse (f <◻> g) t) = traverse g t
    pose (ApplicativeMorphism_pi2 G1 G2).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
a:= ApplicativeMorphism_pi2 G1 G2: ApplicativeMorphism (G1 ◻ G2) G2 (@pi2 G1 G2)
pi2 (traverse (f <◻> g) t) = traverse g t
    compose near t on left.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
a:= ApplicativeMorphism_pi2 G1 G2: ApplicativeMorphism (G1 ◻ G2) G2 (@pi2 G1 G2)
(pi2 ∘ traverse (f <◻> g)) t = traverse g t
    rewrite trf_traverse_morphism.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
a:= ApplicativeMorphism_pi2 G1 G2: ApplicativeMorphism (G1 ◻ G2) G2 (@pi2 G1 G2)
traverse (pi2 ∘ (f <◻> g)) t = traverse g t
    reflexivity.
  Qed.

  Theorem traverse_product_spec:
    traverse (f <◻> g) = traverse f <◻> traverse g.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
traverse (f <◻> g) = traverse f <◻> traverse g
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
traverse (f <◻> g) = traverse f <◻> traverse g
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
traverse (f <◻> g) = traverse f <◻> traverse g
    ext t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
traverse (f <◻> g) t = (traverse f <◻> traverse g) t
    unfold applicative_arrow_combine at 2.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
traverse (f <◻> g) t =
product (traverse f t) (traverse g t)
    erewrite <- traverse_product1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
traverse (f <◻> g) t =
product (pi1 (traverse (f <◻> g) t)) (traverse g t)
    erewrite <- traverse_product2.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
traverse (f <◻> g) t =
product (pi1 (traverse (f <◻> g) t))
  (pi2 (traverse (f <◻> g) t))
    rewrite <- product_eta.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A, B: Type
f: A -> G1 B
g: A -> G2 B
t: T A
traverse (f <◻> g) t = traverse (f <◻> g) t
    reflexivity.
  Qed.

End traverse_applicative_product.

(** ** Constant Applicative Functors *)
(**********************************************************************)
Section constant_applicatives.

  Context
    `{Kleisli.TraversableFunctor.TraversableFunctor T}
    `{Monoid M}.

  Import Kleisli.TraversableFunctor.DerivedOperations.

  Lemma traverse_const1:
    forall {A: Type} (B: Type) `(f: A -> M),
      traverse (G := const M) (B := False) f =
        traverse (G := const M) (B := B) f.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (A B : Type) (f : A -> M),
traverse f = traverse f
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (A B : Type) (f : A -> M),
traverse f = traverse f
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
A, B: Type
f: A -> M
traverse f = traverse f
    change_left
      (map (F := const M) (A := T False)
         (B := T B) (map (F := T) (A := False) (B := B) exfalso)
         ∘ traverse (T := T) (G := const M)
         (B := False) (f: A -> const M False)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
A, B: Type
f: A -> M
map (map exfalso) ∘ traverse (f : A -> const M False) =
traverse f
    rewrite (map_traverse (G1 := const M)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
A, B: Type
f: A -> M
traverse (map exfalso ∘ f) = traverse f
    reflexivity.
  Qed.

  Lemma traverse_const2:
    forall {A: Type} (f: A -> M) (fake1 fake2: Type),
      traverse (G := const M) (B := fake1) f =
        traverse (G := const M) (B := fake2) f.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (A : Type) (f : A -> M) (fake1 fake2 : Type),
traverse f = traverse f
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (A : Type) (f : A -> M) (fake1 fake2 : Type),
traverse f = traverse f
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
A: Type
f: A -> M
fake1, fake2: Type
traverse f = traverse f
    rewrite <- (traverse_const1 fake1).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
A: Type
f: A -> M
fake1, fake2: Type
traverse f = traverse f
    rewrite -> (traverse_const1 fake2).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
A: Type
f: A -> M
fake1, fake2: Type
traverse f = traverse f
    reflexivity.
  Qed.

End constant_applicatives.

(** ** Traversals by Commutative Applicatives *)
(**********************************************************************)
Section traversals_commutative.

  Import Coalgebraic.TraversableFunctor.
  Import KleisliToCoalgebraic.TraversableFunctor.
  Import KleisliToCoalgebraic.TraversableFunctor.DerivedOperations.

  Lemma traverse_commutative:
    forall `{Kleisli.TraversableFunctor.TraversableFunctor T}
      `{ApplicativeCommutative G}
      (A B: Type) (f: A -> G B),
      forwards ∘ traverse (T := T)
        (G := Backwards G) (mkBackwards ∘ f) =
        traverse (T := T) f.forall (T : Type -> Type) (Traverse_T : Traverse T),
Kleisli.TraversableFunctor.TraversableFunctor T ->
forall (G : Type -> Type) (mapG : Map G)
  (pureG : Pure G) (multG : Mult G),
ApplicativeCommutative G ->
forall (A B : Type) (f : A -> G B),
forwards ∘ traverse (mkBackwards ∘ f) = traverse f
  Proof.forall (T : Type -> Type) (Traverse_T : Traverse T),
Kleisli.TraversableFunctor.TraversableFunctor T ->
forall (G : Type -> Type) (mapG : Map G)
  (pureG : Pure G) (multG : Mult G),
ApplicativeCommutative G ->
forall (A B : Type) (f : A -> G B),
forwards ∘ traverse (mkBackwards ∘ f) = traverse f
    intros.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
forwards ∘ traverse (mkBackwards ∘ f) = traverse f ext t.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
(forwards ∘ traverse (mkBackwards ∘ f)) t =
traverse f t unfold compose.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
forwards (traverse (mkBackwards ○ f) t) = traverse f t
    do 2 rewrite traverse_through_runBatch.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
forwards ((runBatch (mkBackwards ○ f) ∘ toBatch) t) =
(runBatch f ∘ toBatch) t
    unfold compose.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
forwards (runBatch (mkBackwards ○ f) (toBatch t)) =
runBatch f (toBatch t)
    induction (toBatch t).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
c: C
forwards (runBatch (mkBackwards ○ f) (Done c)) =
runBatch f (Done c)
T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
b: Batch A B (B -> C)
a: A
IHb: forwards (runBatch (mkBackwards ○ f) b) =
runBatch f b
forwards (runBatch (mkBackwards ○ f) (Step b a)) =
runBatch f (Step b a)
    -T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
c: C
forwards (runBatch (mkBackwards ○ f) (Done c)) =
runBatch f (Done c) reflexivity.
    - (*LHS *)T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
b: Batch A B (B -> C)
a: A
IHb: forwards (runBatch (mkBackwards ○ f) b) =
runBatch f b
forwards (runBatch (mkBackwards ○ f) (Step b a)) =
runBatch f (Step b a)
      rewrite runBatch_rw2.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
b: Batch A B (B -> C)
a: A
IHb: forwards (runBatch (mkBackwards ○ f) b) =
runBatch f b
forwards
  (runBatch (mkBackwards ○ f) b <⋆>
   {| forwards := f a |}) = runBatch f (Step b a)
      rewrite forwards_ap.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
b: Batch A B (B -> C)
a: A
IHb: forwards (runBatch (mkBackwards ○ f) b) =
runBatch f b
map evalAt (forwards {| forwards := f a |}) <⋆>
forwards (runBatch (mkBackwards ○ f) b) =
runBatch f (Step b a)
      rewrite IHb.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
b: Batch A B (B -> C)
a: A
IHb: forwards (runBatch (mkBackwards ○ f) b) =
runBatch f b
map evalAt (forwards {| forwards := f a |}) <⋆>
runBatch f b = runBatch f (Step b a)
      (* RHS *)
      rewrite runBatch_rw2.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
b: Batch A B (B -> C)
a: A
IHb: forwards (runBatch (mkBackwards ○ f) b) =
runBatch f b
map evalAt (forwards {| forwards := f a |}) <⋆>
runBatch f b = runBatch f b <⋆> f a
      rewrite <- (ap_swap (a := f a)).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H0: ApplicativeCommutative G
A, B: Type
f: A -> G B
t: T A
C: Type
b: Batch A B (B -> C)
a: A
IHb: forwards (runBatch (mkBackwards ○ f) b) =
runBatch f b
runBatch f b <⋆> f a = runBatch f b <⋆> f a
      reflexivity.
  Qed.

End traversals_commutative.

(*
(** ** Traversals by Subset *)
(**********************************************************************)
Section traversals_by_subset.

  Import Coalgebraic.TraversableFunctor.
  Import KleisliToCoalgebraic.TraversableFunctor.

  Lemma traverse_by_subset:
    forall `{Kleisli.TraversableFunctor.TraversableFunctor T}
      `{ToBatch T}
      `{! Compat_ToBatch_Traverse T}
      (A B: Type) (f: A -> subset B),
      forwards ∘ traverse (T := T)
        (G := Backwards subset) (mkBackwards ∘ f) =
        traverse (T := T) f.
  Proof.
    intros.
    rewrite traverse_commutative.
    intros. ext t. unfold compose.
    do 2 rewrite traverse_through_runBatch.
    unfold compose.
    induction (toBatch t).
    - reflexivity.
    - cbn. rewrite IHb.
      unfold ap.
      ext c.
      unfold_ops @Mult_subset.
      unfold_ops @Map_subset.
      propext.
      { intros [[mk b'] [[[b'' c'] [rest1 rest2]] Heq]].
        cbn in rest2.
        inversion rest2. subst.
        exists (mk, b'). tauto. }
      { intros [[mk b'] [rest1 rest2]].
        subst. exists (mk, b'). split; auto.
        exists (b', mk). tauto. }
  Qed.

End traversals_by_subset.
*)

(** * Derived Operation: <<mapReduce>> *)
(**********************************************************************)

(** ** Operation <<mapReduce>> *)
(**********************************************************************)
Definition mapReduce
  {T: Type -> Type}
  `{Traverse T}
  `{op: Monoid_op M} `{unit: Monoid_unit M}
  {A: Type} (f: A -> M): T A -> M :=
  traverse (G := const M) (B := False) f.

Section mapReduce.

  (** ** As a Special Case of <<traverse>> *)
  (********************************************************************)
  Section to_traverse.

    Context
      `{Traverse T}
      `{! TraversableFunctor T}.

    Lemma mapReduce_to_traverse1 `{Monoid M}:
      forall `(f: A -> M),
        mapReduce (T := T) f =
          traverse (G := const M) (B := False) f.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f = traverse f
    Proof.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f = traverse f
      reflexivity.
    Qed.

    Lemma mapReduce_to_traverse2 `{Monoid M}:
      forall (fake: Type) `(f: A -> M),
        mapReduce (T := T) f = traverse (G := const M) (B := fake) f.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (fake A : Type) (f : A -> M),
mapReduce f = traverse f
    Proof.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (fake A : Type) (f : A -> M),
mapReduce f = traverse f
      intros.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
fake, A: Type
f: A -> M
mapReduce f = traverse f
      rewrite mapReduce_to_traverse1.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
fake, A: Type
f: A -> M
traverse f = traverse f
      rewrite (traverse_const1 fake f).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
fake, A: Type
f: A -> M
traverse f = traverse f
      reflexivity.
    Qed.

    (** ** Composition with <<map>> and <<traverse>> *)
    (******************************************************************)
    Lemma mapReduce_traverse
      `{Monoid M} (G: Type -> Type) {B: Type} `{Applicative G}:
      forall `(g: B -> M) `(f: A -> G B),
        map (A := T B) (B := M) (mapReduce g) ∘ traverse f =
          mapReduce (map g ∘ f).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
forall (g : B -> M) (A : Type) (f : A -> G B),
map (mapReduce g) ∘ traverse f = mapReduce (map g ∘ f)
    Proof.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
forall (g : B -> M) (A : Type) (f : A -> G B),
map (mapReduce g) ∘ traverse f = mapReduce (map g ∘ f)
      intros.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
g: B -> M
A: Type
f: A -> G B
map (mapReduce g) ∘ traverse f = mapReduce (map g ∘ f)
      rewrite mapReduce_to_traverse1.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
g: B -> M
A: Type
f: A -> G B
map (traverse g) ∘ traverse f = mapReduce (map g ∘ f)
      rewrite (trf_traverse_traverse (G1 := G) (G2 := const M) A B False).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
g: B -> M
A: Type
f: A -> G B
traverse (g ⋆2 f) = mapReduce (map g ∘ f)
      rewrite mapReduce_to_traverse1.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
g: B -> M
A: Type
f: A -> G B
traverse (g ⋆2 f) = traverse (map g ∘ f)
      rewrite map_compose_const.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
g: B -> M
A: Type
f: A -> G B
traverse (g ⋆2 f) = traverse (map g ∘ f)
      rewrite mult_compose_const.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
G: Type -> Type
B: Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
g: B -> M
A: Type
f: A -> G B
traverse (g ⋆2 f) = traverse (map g ∘ f)
      reflexivity.
    Qed.

    Corollary mapReduce_map `{Map T} `{! Compat_Map_Traverse T}
      `{Monoid M}: forall `(g: B -> M) `(f: A -> B),
        mapReduce (T := T) g ∘ map f = mapReduce (g ∘ f).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
forall (B : Type) (g : B -> M) (A : Type) (f : A -> B),
mapReduce g ∘ map f = mapReduce (g ∘ f)
    Proof.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
forall (B : Type) (g : B -> M) (A : Type) (f : A -> B),
mapReduce g ∘ map f = mapReduce (g ∘ f)
      intros.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
B: Type
g: B -> M
A: Type
f: A -> B
mapReduce g ∘ map f = mapReduce (g ∘ f)
      rewrite map_to_traverse.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
B: Type
g: B -> M
A: Type
f: A -> B
mapReduce g ∘ traverse f = mapReduce (g ∘ f)
      change (mapReduce g) with
        (map (F := fun A => A) (A := T B) (B := M) (mapReduce g)).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
B: Type
g: B -> M
A: Type
f: A -> B
map (mapReduce g) ∘ traverse f = mapReduce (g ∘ f)
      now rewrite (mapReduce_traverse (fun X => X)).
    Qed.

    (** ** Composition with Homomorphisms *)
    (******************************************************************)
    Lemma mapReduce_morphism (M1 M2: Type)
      `{morphism: Monoid_Morphism M1 M2 ϕ}:
      forall `(f: A -> M1), ϕ ∘ mapReduce f = mapReduce (ϕ ∘ f).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M1, M2: Type
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
ϕ: M1 -> M2
morphism: Monoid_Morphism M1 M2 ϕ
forall (A : Type) (f : A -> M1),
ϕ ∘ mapReduce f = mapReduce (ϕ ∘ f)
    Proof.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M1, M2: Type
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
ϕ: M1 -> M2
morphism: Monoid_Morphism M1 M2 ϕ
forall (A : Type) (f : A -> M1),
ϕ ∘ mapReduce f = mapReduce (ϕ ∘ f)
      intros.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M1, M2: Type
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
ϕ: M1 -> M2
morphism: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
ϕ ∘ mapReduce f = mapReduce (ϕ ∘ f)
      inversion morphism.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M1, M2: Type
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
ϕ: M1 -> M2
morphism: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
ϕ ∘ mapReduce f = mapReduce (ϕ ∘ f)
      rewrite mapReduce_to_traverse1.T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M1, M2: Type
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
ϕ: M1 -> M2
morphism: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
ϕ ∘ traverse f = mapReduce (ϕ ∘ f)
      change ϕ with (const ϕ (T False)).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M1, M2: Type
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
ϕ: M1 -> M2
morphism: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
const ϕ (T False) ∘ traverse f =
mapReduce (const ϕ (T False) ∘ f)
      rewrite (trf_traverse_morphism (T := T)
                 (G1 := const M1) (G2 := const M2) A False).T: Type -> Type
H: Traverse T
TraversableFunctor0: TraversableFunctor T
M1, M2: Type
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
ϕ: M1 -> M2
morphism: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
traverse (const ϕ False ∘ f) =
mapReduce (const ϕ (T False) ∘ f)
      reflexivity.
    Qed.

  End to_traverse.

  (** ** Factorizing through <<runBatch>> *)
  (********************************************************************)
  Section runBatch.

    Import Coalgebraic.TraversableFunctor.
    Import KleisliToCoalgebraic.TraversableFunctor.

    Context
      `{Traverse T}
      `{! Kleisli.TraversableFunctor.TraversableFunctor T}
      `{ToBatch T}
      `{! Compat_ToBatch_Traverse T}.

    Lemma mapReduce_through_runBatch1
      {A: Type} `{Monoid M}: forall `(f: A -> M),
        mapReduce f = runBatch (G := const M) f (B := False) ∘
                      toBatch (A := A) (A' := False).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
forall f : A -> M, mapReduce f = runBatch f ∘ toBatch
    Proof.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
forall f : A -> M, mapReduce f = runBatch f ∘ toBatch
      intros.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
f: A -> M
mapReduce f = runBatch f ∘ toBatch
      rewrite mapReduce_to_traverse1.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
f: A -> M
traverse f = runBatch f ∘ toBatch
      rewrite traverse_through_runBatch.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
f: A -> M
runBatch f ∘ toBatch = runBatch f ∘ toBatch
      reflexivity.
    Qed.

    Lemma mapReduce_through_runBatch2
      `{Monoid M}: forall (A fake: Type) `(f: A -> M),
        mapReduce f = runBatch (G := const M) f (B := fake) ∘
                      toBatch (A' := fake).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
forall (A fake : Type) (f : A -> M),
mapReduce f = runBatch f ∘ toBatch
    Proof.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
forall (A fake : Type) (f : A -> M),
mapReduce f = runBatch f ∘ toBatch
      intros.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
mapReduce f = runBatch f ∘ toBatch
      rewrite mapReduce_to_traverse1.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
traverse f = runBatch f ∘ toBatch
      change (fun _: Type => M) with (const (A := Type) M).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
traverse f = runBatch f ∘ toBatch
      rewrite (traverse_const1 fake).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
traverse f = runBatch f ∘ toBatch
      rewrite (traverse_through_runBatch (G := const M)).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
runBatch f ∘ toBatch = runBatch f ∘ toBatch
      reflexivity.
    Qed.

    (** ** Factorizing through <<toBatch>> *)
    (******************************************************************)
    Lemma mapReduce_through_toBatch
      `{Monoid M}: forall (A fake: Type) `(f: A -> M) (t: T A),
        mapReduce (T := T) f t = mapReduce f (toBatch (A' := fake) t).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
forall (A fake : Type) (f : A -> M) (t : T A),
mapReduce f t = mapReduce f (toBatch t)
    Proof.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
forall (A fake : Type) (f : A -> M) (t : T A),
mapReduce f t = mapReduce f (toBatch t)
      intros.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
t: T A
mapReduce f t = mapReduce f (toBatch t)
      rewrite (mapReduce_through_runBatch2 A fake).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
t: T A
(runBatch f ∘ toBatch) t = mapReduce f (toBatch t)
      rewrite runBatch_via_traverse.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
t: T A
(map extract_Batch ∘ traverse f ∘ toBatch) t =
mapReduce f (toBatch t)
      unfold_ops @Map_const.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
t: T A
((fun t : const M (Batch fake fake (T fake)) => t)
 ∘ traverse f ∘ toBatch) t = mapReduce f (toBatch t)
      unfold compose.T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
t: T A
traverse f (toBatch t) = mapReduce f (toBatch t)
      rewrite (mapReduce_to_traverse2 fake).T: Type -> Type
H: Traverse T
H0: Kleisli.TraversableFunctor.TraversableFunctor T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H2: Monoid M
A, fake: Type
f: A -> M
t: T A
traverse f (toBatch t) = traverse f (toBatch t)
      reflexivity.
    Qed.

  End runBatch.

End mapReduce.

(** * <<mapReduce>> Corollary: <<tolist>> *)
(**********************************************************************)

(** ** Operation <<tolist>> *)
(**********************************************************************)
#[export] Instance Tolist_Traverse `{Traverse T}: Tolist T :=
  fun A => mapReduce (ret (T := list)).

Class Compat_Tolist_Traverse
  (T: Type -> Type)
  `{Tolist_inst: Tolist T}
  `{Traverse_inst: Traverse T}: Prop :=
  compat_tolist_traverse:
    Tolist_inst = @Tolist_Traverse T Traverse_inst.

#[export] Instance Compat_Tolist_Traverse_Self
  `{Traverse_T: Traverse T}:
  @Compat_Tolist_Traverse T Tolist_Traverse Traverse_T
  := ltac:(reflexivity).

Lemma tolist_to_traverse
  `{Tolist_inst: Tolist T}
  `{Traverse_T: Traverse T}
  `{! Compat_Tolist_Traverse T}:
  forall (A: Type),
    tolist = mapReduce (ret (T := list) (A := A)).T: Type -> Type
Tolist_inst: Tolist T
Traverse_T: Traverse T
Compat_Tolist_Traverse0: Compat_Tolist_Traverse T
forall A : Type, tolist = mapReduce ret
Proof.T: Type -> Type
Tolist_inst: Tolist T
Traverse_T: Traverse T
Compat_Tolist_Traverse0: Compat_Tolist_Traverse T
forall A : Type, tolist = mapReduce ret
  intros.T: Type -> Type
Tolist_inst: Tolist T
Traverse_T: Traverse T
Compat_Tolist_Traverse0: Compat_Tolist_Traverse T
A: Type
tolist = mapReduce ret
  rewrite compat_tolist_traverse.T: Type -> Type
Tolist_inst: Tolist T
Traverse_T: Traverse T
Compat_Tolist_Traverse0: Compat_Tolist_Traverse T
A: Type
Tolist_Traverse A = mapReduce ret
  reflexivity.
Qed.

(** ** Relating <<mapReduce (T := list)>> to <<mapReduce_list>> *)
(**********************************************************************)
Lemma mapReduce_eq_mapReduce_list `{Monoid M}: forall (A: Type) (f: A -> M),
    mapReduce (T := list) f = mapReduce_list f.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f = mapReduce_list f
Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f = mapReduce_list f
  intros.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
mapReduce f = mapReduce_list f ext l.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
l: list A
mapReduce f l = mapReduce_list f l induction l.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
mapReduce f nil = mapReduce_list f nil
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce f l = mapReduce_list f l
mapReduce f (a :: l) = mapReduce_list f (a :: l)
  -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
mapReduce f nil = mapReduce_list f nil cbn.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
pure nil = Ƶ reflexivity.
  -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce f l = mapReduce_list f l
mapReduce f (a :: l) = mapReduce_list f (a :: l) cbn.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce f l = mapReduce_list f l
(pure cons ● f a) ● mapReduce f l =
f a ● crush_list (map f l) change (monoid_op ?x ?y) with (x ● y).M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce f l = mapReduce_list f l
(pure cons ● f a) ● mapReduce f l =
f a ● crush_list (map f l)
    unfold_ops @Pure_const.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce f l = mapReduce_list f l
(Ƶ ● f a) ● mapReduce f l = f a ● crush_list (map f l)
    rewrite monoid_id_l.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce f l = mapReduce_list f l
f a ● mapReduce f l = f a ● crush_list (map f l)
    rewrite IHl.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce f l = mapReduce_list f l
f a ● mapReduce_list f l = f a ● crush_list (map f l)
    reflexivity.
Qed.

(** The <<tolist>> operation provided by the traversability of
    <<list>> is the identity. *)
Lemma Tolist_list_id: forall (A: Type),
    @tolist list (@Tolist_Traverse list Traverse_list) A = @id (list A).forall A : Type, tolist = id
Proof.forall A : Type, tolist = id
  intros.A: Type
tolist = id
  unfold_ops @Tolist_Traverse.A: Type
mapReduce ret = id
  rewrite mapReduce_eq_mapReduce_list.A: Type
mapReduce_list ret = id
  rewrite mapReduce_list_ret_id.A: Type
id = id
  reflexivity.
Qed.

Section tolist.

  Context
    `{TraversableFunctor T}
    `{Map T}
    `{! Compat_Map_Traverse T}.

  (** ** Naturality *)
  (********************************************************************)
  #[export] Instance Natural_Tolist_Traverse: Natural (@tolist T _).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
Natural (@tolist T Tolist_Traverse)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
Natural (@tolist T Tolist_Traverse)
    constructor; try typeclasses eauto.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
Functor T
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall (A B : Type) (f : A -> B),
map f ∘ tolist = tolist ∘ map f
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
Functor T apply DerivedInstances.Functor_TraversableFunctor.
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall (A B : Type) (f : A -> B),
map f ∘ tolist = tolist ∘ map f intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
map f ∘ tolist = tolist ∘ map f
      unfold_ops @Tolist_Traverse.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
map f ∘ mapReduce ret = mapReduce ret ∘ map f
      rewrite (mapReduce_morphism (list A) (list B)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
mapReduce (map f ∘ ret) = mapReduce ret ∘ map f
      rewrite mapReduce_map.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
mapReduce (map f ∘ ret) = mapReduce (ret ∘ f)
      rewrite (natural (ϕ := @ret list _)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
mapReduce (ret ∘ map f) = mapReduce (ret ∘ f)
      reflexivity.
  Qed.

  (** ** Rewriting <<tolist>> to <<traverse>> *)
  (********************************************************************)
  Corollary tolist_to_mapReduce: forall (A: Type),
      tolist (F := T) = mapReduce (ret (T := list) (A := A)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall A : Type, tolist = mapReduce ret
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall A : Type, tolist = mapReduce ret
    reflexivity.
  Qed.

  Corollary tolist_to_traverse1: forall (A: Type),
      tolist =
        traverse (G := const (list A)) (B := False) (ret (T := list)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall A : Type, tolist = traverse ret
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall A : Type, tolist = traverse ret
    reflexivity.
  Qed.

  Corollary tolist_to_traverse2: forall (A fake: Type),
      tolist =
        traverse (G := const (list A)) (B := fake) (ret (T := list)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall A fake : Type, tolist = traverse ret
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
forall A fake : Type, tolist = traverse ret
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, fake: Type
tolist = traverse ret
    rewrite tolist_to_traverse1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, fake: Type
traverse ret = traverse ret
    rewrite (traverse_const1 fake).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, fake: Type
traverse ret = traverse ret
    reflexivity.
  Qed.

  (** ** Factoring <<tolist>> through <<runBatch>> and <<toBatch>> *)
  (********************************************************************)
  Import Coalgebraic.TraversableFunctor.
  Import KleisliToCoalgebraic.TraversableFunctor.

  Corollary tolist_through_toBatch
  `{ToBatch T}
  `{! Compat_ToBatch_Traverse T}
    {A: Type} (tag: Type) `(t: T A):
    tolist t = tolist (toBatch (A' := tag) t).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
tolist t = tolist (toBatch t)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
tolist t = tolist (toBatch t)
    rewrite (tolist_to_mapReduce).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
mapReduce ret t = tolist (toBatch t)
    rewrite (mapReduce_through_toBatch A tag).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
mapReduce ret (toBatch t) = tolist (toBatch t)
    reflexivity.
  Qed.

  Corollary tolist_through_runBatch
  `{ToBatch T}
  `{! Compat_ToBatch_Traverse T}
    {A: Type} (tag: Type) `(t: T A):
    tolist t =
      runBatch (G := const (list A))
        (ret (T := list): A -> const (list A) tag)
        (B := tag) (toBatch (A' := tag) t).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
tolist t =
runBatch (ret : A -> const (list A) tag) (toBatch t)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
tolist t =
runBatch (ret : A -> const (list A) tag) (toBatch t)
    rewrite (tolist_to_traverse2 A tag).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
traverse ret t = runBatch ret (toBatch t)
    rewrite (traverse_through_runBatch (G := const (list A))).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
H1: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
t: T A
(runBatch ret ∘ toBatch) t = runBatch ret (toBatch t)
    reflexivity.
  Qed.

  (** ** Factoring any <<mapReduce>> through <<tolist>> *)
  (********************************************************************)
  Corollary mapReduce_through_tolist
    `{Monoid M}: forall (A: Type) (f: A -> M),
    mapReduce (T := T) f = mapReduce (T := list) f ∘ tolist.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f = mapReduce f ∘ tolist
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f = mapReduce f ∘ tolist
    intros.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A: Type
f: A -> M
mapReduce f = mapReduce f ∘ tolist
    rewrite tolist_to_mapReduce.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A: Type
f: A -> M
mapReduce f = mapReduce f ∘ mapReduce ret
    rewrite mapReduce_eq_mapReduce_list.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A: Type
f: A -> M
mapReduce f = mapReduce_list f ∘ mapReduce ret
    rewrite (mapReduce_morphism (list A) M).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A: Type
f: A -> M
mapReduce f = mapReduce (mapReduce_list f ∘ ret)
    rewrite mapReduce_list_ret.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A: Type
f: A -> M
mapReduce f = mapReduce f
    reflexivity.
  Qed.

End tolist.

(** * <<mapReduce>> Corollary: <<tosubset>> *)
(**********************************************************************)

(** ** The <<tosubset>> Operation *)
(**********************************************************************)
#[local] Instance ToSubset_Traverse `{Traverse T}:
  ToSubset T :=
  fun A => mapReduce (ret (T := subset)).

(** ** Compatibility *)
(**********************************************************************)
Class Compat_ToSubset_Traverse
  (T: Type -> Type)
  `{ToSubset_inst: ToSubset T}
  `{Traverse_inst: Traverse T}: Prop :=
  compat_tosubset_traverse:
    ToSubset_inst = @ToSubset_Traverse T Traverse_inst.

#[export] Instance Compat_ToSubset_Traverse_Self
  `{Traverse_T: Traverse T}:
  @Compat_ToSubset_Traverse T ToSubset_Traverse Traverse_T
  := ltac:(reflexivity).

Lemma tosubset_to_traverse
  `{ToSubset_inst: ToSubset T}
  `{Traverse_inst: Traverse T}
  `{! Compat_ToSubset_Traverse T}:
  forall (A: Type), tosubset (A := A) = mapReduce (ret (T := subset)).T: Type -> Type
ToSubset_inst: ToSubset T
Traverse_inst: Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall A : Type, tosubset = mapReduce ret
Proof.T: Type -> Type
ToSubset_inst: ToSubset T
Traverse_inst: Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall A : Type, tosubset = mapReduce ret
  intros.T: Type -> Type
ToSubset_inst: ToSubset T
Traverse_inst: Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
tosubset = mapReduce ret
  rewrite compat_tosubset_traverse.T: Type -> Type
ToSubset_inst: ToSubset T
Traverse_inst: Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
ToSubset_Traverse A = mapReduce ret
  reflexivity.
Qed.

Section elements.

  Context
    `{TraversableFunctor T}
    `{Map T}
    `{ToSubset T}
    `{! Compat_Map_Traverse T}
    `{! Compat_ToSubset_Traverse T}.

  (** ** Naturality *)
  (********************************************************************)
  #[export] Instance Natural_Element_Traverse:
    Natural (@tosubset T ToSubset_Traverse).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Natural (@tosubset T ToSubset_Traverse)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Natural (@tosubset T ToSubset_Traverse)
    constructor; try typeclasses eauto.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Functor T
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (f : A -> B),
map f ∘ tosubset = tosubset ∘ map f
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Functor T apply DerivedInstances.Functor_TraversableFunctor.
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (f : A -> B),
map f ∘ tosubset = tosubset ∘ map f intros A B f.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
f: A -> B
map f ∘ tosubset = tosubset ∘ map f
      unfold tosubset, ToSubset_Traverse.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
f: A -> B
map f ∘ mapReduce ret = mapReduce ret ∘ map f
      rewrite (mapReduce_morphism (subset A) (subset B)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
f: A -> B
mapReduce (map f ∘ ret) = mapReduce ret ∘ map f
      rewrite mapReduce_map.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
f: A -> B
mapReduce (map f ∘ ret) = mapReduce (ret ∘ f)
      rewrite (natural (ϕ := @ret subset _)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
f: A -> B
mapReduce (ret ∘ map f) = mapReduce (ret ∘ f)
      reflexivity.
  Qed.

  (** ** Rewriting <<tosubset>> to <<mapReduce>> *)
  (********************************************************************)
  Lemma tosubset_to_mapReduce `{Compat_ToSubset_Traverse T}:
    forall (A: Type),
      @tosubset T _ A =
        mapReduce (ret (T := subset)) (A := A).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
ToSubset_inst: ToSubset T
Traverse_inst: Traverse T
H2: Compat_ToSubset_Traverse T
forall A : Type, tosubset = mapReduce ret
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
ToSubset_inst: ToSubset T
Traverse_inst: Traverse T
H2: Compat_ToSubset_Traverse T
forall A : Type, tosubset = mapReduce ret
    rewrite compat_tosubset_traverse.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
ToSubset_inst: ToSubset T
Traverse_inst: Traverse T
H2: Compat_ToSubset_Traverse T
forall A : Type, ToSubset_Traverse A = mapReduce ret
    reflexivity.
  Qed.

  (** ** Factoring <<tosubset>> through <<tolist>> *)
  (********************************************************************)
  Corollary tosubset_through_tolist: forall A:Type,
      tosubset (F := T) (A := A) =
        tosubset (F := list) ∘ tolist (A := A).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall A : Type, tosubset = tosubset ∘ tolist
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall A : Type, tosubset = tosubset ∘ tolist
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
tosubset = tosubset ∘ tolist
    rewrite tosubset_to_mapReduce.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
mapReduce ret = tosubset ∘ tolist
    rewrite mapReduce_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
mapReduce ret ∘ tolist = tosubset ∘ tolist
    ext t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
(mapReduce ret ∘ tolist) t = (tosubset ∘ tolist) t unfold compose; induction (tolist t).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
mapReduce ret nil = tosubset nil
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
a: A
l: list A
IHl: mapReduce ret l = tosubset l
mapReduce ret (a :: l) = tosubset (a :: l)
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
mapReduce ret nil = tosubset nil reflexivity.
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
a: A
l: list A
IHl: mapReduce ret l = tosubset l
mapReduce ret (a :: l) = tosubset (a :: l) cbn.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
a: A
l: list A
IHl: mapReduce ret l = tosubset l
(pure cons ● ret a) ● mapReduce ret l =
tosubset (a :: l) rewrite IHl.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
a: A
l: list A
IHl: mapReduce ret l = tosubset l
(pure cons ● ret a) ● tosubset l = tosubset (a :: l)
      unfold transparent tcs.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
t: T A
a: A
l: list A
IHl: mapReduce ret l = tosubset l
Ƶ ∪ (fun b : A => a = b) ∪ (fun a : A => List.In a l) =
(fun a0 : A => List.In a0 (a :: l))
      now simpl_subset.
  Qed.

  (** ** Rewriting <<a ∈ t>> to <<mapReduce>> *)
  (********************************************************************)
  Lemma element_of_to_mapReduce:
    forall (A: Type) (a: A),
      element_of a =
        mapReduce (op := Monoid_op_or)
          (unit := Monoid_unit_false) {{a}}.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A : Type) (a : A),
element_of a = mapReduce {{a}}
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A : Type) (a : A),
element_of a = mapReduce {{a}}
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
element_of a = mapReduce {{a}}
    unfold element_of.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
(fun t : T A => tosubset t a) = mapReduce {{a}}
    rewrite tosubset_to_mapReduce.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
(fun t : T A => mapReduce ret t a) = mapReduce {{a}}
    ext t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
mapReduce ret t a = mapReduce {{a}} t
    change_left (evalAt a (mapReduce (ret (T := subset)) t)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
evalAt a (mapReduce ret t) = mapReduce {{a}} t
    compose near t on left.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
(evalAt a ∘ mapReduce ret) t = mapReduce {{a}} t
    rewrite (mapReduce_morphism
               (subset A) Prop (ϕ := evalAt a)
               (ret (T := subset))).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
mapReduce (evalAt a ∘ ret) t = mapReduce {{a}} t
    fequal.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
evalAt a ∘ ret = {{a}} ext b.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
b: A
(evalAt a ∘ ret) b = {{a}} b cbv.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
b: A
(b = a) = (a = b) now propext.
  Qed.

  (** ** Factoring <<a ∈ t>> through <<tolist>> *)
  (********************************************************************)
  Corollary element_of_through_tolist:
    forall (A: Type) (a: A),
      element_of (F := T) a =
        element_of (F := list) a ∘ tolist (F := T).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A : Type) (a : A),
element_of a = element_of a ∘ tolist
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A : Type) (a : A),
element_of a = element_of a ∘ tolist
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
element_of a = element_of a ∘ tolist
    ext t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
a ∈ t = (element_of a ∘ tolist) t
    unfold compose at 1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
a ∈ t = a ∈ tolist t
    unfold element_of.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
tosubset t a = tosubset (tolist t) a
    rewrite tosubset_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
(tosubset ∘ tolist) t a = tosubset (tolist t) a
    reflexivity.
  Qed.

  Corollary in_iff_in_tolist:
    forall (A: Type) (a: A) (t: T A),
      a ∈ t <-> a ∈ tolist t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A : Type) (a : A) (t : T A),
a ∈ t <-> a ∈ tolist t
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A : Type) (a : A) (t : T A),
a ∈ t <-> a ∈ tolist t
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
a: A
t: T A
a ∈ t <-> a ∈ tolist t
    now rewrite element_of_through_tolist.
  Qed.

  (** ** Factoring <<tosubset>> through <<runBatch>> *)
  (********************************************************************)
  Import Coalgebraic.TraversableFunctor.
  Import KleisliToCoalgebraic.TraversableFunctor.

  Lemma tosubset_through_runBatch1
    `{ToBatch T}
    `{! Compat_ToBatch_Traverse T}
: forall (A: Type),
      tosubset =
        runBatch (G := const (A -> Prop))
          (ret (T := subset) (A := A)) (B := False) ∘
          toBatch (A' := False).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A : Type, tosubset = runBatch ret ∘ toBatch
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A : Type, tosubset = runBatch ret ∘ toBatch
    intros.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
tosubset = runBatch ret ∘ toBatch
    rewrite tosubset_to_mapReduce.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
mapReduce ret = runBatch ret ∘ toBatch
    rewrite mapReduce_through_runBatch1.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
runBatch ret ∘ toBatch = runBatch ret ∘ toBatch
    reflexivity.
  Qed.

  Lemma tosubset_through_runBatch2
    `{ToBatch T}
    `{! Compat_ToBatch_Traverse T}
: forall (A tag: Type),
      tosubset =
        runBatch (G := const (A -> Prop))
          (ret (T := subset)) (B := tag) ∘
          toBatch (A' := tag).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A tag : Type, tosubset = runBatch ret ∘ toBatch
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A tag : Type, tosubset = runBatch ret ∘ toBatch
    intros.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
tosubset = runBatch ret ∘ toBatch
    rewrite tosubset_to_mapReduce.T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
mapReduce ret = runBatch ret ∘ toBatch
    rewrite (mapReduce_through_runBatch2 A tag).T: Type -> Type
Traverse_T: Traverse T
H: Kleisli.TraversableFunctor.TraversableFunctor T
H0: Map T
H1: ToSubset T
Compat_Map_Traverse0: Compat_Map_Traverse T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
H2: ToBatch T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, tag: Type
runBatch ret ∘ toBatch = runBatch ret ∘ toBatch
    reflexivity.
  Qed.

End elements.

#[export] Instance Compat_ToSubset_Tolist_Traverse
  `{TraversableFunctor T}:
  @Compat_ToSubset_Tolist T
    (@ToSubset_Traverse T _)
    (@Tolist_Traverse T _).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Compat_ToSubset_Tolist T
Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Compat_ToSubset_Tolist T
  hnf.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
@tosubset T ToSubset_Traverse =
@tosubset T ToSubset_Tolist
  unfold_ops @ToSubset_Traverse.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
(fun A : Type => mapReduce ret) =
@tosubset T ToSubset_Tolist
  unfold_ops @ToSubset_Tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
(fun A : Type => mapReduce ret) =
(fun A : Type => tosubset ∘ tolist)
  unfold_ops @Tolist_Traverse.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
(fun A : Type => mapReduce ret) =
(fun A : Type => tosubset ∘ mapReduce ret)
  ext A.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
mapReduce ret = tosubset ∘ mapReduce ret
  rewrite (mapReduce_morphism (list A) (subset A)
             (ϕ := @tosubset list ToSubset_list A)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
mapReduce ret = mapReduce (tosubset ∘ ret)
  rewrite tosubset_list_hom1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
mapReduce ret = mapReduce ret
  reflexivity.
Qed.

(** * <<mapReduce>> Corollary: <<Forall, Forany>> *)
(**********************************************************************)
Section quantification.

  Context
    `{TraversableFunctor T}
    `{! ToSubset T}
    `{! Compat_ToSubset_Traverse T}.

  (** ** Operations <<Forall>> and <<Forany>> *)
  (********************************************************************)
  Definition Forall `(P: A -> Prop): T A -> Prop :=
    @mapReduce T _ Prop Monoid_op_and Monoid_unit_true A P.

  Definition Forany `(P: A -> Prop): T A -> Prop :=
    @mapReduce T _ Prop Monoid_op_or Monoid_unit_false A P.

  (** ** Specification via <<element_of>> *)
  (********************************************************************)
  Lemma forall_iff `(P: A -> Prop) (t: T A):
    Forall P t <-> forall (a: A), a ∈ t -> P a.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forall P t <-> (forall a : A, a ∈ t -> P a)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forall P t <-> (forall a : A, a ∈ t -> P a)
    unfold Forall.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce P t <-> (forall a : A, a ∈ t -> P a)
    rewrite mapReduce_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
(mapReduce P ∘ tolist) t <->
(forall a : A, a ∈ t -> P a)
    unfold compose at 1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce P (tolist t) <->
(forall a : A, a ∈ t -> P a)
    setoid_rewrite in_iff_in_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce P (tolist t) <->
(forall a : A, a ∈ tolist t -> P a)
    rewrite mapReduce_eq_mapReduce_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce_list P (tolist t) <->
(forall a : A, a ∈ tolist t -> P a)
    induction (tolist t).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce_list P nil <->
(forall a : A, a ∈ nil -> P a)
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
mapReduce_list P (a :: l) <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0)
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce_list P nil <->
(forall a : A, a ∈ nil -> P a) simpl_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Ƶ <-> (forall a : A, a ∈ nil -> P a)
      unfold_ops @Monoid_unit_true.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
True <-> (forall a : A, a ∈ nil -> P a)
      unfold_ops @Monoid_unit_subset.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
True <-> (forall a : A, a ∈ nil -> P a)
      setoid_rewrite element_of_list_nil.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
True <-> (forall a : A, False -> P a)
      intuition.
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
mapReduce_list P (a :: l) <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0) simpl_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
P a ● mapReduce_list P l <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0)
      unfold_ops @Monoid_op_and.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
P a /\ mapReduce_list P l <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0)
      unfold_ops @Monoid_op_subset.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
P a /\ mapReduce_list P l <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0)
      unfold_ops @Return_subset.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
P a /\ mapReduce_list P l <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0)
      rewrite IHl.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
P a /\ (forall a : A, a ∈ l -> P a) <->
(forall a0 : A, a0 ∈ (a :: l) -> P a0)
      setoid_rewrite element_of_list_cons.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(forall a : A, a ∈ l -> P a)
P a /\ (forall a : A, a ∈ l -> P a) <->
(forall a0 : A, a0 = a \/ a0 ∈ l -> P a0)
      firstorder.T: Type -> Type
Traverse_T: Traverse T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
trf_traverse_id: forall A : Type, traverse id = id
trf_traverse_traverse: 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 B C : Type)
  (g : B -> G2 C)
  (f : A -> G1 B),
map (traverse g) ∘ traverse f =
traverse (g ⋆2 f)
trf_traverse_morphism: forall (G1 G2 : Type -> Type)
  (H : Map G1) (H0 : Mult G1)
  (H1 : Pure G1) (H2 : Map G2)
  (H3 : Mult G2)
  (H4 : Pure G2)
  (ϕ : forall A : Type,
       G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type)
  (f : A -> G1 B),
ϕ (T B) ∘ traverse f =
traverse (ϕ B ∘ f)
a0: A
H: P a
H3: forall a : A, a ∈ l -> P a
H2: a0 = a
H1: mapReduce_list P l
H0: forall a : A, a ∈ l -> P a
P a0 now subst.
  Qed.

  (* More useful for rewriting *)
  Lemma forall_iff_eq `(P: A -> Prop) (t: T A):
    Forall P t = forall (a: A), a ∈ t -> P a.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forall P t = (forall a : A, a ∈ t -> P a)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forall P t = (forall a : A, a ∈ t -> P a)
    apply propositional_extensionality.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forall P t <-> (forall a : A, a ∈ t -> P a)
    apply forall_iff.
  Qed.

  Lemma forany_iff `(P: A -> Prop) (t: T A):
    Forany P t <-> exists (a: A), a ∈ t /\ P a.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forany P t <-> (exists a : A, a ∈ t /\ P a)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forany P t <-> (exists a : A, a ∈ t /\ P a)
    unfold Forany.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce P t <-> (exists a : A, a ∈ t /\ P a)
    rewrite mapReduce_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
(mapReduce P ∘ tolist) t <->
(exists a : A, a ∈ t /\ P a)
    rewrite mapReduce_eq_mapReduce_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
(mapReduce_list P ∘ tolist) t <->
(exists a : A, a ∈ t /\ P a)
    unfold compose at 1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce_list P (tolist t) <->
(exists a : A, a ∈ t /\ P a)
    setoid_rewrite in_iff_in_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce_list P (tolist t) <->
(exists a : A, a ∈ tolist t /\ P a)
    induction (tolist t).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce_list P nil <->
(exists a : A, a ∈ nil /\ P a)
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
mapReduce_list P (a :: l) <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
mapReduce_list P nil <->
(exists a : A, a ∈ nil /\ P a) rewrite mapReduce_list_nil.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Ƶ <-> (exists a : A, a ∈ nil /\ P a)
      unfold_ops @Monoid_unit_false.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
False <-> (exists a : A, a ∈ nil /\ P a)
      setoid_rewrite element_of_list_nil.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
False <-> (exists a : A, False /\ P a)
      firstorder.
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
mapReduce_list P (a :: l) <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0) simpl_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a ● mapReduce_list P l <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
      unfold_ops @Monoid_op_or.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a \/ mapReduce_list P l <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
      unfold_ops @Monoid_op_subset.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a \/ mapReduce_list P l <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
      unfold_ops @Return_subset.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a \/ mapReduce_list P l <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
      rewrite IHl.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a \/ (exists a : A, a ∈ l /\ P a) <->
(exists a0 : A, a0 ∈ (a :: l) /\ P a0)
      setoid_rewrite element_of_list_cons.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a \/ (exists a : A, a ∈ l /\ P a) <->
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0)
      split.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a \/ (exists a : A, a ∈ l /\ P a) ->
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0) ->
P a \/ (exists a : A, a ∈ l /\ P a)
      +T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
P a \/ (exists a : A, a ∈ l /\ P a) ->
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0 intros [hyp|hyp].T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
hyp: P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
hyp: exists a : A, a ∈ l /\ P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0
        *T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
hyp: P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0 eauto.
        *T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
hyp: exists a : A, a ∈ l /\ P a
exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0 firstorder.
      +T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
(exists a0 : A, (a0 = a \/ a0 ∈ l) /\ P a0) ->
P a \/ (exists a : A, a ∈ l /\ P a) intros [a' [[hyp|hyp] rest]].T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
a': A
hyp: a' = a
rest: P a'
P a \/ (exists a : A, a ∈ l /\ P a)
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
a': A
hyp: a' ∈ l
rest: P a'
P a \/ (exists a : A, a ∈ l /\ P a)
        *T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
a': A
hyp: a' = a
rest: P a'
P a \/ (exists a : A, a ∈ l /\ P a) subst.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
rest: P a
P a \/ (exists a : A, a ∈ l /\ P a) now left.
        *T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
a': A
hyp: a' ∈ l
rest: P a'
P a \/ (exists a : A, a ∈ l /\ P a) right.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
a': A
hyp: a' ∈ l
rest: P a'
exists a : A, a ∈ l /\ P a exists a'.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
a: A
l: list A
IHl: mapReduce_list P l <->
(exists a : A, a ∈ l /\ P a)
a': A
hyp: a' ∈ l
rest: P a'
a' ∈ l /\ P a' auto.
  Qed.

  (* More useful for rewriting *)
  Lemma forany_iff_eq `(P: A -> Prop) (t: T A):
    Forany P t = exists (a: A), a ∈ t /\ P a.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forany P t = (exists a : A, a ∈ t /\ P a)
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forany P t = (exists a : A, a ∈ t /\ P a)
    apply propositional_extensionality.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
t: T A
Forany P t <-> (exists a : A, a ∈ t /\ P a)
    apply forany_iff.
  Qed.

  (** ** Decidability of <<Forall>> and <<Forany>> *)
  (**********************************************************************)
  Section decidability.

    Definition decidable_pred {A: Type} (P: A -> Prop) :=
      forall a, decidable (P a).

    Lemma decidable_pred_not_and `(P: A -> Prop) (X: decidable_pred P) (a1 a2: A):
      (~ (P a1 /\ P a2)) = ~ (P a1) \/ ~ P a2.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
X: decidable_pred P
a1, a2: A
(~ (P a1 /\ P a2)) = (~ P a1 \/ ~ P a2)
    Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
X: decidable_pred P
a1, a2: A
(~ (P a1 /\ P a2)) = (~ P a1 \/ ~ P a2)
      apply propositional_extensionality; split.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
X: decidable_pred P
a1, a2: A
~ (P a1 /\ P a2) -> ~ P a1 \/ ~ P a2
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
X: decidable_pred P
a1, a2: A
~ P a1 \/ ~ P a2 -> ~ (P a1 /\ P a2)
      -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
X: decidable_pred P
a1, a2: A
~ (P a1 /\ P a2) -> ~ P a1 \/ ~ P a2 apply not_and.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
X: decidable_pred P
a1, a2: A
decidable (P a1) apply (X a1).
      -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
X: decidable_pred P
a1, a2: A
~ P a1 \/ ~ P a2 -> ~ (P a1 /\ P a2) intros [Case1|Case2]; intuition.
    Qed.

    Lemma decidable_Forall `(P: A -> Prop) `(Dec: decidable_pred P):
      decidable_pred (Forall P).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
decidable_pred (Forall P)
    Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
decidable_pred (Forall P)
      intro t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (Forall P t)
      unfold decidable.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
Forall P t \/ ~ Forall P t
      unfold Forall.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce P t \/ ~ mapReduce P t
      rewrite mapReduce_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
(mapReduce P ∘ tolist) t \/ ~ (mapReduce P ∘ tolist) t
      rewrite mapReduce_eq_mapReduce_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
(mapReduce_list P ∘ tolist) t \/
~ (mapReduce_list P ∘ tolist) t
      unfold compose.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce_list P (tolist t) \/
~ mapReduce_list P (tolist t) induction (tolist t) as [|a rest IHrest].T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce_list P nil \/ ~ mapReduce_list P nil
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
mapReduce_list P (a :: rest) \/
~ mapReduce_list P (a :: rest)
      -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce_list P nil \/ ~ mapReduce_list P nil now left.
      -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
mapReduce_list P (a :: rest) \/
~ mapReduce_list P (a :: rest) simpl_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
P a ● mapReduce_list P rest \/
~ P a ● mapReduce_list P rest
        simplify_monoid_conjunction.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
P a /\ mapReduce_list P rest \/
~ (P a /\ mapReduce_list P rest)
        destruct IHrest as [yes_rest | no_rest];
          destruct (Dec a) as [yes_a | no_a]; tauto.
    Qed.

    Lemma decidable_Forany `(P: A -> Prop) `(Dec: decidable_pred P):
      decidable_pred (Forany P).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
decidable_pred (Forany P)
    Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
decidable_pred (Forany P)
      intro t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (Forany P t)
      unfold decidable.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
Forany P t \/ ~ Forany P t
      unfold Forany.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce P t \/ ~ mapReduce P t
      rewrite mapReduce_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
(mapReduce P ∘ tolist) t \/ ~ (mapReduce P ∘ tolist) t
      rewrite mapReduce_eq_mapReduce_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
(mapReduce_list P ∘ tolist) t \/
~ (mapReduce_list P ∘ tolist) t
      unfold compose.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce_list P (tolist t) \/
~ mapReduce_list P (tolist t) induction (tolist t) as [|a rest IHrest].T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce_list P nil \/ ~ mapReduce_list P nil
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
mapReduce_list P (a :: rest) \/
~ mapReduce_list P (a :: rest)
      -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
mapReduce_list P nil \/ ~ mapReduce_list P nil now right.
      -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
mapReduce_list P (a :: rest) \/
~ mapReduce_list P (a :: rest) simpl_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
P a ● mapReduce_list P rest \/
~ P a ● mapReduce_list P rest
        simplify_monoid_disjunction.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
rest: list A
IHrest: mapReduce_list P rest \/
~ mapReduce_list P rest
(P a \/ mapReduce_list P rest) \/
~ (P a \/ mapReduce_list P rest)
        destruct IHrest as [yes_rest | no_rest];
          destruct (Dec a) as [yes_a | no_a]; tauto.
    Qed.

    Lemma decidable_Forall_element
      `(P: A -> Prop) `(Dec: decidable_pred P) (t: T A):
      decidable (forall (a: A), a ∈ t -> P a).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (forall a : A, a ∈ t -> P a)
    Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (forall a : A, a ∈ t -> P a)
      rewrite <- forall_iff_eq.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (Forall P t)
      apply decidable_Forall.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable_pred P
      assumption.
    Qed.

    Lemma decidable_Forany_element
      `(P: A -> Prop) `(Dec: decidable_pred P) (t: T A):
      decidable (exists (a: A), a ∈ t /\ P a).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (exists a : A, a ∈ t /\ P a)
    Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (exists a : A, a ∈ t /\ P a)
      rewrite <- forany_iff_eq.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable (Forany P t)
      apply decidable_Forany.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
decidable_pred P
      assumption.
    Qed.

  End decidability.

  (** ** Corollaries of decidability *)
  (**********************************************************************)
  Lemma not_Forall_Forany_lemma1
    `(P: A -> Prop) (Dec: decidable_pred P) (t: T A):
      ~ (Forall P t) -> Forany (not ∘ P) t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ Forall P t -> Forany (not ∘ P) t
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ Forall P t -> Forany (not ∘ P) t
    unfold Forall, Forany.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ mapReduce P t -> mapReduce (not ∘ P) t
    rewrite mapReduce_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ (mapReduce P ∘ tolist) t -> mapReduce (not ∘ P) t
    rewrite (mapReduce_through_tolist _ (not ∘ P)).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ (mapReduce P ∘ tolist) t ->
(mapReduce (not ∘ P) ∘ tolist) t
    unfold compose.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ mapReduce P (tolist t) ->
mapReduce (not ○ P) (tolist t)
    induction (tolist t).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ mapReduce P nil -> mapReduce (not ○ P) nil
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
l: list A
IHl: ~ mapReduce P l -> mapReduce (not ○ P) l
~ mapReduce P (a :: l) -> mapReduce (not ○ P) (a :: l)
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ mapReduce P nil -> mapReduce (not ○ P) nil cbv.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
(True -> False) -> False firstorder.
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
l: list A
IHl: ~ mapReduce P l -> mapReduce (not ○ P) l
~ mapReduce P (a :: l) -> mapReduce (not ○ P) (a :: l) do 2 rewrite mapReduce_eq_mapReduce_list in *.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
l: list A
IHl: ~ mapReduce_list P l ->
mapReduce_list (not ○ P) l
~ mapReduce_list P (a :: l) ->
mapReduce_list (not ○ P) (a :: l)
      simpl_list.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
l: list A
IHl: ~ mapReduce_list P l ->
mapReduce_list (not ○ P) l
~ P a ● mapReduce_list P l ->
(~ P a) ● mapReduce_list (not ○ P) l
      simplify_monoid_conjunction.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
l: list A
IHl: ~ mapReduce_list P l ->
mapReduce_list (not ○ P) l
~ (P a /\ mapReduce_list P l) ->
(~ P a) ● mapReduce_list (not ○ P) l
      simplify_monoid_disjunction.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
a: A
l: list A
IHl: ~ mapReduce_list P l ->
mapReduce_list (not ○ P) l
~ (P a /\ mapReduce_list P l) ->
~ P a \/ mapReduce_list (not ○ P) l
      firstorder.
  Qed.

  Lemma not_Forall_Forany
    `(P: A -> Prop) (Dec: decidable_pred P) (t: T A):
      ~ (Forall P t) <-> Forany (not ∘ P) t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ Forall P t <-> Forany (not ∘ P) t
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ Forall P t <-> Forany (not ∘ P) t
    unfold not at 2, compose at 1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
~ Forall P t <-> Forany (fun a : A => P a -> False) t
    destruct (decidable_Forall P Dec t) as [YesAll | NotAll].T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: Forall P t
~ Forall P t <-> Forany (fun a : A => P a -> False) t
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
NotAll: ~ Forall P t
~ Forall P t <-> Forany (fun a : A => P a -> False) t
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: Forall P t
~ Forall P t <-> Forany (fun a : A => P a -> False) t split.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: Forall P t
~ Forall P t -> Forany (fun a : A => P a -> False) t
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: Forall P t
Forany (fun a : A => P a -> False) t -> ~ Forall P t
      +T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: Forall P t
~ Forall P t -> Forany (fun a : A => P a -> False) t contradiction.
      +T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: Forall P t
Forany (fun a : A => P a -> False) t -> ~ Forall P t rewrite forall_iff, forany_iff in *.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: forall a : A, a ∈ t -> P a
(exists a : A, a ∈ t /\ (P a -> False)) ->
~ (forall a : A, a ∈ t -> P a)
        intros [a [Hin HP]] _.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
YesAll: forall a : A, a ∈ t -> P a
a: A
Hin: a ∈ t
HP: P a -> False
False
        intuition.
    -T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
NotAll: ~ Forall P t
~ Forall P t <-> Forany (fun a : A => P a -> False) t split.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
NotAll: ~ Forall P t
~ Forall P t -> Forany (fun a : A => P a -> False) t
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
NotAll: ~ Forall P t
Forany (fun a : A => P a -> False) t -> ~ Forall P t
      +T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
NotAll: ~ Forall P t
~ Forall P t -> Forany (fun a : A => P a -> False) t apply not_Forall_Forany_lemma1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
NotAll: ~ Forall P t
decidable_pred P
        assumption.
      +T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
ToSubset0: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A: Type
P: A -> Prop
Dec: decidable_pred P
t: T A
NotAll: ~ Forall P t
Forany (fun a : A => P a -> False) t -> ~ Forall P t easy.
  Qed.

End quantification.

(** * <<mapReduce>> Corollary: <<plength>> *)
(**********************************************************************)
From Tealeaves Require Import Misc.NaturalNumbers.

Definition plength `{Traverse T}: forall {A}, T A -> nat :=
  fun A => mapReduce (fun _ => 1).

(** ** <<plength>> of a <<list>> *)
(**********************************************************************)
Lemma list_plength_length: forall (A: Type) (l: list A),
    plength l = length l.forall (A : Type) (l : list A), plength l = length l
Proof.forall (A : Type) (l : list A), plength l = length l
  intros.A: Type
l: list A
plength l = length l
  induction l.A: Type
plength nil = length nil
A: Type
a: A
l: list A
IHl: plength l = length l
plength (a :: l) = length (a :: l)
  -A: Type
plength nil = length nil reflexivity.
  -A: Type
a: A
l: list A
IHl: plength l = length l
plength (a :: l) = length (a :: l) cbn.A: Type
a: A
l: list A
IHl: plength l = length l
S (plength l) = S (length l) now rewrite IHl.
Qed.

(** ** Factoring <<plength>> through <<list>> *)
(**********************************************************************)
Lemma plength_through_tolist `{TraversableFunctor T}:
  forall (A: Type) (t: T A),
    plength t = length (tolist t).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (A : Type) (t : T A),
plength t = length (tolist t)
Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (A : Type) (t : T A),
plength t = length (tolist t)
  intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
t: T A
plength t = length (tolist t)
  unfold plength.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
t: T A
mapReduce (fun _ : A => 1) t = length (tolist t)
  rewrite mapReduce_through_tolist.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
t: T A
(mapReduce (fun _ : A => 1) ∘ tolist) t =
length (tolist t)
  unfold compose at 1.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
t: T A
mapReduce (fun _ : A => 1) (tolist t) =
length (tolist t)
  rewrite <- list_plength_length.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
t: T A
mapReduce (fun _ : A => 1) (tolist t) =
plength (tolist t)
  reflexivity.
Qed.

(** ** Naturality of <<plength>> *)
(**********************************************************************)
From Tealeaves Require Import
  Classes.Categorical.ShapelyFunctor (shape, shape_map).

Section naturality_plength.

  Context
    `{TraversableFunctor T}
    `{Map T}
    `{! Compat_Map_Traverse T}.

  Lemma natural_plength
    {A B: Type}:
    forall (f: A -> B) (t: T A),
      plength (map f t) = plength t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
forall (f : A -> B) (t : T A),
plength (map f t) = plength t
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
forall (f : A -> B) (t : T A),
plength (map f t) = plength t
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
t: T A
plength (map f t) = plength t
    compose near t on left.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
t: T A
(plength ∘ map f) t = plength t
    unfold plength.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
t: T A
(mapReduce (fun _ : B => 1) ∘ map f) t =
mapReduce (fun _ : A => 1) t
    rewrite (mapReduce_map).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
f: A -> B
t: T A
mapReduce ((fun _ : B => 1) ∘ f) t =
mapReduce (fun _ : A => 1) t
    reflexivity.
  Qed.

  Corollary plength_shape
    {A: Type}:
    forall (t: T A),
      plength (shape t) = plength t.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A: Type
forall t : T A, plength (shape t) = plength t
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A: Type
forall t : T A, plength (shape t) = plength t
    intros.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A: Type
t: T A
plength (shape t) = plength t
    unfold shape.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A: Type
t: T A
plength (map (const tt) t) = plength t
    rewrite natural_plength.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A: Type
t: T A
plength t = plength t
    reflexivity.
  Qed.

  Corollary same_shape_implies_plength
    {A B: Type}:
    forall (t: T A) (u: T B),
      shape t = shape u ->
      plength t = plength u.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
forall (t : T A) (u : T B),
shape t = shape u -> plength t = plength u
  Proof.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
forall (t : T A) (u : T B),
shape t = shape u -> plength t = plength u
    introv Hshape.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
t: T A
u: T B
Hshape: shape t = shape u
plength t = plength u
    rewrite <- plength_shape.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
t: T A
u: T B
Hshape: shape t = shape u
plength (shape t) = plength u
    rewrite <- (plength_shape u).T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
t: T A
u: T B
Hshape: shape t = shape u
plength (shape t) = plength (shape u)
    rewrite Hshape.T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
H0: Map T
Compat_Map_Traverse0: Compat_Map_Traverse T
A, B: Type
t: T A
u: T B
Hshape: shape t = shape u
plength (shape u) = plength (shape u)
    reflexivity.
  Qed.

End naturality_plength.

(** * <<mapReduce>> by a Commutative Monoid *)
(**********************************************************************)
Section mapReduce_commutative_monoid.

  Import List.ListNotations.

  #[local] Arguments mapReduce {T}%function_scope {H} {M}%type_scope
    (op) {unit} {A}%type_scope f%function_scope _.

  Lemma mapReduce_opposite_list
    `{unit: Monoid_unit M}
    `{op: Monoid_op M}
    `{! Monoid M} {A}: forall (f: A -> M) (l: list A),
      mapReduce op f l = mapReduce (Monoid_op_Opposite op) f (List.rev l).M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
forall (f : A -> M) (l : list A),
mapReduce op f l =
mapReduce (Monoid_op_Opposite op) f (List.rev l)
  Proof.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
forall (f : A -> M) (l : list A),
mapReduce op f l =
mapReduce (Monoid_op_Opposite op) f (List.rev l)
    intros.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
l: list A
mapReduce op f l =
mapReduce (Monoid_op_Opposite op) f (List.rev l)
    do 2 rewrite mapReduce_eq_mapReduce_list.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
l: list A
mapReduce_list f l = mapReduce_list f (List.rev l)
    induction l.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
mapReduce_list f [] = mapReduce_list f (List.rev [])
M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
mapReduce_list f (a :: l) =
mapReduce_list f (List.rev (a :: l))
    -M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
mapReduce_list f [] = mapReduce_list f (List.rev []) reflexivity.
    -M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
mapReduce_list f (a :: l) =
mapReduce_list f (List.rev (a :: l)) rewrite mapReduce_list_cons.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
f a ● mapReduce_list f l =
mapReduce_list f (List.rev (a :: l))
      change (List.rev (a :: l)) with (List.rev l ++ [a]).M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
f a ● mapReduce_list f l =
mapReduce_list f (List.rev l ++ [a])
      rewrite mapReduce_list_app.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
f a ● mapReduce_list f l =
mapReduce_list f (List.rev l) ● mapReduce_list f [a]
      rewrite IHl.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
f a ● mapReduce_list f (List.rev l) =
mapReduce_list f (List.rev l) ● mapReduce_list f [a]
      unfold_ops @Monoid_op_Opposite.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
f a ● mapReduce_list f (List.rev l) =
mapReduce_list f [a] ● mapReduce_list f (List.rev l)
      rewrite mapReduce_list_one.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
f: A -> M
a: A
l: list A
IHl: mapReduce_list f l =
mapReduce_list f (List.rev l)
f a ● mapReduce_list f (List.rev l) =
f a ● mapReduce_list f (List.rev l)
      reflexivity.
  Qed.

  Lemma mapReduce_comm_list
    `{unit: Monoid_unit M}
    `{op: Monoid_op M}
    `{! Monoid M}
    {A: Type}
    `{comm: ! CommutativeMonoidOp op}
: forall (f: A -> M) (l: list A),
      mapReduce op f l = mapReduce op f (List.rev l).M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
forall (f : A -> M) (l : list A),
mapReduce op f l = mapReduce op f (List.rev l)
  Proof.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
forall (f : A -> M) (l : list A),
mapReduce op f l = mapReduce op f (List.rev l)
    intros.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
l: list A
mapReduce op f l = mapReduce op f (List.rev l)
    induction l.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
mapReduce op f [] = mapReduce op f (List.rev [])
M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce op f (a :: l) =
mapReduce op f (List.rev (a :: l))
    -M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
mapReduce op f [] = mapReduce op f (List.rev []) reflexivity.
    -M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce op f (a :: l) =
mapReduce op f (List.rev (a :: l)) rewrite mapReduce_eq_mapReduce_list.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce_list f (a :: l) =
mapReduce_list f (List.rev (a :: l))
      rewrite mapReduce_list_cons.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
f a ● mapReduce_list f l =
mapReduce_list f (List.rev (a :: l))
      rewrite (comm_mon_swap (f a)).M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce_list f l ● f a =
mapReduce_list f (List.rev (a :: l))
      change (List.rev (a :: l)) with (List.rev l ++ [a]).M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce_list f l ● f a =
mapReduce_list f (List.rev l ++ [a])
      rewrite mapReduce_list_app.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce_list f l ● f a =
mapReduce_list f (List.rev l) ● mapReduce_list f [a]
      rewrite mapReduce_list_one.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce_list f l ● f a =
mapReduce_list f (List.rev l) ● f a
      rewrite <- mapReduce_eq_mapReduce_list.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce op f l ● f a =
mapReduce op f (List.rev l) ● f a
      rewrite IHl.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
A: Type
comm: CommutativeMonoidOp op
f: A -> M
a: A
l: list A
IHl: mapReduce op f l = mapReduce op f (List.rev l)
mapReduce op f (List.rev l) ● f a =
mapReduce op f (List.rev l) ● f a
      reflexivity.
  Qed.

  Lemma mapReduce_comm
    `{unit: Monoid_unit M}
    `{op: Monoid_op M}
    `{! Monoid M}
    `{comm: ! CommutativeMonoidOp op}
    `{TraversableFunctor T} {A: Type}:
    forall (f: A -> M) (t: T A),
      mapReduce op f t =
        mapReduce (Monoid_op_Opposite op) f t.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
forall (f : A -> M) (t : T A),
mapReduce op f t =
mapReduce (Monoid_op_Opposite op) f t
  Proof.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
forall (f : A -> M) (t : T A),
mapReduce op f t =
mapReduce (Monoid_op_Opposite op) f t
    intros.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
f: A -> M
t: T A
mapReduce op f t =
mapReduce (Monoid_op_Opposite op) f t
    rewrite (mapReduce_through_tolist _ f).M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
f: A -> M
t: T A
(mapReduce op f ∘ tolist) t =
mapReduce (Monoid_op_Opposite op) f t
    rewrite (mapReduce_through_tolist (op := Monoid_op_Opposite op)).M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
f: A -> M
t: T A
(mapReduce op f ∘ tolist) t =
(mapReduce (Monoid_op_Opposite op) f ∘ tolist) t
    unfold compose.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
f: A -> M
t: T A
mapReduce op f (tolist t) =
mapReduce (Monoid_op_Opposite op) f (tolist t)
    rewrite mapReduce_opposite_list.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
f: A -> M
t: T A
mapReduce (Monoid_op_Opposite op) f
  (List.rev (tolist t)) =
mapReduce (Monoid_op_Opposite op) f (tolist t)
    rewrite <- mapReduce_comm_list.M: Type
unit: Monoid_unit M
op: Monoid_op M
Monoid0: Monoid M
comm: CommutativeMonoidOp op
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
f: A -> M
t: T A
mapReduce (Monoid_op_Opposite op) f (tolist t) =
mapReduce (Monoid_op_Opposite op) f (tolist t)
    reflexivity.
  Qed.

End mapReduce_commutative_monoid.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Notation "f <◻> g" := (applicative_arrow_combine f g)
                          (at level 60): tealeaves_scope.
End Notations.