List.v

From Tealeaves Require Export
  Classes.Functor
  Classes.Monoid.

From Tealeaves Require Import
  Classes.Categorical.Monad
  Classes.Categorical.ContainerFunctor
  Classes.Kleisli.Monad
  Classes.Kleisli.TraversableMonad
  Classes.Kleisli.TraversableFunctor.

Import Kleisli.TraversableMonad.Notations.
Import Kleisli.TraversableFunctor.Notations.
Import Kleisli.Monad.Notations.
Import List.ListNotations.
Import Monoid.Notations.
Import Subset.Notations.
Import ContainerFunctor.Notations.
Import Applicative.Notations.
Open Scope list_scope.

#[local] Generalizable Variables A B M ϕ G.

(** * Automation: <<simpl_list>> *)
(**********************************************************************)
Create HintDb tea_list.
Tactic Notation "simpl_list" :=
  (autorewrite with tea_list).
Tactic Notation "simpl_list" "in" hyp(H) :=
  (autorewrite with tea_list H).
Tactic Notation "simpl_list" "in" "*" :=
  (autorewrite with tea_list in *).

(** * Monoid Instance *)
(**********************************************************************)
#[export] Instance Monoid_op_list {A}: Monoid_op (list A) := @app A.

#[export] Instance Monoid_unit_list {A}: Monoid_unit (list A) := nil.

#[export, program] Instance Monoid_list {A}:
  @Monoid (list A) (@Monoid_op_list A) (@Monoid_unit_list A).

Solve Obligations with
  (intros; unfold transparent tcs; auto with datatypes).

(** ** Simplification *)
(**********************************************************************)
Lemma monoid_append_rw:
  forall {A} (l1 l2: list A),
    monoid_op (Monoid_op := Monoid_op_list) l1 l2 = l1 ++ l2.forall (A : Type) (l1 l2 : list A), l1 ● l2 = l1 ++ l2
Proof.forall (A : Type) (l1 l2 : list A), l1 ● l2 = l1 ++ l2
  reflexivity.
Qed.

Lemma monoid_list_unit_rw:
  forall {A}, (Ƶ: list A) = [].forall A : Type, (Ƶ : list A) = []
Proof.forall A : Type, (Ƶ : list A) = []
  reflexivity.
Qed.

Ltac simplify_monoid_list :=
  repeat first [ rewrite monoid_list_unit_rw
               | rewrite monoid_append_rw
    ].

(** * [Functor] Instance *)
(**********************************************************************)
#[export] Instance Map_list: Map list :=
  fun A B => @List.map A B.

(** ** Rewriting Laws for <<map>> *)
(**********************************************************************)
Section map_list_rw.

  Context
    {A B: Type}
    (f: A -> B).

  Lemma map_list_nil: map f (@nil A) = @nil B.A, B: Type
f: A -> B
map f [] = []
  Proof.A, B: Type
f: A -> B
map f [] = []
    reflexivity.
  Qed.

  Lemma map_list_cons: forall (x: A) (xs: list A),
      map f (x :: xs) = f x :: map f xs.A, B: Type
f: A -> B
forall (x : A) (xs : list A),
map f (x :: xs) = f x :: map f xs
  Proof.A, B: Type
f: A -> B
forall (x : A) (xs : list A),
map f (x :: xs) = f x :: map f xs
    reflexivity.
  Qed.

  Lemma map_list_one (a: A): map f [ a ] = [f a].A, B: Type
f: A -> B
a: A
map f [a] = [f a]
  Proof.A, B: Type
f: A -> B
a: A
map f [a] = [f a]
    reflexivity.
  Qed.

  Lemma map_list_app: forall (l1 l2: list A),
      map f (l1 ++ l2) = map f l1 ++ map f l2.A, B: Type
f: A -> B
forall l1 l2 : list A,
map f (l1 ++ l2) = map f l1 ++ map f l2
  Proof.A, B: Type
f: A -> B
forall l1 l2 : list A,
map f (l1 ++ l2) = map f l1 ++ map f l2
    intros.A, B: Type
f: A -> B
l1, l2: list A
map f (l1 ++ l2) = map f l1 ++ map f l2
    unfold transparent tcs.A, B: Type
f: A -> B
l1, l2: list A
List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2
    now rewrites List.map_app.
  Qed.

End map_list_rw.

#[export] Hint Rewrite @map_list_nil @map_list_cons
  @map_list_one @map_list_app: tea_list.

(** ** Functor Laws *)
(**********************************************************************)
Theorem map_id_list {A}: map (F := list) (@id A) = id.A: Type
map id = id
Proof.A: Type
map id = id
  ext l.A: Type
l: list A
map id l = id l induction l as [| ? ? IH]; simpl_list.A: Type
[] = id []
A: Type
a: A
l: list A
IH: map id l = id l
id a :: map id l = id (a :: l)
  trivial.A: Type
a: A
l: list A
IH: map id l = id l
id a :: map id l = id (a :: l) now rewrite IH.
Qed.

Theorem map_map_list {A B C}: forall (f: A -> B) (g: B -> C),
    map g ∘ map f = map (F := list) (g ∘ f).A, B, C: Type
forall (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
Proof.A, B, C: Type
forall (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  intros.A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) unfold compose.A, B, C: Type
f: A -> B
g: B -> C
map g ○ map f = map (g ○ f) ext l.A, B, C: Type
f: A -> B
g: B -> C
l: list A
map g (map f l) = map (g ○ f) l induction l as [| ? ? IH]; simpl_list.A, B, C: Type
f: A -> B
g: B -> C
[] = []
A, B, C: Type
f: A -> B
g: B -> C
a: A
l: list A
IH: map g (map f l) = map (g ○ f) l
g (f a) :: map g (map f l) = g (f a) :: map (g ○ f) l
  trivial.A, B, C: Type
f: A -> B
g: B -> C
a: A
l: list A
IH: map g (map f l) = map (g ○ f) l
g (f a) :: map g (map f l) = g (f a) :: map (g ○ f) l now rewrite IH.
Qed.

#[export] Instance Functor_list: Functor list :=
  {| fun_map_id := @map_id_list;
     fun_map_map := @map_map_list;
  |}.

(** ** <<map>> is a Monoid Homomorphism *)
(**********************************************************************)
#[export, program] Instance Monmor_list_map `(f: A -> B):
  Monoid_Morphism (list A) (list B) (map f) :=
  {| monmor_op := map_list_app f;
  |}.

(** * Monad Instance (Categorical) *)
(**********************************************************************)

(** ** Monad Operations *)
(**********************************************************************)
#[export] Instance Return_list: Return list := fun A a => cons a nil.

#[export] Instance Join_list: Join list := @List.concat.

(** ** Rewriting Laws for <<join>> *)
(**********************************************************************)
Lemma join_list_nil:
  `(join ([]: list (list A)) = []).forall A : Type, join ([] : list (list A)) = []
Proof.forall A : Type, join ([] : list (list A)) = []
  reflexivity.
Qed.

Lemma join_list_cons: forall A (l: list A) (ll: list (list A)),
    join (l :: ll) = l ++ join ll.forall (A : Type) (l : list A) (ll : list (list A)),
join (l :: ll) = l ++ join ll
Proof.forall (A : Type) (l : list A) (ll : list (list A)),
join (l :: ll) = l ++ join ll
  reflexivity.
Qed.

Lemma join_list_one: forall A (l: list A),
    join [ l ] = l.forall (A : Type) (l : list A), join [l] = l
Proof.forall (A : Type) (l : list A), join [l] = l
  intros.A: Type
l: list A
join [l] = l cbn.A: Type
l: list A
l ++ [] = l now List.simpl_list.
Qed.

Lemma join_list_app: forall A (l1 l2: list (list A)),
    join (l1 ++ l2) = join l1 ++ join l2.forall (A : Type) (l1 l2 : list (list A)),
join (l1 ++ l2) = join l1 ++ join l2
Proof.forall (A : Type) (l1 l2 : list (list A)),
join (l1 ++ l2) = join l1 ++ join l2
  apply List.concat_app.
Qed.

#[export] Hint Rewrite join_list_nil join_list_cons
  join_list_one join_list_app: tea_list.

(** ** Monad Laws *)
(**********************************************************************)
#[export] Instance Natural_ret_list: Natural (@ret list _).Natural (@ret list Return_list)
Proof.Natural (@ret list Return_list)
  constructor; try typeclasses eauto.forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f
  introv.A, B: Type
f: A -> B
map f ∘ ret = ret ∘ map f now ext l.
Qed.

#[export] Instance Natural_join_list: Natural (@join list _).Natural (@join list Join_list)
Proof.Natural (@join list Join_list)
  constructor; try typeclasses eauto.forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map f
  intros ? ? f.A, B: Type
f: A -> B
map f ∘ join = join ∘ map f ext l.A, B: Type
f: A -> B
l: (list ∘ list) A
(map f ∘ join) l = (join ∘ map f) l unfold compose.A, B: Type
f: A -> B
l: (list ∘ list) A
map f (join l) = join (map f l) induction l as [| ? ? IHl].A, B: Type
f: A -> B
map f (join []) = join (map f [])
A, B: Type
f: A -> B
a: list A
l: list (list A)
IHl: map f (join l) = join (map f l)
map f (join (a :: l)) = join (map f (a :: l))
  -A, B: Type
f: A -> B
map f (join []) = join (map f []) reflexivity.
  -A, B: Type
f: A -> B
a: list A
l: list (list A)
IHl: map f (join l) = join (map f l)
map f (join (a :: l)) = join (map f (a :: l)) simpl_list.A, B: Type
f: A -> B
a: list A
l: list (list A)
IHl: map f (join l) = join (map f l)
map f a ++ map f (join l) = join (map f (a :: l)) now rewrite IHl.
Qed.

Theorem join_ret_list {A}:
  join ∘ ret (T := list) = @id (list A).A: Type
join ∘ ret = id
Proof.A: Type
join ∘ ret = id
  ext l.A: Type
l: list A
(join ∘ ret) l = id l unfold compose.A: Type
l: list A
join (ret l) = id l destruct l.A: Type
join (ret []) = id []
A: Type
a: A
l: list A
join (ret (a :: l)) = id (a :: l)
  -A: Type
join (ret []) = id [] reflexivity.
  -A: Type
a: A
l: list A
join (ret (a :: l)) = id (a :: l) cbn.A: Type
a: A
l: list A
a :: l ++ [] = id (a :: l) now List.simpl_list.
Qed.

Theorem join_map_ret_list {A}:
  join ∘ map (F := list) (ret (T := list)) = @id (list A).A: Type
join ∘ map ret = id
Proof.A: Type
join ∘ map ret = id
  ext l.A: Type
l: list A
(join ∘ map ret) l = id l unfold compose.A: Type
l: list A
join (map ret l) = id l induction l as [| ? ? IHl].A: Type
join (map ret []) = id []
A: Type
a: A
l: list A
IHl: join (map ret l) = id l
join (map ret (a :: l)) = id (a :: l)
  -A: Type
join (map ret []) = id [] reflexivity.
  -A: Type
a: A
l: list A
IHl: join (map ret l) = id l
join (map ret (a :: l)) = id (a :: l) simpl_list.A: Type
a: A
l: list A
IHl: join (map ret l) = id l
ret a ++ join (map ret l) = id (a :: l) now rewrite IHl.
Qed.

Theorem join_join_list {A}:
  join (T := list) ∘ join (T := list) (A:=list A) =
    join ∘ map (F := list) (join).A: Type
join ∘ join = join ∘ map join
Proof.A: Type
join ∘ join = join ∘ map join
  ext l.A: Type
l: (list ∘ list) (list A)
(join ∘ join) l = (join ∘ map join) l unfold compose.A: Type
l: (list ∘ list) (list A)
join (join l) = join (map join l) induction l as [| ? ? IHl].A: Type
join (join []) = join (map join [])
A: Type
a: list (list A)
l: list (list (list A))
IHl: join (join l) = join (map join l)
join (join (a :: l)) = join (map join (a :: l))
  -A: Type
join (join []) = join (map join []) reflexivity.
  -A: Type
a: list (list A)
l: list (list (list A))
IHl: join (join l) = join (map join l)
join (join (a :: l)) = join (map join (a :: l)) simpl_list.A: Type
a: list (list A)
l: list (list (list A))
IHl: join (join l) = join (map join l)
join a ++ join (join l) = join a ++ join (map join l) now rewrite IHl.
Qed.

#[export] Instance CategoricalMonad_list:
  Categorical.Monad.Monad list :=
  {| mon_join_ret := @join_ret_list;
     mon_join_map_ret := @join_map_ret_list;
     mon_join_join := @join_join_list;
  |}.

(** ** [join] is a monoid homomorphism *)
(** This is a special case of the fact that monoid homomorphisms on
    free monoids are exact those of of the form <<mapReduce f>> *)
#[export] Instance Monmor_join (A: Type):
  Monoid_Morphism (list (list A)) (list A) (join (A := A)) :=
  {| monmor_unit := @join_list_nil A;
     monmor_op := @join_list_app A;
  |}.

(** * Traversable Monad Instance (Kleisli) *)
(**********************************************************************)

(** ** The <<bindt>> Operation *)
(**********************************************************************)
Fixpoint bindt_list (G: Type -> Type)
  `{Map G} `{Pure G} `{Mult G}
  (A B: Type) (f: A -> G (list B)) (l: list A)
: G (list B) :=
  match l with
  | nil => pure (@nil B)
  | x :: xs =>
      pure (@List.app B) <⋆> f x <⋆> bindt_list G A B f xs
  end.

#[export] Instance Bindt_list: Bindt list list := @bindt_list.

#[export] Instance Compat_Map_Bindt_list:
  Compat_Map_Bindt list list.Compat_Map_Bindt list list
Proof.Compat_Map_Bindt list list
  hnf.Map_list = DerivedOperations.Map_Bindt list list ext A B f l.A, B: Type
f: A -> B
l: list A
Map_list A B f l =
DerivedOperations.Map_Bindt list list A B f l
  induction l as [|a rest IHrest].A, B: Type
f: A -> B
Map_list A B f [] =
DerivedOperations.Map_Bindt list list A B f []
A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Bindt list list A B f
  rest
Map_list A B f (a :: rest) =
DerivedOperations.Map_Bindt list list A B f
  (a :: rest)
  -A, B: Type
f: A -> B
Map_list A B f [] =
DerivedOperations.Map_Bindt list list A B f [] reflexivity.
  -A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Bindt list list A B f
  rest
Map_list A B f (a :: rest) =
DerivedOperations.Map_Bindt list list A B f
  (a :: rest) cbn.A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Bindt list list A B f
  rest
f a :: Map_list A B f rest =
f a
:: DerivedOperations.Map_Bindt list list A B f rest now rewrite IHrest.
Qed.

(** ** Rewriting Laws for <<bindt>> *)
(**********************************************************************)
Section bindt_rewriting_lemmas.

  Context
    (G: Type -> Type)
    `{Applicative G}
    (A B: Type).

  Lemma bindt_list_nil: forall (f: A -> G (list B)),
      bindt f (@nil A) = pure (@nil B).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall f : A -> G (list B), bindt f [] = pure []
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall f : A -> G (list B), bindt f [] = pure []
    reflexivity.
  Qed.

  Lemma bindt_list_one: forall (f: A -> G (list B)) (a: A),
      bindt f (ret (T := list) a) = f a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G (list B)) (a : A),
bindt f (ret a) = f a
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G (list B)) (a : A),
bindt f (ret a) = f a
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
bindt f (ret a) = f a
    cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
pure (app (A:=B)) <⋆> f a <⋆> pure [] = f a
    rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
pure (evalAt []) <⋆> (pure (app (A:=B)) <⋆> f a) = f a
    rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
pure compose <⋆> pure (evalAt []) <⋆>
pure (app (A:=B)) <⋆> f a = f a
    rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
pure (compose (evalAt [])) <⋆> pure (app (A:=B)) <⋆>
f a = f a
    rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
pure (evalAt [] ∘ app (A:=B)) <⋆> f a = f a
    rewrite <- ap1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
pure (evalAt [] ∘ app (A:=B)) <⋆> f a =
pure id <⋆> f a
    unfold compose; do 2 fequal;
      ext l; rewrite (List.app_nil_end).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l: list B
evalAt [] (app l) = id l ++ []
    reflexivity.
  Qed.

  Lemma bindt_list_cons: forall (f: A -> G (list B)) (a: A) (l: list A),
      bindt f (a :: l) =
        pure (@app B) <⋆> f a <⋆> bindt f l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G (list B)) (a : A) (l : list A),
bindt f (a :: l) =
pure (app (A:=B)) <⋆> f a <⋆> bindt f l
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G (list B)) (a : A) (l : list A),
bindt f (a :: l) =
pure (app (A:=B)) <⋆> f a <⋆> bindt f l
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l: list A
bindt f (a :: l) =
pure (app (A:=B)) <⋆> f a <⋆> bindt f l
    reflexivity.
  Qed.

  Lemma bindt_list_app: forall (f: A -> G (list B)) (l1 l2: list A),
      bindt f (l1 ++ l2) =
        pure (@app B) <⋆> bindt f l1 <⋆> bindt f l2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G (list B)) (l1 l2 : list A),
bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G (list B)) (l1 l2 : list A),
bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
l1, l2: list A
bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
    induction l1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
l2: list A
bindt f ([] ++ l2) =
pure (app (A:=B)) <⋆> bindt f [] <⋆> bindt f l2
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
bindt f ((a :: l1) ++ l2) =
pure (app (A:=B)) <⋆> bindt f (a :: l1) <⋆> bindt f l2
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
l2: list A
bindt f ([] ++ l2) =
pure (app (A:=B)) <⋆> bindt f [] <⋆> bindt f l2 cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
l2: list A
bindt f l2 =
pure (app (A:=B)) <⋆> pure [] <⋆> bindt f l2 rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
l2: list A
bindt f l2 = pure (app []) <⋆> bindt f l2
      rewrite ap1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
l2: list A
bindt f l2 = bindt f l2
      reflexivity.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
bindt f ((a :: l1) ++ l2) =
pure (app (A:=B)) <⋆> bindt f (a :: l1) <⋆> bindt f l2 cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
pure (app (A:=B)) <⋆> f a <⋆> bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆>
(pure (app (A:=B)) <⋆> f a <⋆> bindt f l1) <⋆>
bindt f l2
      rewrite IHl1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
pure (app (A:=B)) <⋆> f a <⋆>
(pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2) =
pure (app (A:=B)) <⋆>
(pure (app (A:=B)) <⋆> f a <⋆> bindt f l1) <⋆>
bindt f l2
      repeat rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure (app (A:=B)) <⋆> f a <⋆>
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2 =
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure (app (A:=B)) <⋆> pure (app (A:=B)) <⋆> f a <⋆>
bindt f l1 <⋆> bindt f l2
      repeat rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
pure
  ((compose ∘ compose) compose compose compose compose
     (app (A:=B))) <⋆> f a <⋆> pure (app (A:=B)) <⋆>
bindt f l1 <⋆> bindt f l2 =
pure ((compose ∘ compose) (app (A:=B)) (app (A:=B))) <⋆>
f a <⋆> bindt f l1 <⋆> bindt f l2
      rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
pure (evalAt (app (A:=B))) <⋆>
(pure
   ((compose ∘ compose) compose compose compose
      compose (app (A:=B))) <⋆> f a) <⋆> bindt f l1 <⋆>
bindt f l2 =
pure ((compose ∘ compose) (app (A:=B)) (app (A:=B))) <⋆>
f a <⋆> bindt f l1 <⋆> bindt f l2
      repeat rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
pure compose <⋆> pure (evalAt (app (A:=B))) <⋆>
pure
  ((compose ∘ compose) compose compose compose compose
     (app (A:=B))) <⋆> f a <⋆> bindt f l1 <⋆>
bindt f l2 =
pure ((compose ∘ compose) (app (A:=B)) (app (A:=B))) <⋆>
f a <⋆> bindt f l1 <⋆> bindt f l2
      repeat rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
pure
  (evalAt (app (A:=B))
   ∘ (compose ∘ compose) compose compose compose
       compose (app (A:=B))) <⋆> f a <⋆> bindt f l1 <⋆>
bindt f l2 =
pure ((compose ∘ compose) (app (A:=B)) (app (A:=B))) <⋆>
f a <⋆> bindt f l1 <⋆> bindt f l2
      repeat fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
evalAt (app (A:=B))
∘ (compose ∘ compose) compose compose compose compose
    (app (A:=B)) =
(compose ∘ compose) (app (A:=B)) (app (A:=B))
      ext x y z.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
x, y, z: list B
(evalAt (app (A:=B))
 ∘ (compose ∘ compose) compose compose compose compose
     (app (A:=B))) x y z =
(compose ∘ compose) (app (A:=B)) (app (A:=B)) x y z unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
x, y, z: list B
evalAt (app (A:=B))
  (fun (f : list B -> list B -> list B) (a : list B)
   => app x ○ f a) y z = (x ++ y) ++ z
      unfold evalAt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (list B)
a: A
l1, l2: list A
IHl1: bindt f (l1 ++ l2) =
pure (app (A:=B)) <⋆> bindt f l1 <⋆> bindt f l2
x, y, z: list B
x ++ y ++ z = (x ++ y) ++ z
      now rewrite List.app_assoc.
  Qed.

End bindt_rewriting_lemmas.

#[export] Hint Rewrite bindt_list_nil bindt_list_cons
  bindt_list_one bindt_list_app:
  tea_list.

(** ** Traversable Monad Laws *)
(**********************************************************************)
Section bindt_laws.

  Context
    (G: Type -> Type)
    `{Applicative G}
    `{Applicative G1}
    `{Applicative G2}
    (A B C: Type).

  Lemma list_bindt0: forall (f: A -> G (list B)),
      bindt f ∘ ret = f.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
forall f : A -> G (list B), bindt f ∘ ret = f
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
forall f : A -> G (list B), bindt f ∘ ret = f
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
f: A -> G (list B)
bindt f ∘ ret = f ext a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
f: A -> G (list B)
a: A
(bindt f ∘ ret) a = f a
    apply (bindt_list_one G).
  Qed.

  Lemma list_bindt1:
    bindt (T := list) (U := list)
      (A := A) (B := A) (G := fun A => A) (ret (T := list)) = id.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
bindt ret = id
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
bindt ret = id
    ext l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
l: list A
bindt ret l = id l induction l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
bindt ret [] = id []
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: bindt ret l = id l
bindt ret (a :: l) = id (a :: l)
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
bindt ret [] = id [] reflexivity.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: bindt ret l = id l
bindt ret (a :: l) = id (a :: l) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: bindt ret l = id l
a :: bindt ret l = id (a :: l) rewrite IHl.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: bindt ret l = id l
a :: id l = id (a :: l)
      reflexivity.
  Qed.

  Lemma list_bindt2:
    forall (g: B -> G2 (list C)) (f: A -> G1 (list B)),
      map (F := G1) (bindt g) ∘ bindt f =
        bindt (G := G1 ∘ G2) (g ⋆6 f).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
forall (g : B -> G2 (list C)) (f : A -> G1 (list B)),
map (bindt g) ∘ bindt f = bindt (g ⋆6 f)
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
forall (g : B -> G2 (list C)) (f : A -> G1 (list B)),
map (bindt g) ∘ bindt f = bindt (g ⋆6 f)
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
map (bindt g) ∘ bindt f = bindt (g ⋆6 f) ext l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
l: list A
(map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l induction l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
(map (bindt g) ∘ bindt f) [] = bindt (g ⋆6 f) []
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
(map (bindt g) ∘ bindt f) (a :: l) =
bindt (g ⋆6 f) (a :: l)
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
(map (bindt g) ∘ bindt f) [] = bindt (g ⋆6 f) [] unfold compose; cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
map (bindt g) (pure []) = pure []
      rewrite app_pure_natural.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
pure (bindt g []) = pure []
      rewrite bindt_list_nil.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
pure (pure []) = pure []
      reflexivity.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
(map (bindt g) ∘ bindt f) (a :: l) =
bindt (g ⋆6 f) (a :: l) unfold compose at 1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
map (bindt g) (bindt f (a :: l)) =
bindt (g ⋆6 f) (a :: l)
      rewrite bindt_list_cons.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
map (bindt g)
  (pure (app (A:=B)) <⋆> f a <⋆> bindt f l) =
bindt (g ⋆6 f) (a :: l)
      rewrite map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure (bindt g) <⋆>
(pure (app (A:=B)) <⋆> f a <⋆> bindt f l) =
bindt (g ⋆6 f) (a :: l)
      do 3 rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure (bindt g) <⋆> pure (app (A:=B)) <⋆> f a <⋆>
bindt f l = bindt (g ⋆6 f) (a :: l)
      do 4 rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l = bindt (g ⋆6 f) (a :: l)
      rewrite bindt_list_cons.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure (app (A:=C)) <⋆> (g ⋆6 f) a <⋆> bindt (g ⋆6 f) l
      rewrite <- IHl.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure (app (A:=C)) <⋆> (g ⋆6 f) a <⋆>
(map (bindt g) ∘ bindt f) l
      unfold compose at 7.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure (app (A:=C)) <⋆> (g ⋆6 f) a <⋆>
map (bindt g) (bindt f l)
      do 2 rewrite (ap_compose1 G2 G1).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure (ap G2) <⋆>
(pure (ap G2) <⋆> pure (app (A:=C)) <⋆> (g ⋆6 f) a) <⋆>
map (bindt g) (bindt f l)
      unfold_ops @Pure_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure (ap G2) <⋆>
(pure (ap G2) <⋆> pure (pure (app (A:=C))) <⋆>
 (g ⋆6 f) a) <⋆> map (bindt g) (bindt f l)
      rewrite map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure (ap G2) <⋆>
(pure (ap G2) <⋆> pure (pure (app (A:=C))) <⋆>
 (g ⋆6 f) a) <⋆> (pure (bindt g) <⋆> bindt f l)
      rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure compose <⋆>
(pure (ap G2) <⋆>
 (pure (ap G2) <⋆> pure (pure (app (A:=C))) <⋆>
  (g ⋆6 f) a)) <⋆> pure (bindt g) <⋆> bindt f l
      rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure compose <⋆> pure compose <⋆> pure (ap G2) <⋆>
(pure (ap G2) <⋆> pure (pure (app (A:=C))) <⋆>
 (g ⋆6 f) a) <⋆> pure (bindt g) <⋆> bindt f l
      rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure compose <⋆>
(pure compose <⋆> pure compose <⋆> pure (ap G2)) <⋆>
(pure (ap G2) <⋆> pure (pure (app (A:=C)))) <⋆>
(g ⋆6 f) a <⋆> pure (bindt g) <⋆> bindt f l
      rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure compose <⋆>
(pure compose <⋆>
 (pure compose <⋆> pure compose <⋆> pure (ap G2))) <⋆>
pure (ap G2) <⋆> pure (pure (app (A:=C))) <⋆>
(g ⋆6 f) a <⋆> pure (bindt g) <⋆> bindt f l
      do 6 rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure
  ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C)))) <⋆> (g ⋆6 f) a <⋆>
pure (bindt g) <⋆> bindt f l
      unfold kc6.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure
  ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C)))) <⋆> (map (bindt g) ∘ f) a <⋆>
pure (bindt g) <⋆> bindt f l
      unfold compose at 8.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure
  ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C)))) <⋆> map (bindt g) (f a) <⋆>
pure (bindt g) <⋆> bindt f l
      rewrite map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure
  ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C)))) <⋆> (pure (bindt g) <⋆> f a) <⋆>
pure (bindt g) <⋆> bindt f l
      rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure compose <⋆>
pure
  ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C)))) <⋆> pure (bindt g) <⋆> f a <⋆>
pure (bindt g) <⋆> bindt f l
      do 2 rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure
  ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C))) ∘ bindt g) <⋆> f a <⋆>
pure (bindt g) <⋆> bindt f l
      rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure (evalAt (bindt g)) <⋆>
(pure
   ((compose (compose ∘ ap G2) ∘ ap G2)
      (pure (app (A:=C))) ∘ bindt g) <⋆> f a) <⋆>
bindt f l
      rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure compose <⋆> pure (evalAt (bindt g)) <⋆>
pure
  ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C))) ∘ bindt g) <⋆> f a <⋆>
bindt f l
      do 2 rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a <⋆> bindt f l =
pure
  (evalAt (bindt g)
   ∘ ((compose (compose ∘ ap G2) ∘ ap G2)
        (pure (app (A:=C))) ∘ bindt g)) <⋆> f a <⋆>
bindt f l
      fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) <⋆>
f a =
pure
  (evalAt (bindt g)
   ∘ ((compose (compose ∘ ap G2) ∘ ap G2)
        (pure (app (A:=C))) ∘ bindt g)) <⋆> f a
      fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
pure ((compose ∘ compose) (bindt g) (app (A:=B))) =
pure
  (evalAt (bindt g)
   ∘ ((compose (compose ∘ ap G2) ∘ ap G2)
        (pure (app (A:=C))) ∘ bindt g))
      fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
(compose ∘ compose) (bindt g) (app (A:=B)) =
evalAt (bindt g)
∘ ((compose (compose ∘ ap G2) ∘ ap G2)
     (pure (app (A:=C))) ∘ bindt g) ext l1 l2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
l1, l2: list B
(compose ∘ compose) (bindt g) (app (A:=B)) l1 l2 =
(evalAt (bindt g)
 ∘ ((compose (compose ∘ ap G2) ∘ ap G2)
      (pure (app (A:=C))) ∘ bindt g)) l1 l2
      unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
l1, l2: list B
bindt g (l1 ++ l2) =
evalAt (bindt g)
  (fun f : list B -> G2 (list C) =>
   ap G2 (pure (app (A:=C)) <⋆> bindt g l1) ○ f) l2 rewrite (bindt_list_app G2).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A, B, C: Type
g: B -> G2 (list C)
f: A -> G1 (list B)
a: A
l: list A
IHl: (map (bindt g) ∘ bindt f) l = bindt (g ⋆6 f) l
l1, l2: list B
pure (app (A:=C)) <⋆> bindt g l1 <⋆> bindt g l2 =
evalAt (bindt g)
  (fun f : list B -> G2 (list C) =>
   ap G2 (pure (app (A:=C)) <⋆> bindt g l1) ○ f) l2
      reflexivity.
  Qed.

End bindt_laws.

Lemma list_morph:
  forall `(morph: ApplicativeMorphism G1 G2 ϕ),
  forall (A B: Type) (f: A -> G1 (list B)),
    ϕ (list B) ∘ bindt f = bindt (ϕ (list B) ∘ f).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 (list B)),
ϕ (list B) ∘ bindt f = bindt (ϕ (list B) ∘ f)
Proof.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 (list B)),
ϕ (list B) ∘ bindt f = bindt (ϕ (list B) ∘ f)
  intros.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
ϕ (list B) ∘ bindt f = bindt (ϕ (list B) ∘ f) unfold compose at 1 2.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
ϕ (list B) ○ bindt f = bindt (ϕ (list B) ○ f) ext l.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
l: list A
ϕ (list B) (bindt f l) = bindt (ϕ (list B) ○ f) l
  induction l.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
ϕ (list B) (bindt f []) = bindt (ϕ (list B) ○ f) []
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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
a: A
l: list A
IHl: ϕ (list B) (bindt f l) =
bindt (ϕ (list B) ○ f) l
ϕ (list B) (bindt f (a :: l)) =
bindt (ϕ (list B) ○ f) (a :: l)
  -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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
ϕ (list B) (bindt f []) = bindt (ϕ (list B) ○ f) [] cbn.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
ϕ (list B) (pure []) = pure [] rewrite appmor_pure.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
pure [] = pure [] reflexivity.
  -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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
a: A
l: list A
IHl: ϕ (list B) (bindt f l) =
bindt (ϕ (list B) ○ f) l
ϕ (list B) (bindt f (a :: l)) =
bindt (ϕ (list B) ○ f) (a :: l) cbn.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
a: A
l: list A
IHl: ϕ (list B) (bindt f l) =
bindt (ϕ (list B) ○ f) l
ϕ (list B) (pure (app (A:=B)) <⋆> f a <⋆> bindt f l) =
pure (app (A:=B)) <⋆> ϕ (list B) (f a) <⋆>
bindt (ϕ (list B) ○ f) l
    rewrite (ap_morphism_1 (G := G1)).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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
a: A
l: list A
IHl: ϕ (list B) (bindt f l) =
bindt (ϕ (list B) ○ f) l
ϕ (list B -> list B) (pure (app (A:=B)) <⋆> f a) <⋆>
ϕ (list B) (bindt f l) =
pure (app (A:=B)) <⋆> ϕ (list B) (f a) <⋆>
bindt (ϕ (list B) ○ f) l
    rewrite (ap_morphism_1 (G := G1)).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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
a: A
l: list A
IHl: ϕ (list B) (bindt f l) =
bindt (ϕ (list B) ○ f) l
ϕ (list B -> list B -> list B) (pure (app (A:=B))) <⋆>
ϕ (list B) (f a) <⋆> ϕ (list B) (bindt f l) =
pure (app (A:=B)) <⋆> ϕ (list B) (f a) <⋆>
bindt (ϕ (list B) ○ f) l
    rewrite appmor_pure.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
a: A
l: list A
IHl: ϕ (list B) (bindt f l) =
bindt (ϕ (list B) ○ f) l
pure (app (A:=B)) <⋆> ϕ (list B) (f a) <⋆>
ϕ (list B) (bindt f l) =
pure (app (A:=B)) <⋆> ϕ (list B) (f a) <⋆>
bindt (ϕ (list B) ○ f) l
    rewrite IHl.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
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (list B)
a: A
l: list A
IHl: ϕ (list B) (bindt f l) =
bindt (ϕ (list B) ○ f) l
pure (app (A:=B)) <⋆> ϕ (list B) (f a) <⋆>
bindt (ϕ (list B) ○ f) l =
pure (app (A:=B)) <⋆> ϕ (list B) (f a) <⋆>
bindt (ϕ (list B) ○ f) l
    reflexivity.
Qed.

(** ** Typeclass Instance *)
(**********************************************************************)
#[export] Instance TraversableRightPreModule_list:
  TraversableRightPreModule list list :=
  {| ktm_bindt1 := list_bindt1;
     ktm_bindt2 := @list_bindt2;
     ktm_morph := @list_morph;
  |}.

#[export] Instance TraversableMonad_list:
  TraversableMonad list :=
  {| ktm_bindt0 := list_bindt0;
  |}.

#[export] Instance TraversableRightModule_list:
  TraversableRightModule list list :=
  DerivedInstances.TraversableRightModule_TraversableMonad.

(** * Traversable Functor Instance (Kleisli) *)
(**********************************************************************)
Fixpoint traverse_list (G: Type -> Type)
  `{Map G} `{Pure G} `{Mult G}
  (A B: Type) (f: A -> G B) (l: list A)
: G (list B) :=
  match l with
  | nil => pure (@nil B)
  | x :: xs =>
      pure (@List.cons B) <⋆> f x <⋆> (traverse_list G A B f xs)
  end.

#[export] Instance Traverse_list: Traverse list := @traverse_list.

#[export] Instance Compat_Traverse_Bindt_list:
  Compat_Traverse_Bindt list list.Compat_Traverse_Bindt list list
Proof.Compat_Traverse_Bindt list list
  hnf.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
Traverse_list G Map_G Pure_G Mult_G =
DerivedOperations.Traverse_Bindt list list G Map_G
  Pure_G Mult_G intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
Traverse_list G Map_G Pure_G Mult_G =
DerivedOperations.Traverse_Bindt list list G Map_G
  Pure_G Mult_G
  ext A B f l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
l: list A
Traverse_list G Map_G Pure_G Mult_G A B f l =
DerivedOperations.Traverse_Bindt list list G Map_G
  Pure_G Mult_G A B f l
  unfold DerivedOperations.Traverse_Bindt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
l: list A
Traverse_list G Map_G Pure_G Mult_G A B f l =
bindt (map ret ∘ f) l
  induction l as [| a rest IHrest].G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
Traverse_list G Map_G Pure_G Mult_G A B f [] =
bindt (map ret ∘ f) []
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: Traverse_list G Map_G Pure_G Mult_G A B f
  rest = bindt (map ret ∘ f) rest
Traverse_list G Map_G Pure_G Mult_G A B f (a :: rest) =
bindt (map ret ∘ f) (a :: rest)
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
Traverse_list G Map_G Pure_G Mult_G A B f [] =
bindt (map ret ∘ f) [] reflexivity.
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: Traverse_list G Map_G Pure_G Mult_G A B f
  rest = bindt (map ret ∘ f) rest
Traverse_list G Map_G Pure_G Mult_G A B f (a :: rest) =
bindt (map ret ∘ f) (a :: rest) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: Traverse_list G Map_G Pure_G Mult_G A B f
  rest = bindt (map ret ∘ f) rest
pure cons <⋆> f a <⋆>
Traverse_list G Map_G Pure_G Mult_G A B f rest =
pure (app (A:=B)) <⋆> (map ret ∘ f) a <⋆>
bindt (map ret ∘ f) rest
    rewrite IHrest.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: Traverse_list G Map_G Pure_G Mult_G A B f
  rest = bindt (map ret ∘ f) rest
pure cons <⋆> f a <⋆> bindt (map ret ∘ f) rest =
pure (app (A:=B)) <⋆> (map ret ∘ f) a <⋆>
bindt (map ret ∘ f) rest
    unfold compose at 2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: Traverse_list G Map_G Pure_G Mult_G A B f
  rest = bindt (map ret ∘ f) rest
pure cons <⋆> f a <⋆> bindt (map ret ∘ f) rest =
pure (app (A:=B)) <⋆> map ret (f a) <⋆>
bindt (map ret ∘ f) rest
    rewrite pure_ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: Traverse_list G Map_G Pure_G Mult_G A B f
  rest = bindt (map ret ∘ f) rest
pure cons <⋆> f a <⋆> bindt (map ret ∘ f) rest =
map (app (A:=B) ∘ ret) (f a) <⋆>
bindt (map ret ∘ f) rest
    rewrite map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
Applicative0: Applicative G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: Traverse_list G Map_G Pure_G Mult_G A B f
  rest = bindt (map ret ∘ f) rest
pure cons <⋆> f a <⋆> bindt (map ret ∘ f) rest =
pure (app (A:=B) ∘ ret) <⋆> f a <⋆>
bindt (map ret ∘ f) rest
    reflexivity.
Qed.

#[export] Instance Compat_Map_Traverse_list:
  Compat_Map_Traverse list :=
  Compat_Map_Traverse_Bindt.

(** ** Rewriting Laws for <<traverse>> *)
(**********************************************************************)
Section traverse_rewriting_lemmas.

  Context
    (G: Type -> Type)
    `{Applicative G}
    (A B: Type).

  Lemma traverse_list_nil: forall (f: A -> G B),
      traverse f (@nil A) = pure (@nil B).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall f : A -> G B, traverse f [] = pure []
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall f : A -> G B, traverse f [] = pure []
    reflexivity.
  Qed.

  Lemma traverse_list_one: forall (f: A -> G B) (a: A),
      traverse f (ret (T := list) a) = map ret (f a).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (a : A),
traverse f (ret a) = map ret (f a)
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (a : A),
traverse f (ret a) = map ret (f a)
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
traverse f (ret a) = map ret (f a)
    cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
pure cons <⋆> f a <⋆> pure [] = map ret (f a)
    rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
pure (evalAt []) <⋆> (pure cons <⋆> f a) =
map ret (f a)
    rewrite <- ap4;
      rewrite ap2;
      rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
pure (evalAt [] ∘ cons) <⋆> f a = map ret (f a)
    rewrite <- map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
map (evalAt [] ∘ cons) (f a) = map ret (f a)
    reflexivity.
  Qed.

  Lemma traverse_list_cons: forall (f: A -> G B) (a: A) (l: list A),
      traverse f (a :: l) =
        pure (@cons B) <⋆> f a <⋆> traverse f l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (a : A) (l : list A),
traverse f (a :: l) =
pure cons <⋆> f a <⋆> traverse f l
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (a : A) (l : list A),
traverse f (a :: l) =
pure cons <⋆> f a <⋆> traverse f l
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
traverse f (a :: l) =
pure cons <⋆> f a <⋆> traverse f l
    reflexivity.
  Qed.

  Lemma traverse_list_app: forall (f: A -> G B) (l1 l2: list A),
      traverse f (l1 ++ l2) =
        pure (@app B) <⋆> traverse f l1 <⋆> traverse f l2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (l1 l2 : list A),
traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆> traverse f l2
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (l1 l2 : list A),
traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆> traverse f l2
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l1, l2: list A
traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆> traverse f l2
    induction l1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l2: list A
traverse f ([] ++ l2) =
pure (app (A:=B)) <⋆> traverse f [] <⋆> traverse f l2
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
traverse f ((a :: l1) ++ l2) =
pure (app (A:=B)) <⋆> traverse f (a :: l1) <⋆>
traverse f l2
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l2: list A
traverse f ([] ++ l2) =
pure (app (A:=B)) <⋆> traverse f [] <⋆> traverse f l2 cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l2: list A
traverse f l2 =
pure (app (A:=B)) <⋆> pure [] <⋆> traverse f l2 rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l2: list A
traverse f l2 = pure (app []) <⋆> traverse f l2
      rewrite ap1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l2: list A
traverse f l2 = traverse f l2
      reflexivity.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
traverse f ((a :: l1) ++ l2) =
pure (app (A:=B)) <⋆> traverse f (a :: l1) <⋆>
traverse f l2 cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
pure cons <⋆> f a <⋆> traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆>
(pure cons <⋆> f a <⋆> traverse f l1) <⋆>
traverse f l2
      rewrite IHl1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
pure cons <⋆> f a <⋆>
(pure (app (A:=B)) <⋆> traverse f l1 <⋆> traverse f l2) =
pure (app (A:=B)) <⋆>
(pure cons <⋆> f a <⋆> traverse f l1) <⋆>
traverse f l2
      repeat rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure cons <⋆> f a <⋆>
pure (app (A:=B)) <⋆> traverse f l1 <⋆> traverse f l2 =
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure (app (A:=B)) <⋆> pure cons <⋆> f a <⋆>
traverse f l1 <⋆> traverse f l2
      repeat rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
pure
  ((compose ∘ compose) compose compose compose compose
     cons) <⋆> f a <⋆> pure (app (A:=B)) <⋆>
traverse f l1 <⋆> traverse f l2 =
pure ((compose ∘ compose) (app (A:=B)) cons) <⋆> f a <⋆>
traverse f l1 <⋆> traverse f l2
      rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
pure (evalAt (app (A:=B))) <⋆>
(pure
   ((compose ∘ compose) compose compose compose
      compose cons) <⋆> f a) <⋆> traverse f l1 <⋆>
traverse f l2 =
pure ((compose ∘ compose) (app (A:=B)) cons) <⋆> f a <⋆>
traverse f l1 <⋆> traverse f l2
      repeat rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
pure compose <⋆> pure (evalAt (app (A:=B))) <⋆>
pure
  ((compose ∘ compose) compose compose compose compose
     cons) <⋆> f a <⋆> traverse f l1 <⋆> traverse f l2 =
pure ((compose ∘ compose) (app (A:=B)) cons) <⋆> f a <⋆>
traverse f l1 <⋆> traverse f l2
      repeat rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l1, l2: list A
IHl1: traverse f (l1 ++ l2) =
pure (app (A:=B)) <⋆> traverse f l1 <⋆>
traverse f l2
pure
  (evalAt (app (A:=B))
   ∘ (compose ∘ compose) compose compose compose
       compose cons) <⋆> f a <⋆> traverse f l1 <⋆>
traverse f l2 =
pure ((compose ∘ compose) (app (A:=B)) cons) <⋆> f a <⋆>
traverse f l1 <⋆> traverse f l2
      reflexivity.
  Qed.

  Definition snoc {A: Type} (l: list A) (a: A) := l ++ [a].

  Lemma traverse_list_snoc: forall (f: A -> G B) (l: list A) (a: A),
      traverse f (l ++ a :: nil) =
        pure (@snoc B) <⋆> traverse f l <⋆> f a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (l : list A) (a : A),
traverse f (l ++ [a]) =
pure snoc <⋆> traverse f l <⋆> f a
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
forall (f : A -> G B) (l : list A) (a : A),
traverse f (l ++ [a]) =
pure snoc <⋆> traverse f l <⋆> f a
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
traverse f (l ++ [a]) =
pure snoc <⋆> traverse f l <⋆> f a
    rewrite traverse_list_app.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure (app (A:=B)) <⋆> traverse f l <⋆> traverse f [a] =
pure snoc <⋆> traverse f l <⋆> f a
    cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure (app (A:=B)) <⋆> traverse f l <⋆>
(pure cons <⋆> f a <⋆> pure []) =
pure snoc <⋆> traverse f l <⋆> f a
    repeat rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure (app (A:=B)) <⋆> traverse f l <⋆>
pure cons <⋆> f a <⋆> pure [] =
pure snoc <⋆> traverse f l <⋆> f a
    repeat rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure
  ((compose ∘ compose) compose compose compose compose
     (app (A:=B))) <⋆> traverse f l <⋆> pure cons <⋆>
f a <⋆> pure [] = pure snoc <⋆> traverse f l <⋆> f a
    rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure (evalAt []) <⋆>
(pure
   ((compose ∘ compose) compose compose compose
      compose (app (A:=B))) <⋆> traverse f l <⋆>
 pure cons <⋆> f a) =
pure snoc <⋆> traverse f l <⋆> f a
    repeat rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure (evalAt []) <⋆>
pure
  ((compose ∘ compose) compose compose compose compose
     (app (A:=B))) <⋆> traverse f l <⋆> pure cons <⋆>
f a = pure snoc <⋆> traverse f l <⋆> f a
    repeat rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure
  ((compose ∘ compose) compose compose compose compose
     compose (evalAt [])
     ((compose ∘ compose) compose compose compose
        compose (app (A:=B)))) <⋆> traverse f l <⋆>
pure cons <⋆> f a = pure snoc <⋆> traverse f l <⋆> f a
    rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure (evalAt cons) <⋆>
(pure
   ((compose ∘ compose) compose compose compose
      compose compose (evalAt [])
      ((compose ∘ compose) compose compose compose
         compose (app (A:=B)))) <⋆> traverse f l) <⋆>
f a = pure snoc <⋆> traverse f l <⋆> f a
    repeat rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure compose <⋆> pure (evalAt cons) <⋆>
pure
  ((compose ∘ compose) compose compose compose compose
     compose (evalAt [])
     ((compose ∘ compose) compose compose compose
        compose (app (A:=B)))) <⋆> traverse f l <⋆>
f a = pure snoc <⋆> traverse f l <⋆> f a
    repeat rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure
  (evalAt cons
   ∘ (compose ∘ compose) compose compose compose
       compose compose (evalAt [])
       ((compose ∘ compose) compose compose compose
          compose (app (A:=B)))) <⋆> traverse f l <⋆>
f a = pure snoc <⋆> traverse f l <⋆> f a
    unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
a: A
pure
  (fun a : list B =>
   evalAt cons
     (fun (a0 : B -> list B -> list B) (a1 : B) =>
      evalAt [] (app a ○ a0 a1))) <⋆> traverse f l <⋆>
f a = pure snoc <⋆> traverse f l <⋆> f a
    reflexivity.
  Qed.

End traverse_rewriting_lemmas.

#[export] Hint Rewrite traverse_list_nil traverse_list_cons
  traverse_list_one traverse_list_snoc traverse_list_app:
  tea_list.

#[export] Instance TraversableFunctor_list:
  TraversableFunctor list :=
  DerivedInstances.TraversableFunctor_TraversableMonad.

(** * Monad Instance (Kleisli) *)
(**********************************************************************)
Fixpoint bind_list (A B: Type) (f: A -> list B) (l: list A): list B :=
  match l with
  | nil => @nil B
  | x :: xs =>
      f x ● bind_list A B f xs
  end.

#[export] Instance Bind_list: Bind list list := @bind_list.

#[export] Instance Compat_Bind_Bindt_list:
  Compat_Bind_Bindt list list.Compat_Bind_Bindt list list
Proof.Compat_Bind_Bindt list list
  hnf.Bind_list = DerivedOperations.Bind_Bindt list list ext A B f l.A, B: Type
f: A -> list B
l: list A
Bind_list A B f l =
DerivedOperations.Bind_Bindt list list A B f l
  induction l as [|a rest IHrest].A, B: Type
f: A -> list B
Bind_list A B f [] =
DerivedOperations.Bind_Bindt list list A B f []
A, B: Type
f: A -> list B
a: A
rest: list A
IHrest: Bind_list A B f rest =
DerivedOperations.Bind_Bindt list list A B f
  rest
Bind_list A B f (a :: rest) =
DerivedOperations.Bind_Bindt list list A B f
  (a :: rest)
  -A, B: Type
f: A -> list B
Bind_list A B f [] =
DerivedOperations.Bind_Bindt list list A B f [] reflexivity.
  -A, B: Type
f: A -> list B
a: A
rest: list A
IHrest: Bind_list A B f rest =
DerivedOperations.Bind_Bindt list list A B f
  rest
Bind_list A B f (a :: rest) =
DerivedOperations.Bind_Bindt list list A B f
  (a :: rest) cbn.A, B: Type
f: A -> list B
a: A
rest: list A
IHrest: Bind_list A B f rest =
DerivedOperations.Bind_Bindt list list A B f
  rest
f a ● Bind_list A B f rest =
pure (app (A:=B)) (f a)
  (DerivedOperations.Bind_Bindt list list A B f rest) now rewrite IHrest.
Qed.

#[export] Instance Compat_Map_Bind_list:
  Compat_Map_Bind list list
  := ltac:(typeclasses eauto).

(** ** Rewriting Laws for <<bind>> *)
(**********************************************************************)
Section bind_rewriting_lemmas.

  Context
    (A B: Type).

  Lemma bind_list_nil: forall (f: A -> list B),
      bind f (@nil A) = @nil B.A, B: Type
forall f : A -> list B, bind f [] = []
  Proof.A, B: Type
forall f : A -> list B, bind f [] = []
    reflexivity.
  Qed.

  Lemma bind_list_one: forall (f: A -> list B) (a: A),
      bind f (ret a) = f a.A, B: Type
forall (f : A -> list B) (a : A), bind f (ret a) = f a
  Proof.A, B: Type
forall (f : A -> list B) (a : A), bind f (ret a) = f a
    intros.A, B: Type
f: A -> list B
a: A
bind f (ret a) = f a
    cbn.A, B: Type
f: A -> list B
a: A
f a ● [] = f a change (@nil B) with (Ƶ: list B).A, B: Type
f: A -> list B
a: A
f a ● (Ƶ : list B) = f a
    now simpl_monoid.
  Qed.

  Lemma bind_list_cons: forall (f: A -> list B) (a: A) (l: list A),
      bind f (a :: l) = f a ++ bind f l.A, B: Type
forall (f : A -> list B) (a : A) (l : list A),
bind f (a :: l) = f a ++ bind f l
  Proof.A, B: Type
forall (f : A -> list B) (a : A) (l : list A),
bind f (a :: l) = f a ++ bind f l
    reflexivity.
  Qed.

  Lemma bind_list_app: forall (f: A -> list B) (l1 l2: list A),
      bind f (l1 ++ l2) = bind f l1 ++ bind f l2.A, B: Type
forall (f : A -> list B) (l1 l2 : list A),
bind f (l1 ++ l2) = bind f l1 ++ bind f l2
  Proof.A, B: Type
forall (f : A -> list B) (l1 l2 : list A),
bind f (l1 ++ l2) = bind f l1 ++ bind f l2
    intros.A, B: Type
f: A -> list B
l1, l2: list A
bind f (l1 ++ l2) = bind f l1 ++ bind f l2
    induction l1.A, B: Type
f: A -> list B
l2: list A
bind f ([] ++ l2) = bind f [] ++ bind f l2
A, B: Type
f: A -> list B
a: A
l1, l2: list A
IHl1: bind f (l1 ++ l2) = bind f l1 ++ bind f l2
bind f ((a :: l1) ++ l2) =
bind f (a :: l1) ++ bind f l2
    -A, B: Type
f: A -> list B
l2: list A
bind f ([] ++ l2) = bind f [] ++ bind f l2 cbn.A, B: Type
f: A -> list B
l2: list A
bind f l2 = bind f l2 reflexivity.
    -A, B: Type
f: A -> list B
a: A
l1, l2: list A
IHl1: bind f (l1 ++ l2) = bind f l1 ++ bind f l2
bind f ((a :: l1) ++ l2) =
bind f (a :: l1) ++ bind f l2 cbn.A, B: Type
f: A -> list B
a: A
l1, l2: list A
IHl1: bind f (l1 ++ l2) = bind f l1 ++ bind f l2
f a ● bind f (l1 ++ l2) =
(f a ● bind f l1) ++ bind f l2
      rewrite IHl1.A, B: Type
f: A -> list B
a: A
l1, l2: list A
IHl1: bind f (l1 ++ l2) = bind f l1 ++ bind f l2
f a ● (bind f l1 ++ bind f l2) =
(f a ● bind f l1) ++ bind f l2
      change (?f ● ?g) with (f ++ g).A, B: Type
f: A -> list B
a: A
l1, l2: list A
IHl1: bind f (l1 ++ l2) = bind f l1 ++ bind f l2
f a ++ bind f l1 ++ bind f l2 =
(f a ++ bind f l1) ++ bind f l2
      rewrite List.app_assoc.A, B: Type
f: A -> list B
a: A
l1, l2: list A
IHl1: bind f (l1 ++ l2) = bind f l1 ++ bind f l2
(f a ++ bind f l1) ++ bind f l2 =
(f a ++ bind f l1) ++ bind f l2
      reflexivity.
  Qed.

End bind_rewriting_lemmas.

#[export] Hint Rewrite bind_list_nil bind_list_cons
  bind_list_one bind_list_app: tea_list.

(** ** [bind] is a Monoid Homomorphism *)
(**********************************************************************)
#[export] Instance Monmor_bind (A B: Type) (f: A -> list B):
  Monoid_Morphism (list A) (list B) (bind f).A, B: Type
f: A -> list B
Monoid_Morphism (list A) (list B) (bind f)
Proof.A, B: Type
f: A -> list B
Monoid_Morphism (list A) (list B) (bind f)
  constructor; try typeclasses eauto.A, B: Type
f: A -> list B
bind f Ƶ = Ƶ
A, B: Type
f: A -> list B
forall a1 a2 : list A,
bind f (a1 ● a2) = bind f a1 ● bind f a2
  -A, B: Type
f: A -> list B
bind f Ƶ = Ƶ reflexivity.
  -A, B: Type
f: A -> list B
forall a1 a2 : list A,
bind f (a1 ● a2) = bind f a1 ● bind f a2 intros.A, B: Type
f: A -> list B
a1, a2: list A
bind f (a1 ● a2) = bind f a1 ● bind f a2 induction a1.A, B: Type
f: A -> list B
a2: list A
bind f ([] ● a2) = bind f [] ● bind f a2
A, B: Type
f: A -> list B
a: A
a1, a2: list A
IHa1: bind f (a1 ● a2) = bind f a1 ● bind f a2
bind f ((a :: a1) ● a2) = bind f (a :: a1) ● bind f a2
    +A, B: Type
f: A -> list B
a2: list A
bind f ([] ● a2) = bind f [] ● bind f a2 reflexivity.
    +A, B: Type
f: A -> list B
a: A
a1, a2: list A
IHa1: bind f (a1 ● a2) = bind f a1 ● bind f a2
bind f ((a :: a1) ● a2) = bind f (a :: a1) ● bind f a2 cbn.A, B: Type
f: A -> list B
a: A
a1, a2: list A
IHa1: bind f (a1 ● a2) = bind f a1 ● bind f a2
f a ● bind f (a1 ● a2) = (f a ● bind f a1) ● bind f a2 rewrite IHa1.A, B: Type
f: A -> list B
a: A
a1, a2: list A
IHa1: bind f (a1 ● a2) = bind f a1 ● bind f a2
f a ● (bind f a1 ● bind f a2) =
(f a ● bind f a1) ● bind f a2
      now rewrite monoid_assoc.
Qed.


(** * Traversable Instance (Categorical) *)
(**********************************************************************)
From Tealeaves Require Import
  Classes.Categorical.TraversableFunctor.

#[global] Instance Dist_list: ApplicativeDist list :=
  fun G map mlt pur A =>
    (fix dist (l: list (G A)) :=
       match l with
       | nil => pure nil
       | cons x xs =>
           pure (F := G) (@cons A) <⋆> x <⋆> (dist xs)
       end).

(** ** Rewriting Laws *)
(**********************************************************************)
Section list_dist_rewrite.

  Context
    `{Applicative G}.

  Variable (A: Type).

  Lemma dist_list_nil:
    dist list G (@nil (G A)) = pure nil.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
dist list G [] = pure []
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
dist list G [] = pure []
    reflexivity.
  Qed.

  Lemma dist_list_cons_1:
    forall (x: G A) (xs: list (G A)),
      dist list G (x :: xs) =
      pure cons <⋆> x <⋆> (dist list G xs).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (x : G A) (xs : list (G A)),
dist list G (x :: xs) =
pure cons <⋆> x <⋆> dist list G xs
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (x : G A) (xs : list (G A)),
dist list G (x :: xs) =
pure cons <⋆> x <⋆> dist list G xs
    reflexivity.
  Qed.

  Lemma dist_list_cons_2:
    forall (x: G A) (xs: list (G A)),
      dist list G (x :: xs) =
      map (@cons A) x <⋆> dist list G xs.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (x : G A) (xs : list (G A)),
dist list G (x :: xs) = map cons x <⋆> dist list G xs
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (x : G A) (xs : list (G A)),
dist list G (x :: xs) = map cons x <⋆> dist list G xs
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
x: G A
xs: list (G A)
dist list G (x :: xs) = map cons x <⋆> dist list G xs rewrite dist_list_cons_1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
x: G A
xs: list (G A)
pure cons <⋆> x <⋆> dist list G xs =
map cons x <⋆> dist list G xs
    now rewrite map_to_ap.
  Qed.

  Lemma dist_list_one (a: G A):
    dist list G [ a ] = map (ret (T := list)) a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
dist list G [a] = map ret a
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
dist list G [a] = map ret a
    cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
pure cons <⋆> a <⋆> pure [] = map ret a rewrite map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
pure cons <⋆> a <⋆> pure [] = pure ret <⋆> a rewrite ap3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
pure (evalAt []) <⋆> (pure cons <⋆> a) =
pure ret <⋆> a
    rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
pure compose <⋆> pure (evalAt []) <⋆> pure cons <⋆> a =
pure ret <⋆> a now do 2 rewrite ap2.
  Qed.

  Lemma dist_list_app:
    forall (l1 l2: list (G A)),
      dist list G (l1 ++ l2) =
        pure (@app _) <⋆> dist list G l1 <⋆> dist list G l2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall l1 l2 : list (G A),
dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall l1 l2 : list (G A),
dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
l1, l2: list (G A)
dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2 induction l1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
l2: list (G A)
dist list G ([] ++ l2) =
pure (app (A:=A)) <⋆> dist list G [] <⋆>
dist list G l2
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
IHl1: dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2
dist list G ((a :: l1) ++ l2) =
pure (app (A:=A)) <⋆> dist list G (a :: l1) <⋆>
dist list G l2
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
l2: list (G A)
dist list G ([] ++ l2) =
pure (app (A:=A)) <⋆> dist list G [] <⋆>
dist list G l2 cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
l2: list (G A)
dist list G l2 =
pure (app (A:=A)) <⋆> pure [] <⋆> dist list G l2 rewrite ap2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
l2: list (G A)
dist list G l2 = pure (app []) <⋆> dist list G l2 change (app []) with (@id (list A)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
l2: list (G A)
dist list G l2 = pure id <⋆> dist list G l2
      now rewrite ap1.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
IHl1: dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2
dist list G ((a :: l1) ++ l2) =
pure (app (A:=A)) <⋆> dist list G (a :: l1) <⋆>
dist list G l2 cbn [app].G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
IHl1: dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2
dist list G (a :: l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G (a :: l1) <⋆>
dist list G l2 rewrite dist_list_cons_2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
IHl1: dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2
map cons a <⋆> dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G (a :: l1) <⋆>
dist list G l2
      rewrite dist_list_cons_2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
IHl1: dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> dist list G l1 <⋆>
dist list G l2
map cons a <⋆> dist list G (l1 ++ l2) =
pure (app (A:=A)) <⋆> (map cons a <⋆> dist list G l1) <⋆>
dist list G l2
      rewrite IHl1; clear IHl1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map cons a <⋆>
(pure (app (A:=A)) <⋆> dist list G l1 <⋆>
 dist list G l2) =
pure (app (A:=A)) <⋆> (map cons a <⋆> dist list G l1) <⋆>
dist list G l2
      rewrite <- map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map cons a <⋆>
(map (app (A:=A)) (dist list G l1) <⋆> dist list G l2) =
pure (app (A:=A)) <⋆> (map cons a <⋆> dist list G l1) <⋆>
dist list G l2
      rewrite <- map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map cons a <⋆>
(map (app (A:=A)) (dist list G l1) <⋆> dist list G l2) =
map (app (A:=A)) (map cons a <⋆> dist list G l1) <⋆>
dist list G l2
      rewrite <- ap4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
pure compose <⋆> map cons a <⋆>
map (app (A:=A)) (dist list G l1) <⋆> dist list G l2 =
map (app (A:=A)) (map cons a <⋆> dist list G l1) <⋆>
dist list G l2 rewrite <- map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map compose (map cons a) <⋆>
map (app (A:=A)) (dist list G l1) <⋆> dist list G l2 =
map (app (A:=A)) (map cons a <⋆> dist list G l1) <⋆>
dist list G l2
      fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map compose (map cons a) <⋆>
map (app (A:=A)) (dist list G l1) =
map (app (A:=A)) (map cons a <⋆> dist list G l1) rewrite <- ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map (precompose (app (A:=A)))
  (map compose (map cons a)) <⋆> dist list G l1 =
map (app (A:=A)) (map cons a <⋆> dist list G l1)
      rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map (precompose (app (A:=A)))
  (map compose (map cons a)) <⋆> dist list G l1 =
map (compose (app (A:=A))) (map cons a) <⋆>
dist list G l1 fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map (precompose (app (A:=A)))
  (map compose (map cons a)) =
map (compose (app (A:=A))) (map cons a)
      compose near a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map (precompose (app (A:=A)))
  ((map compose ∘ map cons) a) =
(map (compose (app (A:=A))) ∘ map cons) a
      rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map (precompose (app (A:=A))) (map (compose ∘ cons) a) =
(map (compose (app (A:=A))) ∘ map cons) a
      rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
map (precompose (app (A:=A))) (map (compose ∘ cons) a) =
map (compose (app (A:=A)) ∘ cons) a
      compose near a on left.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
l1, l2: list (G A)
(map (precompose (app (A:=A))) ∘ map (compose ∘ cons))
  a = map (compose (app (A:=A)) ∘ cons) a
      now rewrite (fun_map_map).
  Qed.

End list_dist_rewrite.

#[export] Hint Rewrite @dist_list_nil @dist_list_cons_1
     @dist_list_one @dist_list_app: tea_list.

(** ** Traversable Functor Laws *)
(**********************************************************************)
Section dist_list_properties.

  #[local] Arguments map F%function_scope {Map}
    {A B}%type_scope f%function_scope _.
  #[local] Arguments dist _%function_scope {ApplicativeDist}
    _%function_scope {H H0 H1} A%type_scope _.


  Lemma dist_list_1:
    forall `{Applicative G}
      `(f: A -> B) (a: G A) (l: list (G A)),
      map G (map list f)
        (map G (@cons A) a <⋆> dist list G A l) =
        (map G (@cons B ○ f) a) <⋆>
          map G (map list f) (dist list G A l).forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B) (a : G A)
  (l : list (G A)),
map G (map list f) (map G cons a <⋆> dist list G A l) =
map G (cons ○ f) a <⋆>
map G (map list f) (dist list G A l)
  Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B) (a : G A)
  (l : list (G A)),
map G (map list f) (map G cons a <⋆> dist list G A l) =
map G (cons ○ f) a <⋆>
map G (map list f) (dist list G A l)
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (map list f) (map G cons a <⋆> dist list G A l) =
map G (cons ○ f) a <⋆>
map G (map list f) (dist list G A l)
    rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (compose (map list f)) (map G cons a) <⋆>
dist list G A l =
map G (cons ○ f) a <⋆>
map G (map list f) (dist list G A l)
    rewrite <- ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (compose (map list f)) (map G cons a) <⋆>
dist list G A l =
map G (precompose (map list f)) (map G (cons ○ f) a) <⋆>
dist list G A l
    compose near a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
(map G (compose (map list f)) ∘ map G cons) a <⋆>
dist list G A l =
(map G (precompose (map list f)) ∘ map G (cons ○ f)) a <⋆>
dist list G A l
    rewrite 2(fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (compose (map list f) ∘ cons) a <⋆>
dist list G A l =
map G (precompose (map list f) ∘ (cons ○ f)) a <⋆>
dist list G A l
    reflexivity.
  Qed.

  Lemma dist_list_2:
    forall `{Applicative G} `(f: A -> B) (a: G A) (l: list (G A)),
      map G (map list f)
        (pure (@cons A) <⋆> a <⋆> dist list G A l) =
        pure cons <⋆>
          map G f a <⋆>
          map G (map list f) (dist list G A l).forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B) (a : G A)
  (l : list (G A)),
map G (map list f)
  (pure cons <⋆> a <⋆> dist list G A l) =
pure cons <⋆> map G f a <⋆>
map G (map list f) (dist list G A l)
  Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B) (a : G A)
  (l : list (G A)),
map G (map list f)
  (pure cons <⋆> a <⋆> dist list G A l) =
pure cons <⋆> map G f a <⋆>
map G (map list f) (dist list G A l)
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (map list f)
  (pure cons <⋆> a <⋆> dist list G A l) =
pure cons <⋆> map G f a <⋆>
map G (map list f) (dist list G A l)
    rewrite <- map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (map list f) (map G cons a <⋆> dist list G A l) =
pure cons <⋆> map G f a <⋆>
map G (map list f) (dist list G A l)
    rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (compose (map list f)) (map G cons a) <⋆>
dist list G A l =
pure cons <⋆> map G f a <⋆>
map G (map list f) (dist list G A l)
    compose near a on left.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
(map G (compose (map list f)) ∘ map G cons) a <⋆>
dist list G A l =
pure cons <⋆> map G f a <⋆>
map G (map list f) (dist list G A l)
    rewrite fun_map_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (compose (map list f) ∘ cons) a <⋆>
dist list G A l =
pure cons <⋆> map G f a <⋆>
map G (map list f) (dist list G A l)
    rewrite pure_ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (compose (map list f) ∘ cons) a <⋆>
dist list G A l =
map G (cons ∘ f) a <⋆>
map G (map list f) (dist list G A l)
    unfold ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (fun '(f, a) => f a)
  (map G (compose (map list f) ∘ cons) a
   ⊗ dist list G A l) =
map G (fun '(f, a) => f a)
  (map G (cons ∘ f) a
   ⊗ map G (map list f) (dist list G A l))
    rewrite (app_mult_natural).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G (fun '(f, a) => f a)
  (map G (compose (map list f) ∘ cons) a
   ⊗ dist list G A l) =
map G (fun '(f, a) => f a)
  (map G (map_tensor (cons ∘ f) (map list f))
     (a ⊗ dist list G A l))
    rewrite (app_mult_natural_1 G).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G
  ((fun '(f, a) => f a)
   ∘ map_fst (compose (map list f) ∘ cons))
  (a ⊗ dist list G A l) =
map G (fun '(f, a) => f a)
  (map G (map_tensor (cons ∘ f) (map list f))
     (a ⊗ dist list G A l))
    compose near ((a ⊗ dist list G A l)) on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G
  ((fun '(f, a) => f a)
   ∘ map_fst (compose (map list f) ∘ cons))
  (a ⊗ dist list G A l) =
(map G (fun '(f, a) => f a)
 ∘ map G (map_tensor (cons ∘ f) (map list f)))
  (a ⊗ dist list G A l)
    rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
map G
  ((fun '(f, a) => f a)
   ∘ map_fst (compose (map list f) ∘ cons))
  (a ⊗ dist list G A l) =
map G
  ((fun '(f, a) => f a)
   ∘ map_tensor (cons ∘ f) (map list f))
  (a ⊗ dist list G A l) fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
(fun '(f, a) => f a)
∘ map_fst (compose (map list f) ∘ cons) =
(fun '(f, a) => f a)
∘ map_tensor (cons ∘ f) (map list f) ext [? ?].G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
a0: A
l0: list A
((fun '(f, a) => f a)
 ∘ map_fst (compose (map list f) ∘ cons)) (a0, l0) =
((fun '(f, a) => f a)
 ∘ map_tensor (cons ∘ f) (map list f)) (a0, l0)
    reflexivity.
  Qed.

  Lemma dist_natural_list:
    forall `{Applicative G} `(f: A -> B),
      map (G ∘ list) f ∘ dist list G A =
      dist list G B ∘ map (list ∘ G) f.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B),
map (G ∘ list) f ∘ dist list G A =
dist list G B ∘ map (list ∘ G) f
  Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> B),
map (G ∘ list) f ∘ dist list G A =
dist list G B ∘ map (list ∘ G) f
    intros; cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (G ∘ list) f ∘ dist list G A =
dist list G B ∘ map (list ∘ G) f unfold_ops @Map_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map G (map list f) ∘ dist list G A =
dist list G B ∘ map list (map G f) unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map G (map list f) ○ dist list G A =
dist list G B ○ map list (map G f)
    ext l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
l: list (G A)
map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l) induction l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map G (map list f) (dist list G A []) =
dist list G B (map list (map G f) [])
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
IHl: map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l)
map G (map list f) (dist list G A (a :: l)) =
dist list G B (map list (map G f) (a :: l))
    +G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map G (map list f) (dist list G A []) =
dist list G B (map list (map G f) []) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map G (map list f) (pure []) = pure [] now rewrite (app_pure_natural).
    +G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
IHl: map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l)
map G (map list f) (dist list G A (a :: l)) =
dist list G B (map list (map G f) (a :: l)) rewrite dist_list_cons_2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
IHl: map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l)
map G (map list f) (map G cons a <⋆> dist list G A l) =
dist list G B (map list (map G f) (a :: l))
      rewrite map_list_cons, dist_list_cons_2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
IHl: map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l)
map G (map list f) (map G cons a <⋆> dist list G A l) =
map G cons (map G f a) <⋆>
dist list G B (map list (map G f) l)
      rewrite <- IHl.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
IHl: map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l)
map G (map list f) (map G cons a <⋆> dist list G A l) =
map G cons (map G f a) <⋆>
map G (map list f) (dist list G A l) rewrite dist_list_1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
IHl: map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l)
map G (cons ○ f) a <⋆>
map G (map list f) (dist list G A l) =
map G cons (map G f a) <⋆>
map G (map list f) (dist list G A l)
      compose near a on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
l: list (G A)
IHl: map G (map list f) (dist list G A l) =
dist list G B (map list (map G f) l)
map G (cons ○ f) a <⋆>
map G (map list f) (dist list G A l) =
(map G cons ∘ map G f) a <⋆>
map G (map list f) (dist list G A l)
      now rewrite (fun_map_map).
  Qed.

  #[export] Instance dist_natural_list_:
    forall `{Applicative G},
      Natural (@dist list _ G _ _ _).forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G -> Natural (dist list G)
  Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G -> Natural (dist list G)
    constructor; try typeclasses eauto.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> B),
map (G ○ list) f ∘ dist list G A =
dist list G B ∘ map (list ○ G) f
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (G ○ list) f ∘ dist list G A =
dist list G B ∘ map (list ○ G) f eapply (dist_natural_list f).
  Qed.

  Lemma dist_morph_list:
    forall `{ApplicativeMorphism G1 G2 ϕ} A,
      dist list G2 A ∘ map list (ϕ A) =
        ϕ (list A) ∘ dist list G1 A.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 : Type,
dist list G2 A ∘ map list (ϕ A) =
ϕ (list A) ∘ dist list G1 A
  Proof.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 : Type,
dist list G2 A ∘ map list (ϕ A) =
ϕ (list A) ∘ dist list G1 A
    intros.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
dist list G2 A ∘ map list (ϕ A) =
ϕ (list A) ∘ dist list G1 A ext l.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
l: list (G1 A)
(dist list G2 A ∘ map list (ϕ A)) l =
(ϕ (list A) ∘ dist list G1 A) l unfold compose.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
l: list (G1 A)
dist list G2 A (map list (ϕ A) l) =
ϕ (list A) (dist list G1 A l) induction l.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
dist list G2 A (map list (ϕ A) []) =
ϕ (list A) (dist list G1 A [])
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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
dist list G2 A (map list (ϕ A) (a :: l)) =
ϕ (list A) (dist list G1 A (a :: l))
    -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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
dist list G2 A (map list (ϕ A) []) =
ϕ (list A) (dist list G1 A []) rewrite map_list_nil.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
dist list G2 A [] = ϕ (list A) (dist list G1 A [])
      rewrite dist_list_nil.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
pure [] = ϕ (list A) (dist list G1 A [])
      rewrite dist_list_nil.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
pure [] = ϕ (list A) (pure [])
      rewrite appmor_pure.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
pure [] = pure []
      reflexivity.
    -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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
dist list G2 A (map list (ϕ A) (a :: l)) =
ϕ (list A) (dist list G1 A (a :: l)) infer_applicative_instances.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
app1: Applicative G1
app2: Applicative G2
dist list G2 A (map list (ϕ A) (a :: l)) =
ϕ (list A) (dist list G1 A (a :: l))
      rewrite map_list_cons.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
app1: Applicative G1
app2: Applicative G2
dist list G2 A (ϕ A a :: map list (ϕ A) l) =
ϕ (list A) (dist list G1 A (a :: l))
      rewrite dist_list_cons_2.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
app1: Applicative G1
app2: Applicative G2
map G2 cons (ϕ A a) <⋆>
dist list G2 A (map list (ϕ A) l) =
ϕ (list A) (dist list G1 A (a :: l))
      rewrite dist_list_cons_2.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
app1: Applicative G1
app2: Applicative G2
map G2 cons (ϕ A a) <⋆>
dist list G2 A (map list (ϕ A) l) =
ϕ (list A) (map G1 cons a <⋆> dist list G1 A l)
      rewrite IHl.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
app1: Applicative G1
app2: Applicative G2
map G2 cons (ϕ A a) <⋆> ϕ (list A) (dist list G1 A l) =
ϕ (list A) (map G1 cons a <⋆> dist list G1 A l)
      rewrite ap_morphism_1.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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
app1: Applicative G1
app2: Applicative G2
map G2 cons (ϕ A a) <⋆> ϕ (list A) (dist list G1 A l) =
ϕ (list A -> list A) (map G1 cons a) <⋆>
ϕ (list A) (dist list G1 A l)
      rewrite (appmor_natural).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
H5: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
l: list (G1 A)
IHl: dist list G2 A (map list (ϕ A) l) = ϕ (list A) (dist list G1 A l)
app1: Applicative G1
app2: Applicative G2
map G2 cons (ϕ A a) <⋆> ϕ (list A) (dist list G1 A l) =
map G2 cons (ϕ A a) <⋆> ϕ (list A) (dist list G1 A l)
      reflexivity.
  Qed.

  Lemma dist_unit_list: forall (A: Type),
      dist list (fun A => A) A = @id (list A).forall A : Type,
dist list (fun A0 : Type => A0) A = id
  Proof.forall A : Type,
dist list (fun A0 : Type => A0) A = id
    intros.A: Type
dist list (fun A : Type => A) A = id ext l.A: Type
l: list A
dist list (fun A : Type => A) A l = id l induction l.A: Type
dist list (fun A : Type => A) A [] = id []
A: Type
a: A
l: list A
IHl: dist list (fun A : Type => A) A l = id l
dist list (fun A : Type => A) A (a :: l) = id (a :: l)
    -A: Type
dist list (fun A : Type => A) A [] = id [] reflexivity.
    -A: Type
a: A
l: list A
IHl: dist list (fun A : Type => A) A l = id l
dist list (fun A : Type => A) A (a :: l) = id (a :: l) cbn.A: Type
a: A
l: list A
IHl: dist list (fun A : Type => A) A l = id l
pure cons a (dist list (fun A : Type => A) A l) =
id (a :: l) now rewrite IHl.
  Qed.

  #[local] Set Keyed Unification.
  Lemma dist_linear_list
   : forall `{Applicative G1} `{Applicative G2} (A: Type),
      dist list (G1 ∘ G2) A =
      map G1 (dist list G2 A) ∘ dist list G1 (G2 A).forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall A : Type,
dist list (G1 ∘ G2) A =
map G1 (dist list G2 A) ∘ dist list G1 (G2 A)
  Proof.forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall A : Type,
dist list (G1 ∘ G2) A =
map G1 (dist list G2 A) ∘ dist list G1 (G2 A)
    intros.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
dist list (G1 ∘ G2) A =
map G1 (dist list G2 A) ∘ dist list G1 (G2 A) unfold compose.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
dist list (G1 ○ G2) A =
map G1 (dist list G2 A) ○ dist list G1 (G2 A) ext l.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
l: list (G1 (G2 A))
dist list (G1 ○ G2) A l =
map G1 (dist list G2 A) (dist list G1 (G2 A) l) induction l.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
dist list (G1 ○ G2) A [] =
map G1 (dist list G2 A) (dist list G1 (G2 A) [])
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
IHl: dist list (G1 ○ G2) A l =
map G1 (dist list G2 A) (dist list G1 (G2 A) l)
dist list (G1 ○ G2) A (a :: l) =
map G1 (dist list G2 A) (dist list G1 (G2 A) (a :: l))
    -G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
dist list (G1 ○ G2) A [] =
map G1 (dist list G2 A) (dist list G1 (G2 A) []) cbn.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
pure [] = map G1 (dist list G2 A) (pure []) unfold_ops @Pure_compose.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
pure (pure []) = map G1 (dist list G2 A) (pure [])
      rewrite map_to_ap.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
pure (pure []) = pure (dist list G2 A) <⋆> pure [] now rewrite ap2.
    -G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
IHl: dist list (G1 ○ G2) A l =
map G1 (dist list G2 A) (dist list G1 (G2 A) l)
dist list (G1 ○ G2) A (a :: l) =
map G1 (dist list G2 A) (dist list G1 (G2 A) (a :: l)) rewrite (dist_list_cons_2 (G := G1 ○ G2)).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
IHl: dist list (G1 ○ G2) A l =
map G1 (dist list G2 A) (dist list G1 (G2 A) l)
map (G1 ○ G2) cons a <⋆> dist list (G1 ○ G2) A l =
map G1 (dist list G2 A) (dist list G1 (G2 A) (a :: l))
      rewrite (dist_list_cons_2 (G := G1)).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
IHl: dist list (G1 ○ G2) A l =
map G1 (dist list G2 A) (dist list G1 (G2 A) l)
map (G1 ○ G2) cons a <⋆> dist list (G1 ○ G2) A l =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      rewrite IHl; clear IHl.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map (G1 ○ G2) cons a <⋆>
map G1 (dist list G2 A) (dist list G1 (G2 A) l) =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      unfold_ops @Mult_compose @Pure_compose @Map_compose.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (map G2 cons) a <⋆>
map G1 (dist list G2 A) (dist list G1 (G2 A) l) =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      rewrite (ap_compose2 G2 G1).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (ap G2) (map G1 (map G2 cons) a) <⋆>
map G1 (dist list G2 A) (dist list G1 (G2 A) l) =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      compose near a on left.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
(map G1 (ap G2) ∘ map G1 (map G2 cons)) a <⋆>
map G1 (dist list G2 A) (dist list G1 (G2 A) l) =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      rewrite (fun_map_map).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (ap G2 ∘ map G2 cons) a <⋆>
map G1 (dist list G2 A) (dist list G1 (G2 A) l) =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      unfold ap at 1.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (fun '(f, a) => f a)
  (map G1 (ap G2 ∘ map G2 cons) a
   ⊗ map G1 (dist list G2 A) (dist list G1 (G2 A) l)) =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      rewrite (app_mult_natural).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (fun '(f, a) => f a)
  (map G1
     (map_tensor (ap G2 ∘ map G2 cons)
        (dist list G2 A)) (a ⊗ dist list G1 (G2 A) l)) =
map G1 (dist list G2 A)
  (map G1 cons a <⋆> dist list G1 (G2 A) l)
      unfold ap at 2.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (fun '(f, a) => f a)
  (map G1
     (map_tensor (ap G2 ∘ map G2 cons)
        (dist list G2 A)) (a ⊗ dist list G1 (G2 A) l)) =
map G1 (dist list G2 A)
  (map G1 (fun '(f, a) => f a)
     (map G1 cons a ⊗ dist list G1 (G2 A) l)) rewrite (app_mult_natural_1 G1).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (fun '(f, a) => f a)
  (map G1
     (map_tensor (ap G2 ∘ map G2 cons)
        (dist list G2 A)) (a ⊗ dist list G1 (G2 A) l)) =
map G1 (dist list G2 A)
  (map G1 ((fun '(f, a) => f a) ∘ map_fst cons)
     (a ⊗ dist list G1 (G2 A) l))
      fequal.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1 (fun '(f, a) => f a)
  (map G1
     (map_tensor (ap G2 ∘ map G2 cons)
        (dist list G2 A)) (a ⊗ dist list G1 (G2 A) l)) =
map G1 (dist list G2 A)
  (map G1 ((fun '(f, a) => f a) ∘ map_fst cons)
     (a ⊗ dist list G1 (G2 A) l)) compose near (a ⊗ dist list G1 (G2 A) l).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
(map G1 (fun '(f, a) => f a)
 ∘ map G1
     (map_tensor (ap G2 ∘ map G2 cons)
        (dist list G2 A))) (a ⊗ dist list G1 (G2 A) l) =
(map G1 (dist list G2 A)
 ∘ map G1 ((fun '(f, a) => f a) ∘ map_fst cons))
  (a ⊗ dist list G1 (G2 A) l)
      rewrite (fun_map_map).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1
  ((fun '(f, a) => f a)
   ∘ map_tensor (ap G2 ∘ map G2 cons) (dist list G2 A))
  (a ⊗ dist list G1 (G2 A) l) =
(map G1 (dist list G2 A)
 ∘ map G1 ((fun '(f, a) => f a) ∘ map_fst cons))
  (a ⊗ dist list G1 (G2 A) l)
      rewrite (fun_map_map).G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
map G1
  ((fun '(f, a) => f a)
   ∘ map_tensor (ap G2 ∘ map G2 cons) (dist list G2 A))
  (a ⊗ dist list G1 (G2 A) l) =
map G1
  (dist list G2 A
   ∘ ((fun '(f, a) => f a) ∘ map_fst cons))
  (a ⊗ dist list G1 (G2 A) l)
      fequal.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
(fun '(f, a) => f a)
∘ map_tensor (ap G2 ∘ map G2 cons) (dist list G2 A) =
dist list G2 A ∘ ((fun '(f, a) => f a) ∘ map_fst cons)
      ext [? ?].G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
g: G2 A
l0: list (G2 A)
((fun '(f, a) => f a)
 ∘ map_tensor (ap G2 ∘ map G2 cons) (dist list G2 A))
  (g, l0) =
(dist list G2 A
 ∘ ((fun '(f, a) => f a) ∘ map_fst cons)) (g, l0)
      cbn.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
g: G2 A
l0: list (G2 A)
(ap G2 ∘ map G2 cons) g (dist list G2 A l0) =
pure cons <⋆> g <⋆> dist list G2 A (id l0) unfold compose.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A: Type
a: G1 (G2 A)
l: list (G1 (G2 A))
g: G2 A
l0: list (G2 A)
map G2 cons g <⋆> dist list G2 A l0 =
pure cons <⋆> g <⋆> dist list G2 A (id l0)
      now rewrite map_to_ap.
  Qed.
  #[local] Unset Keyed Unification.

End dist_list_properties.

(** ** Typeclass Instance *)
(**********************************************************************)
#[export] Instance Traversable_Categorical_list: Categorical.TraversableFunctor.TraversableFunctor list :=
  {| dist_natural := @dist_natural_list_;
     dist_morph := @dist_morph_list;
     dist_unit := @dist_unit_list;
     dist_linear := @dist_linear_list;
  |}.

(** * Folding over lists *)
(**********************************************************************)
Fixpoint crush_list
  `{op: Monoid_op M}
  `{unit: Monoid_unit M} (l: list M): M :=
  match l with
  | nil => Ƶ
  | cons x l' => x ● crush_list l'
  end.

(** ** Rewriting Laws for [crush_list] *)
(**********************************************************************)
Section crush_list_rewriting_lemmas.

  Context
    `{Monoid M}.

  Lemma crush_list_nil: crush_list (@nil M) = Ƶ.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
crush_list [] = Ƶ
  Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
crush_list [] = Ƶ
    reflexivity.
  Qed.

  Lemma crush_list_cons: forall (m: M) (l: list M),
      crush_list (m :: l) = m ● crush_list l.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (m : M) (l : list M),
crush_list (m :: l) = m ● crush_list l
  Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (m : M) (l : list M),
crush_list (m :: l) = m ● crush_list l
    reflexivity.
  Qed.

  Lemma crush_list_one: forall (m: M), crush_list [ m ] = m.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall m : M, crush_list [m] = m
  Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall m : M, crush_list [m] = m
    intro.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
m: M
crush_list [m] = m cbn.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
m: M
m ● Ƶ = m now simpl_monoid.
  Qed.

  Lemma crush_list_app: forall (l1 l2: list M),
      crush_list (l1 ++ l2) = crush_list l1 ● crush_list l2.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall l1 l2 : list M,
crush_list (l1 ++ l2) = crush_list l1 ● crush_list l2
  Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall l1 l2 : list M,
crush_list (l1 ++ l2) = crush_list l1 ● crush_list l2
    intros l1 ?.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l1, l2: list M
crush_list (l1 ++ l2) = crush_list l1 ● crush_list l2 induction l1 as [| ? ? IHl].M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l2: list M
crush_list ([] ++ l2) = crush_list [] ● crush_list l2
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: M
l1, l2: list M
IHl: crush_list (l1 ++ l2) =
crush_list l1 ● crush_list l2
crush_list ((a :: l1) ++ l2) =
crush_list (a :: l1) ● crush_list l2
    -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l2: list M
crush_list ([] ++ l2) = crush_list [] ● crush_list l2 cbn.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l2: list M
crush_list l2 = Ƶ ● crush_list l2 now simpl_monoid.
    -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: M
l1, l2: list M
IHl: crush_list (l1 ++ l2) =
crush_list l1 ● crush_list l2
crush_list ((a :: l1) ++ l2) =
crush_list (a :: l1) ● crush_list l2 cbn.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: M
l1, l2: list M
IHl: crush_list (l1 ++ l2) =
crush_list l1 ● crush_list l2
a ● crush_list (l1 ++ l2) =
(a ● crush_list l1) ● crush_list l2 rewrite IHl.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: M
l1, l2: list M
IHl: crush_list (l1 ++ l2) =
crush_list l1 ● crush_list l2
a ● (crush_list l1 ● crush_list l2) =
(a ● crush_list l1) ● crush_list l2 now simpl_monoid.
  Qed.

End crush_list_rewriting_lemmas.

(** ** <<crush_list>> is a Monoid Morphism *)
(** <<crush_list: list M -> M>> is homomorphism of monoids. *)
(**********************************************************************)
#[export] Instance Monmor_crush_list (M: Type) `{Monoid M}:
  Monoid_Morphism (list M) M crush_list :=
  {| monmor_unit := crush_list_nil;
     monmor_op := crush_list_app;
  |}.

(** ** Miscellaneous properties *)
(**********************************************************************)

(** *** <<crush_list>> commutes with monoid homomorphisms *)
Lemma crush_list_mon_hom:
  forall `(ϕ: M1 -> M2) `{Monoid_Morphism M1 M2 ϕ},
    ϕ ∘ crush_list = crush_list ∘ map ϕ.forall (M1 M2 : Type) (ϕ : M1 -> M2)
  (src_op : Monoid_op M1) (src_unit : Monoid_unit M1)
  (tgt_op : Monoid_op M2) (tgt_unit : Monoid_unit M2),
Monoid_Morphism M1 M2 ϕ ->
ϕ ∘ crush_list = crush_list ∘ map ϕ
Proof.forall (M1 M2 : Type) (ϕ : M1 -> M2)
  (src_op : Monoid_op M1) (src_unit : Monoid_unit M1)
  (tgt_op : Monoid_op M2) (tgt_unit : Monoid_unit M2),
Monoid_Morphism M1 M2 ϕ ->
ϕ ∘ crush_list = crush_list ∘ map ϕ
  intros ? ? ϕ ? ? ? ? ?.M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
ϕ ∘ crush_list = crush_list ∘ map ϕ unfold compose.M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
ϕ ○ crush_list = crush_list ○ map ϕ ext l.M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
l: list M1
ϕ (crush_list l) = crush_list (map ϕ l)
  induction l as [| ? ? IHl].M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
ϕ (crush_list []) = crush_list (map ϕ [])
M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
a: M1
l: list M1
IHl: ϕ (crush_list l) = crush_list (map ϕ l)
ϕ (crush_list (a :: l)) = crush_list (map ϕ (a :: l))
  -M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
ϕ (crush_list []) = crush_list (map ϕ []) cbn.M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
ϕ Ƶ = Ƶ apply monmor_unit.
  -M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
a: M1
l: list M1
IHl: ϕ (crush_list l) = crush_list (map ϕ l)
ϕ (crush_list (a :: l)) = crush_list (map ϕ (a :: l)) cbn.M1, M2: Type
ϕ: M1 -> M2
src_op: Monoid_op M1
src_unit: Monoid_unit M1
tgt_op: Monoid_op M2
tgt_unit: Monoid_unit M2
H: Monoid_Morphism M1 M2 ϕ
a: M1
l: list M1
IHl: ϕ (crush_list l) = crush_list (map ϕ l)
ϕ (a ● crush_list l) = ϕ a ● crush_list (map ϕ l) now rewrite (monmor_op (ϕ := ϕ)), IHl.
Qed.

(** *** <<crush_list>> for the list monoid is <<join>> *)
Lemma crush_list_equal_join: forall {A},
    crush_list (M := list A) = join (T := list) (A:=A).forall A : Type, crush_list = join
Proof.forall A : Type, crush_list = join
  intros.A: Type
crush_list = join ext l.A: Type
l: list (list A)
crush_list l = join l induction l as [| ? ? IHl].A: Type
crush_list [] = join []
A: Type
a: list A
l: list (list A)
IHl: crush_list l = join l
crush_list (a :: l) = join (a :: l)
  -A: Type
crush_list [] = join [] reflexivity.
  -A: Type
a: list A
l: list (list A)
IHl: crush_list l = join l
crush_list (a :: l) = join (a :: l) cbn.A: Type
a: list A
l: list (list A)
IHl: crush_list l = join l
a ● crush_list l = a ++ join l now rewrite IHl.
Qed.

(** ** The <<mapReduce_list>> Operation *)
(**********************************************************************)
Definition mapReduce_list {M: Type} `{op: Monoid_op M}
  `{unit: Monoid_unit M} {A: Type} (f: A -> M):
  list A -> M := crush_list ∘ map f.

(** ** <<mapReduce_list>> is a Monoid Homomorphism *)
(**********************************************************************)
(** <<mapReduce_list>> is a monoid homomorphism *)
#[export] Instance Monoid_Morphism_mapReduce_list
  `{Monoid M} {A: Type}
  `(f: A -> M): Monoid_Morphism (list A) M (mapReduce_list f).M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid_Morphism (list A) M (mapReduce_list f)
Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid_Morphism (list A) M (mapReduce_list f)
  unfold mapReduce_list.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid_Morphism (list A) M (crush_list ∘ map f)
  eapply Monoid_Morphism_compose.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid (list A)
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid M
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid_Morphism (list A) (list M) (map f)
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid_Morphism (list M) M crush_list
  -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid (list A) typeclasses eauto.
  -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid M typeclasses eauto.
  -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid_Morphism (list A) (list M) (map f) typeclasses eauto.
  -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
Monoid_Morphism (list M) M crush_list typeclasses eauto.
Qed.

(** ** <<mapReduce_list>> Commutes with Monoid Homomorphism *)
(**********************************************************************)
Lemma mapReduce_list_morphism `{Monoid_Morphism M1 M2 ϕ}
: forall `(f: A -> M1),
    ϕ ∘ mapReduce_list f = mapReduce_list (ϕ ∘ f).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
H: Monoid_Morphism M1 M2 ϕ
forall (A : Type) (f : A -> M1),
ϕ ∘ mapReduce_list f = mapReduce_list (ϕ ∘ f)
Proof.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
H: Monoid_Morphism M1 M2 ϕ
forall (A : Type) (f : A -> M1),
ϕ ∘ mapReduce_list f = mapReduce_list (ϕ ∘ f)
  intros.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
H: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
ϕ ∘ mapReduce_list f = mapReduce_list (ϕ ∘ f) unfold mapReduce_list.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
H: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
ϕ ∘ (crush_list ∘ map f) = crush_list ∘ map (ϕ ∘ f)
  reassociate <- on left.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
H: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
ϕ ∘ crush_list ∘ map f = crush_list ∘ map (ϕ ∘ f)
  rewrite (crush_list_mon_hom ϕ).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
H: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
crush_list ∘ map ϕ ∘ map f = crush_list ∘ map (ϕ ∘ f)
  reassociate -> on left.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
H: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
crush_list ∘ (map ϕ ∘ map f) =
crush_list ∘ map (ϕ ∘ f)
  rewrite fun_map_map.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
H: Monoid_Morphism M1 M2 ϕ
A: Type
f: A -> M1
crush_list ∘ map (ϕ ∘ f) = crush_list ∘ map (ϕ ∘ f)
  reflexivity.
Qed.

(** ** Rewriting Laws for <<mapReduce_list>> *)
(**********************************************************************)
Section mapReduce_list_rw.

  Context
    {A M: Type}
    `{Monoid M}
    (f: A -> M).

  Lemma mapReduce_list_nil: mapReduce_list f (@nil A) = Ƶ.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce_list f [] = Ƶ
  Proof.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce_list f [] = Ƶ
    reflexivity.
  Qed.

  Lemma mapReduce_list_cons: forall (x: A) (xs: list A),
      mapReduce_list f (x :: xs) = f x ● mapReduce_list f xs.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall (x : A) (xs : list A),
mapReduce_list f (x :: xs) = f x ● mapReduce_list f xs
  Proof.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall (x : A) (xs : list A),
mapReduce_list f (x :: xs) = f x ● mapReduce_list f xs
    reflexivity.
  Qed.

  Lemma mapReduce_list_one (a: A): mapReduce_list f [ a ] = f a.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
a: A
mapReduce_list f [a] = f a
  Proof.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
a: A
mapReduce_list f [a] = f a
    cbv.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
a: A
op (f a) unit0 = f a apply monoid_id_r.
  Qed.

  Lemma mapReduce_list_ret: mapReduce_list f ∘ ret = f.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce_list f ∘ ret = f
  Proof.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
mapReduce_list f ∘ ret = f
    ext a; cbn.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
a: A
f a ● Ƶ = f a apply monoid_id_r.
  Qed.

  Lemma mapReduce_list_app: forall (l1 l2: list A),
      mapReduce_list f (l1 ++ l2) = mapReduce_list f l1 ● mapReduce_list f l2.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall l1 l2 : list A,
mapReduce_list f (l1 ++ l2) =
mapReduce_list f l1 ● mapReduce_list f l2
  Proof.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
forall l1 l2 : list A,
mapReduce_list f (l1 ++ l2) =
mapReduce_list f l1 ● mapReduce_list f l2
    intros.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
mapReduce_list f (l1 ++ l2) =
mapReduce_list f l1 ● mapReduce_list f l2
    unfold mapReduce_list.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
(crush_list ∘ map f) (l1 ++ l2) =
(crush_list ∘ map f) l1 ● (crush_list ∘ map f) l2
    unfold compose.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
crush_list (map f (l1 ++ l2)) =
crush_list (map f l1) ● crush_list (map f l2) autorewrite with tea_list.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
crush_list (map f l1 ++ map f l2) =
crush_list (map f l1) ● crush_list (map f l2)
    rewrite crush_list_app.A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
f: A -> M
l1, l2: list A
crush_list (map f l1) ● crush_list (map f l2) =
crush_list (map f l1) ● crush_list (map f l2)
    reflexivity.
  Qed.

End mapReduce_list_rw.

#[export] Hint Rewrite @mapReduce_list_nil @mapReduce_list_cons
  @mapReduce_list_one @mapReduce_list_app: tea_list.

Lemma mapReduce_list_ret_id: forall A, mapReduce_list (@ret list _ A) = id.forall A : Type, mapReduce_list ret = id
Proof.forall A : Type, mapReduce_list ret = id
  intros.A: Type
mapReduce_list ret = id
  ext l.A: Type
l: list A
mapReduce_list ret l = id l
  induction l as [|x rest IHrest];
    autorewrite with tea_list.A: Type
Ƶ = id []
A: Type
x: A
rest: list A
IHrest: mapReduce_list ret rest = id rest
ret x ● mapReduce_list ret rest = id (x :: rest)
  reflexivity.A: Type
x: A
rest: list A
IHrest: mapReduce_list ret rest = id rest
ret x ● mapReduce_list ret rest = id (x :: rest)
  now rewrite IHrest.
Qed.

(** ** Monoids form list (monad-)algebras *)
(** In fact, list algebras are precisely monoids. *)
(**********************************************************************)
Section foldable_list.

  Context
    `{Monoid M}.

  Lemma crush_list_ret: forall (x: M),
      crush_list (ret x: list M) = x.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall x : M, crush_list (ret x : list M) = x
  Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall x : M, crush_list (ret x : list M) = x
    apply monoid_id_r.
  Qed.

  Lemma crush_list_join: forall (l: list (list M)),
      crush_list (join l) = crush_list (map crush_list l).M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall l : list (list M),
crush_list (join l) = crush_list (map crush_list l)
  Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall l : list (list M),
crush_list (join l) = crush_list (map crush_list l)
    intro l.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l: list (list M)
crush_list (join l) = crush_list (map crush_list l) rewrite <- crush_list_equal_join.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l: list (list M)
crush_list (crush_list l) =
crush_list (map crush_list l)
    compose near l on left.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l: list (list M)
(crush_list ∘ crush_list) l =
crush_list (map crush_list l)
    now rewrite (crush_list_mon_hom crush_list).
  Qed.

  Lemma crush_list_constant_unit: forall (l: list M),
      crush_list (map (fun _ => Ƶ) l) = Ƶ.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall l : list M,
crush_list (map (fun _ : M => Ƶ) l) = Ƶ
  Proof.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall l : list M,
crush_list (map (fun _ : M => Ƶ) l) = Ƶ
    intro l.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
l: list M
crush_list (map (fun _ : M => Ƶ) l) = Ƶ induction l.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
crush_list (map (fun _ : M => Ƶ) []) = Ƶ
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: M
l: list M
IHl: crush_list (map (fun _ : M => Ƶ) l) = Ƶ
crush_list (map (fun _ : M => Ƶ) (a :: l)) = Ƶ
    -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
crush_list (map (fun _ : M => Ƶ) []) = Ƶ reflexivity.
    -M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: M
l: list M
IHl: crush_list (map (fun _ : M => Ƶ) l) = Ƶ
crush_list (map (fun _ : M => Ƶ) (a :: l)) = Ƶ cbn.M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: M
l: list M
IHl: crush_list (map (fun _ : M => Ƶ) l) = Ƶ
Ƶ ● crush_list (map (fun _ : M => Ƶ) l) = Ƶ now simpl_monoid.
  Qed.

End foldable_list.

(** * Container Instance *)
(**********************************************************************)
#[export] Instance ToSubset_list: ToSubset list :=
  fun (A: Type) (l: list A) => (fun a: A => @List.In A a l).

(** ** Rewriting Laws for <<tosubset>> *)
(**********************************************************************)
Lemma tosubset_list_nil: forall (A: Type),
    tosubset (@nil A) = ∅.forall A : Type, tosubset [] = ∅
Proof.forall A : Type, tosubset [] = ∅
  intros.A: Type
tosubset [] = ∅ extensionality a.A: Type
a: A
tosubset [] a = ∅ a reflexivity.
Qed.

Lemma tosubset_list_one: forall (A: Type) (a: A),
    tosubset [a] = {{ a }}.forall (A : Type) (a : A), tosubset [a] = {{a}}
Proof.forall (A : Type) (a : A), tosubset [a] = {{a}}
  intros.A: Type
a: A
tosubset [a] = {{a}} solve_basic_subset.
Qed.

Lemma tosubset_list_ret: forall (A: Type) (a: A),
    tosubset (ret a) = {{ a }}.forall (A : Type) (a : A), tosubset (ret a) = {{a}}
Proof.forall (A : Type) (a : A), tosubset (ret a) = {{a}}
  intros.A: Type
a: A
tosubset (ret a) = {{a}} solve_basic_subset.
Qed.

Lemma tosubset_list_cons:
  forall (A: Type) (a: A) (l: list A),
    tosubset (a :: l) = {{ a }} ∪ tosubset l.forall (A : Type) (a : A) (l : list A),
tosubset (a :: l) = {{a}} ∪ tosubset l
Proof.forall (A : Type) (a : A) (l : list A),
tosubset (a :: l) = {{a}} ∪ tosubset l
  intros.A: Type
a: A
l: list A
tosubset (a :: l) = {{a}} ∪ tosubset l extensionality a'.A: Type
a: A
l: list A
a': A
tosubset (a :: l) a' = ({{a}} ∪ tosubset l) a' reflexivity.
Qed.

Lemma tosubset_list_app: forall (A: Type) (l1 l2: list A),
    tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2.forall (A : Type) (l1 l2 : list A),
tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2
Proof.forall (A : Type) (l1 l2 : list A),
tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2
  intros.A: Type
l1, l2: list A
tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2 induction l1.A: Type
l2: list A
tosubset ([] ++ l2) = tosubset [] ∪ tosubset l2
A: Type
a: A
l1, l2: list A
IHl1: tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2
tosubset ((a :: l1) ++ l2) =
tosubset (a :: l1) ∪ tosubset l2
  -A: Type
l2: list A
tosubset ([] ++ l2) = tosubset [] ∪ tosubset l2 cbn.A: Type
l2: list A
tosubset l2 = tosubset [] ∪ tosubset l2 rewrite tosubset_list_nil.A: Type
l2: list A
tosubset l2 = ∅ ∪ tosubset l2
    solve_basic_subset.
  -A: Type
a: A
l1, l2: list A
IHl1: tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2
tosubset ((a :: l1) ++ l2) =
tosubset (a :: l1) ∪ tosubset l2 cbn.A: Type
a: A
l1, l2: list A
IHl1: tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2
tosubset (a :: l1 ++ l2) =
tosubset (a :: l1) ∪ tosubset l2
    do 2 rewrite tosubset_list_cons.A: Type
a: A
l1, l2: list A
IHl1: tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2
{{a}} ∪ tosubset (l1 ++ l2) =
{{a}} ∪ tosubset l1 ∪ tosubset l2
    rewrite IHl1.A: Type
a: A
l1, l2: list A
IHl1: tosubset (l1 ++ l2) = tosubset l1 ∪ tosubset l2
{{a}} ∪ (tosubset l1 ∪ tosubset l2) =
{{a}} ∪ tosubset l1 ∪ tosubset l2 solve_basic_subset.
Qed.

#[export] Hint Rewrite
  tosubset_list_nil tosubset_list_one tosubset_list_ret
  tosubset_list_cons tosubset_list_app: tea_list.

(** ** Naturality of <<tosubset>> *)
(**********************************************************************)
#[export] Instance Natural_ToSubset_list: Natural (@tosubset list _).Natural (@tosubset list ToSubset_list)
Proof.Natural (@tosubset list ToSubset_list)
  constructor; try typeclasses eauto.forall (A B : Type) (f : A -> B),
map f ∘ tosubset = tosubset ∘ map f
  intros A B f.A, B: Type
f: A -> B
map f ∘ tosubset = tosubset ∘ map f ext l.A, B: Type
f: A -> B
l: list A
(map f ∘ tosubset) l = (tosubset ∘ map f) l
  unfold compose at 1 2.A, B: Type
f: A -> B
l: list A
map f (tosubset l) = tosubset (map f l)
  induction l.A, B: Type
f: A -> B
map f (tosubset []) = tosubset (map f [])
A, B: Type
f: A -> B
a: A
l: list A
IHl: map f (tosubset l) = tosubset (map f l)
map f (tosubset (a :: l)) = tosubset (map f (a :: l))
  -A, B: Type
f: A -> B
map f (tosubset []) = tosubset (map f []) solve_basic_subset.
  -A, B: Type
f: A -> B
a: A
l: list A
IHl: map f (tosubset l) = tosubset (map f l)
map f (tosubset (a :: l)) = tosubset (map f (a :: l)) rewrite tosubset_list_cons.A, B: Type
f: A -> B
a: A
l: list A
IHl: map f (tosubset l) = tosubset (map f l)
map f ({{a}} ∪ tosubset l) = tosubset (map f (a :: l))
    autorewrite with tea_set tea_list.A, B: Type
f: A -> B
a: A
l: list A
IHl: map f (tosubset l) = tosubset (map f l)
{{f a}} ∪ map f (tosubset l) =
{{f a}} ∪ tosubset (map f l)
    rewrite IHl.A, B: Type
f: A -> B
a: A
l: list A
IHl: map f (tosubset l) = tosubset (map f l)
{{f a}} ∪ tosubset (map f l) =
{{f a}} ∪ tosubset (map f l)
    solve_basic_subset.
Qed.

(** ** [tosubset] is a Monoid Homomorphism *)
(**********************************************************************)
#[export] Instance Monoid_Morphism_tosubset_list (A: Type):
  Monoid_Morphism (list A) (subset A) (tosubset (A := A)) :=
  {| monmor_unit := @tosubset_list_nil A;
     monmor_op := @tosubset_list_app A;
  |}.

(** ** Rewriting Laws for <<x ∈ _>> *)
(**********************************************************************)
Lemma element_of_list_nil {A}: forall (p: A), p ∈ @nil A <-> False.A: Type
forall p : A, p ∈ [] <-> False
Proof.A: Type
forall p : A, p ∈ [] <-> False
  reflexivity.
Qed.

Lemma element_of_list_one {A} (a1 a2: A): a1 ∈ [ a2 ] <-> a1 = a2.A: Type
a1, a2: A
a1 ∈ [a2] <-> a1 = a2
Proof.A: Type
a1, a2: A
a1 ∈ [a2] <-> a1 = a2
  intros.A: Type
a1, a2: A
a1 ∈ [a2] <-> a1 = a2 unfold element_of.A: Type
a1, a2: A
tosubset [a2] a1 <-> a1 = a2
  simpl_list; simpl_subset.A: Type
a1, a2: A
a2 = a1 \/ False <-> a1 = a2
  intuition congruence.
Qed.

Lemma element_of_list_cons {A}: forall (a1 a2: A) (xs: list A),
    a1 ∈ (a2 :: xs) <-> a1 = a2 \/ a1 ∈ xs.A: Type
forall (a1 a2 : A) (xs : list A),
a1 ∈ (a2 :: xs) <-> a1 = a2 \/ a1 ∈ xs
Proof.A: Type
forall (a1 a2 : A) (xs : list A),
a1 ∈ (a2 :: xs) <-> a1 = a2 \/ a1 ∈ xs
  intros; unfold element_of.A: Type
a1, a2: A
xs: list A
tosubset (a2 :: xs) a1 <-> a1 = a2 \/ tosubset xs a1
  simpl_list; simpl_subset.A: Type
a1, a2: A
xs: list A
a2 = a1 \/ tosubset xs a1 <->
a1 = a2 \/ tosubset xs a1
  intuition congruence.
Qed.

Lemma element_of_list_ret {A} (a1 a2: A): a1 ∈ ret a2 <-> a1 = a2.A: Type
a1, a2: A
a1 ∈ ret a2 <-> a1 = a2
Proof.A: Type
a1, a2: A
a1 ∈ ret a2 <-> a1 = a2
  intros.A: Type
a1, a2: A
a1 ∈ ret a2 <-> a1 = a2 unfold element_of.A: Type
a1, a2: A
tosubset (ret a2) a1 <-> a1 = a2
  simpl_list; simpl_subset.A: Type
a1, a2: A
a2 = a1 <-> a1 = a2
  easy.
Qed.

Lemma element_of_list_app {A}: forall (a: A) (xs ys: list A),
    a ∈ (xs ++ ys) <-> a ∈ xs \/ a ∈ ys.A: Type
forall (a : A) (xs ys : list A),
a ∈ (xs ++ ys) <-> a ∈ xs \/ a ∈ ys
Proof.A: Type
forall (a : A) (xs ys : list A),
a ∈ (xs ++ ys) <-> a ∈ xs \/ a ∈ ys
  intros.A: Type
a: A
xs, ys: list A
a ∈ (xs ++ ys) <-> a ∈ xs \/ a ∈ ys unfold element_of.A: Type
a: A
xs, ys: list A
tosubset (xs ++ ys) a <->
tosubset xs a \/ tosubset ys a
  simpl_list; simpl_subset.A: Type
a: A
xs, ys: list A
tosubset xs a \/ tosubset ys a <->
tosubset xs a \/ tosubset ys a
  easy.
Qed.

(* TODO: element_of_list_nil is sometimes applied at weird times, e.g.:

   Hint Rewrite @element_of_list_nil: tea_test.
   Goal (@monoid_unit Prop Monoid_unit_false).
   autorewrite with tea_test.
   Abort.

   I'm not sure what is causing this behavior
 *)
#[export] Hint Rewrite (* @element_of_list_nil *)
  @element_of_list_cons @element_of_list_one
  @element_of_list_ret @element_of_list_app: tea_list.

(** ** <<x ∈>> is a Monoid Homomorphism *)
(**********************************************************************)
#[export] Instance Monoid_Morphism_element_list (A: Type) (a: A):
  Monoid_Morphism (list A) Prop
    (tgt_op := Monoid_op_or)
    (tgt_unit := Monoid_unit_false)
    (element_of a).A: Type
a: A
Monoid_Morphism (list A) Prop (element_of a)
Proof.A: Type
a: A
Monoid_Morphism (list A) Prop (element_of a)
  rewrite element_of_tosubset.A: Type
a: A
Monoid_Morphism (list A) Prop (evalAt a ∘ tosubset)
  eapply Monoid_Morphism_compose;
    typeclasses eauto.
Qed.

(** ** Respectfulness Conditions *)
(**********************************************************************)
Theorem map_rigidly_respectful_list:
  forall (A B: Type) (f g: A -> B) (l: list A),
    (forall (a: A), a ∈ l -> f a = g a) <-> map f l = map g l.forall (A B : Type) (f g : A -> B) (l : list A),
(forall a : A, a ∈ l -> f a = g a) <->
map f l = map g l
Proof.forall (A B : Type) (f g : A -> B) (l : list A),
(forall a : A, a ∈ l -> f a = g a) <->
map f l = map g l
  intros.A, B: Type
f, g: A -> B
l: list A
(forall a : A, a ∈ l -> f a = g a) <->
map f l = map g l induction l.A, B: Type
f, g: A -> B
(forall a : A, a ∈ [] -> f a = g a) <->
map f [] = map g []
A, B: Type
f, g: A -> B
a: A
l: list A
IHl: (forall a : A, a ∈ l -> f a = g a) <-> map f l = map g l
(forall a0 : A, a0 ∈ (a :: l) -> f a0 = g a0) <->
map f (a :: l) = map g (a :: l)
  -A, B: Type
f, g: A -> B
(forall a : A, a ∈ [] -> f a = g a) <->
map f [] = map g [] simpl_list.A, B: Type
f, g: A -> B
(forall a : A, a ∈ [] -> f a = g a) <-> [] = []
    setoid_rewrite element_of_list_nil.A, B: Type
f, g: A -> B
(forall a : A, False -> f a = g a) <-> [] = []
    tauto.
  -A, B: Type
f, g: A -> B
a: A
l: list A
IHl: (forall a : A, a ∈ l -> f a = g a) <-> map f l = map g l
(forall a0 : A, a0 ∈ (a :: l) -> f a0 = g a0) <->
map f (a :: l) = map g (a :: l) simpl_list.A, B: Type
f, g: A -> B
a: A
l: list A
IHl: (forall a : A, a ∈ l -> f a = g a) <-> map f l = map g l
(forall a0 : A, a0 ∈ (a :: l) -> f a0 = g a0) <->
f a :: map f l = g a :: map g l
    setoid_rewrite element_of_list_cons.A, B: Type
f, g: A -> B
a: A
l: list A
IHl: (forall a : A, a ∈ l -> f a = g a) <-> map f l = map g l
(forall a0 : A, a0 = a \/ a0 ∈ l -> f a0 = g a0) <->
f a :: map f l = g a :: map g l
    destruct IHl.A, B: Type
f, g: A -> B
a: A
l: list A
H: (forall a : A, a ∈ l -> f a = g a) ->
map f l = map g l
H0: map f l = map g l ->
forall a : A, a ∈ l -> f a = g a
(forall a0 : A, a0 = a \/ a0 ∈ l -> f a0 = g a0) <->
f a :: map f l = g a :: map g l split.A, B: Type
f, g: A -> B
a: A
l: list A
H: (forall a : A, a ∈ l -> f a = g a) ->
map f l = map g l
H0: map f l = map g l ->
forall a : A, a ∈ l -> f a = g a
(forall a0 : A, a0 = a \/ a0 ∈ l -> f a0 = g a0) ->
f a :: map f l = g a :: map g l
A, B: Type
f, g: A -> B
a: A
l: list A
H: (forall a : A, a ∈ l -> f a = g a) ->
map f l = map g l
H0: map f l = map g l ->
forall a : A, a ∈ l -> f a = g a
f a :: map f l = g a :: map g l ->
forall a0 : A, a0 = a \/ a0 ∈ l -> f a0 = g a0
    +A, B: Type
f, g: A -> B
a: A
l: list A
H: (forall a : A, a ∈ l -> f a = g a) ->
map f l = map g l
H0: map f l = map g l ->
forall a : A, a ∈ l -> f a = g a
(forall a0 : A, a0 = a \/ a0 ∈ l -> f a0 = g a0) ->
f a :: map f l = g a :: map g l intro; fequal; auto.
    +A, B: Type
f, g: A -> B
a: A
l: list A
H: (forall a : A, a ∈ l -> f a = g a) ->
map f l = map g l
H0: map f l = map g l ->
forall a : A, a ∈ l -> f a = g a
f a :: map f l = g a :: map g l ->
forall a0 : A, a0 = a \/ a0 ∈ l -> f a0 = g a0 injection 1; intuition (subst; auto).
Qed.

Corollary map_respectful_list:
  forall (A B: Type) (l: list A) (f g: A -> B),
    (forall (a: A), a ∈ l -> f a = g a) -> map f l = map g l.forall (A B : Type) (l : list A) (f g : A -> B),
(forall a : A, a ∈ l -> f a = g a) ->
map f l = map g l
Proof.forall (A B : Type) (l : list A) (f g : A -> B),
(forall a : A, a ∈ l -> f a = g a) ->
map f l = map g l
  intros.A, B: Type
l: list A
f, g: A -> B
H: forall a : A, a ∈ l -> f a = g a
map f l = map g l now rewrite <- map_rigidly_respectful_list.
Qed.

#[export] Instance ContainerFunctor_list: ContainerFunctor list :=
  {| cont_pointwise := map_respectful_list;
  |}.

(** ** <<tosubset>> as a Monad Homomorphism *)
(**********************************************************************)
Lemma tosubset_list_hom1: forall (A: Type),
    tosubset ∘ ret (A := A) = ret (T := subset).forall A : Type, tosubset ∘ ret = ret
Proof.forall A : Type, tosubset ∘ ret = ret
  intros.A: Type
tosubset ∘ ret = ret
  ext a b.A: Type
a, b: A
(tosubset ∘ ret) a b = ret a b propext;
    cbv; intuition.
Qed.

Lemma tosubset_list_hom2: forall (A B: Type) (f: A -> list B),
    tosubset ∘ bind f = bind (T := subset) (tosubset ∘ f) ∘ tosubset.forall (A B : Type) (f : A -> list B),
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset
Proof.forall (A B : Type) (f : A -> list B),
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset
  intros.A, B: Type
f: A -> list B
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset unfold compose.A, B: Type
f: A -> list B
tosubset ○ bind f = bind (tosubset ○ f) ○ tosubset ext l b.A, B: Type
f: A -> list B
l: list A
b: B
tosubset (bind f l) b =
bind (tosubset ○ f) (tosubset l) b
  induction l.A, B: Type
f: A -> list B
b: B
tosubset (bind f []) b =
bind (tosubset ○ f) (tosubset []) b
A, B: Type
f: A -> list B
a: A
l: list A
b: B
IHl: tosubset (bind f l) b = bind (tosubset ○ f) (tosubset l) b
tosubset (bind f (a :: l)) b =
bind (tosubset ○ f) (tosubset (a :: l)) b
  -A, B: Type
f: A -> list B
b: B
tosubset (bind f []) b =
bind (tosubset ○ f) (tosubset []) b propext; cbv.A, B: Type
f: A -> list B
b: B
False ->
exists a : A,
  False /\
  (fix In (a0 : B) (l : list B) {struct l} : Prop :=
     match l with
     | [] => False
     | b :: m => b = a0 \/ In a0 m
     end) b (f a)
A, B: Type
f: A -> list B
b: B
(exists a : A,
   False /\
   (fix In (a0 : B) (l : list B) {struct l} : Prop :=
      match l with
      | [] => False
      | b :: m => b = a0 \/ In a0 m
      end) b (f a)) -> False
    +A, B: Type
f: A -> list B
b: B
False ->
exists a : A,
  False /\
  (fix In (a0 : B) (l : list B) {struct l} : Prop :=
     match l with
     | [] => False
     | b :: m => b = a0 \/ In a0 m
     end) b (f a) intuition.
    +A, B: Type
f: A -> list B
b: B
(exists a : A,
   False /\
   (fix In (a0 : B) (l : list B) {struct l} : Prop :=
      match l with
      | [] => False
      | b :: m => b = a0 \/ In a0 m
      end) b (f a)) -> False intros [a [absurd]]; contradiction.
  -A, B: Type
f: A -> list B
a: A
l: list A
b: B
IHl: tosubset (bind f l) b = bind (tosubset ○ f) (tosubset l) b
tosubset (bind f (a :: l)) b =
bind (tosubset ○ f) (tosubset (a :: l)) b autorewrite with tea_list tea_set.A, B: Type
f: A -> list B
a: A
l: list A
b: B
IHl: tosubset (bind f l) b = bind (tosubset ○ f) (tosubset l) b
(tosubset (f a) b \/ tosubset (bind f l) b) =
(tosubset (f a) b \/
 bind (tosubset ○ f) (tosubset l) b)
    rewrite IHl.A, B: Type
f: A -> list B
a: A
l: list A
b: B
IHl: tosubset (bind f l) b = bind (tosubset ○ f) (tosubset l) b
(tosubset (f a) b \/
 bind (tosubset ○ f) (tosubset l) b) =
(tosubset (f a) b \/
 bind (tosubset ○ f) (tosubset l) b)
    reflexivity.
Qed.

Lemma tosubset_list_map: forall (A B: Type) (f: A -> B),
    tosubset ∘ map f = map f ∘ tosubset.forall (A B : Type) (f : A -> B),
tosubset ∘ map f = map f ∘ tosubset
Proof.forall (A B : Type) (f : A -> B),
tosubset ∘ map f = map f ∘ tosubset
  intros.A, B: Type
f: A -> B
tosubset ∘ map f = map f ∘ tosubset
  now rewrite <- (natural (ϕ := @tosubset list _)).
Qed.

#[export] Instance Monad_Hom_list_tosubset:
  MonadHom list subset (@tosubset list _) :=
  {| kmon_hom_ret := tosubset_list_hom1;
     kmon_hom_bind := tosubset_list_hom2;
  |}.