From Tealeaves Require Import
  Classes.Coalgebraic.DecoratedTraversableFunctor
  Classes.Kleisli.DecoratedTraversableFunctor
  Adapters.KleisliToCoalgebraic.DecoratedTraversableFunctor
  Classes.Kleisli.Theory.DecoratedTraversableFunctor
  Theory.TraversableFunctor
  Functors.List
  Misc.NaturalNumbers.

Import Applicative.Notations.
Import Monoid.Notations.
Import DecoratedTraversableFunctor.Notations.
Import Kleisli.TraversableFunctor.Notations.
Import Subset.Notations.

(** * Telescoping Decoration for the List Functor *)
(**********************************************************************)

(** ** The <<decorate_telescoping_list>> Operation *)
(**********************************************************************)
Fixpoint decorate_telescoping_list_rec (n: nat) {A: Type} (l: list A):
  list (nat * A) :=
  match l with
  | nil => nil
  | x :: xs =>
      (n, x) :: decorate_telescoping_list_rec (S n) xs
  end.

Definition decorate_telescoping_list {A: Type} (l: list A):
  list (nat * A) := decorate_telescoping_list_rec 0 l.

(** ** Alternative Characterization of <<decorate_telescoping_list>> *)
(**********************************************************************)
Fixpoint decorate_telescoping_list_alt {A: Type} (l: list A):
  list (nat * A) :=
  match l with
  | nil => nil
  | x :: xs =>
      (0, x) :: map (F := list) (incr 1) (decorate_telescoping_list_alt xs)
  end.

(** ** Rewriting Rules for <<decorate_telescoping_list>> *)
(**********************************************************************)
Section decorate_telescoping_list_rw.

  Context {A: Type}.

  Lemma decorate_telescoping_list_rw_nil:
    decorate_telescoping_list_alt (@nil A) = @nil (nat * A).
A: Type
decorate_telescoping_list_alt nil = nil
  Proof.
A: Type
decorate_telescoping_list_alt nil = nil
    reflexivity.
  Qed.

  Lemma decorate_telescoping_list_rw_cons: forall (a: A) (l: list A),
      decorate_telescoping_list_alt (a :: l) =
        (0, a) :: map (F := list) (incr 1) (decorate_telescoping_list_alt l).
A: Type
forall (a : A) (l : list A),
decorate_telescoping_list_alt (a :: l) =
(0, a)
:: map (incr 1) (decorate_telescoping_list_alt l)
  Proof.
A: Type
forall (a : A) (l : list A),
decorate_telescoping_list_alt (a :: l) =
(0, a)
:: map (incr 1) (decorate_telescoping_list_alt l)
    reflexivity.
  Qed.

  Lemma decorate_telescoping_list_rw_app: forall (l1 l2: list A),
      decorate_telescoping_list_alt (l1 ++ l2) =
        decorate_telescoping_list_alt l1 ++
          map (F := list) (incr (length l1)) (decorate_telescoping_list_alt l2).
A: Type
forall l1 l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
  Proof.
A: Type
forall l1 l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
    intros.
A: Type
l1, l2: list A
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
    generalize dependent l2.
A: Type
l1: list A
forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
    induction l1; intro l2.
A: Type
l2: list A
decorate_telescoping_list_alt (nil ++ l2) =
decorate_telescoping_list_alt nil ++
map (incr (length nil))
  (decorate_telescoping_list_alt l2)
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
decorate_telescoping_list_alt ((a :: l1) ++ l2) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
    -
A: Type
l2: list A
decorate_telescoping_list_alt (nil ++ l2) =
decorate_telescoping_list_alt nil ++
map (incr (length nil))
  (decorate_telescoping_list_alt l2) cbn.
A: Type
l2: list A
decorate_telescoping_list_alt l2 =
map (incr 0) (decorate_telescoping_list_alt l2)
      change 0 with (Ƶ: nat).
A: Type
l2: list A
decorate_telescoping_list_alt l2 =
map (incr (Ƶ : nat))
  (decorate_telescoping_list_alt l2)
      rewrite incr_zero.
A: Type
l2: list A
decorate_telescoping_list_alt l2 =
map id (decorate_telescoping_list_alt l2)
      rewrite fun_map_id.
A: Type
l2: list A
decorate_telescoping_list_alt l2 =
id (decorate_telescoping_list_alt l2)
      reflexivity.
    -
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
decorate_telescoping_list_alt ((a :: l1) ++ l2) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2) rewrite <- List.app_comm_cons.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
decorate_telescoping_list_alt (a :: l1 ++ l2) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      rewrite decorate_telescoping_list_rw_cons.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
(0, a)
:: map (incr 1)
     (decorate_telescoping_list_alt (l1 ++ l2)) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      rewrite IHl1.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
(0, a)
:: map (incr 1)
     (decorate_telescoping_list_alt l1 ++
      map (incr (length l1))
        (decorate_telescoping_list_alt l2)) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      simpl_list.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
(0, a)
:: map (incr 1) (decorate_telescoping_list_alt l1) ++
   map (incr 1)
     (map (incr (length l1))
        (decorate_telescoping_list_alt l2)) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      compose near (decorate_telescoping_list_alt l2) on left.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
(0, a)
:: map (incr 1) (decorate_telescoping_list_alt l1) ++
   (map (incr 1) ∘ map (incr (length l1)))
     (decorate_telescoping_list_alt l2) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      rewrite (fun_map_map).
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
(0, a)
:: map (incr 1) (decorate_telescoping_list_alt l1) ++
   map (incr 1 ∘ incr (length l1))
     (decorate_telescoping_list_alt l2) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      rewrite incr_incr.
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
(0, a)
:: map (incr 1) (decorate_telescoping_list_alt l1) ++
   map (incr (1 ● length l1))
     (decorate_telescoping_list_alt l2) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      change (1 ● length l1) with (length (a :: l1)).
A: Type
a: A
l1: list A
IHl1: forall l2 : list A,
decorate_telescoping_list_alt (l1 ++ l2) =
decorate_telescoping_list_alt l1 ++
map (incr (length l1))
  (decorate_telescoping_list_alt l2)
l2: list A
(0, a)
:: map (incr 1) (decorate_telescoping_list_alt l1) ++
   map (incr (length (a :: l1)))
     (decorate_telescoping_list_alt l2) =
decorate_telescoping_list_alt (a :: l1) ++
map (incr (length (a :: l1)))
  (decorate_telescoping_list_alt l2)
      reflexivity.
  Qed.

End decorate_telescoping_list_rw.

(** ** Equivalence *)
(**********************************************************************)
Lemma decorate_telescoping_list_equiv: forall (A: Type) (l: list A),
    decorate_telescoping_list l = decorate_telescoping_list_alt l.
forall (A : Type) (l : list A),
decorate_telescoping_list l =
decorate_telescoping_list_alt l
Proof.
forall (A : Type) (l : list A),
decorate_telescoping_list l =
decorate_telescoping_list_alt l
  intros.
A: Type
l: list A
decorate_telescoping_list l =
decorate_telescoping_list_alt l
  unfold decorate_telescoping_list.
A: Type
l: list A
decorate_telescoping_list_rec 0 l =
decorate_telescoping_list_alt l
  assert
    (forall n, decorate_telescoping_list_rec n l =
            map (incr n) (decorate_telescoping_list_alt l)).
A: Type
l: list A
forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
A: Type
l: list A
H: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
decorate_telescoping_list_rec 0 l =
decorate_telescoping_list_alt l
  {
A: Type
l: list A
forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l) induction l.
A: Type
forall n : nat,
decorate_telescoping_list_rec n nil =
map (incr n) (decorate_telescoping_list_alt nil)
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
forall n : nat,
decorate_telescoping_list_rec n (a :: l) =
map (incr n) (decorate_telescoping_list_alt (a :: l))
    -
A: Type
forall n : nat,
decorate_telescoping_list_rec n nil =
map (incr n) (decorate_telescoping_list_alt nil) reflexivity.
    -
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
forall n : nat,
decorate_telescoping_list_rec n (a :: l) =
map (incr n) (decorate_telescoping_list_alt (a :: l)) intros.
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
decorate_telescoping_list_rec n (a :: l) =
map (incr n) (decorate_telescoping_list_alt (a :: l)) cbn.
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a) :: decorate_telescoping_list_rec (S n) l =
(n ● 0, a)
:: map (incr n)
     (map (incr 1) (decorate_telescoping_list_alt l))
      rewrite IHl.
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l) =
(n ● 0, a)
:: map (incr n)
     (map (incr 1) (decorate_telescoping_list_alt l))
      change 0 with (Ƶ: nat) at 1.
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l) =
(n ● (Ƶ : nat), a)
:: map (incr n)
     (map (incr 1) (decorate_telescoping_list_alt l))
      rewrite monoid_id_r.
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l) =
(n, a)
:: map (incr n)
     (map (incr 1) (decorate_telescoping_list_alt l))
      compose near (decorate_telescoping_list_alt l) on right.
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l) =
(n, a)
:: (map (incr n) ∘ map (incr 1))
     (decorate_telescoping_list_alt l)
      rewrite (fun_map_map).
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l) =
(n, a)
:: map (incr n ∘ incr 1)
     (decorate_telescoping_list_alt l)
      rewrite incr_incr.
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l) =
(n, a)
:: map (incr (n ● 1))
     (decorate_telescoping_list_alt l)
      replace (n ● 1) with (S n) by (unfold_ops @Monoid_op_plus; lia).
A: Type
a: A
l: list A
IHl: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
n: nat
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l) =
(n, a)
:: map (incr (S n)) (decorate_telescoping_list_alt l)
      reflexivity. }
A: Type
l: list A
H: forall n : nat,
decorate_telescoping_list_rec n l =
map (incr n) (decorate_telescoping_list_alt l)
decorate_telescoping_list_rec 0 l =
decorate_telescoping_list_alt l
  specialize (H 0).
A: Type
l: list A
H: decorate_telescoping_list_rec 0 l =
map (incr 0) (decorate_telescoping_list_alt l)
decorate_telescoping_list_rec 0 l =
decorate_telescoping_list_alt l
  replace (incr 0) with (@id (nat * A)) in H.
A: Type
l: list A
H: decorate_telescoping_list_rec 0 l =
map id (decorate_telescoping_list_alt l)
decorate_telescoping_list_rec 0 l =
decorate_telescoping_list_alt l
A: Type
l: list A
H: decorate_telescoping_list_rec 0 l =
map (incr 0) (decorate_telescoping_list_alt l)
id = incr 0
  rewrite (fun_map_id) in H.
A: Type
l: list A
H: decorate_telescoping_list_rec 0 l =
id (decorate_telescoping_list_alt l)
decorate_telescoping_list_rec 0 l =
decorate_telescoping_list_alt l
A: Type
l: list A
H: decorate_telescoping_list_rec 0 l =
map (incr 0) (decorate_telescoping_list_alt l)
id = incr 0
  assumption.
A: Type
l: list A
H: decorate_telescoping_list_rec 0 l =
map (incr 0) (decorate_telescoping_list_alt l)
id = incr 0
  change 0 with (Ƶ: nat).
A: Type
l: list A
H: decorate_telescoping_list_rec 0 l =
map (incr 0) (decorate_telescoping_list_alt l)
id = incr (Ƶ : nat)
  now rewrite incr_zero.
Qed.

(** ** Associated <<mapdt>> Operation *)
(**********************************************************************)
Fixpoint mapdt_telescoping_list
  {G: Type -> Type} `{Map G} `{Pure G} `{Mult G}
  {A B: Type} (f: nat * A -> G B) (l: list A)
 : G (list B) :=
  match l with
  | nil => pure (@nil B)
  | x :: xs =>
      pure (@List.cons B) <⋆> f (0, x) <⋆>
        mapdt_telescoping_list (f ⦿ 1) xs
  end.

#[export] Instance Mapdt_Telescoping_List:
  Mapdt nat list := @mapdt_telescoping_list.

Lemma mapdt_telescoping_list_spec:
  forall {G} `{Applicative G} {A B: Type} (f: nat * A -> G B) (l: list A),
    mapdt f l = traverse f (decorate_telescoping_list_alt l).
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : nat * A -> G B) (l : list A),
mapdt f l =
traverse f (decorate_telescoping_list_alt 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 : nat * A -> G B) (l : list A),
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
  intros.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: nat * A -> G B
l: list A
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
  generalize dependent f.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
l: list A
forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
  induction l; intro f.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: nat * A -> G B
mapdt f nil =
traverse f (decorate_telescoping_list_alt nil)
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
f: nat * A -> G B
mapdt f (a :: l) =
traverse f (decorate_telescoping_list_alt (a :: l))
  -
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: nat * A -> G B
mapdt f nil =
traverse f (decorate_telescoping_list_alt nil) reflexivity.
  -
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
f: nat * A -> G B
mapdt f (a :: l) =
traverse f (decorate_telescoping_list_alt (a :: l)) cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
f: nat * A -> G B
pure cons <⋆> f (0, a) <⋆> mapdt (f ⦿ 1) l =
pure cons <⋆> f (0, a) <⋆>
traverse f
  (map (incr 1) (decorate_telescoping_list_alt l)) fequal.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
f: nat * A -> G B
mapdt (f ⦿ 1) l =
traverse f
  (map (incr 1) (decorate_telescoping_list_alt l))
    rewrite IHl.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
f: nat * A -> G B
traverse (f ⦿ 1) (decorate_telescoping_list_alt l) =
traverse f
  (map (incr 1) (decorate_telescoping_list_alt l))
    compose near (decorate_telescoping_list_alt l) on right.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
f: nat * A -> G B
traverse (f ⦿ 1) (decorate_telescoping_list_alt l) =
(traverse f ∘ map (incr 1))
  (decorate_telescoping_list_alt l)
    rewrite (traverse_map).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G B,
mapdt f l =
traverse f (decorate_telescoping_list_alt l)
f: nat * A -> G B
traverse (f ⦿ 1) (decorate_telescoping_list_alt l) =
traverse (f ∘ incr 1)
  (decorate_telescoping_list_alt l)
    reflexivity.
Qed.

(** ** Rewriting Rules for <<decorate_telescoping_list>> *)
(**********************************************************************)
Section mapdt_telescoping_list_rw.

  Context {A B: Type}.

  Context
    {G: Type -> Type}
    `{Applicative G}.

  Implicit Type (f: nat * A -> G B).

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

  Lemma mapdt_telescoping_list_rw_cons: forall f (a: A) (l: list A),
      mapdt_telescoping_list f (a :: l) =
        pure cons
          <⋆> f (0, a)
          <⋆> mapdt_telescoping_list (f ⦿ 1) l.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall f (a : A) (l : list A),
mapdt_telescoping_list f (a :: l) =
pure cons <⋆> f (0, a) <⋆>
mapdt_telescoping_list (f ⦿ 1) l
  Proof.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall f (a : A) (l : list A),
mapdt_telescoping_list f (a :: l) =
pure cons <⋆> f (0, a) <⋆>
mapdt_telescoping_list (f ⦿ 1) l
    reflexivity.
  Qed.

  Lemma mapdt_telescoping_list_rw_app: forall f (l1 l2: list A),
      mapdt_telescoping_list f (l1 ++ l2) =
        pure (@app B)
          <⋆> mapdt_telescoping_list f l1
          <⋆> mapdt_telescoping_list (f ⦿ length l1) l2.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall f (l1 l2 : list A),
mapdt_telescoping_list f (l1 ++ l2) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
  Proof.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall f (l1 l2 : list A),
mapdt_telescoping_list f (l1 ++ l2) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    intros.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
mapdt_telescoping_list f (l1 ++ l2) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    rewrite mapdt_telescoping_list_spec.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
traverse f (decorate_telescoping_list_alt (l1 ++ l2)) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    rewrite decorate_telescoping_list_rw_app.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
traverse f
  (decorate_telescoping_list_alt l1 ++
   map (incr (length l1))
     (decorate_telescoping_list_alt l2)) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    rewrite (traverse_list_app G).
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
pure (app (A:=B)) <⋆>
traverse f (decorate_telescoping_list_alt l1) <⋆>
traverse f
  (map (incr (length l1))
     (decorate_telescoping_list_alt l2)) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    rewrite <- mapdt_telescoping_list_spec.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
pure (app (A:=B)) <⋆> mapdt f l1 <⋆>
traverse f
  (map (incr (length l1))
     (decorate_telescoping_list_alt l2)) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    compose near (decorate_telescoping_list_alt l2).
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
pure (app (A:=B)) <⋆> mapdt f l1 <⋆>
(traverse f ∘ map (incr (length l1)))
  (decorate_telescoping_list_alt l2) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    rewrite traverse_map.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
pure (app (A:=B)) <⋆> mapdt f l1 <⋆>
traverse (f ∘ incr (length l1))
  (decorate_telescoping_list_alt l2) =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    rewrite <- mapdt_telescoping_list_spec.
A, B: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
f: nat * A -> G B
l1, l2: list A
pure (app (A:=B)) <⋆> mapdt f l1 <⋆>
mapdt (f ∘ incr (length l1)) l2 =
pure (app (A:=B)) <⋆> mapdt_telescoping_list f l1 <⋆>
mapdt_telescoping_list (f ⦿ length l1) l2
    reflexivity.
  Qed.

End mapdt_telescoping_list_rw.

(** ** Typeclass Instance *)
(**********************************************************************)
#[export] Instance DecoratedTraversableFunctor_List_Telescope:
  @DecoratedTraversableFunctor
    nat list Mapdt_Telescoping_List.
DecoratedTraversableFunctor nat list
Proof.
DecoratedTraversableFunctor nat list
  constructor;
    unfold_ops @Mapdt_Telescoping_List;
    intros; ext l.
A: Type
l: list A
mapdt_telescoping_list extract l = id l
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
l: list A
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
  -
A: Type
l: list A
mapdt_telescoping_list extract l = id l induction l.
A: Type
mapdt_telescoping_list extract nil = id nil
A: Type
a: A
l: list A
IHl: mapdt_telescoping_list extract l = id l
mapdt_telescoping_list extract (a :: l) = id (a :: l)
    +
A: Type
mapdt_telescoping_list extract nil = id nil rewrite mapdt_telescoping_list_rw_nil.
A: Type
pure nil = id nil
      reflexivity.
    +
A: Type
a: A
l: list A
IHl: mapdt_telescoping_list extract l = id l
mapdt_telescoping_list extract (a :: l) = id (a :: l) rewrite mapdt_telescoping_list_rw_cons.
A: Type
a: A
l: list A
IHl: mapdt_telescoping_list extract l = id l
pure cons <⋆> extract (0, a) <⋆>
mapdt_telescoping_list (extract ⦿ 1) l = 
id (a :: l)
      rewrite Writer.extract_preincr.
A: Type
a: A
l: list A
IHl: mapdt_telescoping_list extract l = id l
pure cons <⋆> extract (0, a) <⋆>
mapdt_telescoping_list extract l = 
id (a :: l)
      rewrite IHl.
A: Type
a: A
l: list A
IHl: mapdt_telescoping_list extract l = id l
pure cons <⋆> extract (0, a) <⋆> id l = id (a :: l)
      reflexivity.
  -
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l generalize dependent f.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
l: list A
forall f : nat * A -> G1 B,
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
    generalize dependent g.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
l: list A
forall (g : nat * B -> G2 C) (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
    induction l; intros g f.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) nil =
mapdt_telescoping_list (g ⋆3 f) nil
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) 
  (a :: l) = mapdt_telescoping_list (g ⋆3 f) (a :: l)
    +
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) nil =
mapdt_telescoping_list (g ⋆3 f) nil unfold compose.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
map (mapdt_telescoping_list g)
  (mapdt_telescoping_list f nil) =
mapdt_telescoping_list (g ⋆3 f) nil
      rewrite mapdt_telescoping_list_rw_nil.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
map (mapdt_telescoping_list g) (pure nil) =
mapdt_telescoping_list (g ⋆3 f) nil
      rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (mapdt_telescoping_list g nil) =
mapdt_telescoping_list (g ⋆3 f) nil
      rewrite mapdt_telescoping_list_rw_nil.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (pure nil) = mapdt_telescoping_list (g ⋆3 f) nil
      rewrite mapdt_telescoping_list_rw_nil.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (pure nil) = pure nil
      reflexivity.
    +
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) 
  (a :: l) = mapdt_telescoping_list (g ⋆3 f) (a :: l) unfold compose.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
map (mapdt_telescoping_list g)
  (mapdt_telescoping_list f (a :: l)) =
mapdt_telescoping_list (g ⋆3 f) (a :: l)
      (* left *)
      rewrite mapdt_telescoping_list_rw_cons.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
map (mapdt_telescoping_list g)
  (pure cons <⋆> f (0, a) <⋆>
   mapdt_telescoping_list (f ⦿ 1) l) =
mapdt_telescoping_list (g ⋆3 f) (a :: l)
      rewrite map_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
map (compose (mapdt_telescoping_list g))
  (pure cons <⋆> f (0, a)) <⋆>
mapdt_telescoping_list (f ⦿ 1) l =
mapdt_telescoping_list (g ⋆3 f) (a :: l)
      rewrite map_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
map (compose (compose (mapdt_telescoping_list g)))
  (pure cons) <⋆> f (0, a) <⋆>
mapdt_telescoping_list (f ⦿ 1) l =
mapdt_telescoping_list (g ⋆3 f) (a :: l)
      rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
mapdt_telescoping_list (g ⋆3 f) (a :: l)
      (* right *)
      rewrite mapdt_telescoping_list_rw_cons.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure cons <⋆> (g ⋆3 f) (0, a) <⋆>
mapdt_telescoping_list ((g ⋆3 f) ⦿ 1) l
      unfold_ops @Pure_compose.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure (pure cons) <⋆> (g ⋆3 f) (0, a) <⋆>
mapdt_telescoping_list ((g ⋆3 f) ⦿ 1) l
      rewrite kc3_preincr.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure (pure cons) <⋆> (g ⋆3 f) (0, a) <⋆>
mapdt_telescoping_list (g ⦿ 1 ⋆3 f ⦿ 1) l
      rewrite kc3_spec.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure (pure cons) <⋆> map (g ∘ pair 0) (f (0, a)) <⋆>
mapdt_telescoping_list (g ⦿ 1 ⋆3 f ⦿ 1) l
      rewrite <- IHl.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure (pure cons) <⋆> map (g ∘ pair 0) (f (0, a)) <⋆>
(map (mapdt_telescoping_list (g ⦿ 1))
 ∘ mapdt_telescoping_list (f ⦿ 1)) l
      unfold compose at 4.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure (pure cons) <⋆> map (g ∘ pair 0) (f (0, a)) <⋆>
map (mapdt_telescoping_list (g ⦿ 1))
  (mapdt_telescoping_list (f ⦿ 1) l)
      rewrite (ap_compose2 G2 G1).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
map (ap G2)
  (pure (pure cons) <⋆> map (g ∘ pair 0) (f (0, a))) <⋆>
map (mapdt_telescoping_list (g ⦿ 1))
  (mapdt_telescoping_list (f ⦿ 1) l)
      rewrite (ap_compose2 G2 G1).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
map (ap G2)
  (map (ap G2) (pure (pure cons)) <⋆>
   map (g ∘ pair 0) (f (0, a))) <⋆>
map (mapdt_telescoping_list (g ⦿ 1))
  (mapdt_telescoping_list (f ⦿ 1) l)
      rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
map (ap G2)
  (pure (ap G2 (pure cons)) <⋆>
   map (g ∘ pair 0) (f (0, a))) <⋆>
map (mapdt_telescoping_list (g ⦿ 1))
  (mapdt_telescoping_list (f ⦿ 1) l)
      rewrite map_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
map (compose (ap G2)) (pure (ap G2 (pure cons))) <⋆>
map (g ∘ pair 0) (f (0, a)) <⋆>
map (mapdt_telescoping_list (g ⦿ 1))
  (mapdt_telescoping_list (f ⦿ 1) l)
      rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure (ap G2 ∘ ap G2 (pure cons)) <⋆>
map (g ∘ pair 0) (f (0, a)) <⋆>
map (mapdt_telescoping_list (g ⦿ 1))
  (mapdt_telescoping_list (f ⦿ 1) l)
      rewrite <- ap_map.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
map (precompose (mapdt_telescoping_list (g ⦿ 1)))
  (pure (ap G2 ∘ ap G2 (pure cons)) <⋆>
   map (g ∘ pair 0) (f (0, a))) <⋆>
mapdt_telescoping_list (f ⦿ 1) l
      rewrite map_ap.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
map
  (compose
     (precompose (mapdt_telescoping_list (g ⦿ 1))))
  (pure (ap G2 ∘ ap G2 (pure cons))) <⋆>
map (g ∘ pair 0) (f (0, a)) <⋆>
mapdt_telescoping_list (f ⦿ 1) l
      rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure
  (precompose (mapdt_telescoping_list (g ⦿ 1))
   ∘ (ap G2 ∘ ap G2 (pure cons))) <⋆>
map (g ∘ pair 0) (f (0, a)) <⋆>
mapdt_telescoping_list (f ⦿ 1) l
      rewrite <- ap_map.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
map (precompose (g ∘ pair 0))
  (pure
     (precompose (mapdt_telescoping_list (g ⦿ 1))
      ∘ (ap G2 ∘ ap G2 (pure cons)))) <⋆> 
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l
      rewrite app_pure_natural.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
a: A
l: list A
IHl: forall (g : nat * B -> G2 C)
  (f : nat * A -> G1 B),
(map (mapdt_telescoping_list g)
 ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (g ⋆3 f) l
g: nat * B -> G2 C
f: nat * A -> G1 B
pure (compose (mapdt_telescoping_list g) ∘ cons) <⋆>
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l =
pure
  (precompose (g ∘ pair 0)
     (precompose (mapdt_telescoping_list (g ⦿ 1))
      ∘ (ap G2 ∘ ap G2 (pure cons)))) <⋆> 
f (0, a) <⋆> mapdt_telescoping_list (f ⦿ 1) l
      reflexivity.
  -
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
l: list A
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l generalize dependent f.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
l: list A
forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
    induction l; intro f.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
(ϕ (list B) ∘ mapdt_telescoping_list f) nil =
mapdt_telescoping_list (ϕ B ∘ f) nil
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
(ϕ (list B) ∘ mapdt_telescoping_list f) (a :: l) =
mapdt_telescoping_list (ϕ B ∘ f) (a :: l)
    +
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
(ϕ (list B) ∘ mapdt_telescoping_list f) nil =
mapdt_telescoping_list (ϕ B ∘ f) nil unfold compose.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
ϕ (list B) (mapdt_telescoping_list f nil) =
mapdt_telescoping_list (ϕ B ○ f) nil cbn.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
ϕ (list B) (pure nil) = pure nil
      now rewrite appmor_pure.
    +
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
(ϕ (list B) ∘ mapdt_telescoping_list f) (a :: l) =
mapdt_telescoping_list (ϕ B ∘ f) (a :: l) unfold compose at 1.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
ϕ (list B) (mapdt_telescoping_list f (a :: l)) =
mapdt_telescoping_list (ϕ B ∘ f) (a :: l)
      rewrite mapdt_telescoping_list_rw_cons.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
ϕ (list B)
  (pure cons <⋆> f (0, a) <⋆>
   mapdt_telescoping_list (f ⦿ 1) l) =
mapdt_telescoping_list (ϕ B ∘ f) (a :: l)
      rewrite ap_morphism_1.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
ϕ (list B -> list B) (pure cons <⋆> f (0, a)) <⋆>
ϕ (list B) (mapdt_telescoping_list (f ⦿ 1) l) =
mapdt_telescoping_list (ϕ B ∘ f) (a :: l)
      rewrite ap_morphism_1.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
ϕ (B -> list B -> list B) (pure cons) <⋆>
ϕ B (f (0, a)) <⋆>
ϕ (list B) (mapdt_telescoping_list (f ⦿ 1) l) =
mapdt_telescoping_list (ϕ B ∘ f) (a :: l)
      rewrite appmor_pure.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
pure cons <⋆> ϕ B (f (0, a)) <⋆>
ϕ (list B) (mapdt_telescoping_list (f ⦿ 1) l) =
mapdt_telescoping_list (ϕ B ∘ f) (a :: l)
      rewrite mapdt_telescoping_list_rw_cons.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
pure cons <⋆> ϕ B (f (0, a)) <⋆>
ϕ (list B) (mapdt_telescoping_list (f ⦿ 1) l) =
pure cons <⋆> (ϕ B ∘ f) (0, a) <⋆>
mapdt_telescoping_list ((ϕ B ∘ f) ⦿ 1) l
      compose near l on left.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
pure cons <⋆> ϕ B (f (0, a)) <⋆>
(ϕ (list B) ∘ mapdt_telescoping_list (f ⦿ 1)) l =
pure cons <⋆> (ϕ B ∘ f) (0, a) <⋆>
mapdt_telescoping_list ((ϕ B ∘ f) ⦿ 1) l
      rewrite IHl.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
a: A
l: list A
IHl: forall f : nat * A -> G1 B,
(ϕ (list B) ∘ mapdt_telescoping_list f) l =
mapdt_telescoping_list (ϕ B ∘ f) l
f: nat * A -> G1 B
pure cons <⋆> ϕ B (f (0, a)) <⋆>
mapdt_telescoping_list (ϕ B ∘ f ⦿ 1) l =
pure cons <⋆> (ϕ B ∘ f) (0, a) <⋆>
mapdt_telescoping_list ((ϕ B ∘ f) ⦿ 1) l
      reflexivity.
Qed.

(** ** Derived Operation Compatibility *)
(**********************************************************************)
#[export] Instance ToBatch3_Telescoping_List: ToBatch3 nat list
  := DerivedOperations.ToBatch3_Mapdt (H := Mapdt_Telescoping_List).

#[export] Instance Mapd_List_Telescope: Mapd nat list :=
  DerivedOperations.Mapd_Mapdt.

#[export] Instance Compat_Mapd_Mapdt_Telescoping_List:
  Compat_Mapd_Mapdt nat list := ltac:(typeclasses eauto).
#[export] Instance Compat_Traverse_Mapdt_Telescoping_List:
  @Compat_Traverse_Mapdt nat list Traverse_list Mapdt_Telescoping_List.
Compat_Traverse_Mapdt nat list
Proof.
Compat_Traverse_Mapdt nat list
  hnf.
Traverse_list = DerivedOperations.Traverse_Mapdt
  ext G MapG PureG MultG.
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
Traverse_list G MapG PureG MultG =
DerivedOperations.Traverse_Mapdt G MapG PureG MultG
  ext A B f l.
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
l: list A
Traverse_list G MapG PureG MultG A B f l =
DerivedOperations.Traverse_Mapdt G MapG PureG MultG A
  B f l
  change_left (traverse f l).
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
l: list A
traverse f l =
DerivedOperations.Traverse_Mapdt G MapG PureG MultG A
  B f l
  unfold DerivedOperations.Traverse_Mapdt.
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
l: list A
traverse f l = mapdt (f ∘ extract) l
  induction l as [|a rest IHrest].
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
traverse f nil = mapdt (f ∘ extract) nil
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: traverse f rest = mapdt (f ∘ extract) rest
traverse f (a :: rest) =
mapdt (f ∘ extract) (a :: rest)
  -
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
traverse f nil = mapdt (f ∘ extract) nil reflexivity.
  -
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: traverse f rest = mapdt (f ∘ extract) rest
traverse f (a :: rest) =
mapdt (f ∘ extract) (a :: rest) cbn.
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: traverse f rest = mapdt (f ∘ extract) rest
pure cons <⋆> f a <⋆> traverse f rest =
pure cons <⋆> (f ∘ extract) (0, a) <⋆>
mapdt ((f ∘ extract) ⦿ 1) rest fequal.
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: traverse f rest = mapdt (f ∘ extract) rest
traverse f rest = mapdt ((f ∘ extract) ⦿ 1) rest
    rewrite IHrest.
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: traverse f rest = mapdt (f ∘ extract) rest
mapdt (f ∘ extract) rest =
mapdt ((f ∘ extract) ⦿ 1) rest
    rewrite Writer.extract_preincr2.
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: A
rest: list A
IHrest: traverse f rest = mapdt (f ∘ extract) rest
mapdt (f ∘ extract) rest = mapdt (f ∘ extract) rest
    reflexivity.
Qed.

#[export] Instance Compat_Map_Mapdt_Telescoping_List:
  @Compat_Map_Mapdt nat list Map_list Mapdt_Telescoping_List.
Compat_Map_Mapdt nat list
Proof.
Compat_Map_Mapdt nat list
  unfold Compat_Map_Mapdt.
Map_list = DerivedOperations.Map_Mapdt
  ext A B f l.
A, B: Type
f: A -> B
l: list A
Map_list A B f l = DerivedOperations.Map_Mapdt A B f l
  induction l as [|a rest IHrest].
A, B: Type
f: A -> B
Map_list A B f nil =
DerivedOperations.Map_Mapdt A B f nil
A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Mapdt A B f rest
Map_list A B f (a :: rest) =
DerivedOperations.Map_Mapdt A B f (a :: rest)
  -
A, B: Type
f: A -> B
Map_list A B f nil =
DerivedOperations.Map_Mapdt A B f nil reflexivity.
  -
A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Mapdt A B f rest
Map_list A B f (a :: rest) =
DerivedOperations.Map_Mapdt 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_Mapdt A B f rest
f a :: Map_list A B f rest =
pure cons ((f ∘ extract) (0, a))
  (mapdt ((f ∘ extract) ⦿ 1) rest) fequal.
A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Mapdt A B f rest
Map_list A B f rest = mapdt ((f ∘ extract) ⦿ 1) rest
    rewrite IHrest.
A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Mapdt A B f rest
DerivedOperations.Map_Mapdt A B f rest =
mapdt ((f ∘ extract) ⦿ 1) rest
    rewrite Writer.extract_preincr2.
A, B: Type
f: A -> B
a: A
rest: list A
IHrest: Map_list A B f rest =
DerivedOperations.Map_Mapdt A B f rest
DerivedOperations.Map_Mapdt A B f rest =
mapdt (f ∘ extract) rest
    reflexivity.
Qed.

(** ** Associated <<toctxlist>> and <<toctxset>> Operations *)
(**********************************************************************)
#[export] Instance ToCtxlist_List_Telescoping:
  ToCtxlist nat list := ToCtxlist_Mapdt.

#[export] Instance ToCtxset_List_Telescoping:
  ToCtxset nat list := ToCtxset_Mapdt.

#[export] Instance Compat_ToSubset_ToCtxset_List_Telescoping:
  @Compat_ToSubset_ToCtxset
    nat list ToCtxset_List_Telescoping ToSubset_list.
Compat_ToSubset_ToCtxset nat list
Proof.
Compat_ToSubset_ToCtxset nat list
  unfold Compat_ToSubset_ToCtxset.
ToSubset_list = ToSubset_ToCtxset
  ext A l a.
A: Type
l: list A
a: A
ToSubset_list A l a = ToSubset_ToCtxset A l a
  change_left (tosubset l a).
A: Type
l: list A
a: A
tosubset l a = ToSubset_ToCtxset A l a
  unfold_ops @ToSubset_ToCtxset.
A: Type
l: list A
a: A
tosubset l a = (map extract ∘ toctxset) l a
  unfold_ops @ToCtxset_List_Telescoping.
A: Type
l: list A
a: A
tosubset l a = (map extract ∘ ToCtxset_Mapdt A) l a
  unfold_ops @ToCtxset_Mapdt.
A: Type
l: list A
a: A
tosubset l a = (map extract ∘ mapdReduce ret) l a
  rewrite mapdReduce_morphism.
A: Type
l: list A
a: A
tosubset l a = mapdReduce (map extract ∘ ret) l a
  rewrite tosubset_to_mapReduce.
A: Type
l: list A
a: A
mapReduce ret l a = mapdReduce (map extract ∘ ret) l a
  rewrite mapReduce_to_mapdReduce.
A: Type
l: list A
a: A
mapdReduce (ret ∘ extract) l a =
mapdReduce (map extract ∘ ret) l a
  rewrite (natural (ϕ := @ret subset _)).
A: Type
l: list A
a: A
mapdReduce (ret ∘ extract) l a =
mapdReduce (ret ∘ map extract) l a
  reflexivity.
Qed.


(** * Fully Recursive Decoration for the List Functor *)
(**********************************************************************)

(** ** The <<decorate_list_full>> Operation *)
(**********************************************************************)
Definition decorate_list_full {A: Type} (l: list A):
  list (nat * A) :=
  map (pair (length l)) l.

(** ** The Associated <<mapdt_list_full>> Operation *)
(**********************************************************************)
Definition mapdt_list_full
  {G: Type -> Type} `{Map G} `{Pure G} `{Mult G}
  {A B: Type} (f: nat * A -> G B) (l: list A)
 : G (list B) :=
  traverse (T := list) (G := G) (f ∘ pair (length l)) l.

#[export] Instance Mapdt_List_Full: Mapdt nat list := @mapdt_list_full.

(** ** <<DecoratedTraversableFunctor>> Typeclass Instance *)
(**********************************************************************)
#[export] Instance DecoratedTraversableFunctor_List_Full:
  @DecoratedTraversableFunctor
    nat list Mapdt_List_Full.
DecoratedTraversableFunctor nat list
Proof.
DecoratedTraversableFunctor nat list
  constructor; intros; ext l;
    unfold_ops @Mapdt_List_Full;
    unfold mapdt_list_full.
A: Type
l: list A
traverse (extract ∘ pair (length l)) l = id l
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
(map
   (fun l : list B => traverse (g ∘ pair (length l)) l)
 ∘ (fun l : list A => traverse (f ∘ pair (length l)) l))
  l = traverse ((g ⋆3 f) ∘ pair (length l)) l
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
l: list A
(ϕ (list B)
 ∘ (fun l : list A => traverse (f ∘ pair (length l)) l))
  l = traverse (ϕ B ∘ f ∘ pair (length l)) l
  -
A: Type
l: list A
traverse (extract ∘ pair (length l)) l = id l rewrite Writer.extract_pair.
A: Type
l: list A
traverse id l = id l
    now rewrite trf_traverse_id.
  -
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
(map
   (fun l : list B => traverse (g ∘ pair (length l)) l)
 ∘ (fun l : list A => traverse (f ∘ pair (length l)) l))
  l = traverse ((g ⋆3 f) ∘ pair (length l)) l unfold compose at 1.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (traverse (f ∘ pair (length l)) l) =
traverse ((g ⋆3 f) ∘ pair (length l)) l
    assert (kc_spec:
             kc3 (G1 := G1)(G2 := G2) g f ∘ pair (length l) =
               kc2 (g ∘ pair (length l)) (f ∘ pair (length l))).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
(g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (traverse (f ∘ pair (length l)) l) =
traverse ((g ⋆3 f) ∘ pair (length l)) l
    {
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
(g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l) ext a.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
a: A
((g ⋆3 f) ∘ pair (length l)) a =
(g ∘ pair (length l) ⋆2 f ∘ pair (length l)) a unfold kc3, kc2, compose; cbn.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
a: A
map g (map (pair (length l)) (f (length l, a))) =
map (g ○ pair (length l)) (f (length l, a))
      compose near (f (length l, a)) on left.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
a: A
(map g ∘ map (pair (length l))) (f (length l, a)) =
map (g ○ pair (length l)) (f (length l, a))
      now rewrite (fun_map_map (F := G1)). }
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (traverse (f ∘ pair (length l)) l) =
traverse ((g ⋆3 f) ∘ pair (length l)) l
    Set Keyed Unification.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (traverse (f ∘ pair (length l)) l) =
traverse ((g ⋆3 f) ∘ pair (length l)) l
    rewrite kc_spec.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (traverse (f ∘ pair (length l)) l) =
traverse (g ∘ pair (length l) ⋆2 f ∘ pair (length l))
  l
    Unset Keyed Unification.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (traverse (f ∘ pair (length l)) l) =
traverse (g ∘ pair (length l) ⋆2 f ∘ pair (length l))
  l
    rewrite <- trf_traverse_traverse.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (traverse (f ∘ pair (length l)) l) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    rewrite traverse_repr.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun l : list B => traverse (g ∘ pair (length l)) l)
  (map (trav_make l)
     (forwards
        (traverse
           (mkBackwards ∘ (f ∘ pair (length l)))
           (trav_contents l)))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    change (map ?g (map ?f ?x)) with ((map g ∘ map f) x).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
(map
   (fun l : list B => traverse (g ∘ pair (length l)) l)
 ∘ map (trav_make l))
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    rewrite (fun_map_map).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  ((fun l : list B => traverse (g ∘ pair (length l)) l)
   ∘ trav_make l)
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    cbn beta.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  ((fun l : list B => traverse (g ∘ pair (length l)) l)
   ∘ trav_make l)
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    unfold compose at 1.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
map
  (fun a : Vector (plength l) B =>
   traverse (g ∘ pair (length (trav_make l a)))
     (trav_make l a))
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    assert
      (cut:
        (fun (a: Vector (plength l) B) =>
           traverse (g ∘ pair (length (trav_make l a))) (trav_make l a))
        =
          (fun (a: Vector (plength l) B) =>
             traverse (g ∘ pair (length l)) (trav_make l a))).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
(fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
cut: (fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
map
  (fun a : Vector (plength l) B =>
   traverse (g ∘ pair (length (trav_make l a)))
     (trav_make l a))
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    {
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
(fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l ext a.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
a: Vector (plength l) B
traverse (g ∘ pair (length (trav_make l a)))
  (trav_make l a) =
traverse (g ∘ pair (length l)) (trav_make l a)
      rewrite <- list_plength_length.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
a: Vector (plength l) B
traverse (g ∘ pair (plength (trav_make l a)))
  (trav_make l a) =
traverse (g ∘ pair (length l)) (trav_make l a)
      rewrite <- list_plength_length.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
a: Vector (plength l) B
traverse (g ∘ pair (plength (trav_make l a)))
  (trav_make l a) =
traverse (g ∘ pair (plength l)) (trav_make l a)
      rewrite <- TraversableFunctor.plength_trav_make.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
a: Vector (plength l) B
traverse (g ∘ pair (plength l)) (trav_make l a) =
traverse (g ∘ pair (plength l)) (trav_make l a)
      reflexivity. }
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
cut: (fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
map
  (fun a : Vector (plength l) B =>
   traverse (g ∘ pair (length (trav_make l a)))
     (trav_make l a))
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    rewrite cut.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
cut: (fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
map (traverse (g ∘ pair (length l)) ○ trav_make l)
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    change (?g ○ trav_make l) with (g ∘ trav_make l).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
cut: (fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
map (traverse (g ∘ pair (length l)) ∘ trav_make l)
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    rewrite <- (fun_map_map).
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
cut: (fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
(map (traverse (g ∘ pair (length l)))
 ∘ map (trav_make l))
  (forwards
     (traverse (mkBackwards ∘ (f ∘ pair (length l)))
        (trav_contents l))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    unfold compose at 1.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
cut: (fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
map (traverse (g ∘ pair (length l)))
  (map (trav_make l)
     (forwards
        (traverse
           (mkBackwards ∘ (f ∘ pair (length l)))
           (trav_contents l)))) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    rewrite <- traverse_repr.
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
A, B, C: Type
g: nat * B -> G2 C
f: nat * A -> G1 B
l: list A
kc_spec: (g ⋆3 f) ∘ pair (length l) =
g ∘ pair (length l) ⋆2 f ∘ pair (length l)
cut: (fun a : Vector (plength l) B =>
 traverse (g ∘ pair (length (trav_make l a)))
   (trav_make l a)) =
traverse (g ∘ pair (length l)) ○ trav_make l
map (traverse (g ∘ pair (length l)))
  (traverse (f ∘ pair (length l)) l) =
(map (traverse (g ∘ pair (length l)))
 ∘ traverse (f ∘ pair (length l))) l
    reflexivity.
  -
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
l: list A
(ϕ (list B)
 ∘ (fun l : list A => traverse (f ∘ pair (length l)) l))
  l = traverse (ϕ B ∘ f ∘ pair (length l)) l reassociate -> on right.
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
l: list A
(ϕ (list B)
 ∘ (fun l : list A => traverse (f ∘ pair (length l)) l))
  l = traverse (ϕ B ∘ (f ∘ pair (length l))) l
    rewrite <- (trf_traverse_morphism).
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 B
l: list A
(ϕ (list B)
 ∘ (fun l : list A => traverse (f ∘ pair (length l)) l))
  l = (ϕ (list B) ∘ traverse (f ∘ pair (length l))) l
    reflexivity.
Qed.

(** ** Derived <<toBatch3>> and <<mapd>> *)
(**********************************************************************)
#[export] Instance ToBatch3_List_Full: ToBatch3 nat list
  := DerivedOperations.ToBatch3_Mapdt (H := Mapdt_List_Full).

#[export] Instance Mapd_List_Full: Mapd nat list :=
  @DerivedOperations.Mapd_Mapdt nat list Mapdt_List_Full.

(** ** Compatibility Instances *)
(**********************************************************************)
#[export] Instance Compat_Traverse_Mapdt_List_Full:
  @Compat_Traverse_Mapdt nat list Traverse_list Mapdt_List_Full.
Compat_Traverse_Mapdt nat list
Proof.
Compat_Traverse_Mapdt nat list
  unfold Compat_Traverse_Mapdt.
Traverse_list = DerivedOperations.Traverse_Mapdt
  reflexivity.
Qed.

#[export] Instance Compat_Mapd_Mapdt_List_Full:
  Compat_Mapd_Mapdt nat list :=
  ltac:(typeclasses eauto).

#[export] Instance Compat_Map_Mapdt_List_Full:
  @Compat_Map_Mapdt nat list Map_list Mapdt_List_Full.
Compat_Map_Mapdt nat list
Proof.
Compat_Map_Mapdt nat list
  unfold Compat_Map_Mapdt.
Map_list = DerivedOperations.Map_Mapdt
  unfold_ops @DerivedOperations.Map_Mapdt.
Map_list =
(fun (A B : Type) (f : A -> B) => mapdt (f ∘ extract))
  unfold_ops @Mapdt_List_Full.
Map_list =
(fun (A B : Type) (f : A -> B) =>
 mapdt_list_full (f ∘ extract))
  unfold mapdt_list_full.
Map_list =
(fun (A B : Type) (f : A -> B) (l : list A) =>
 traverse (f ∘ extract ∘ pair (length l)) l)
  ext A B f l.
A, B: Type
f: A -> B
l: list A
Map_list A B f l =
traverse (f ∘ extract ∘ pair (length l)) l
  reassociate -> on right.
A, B: Type
f: A -> B
l: list A
Map_list A B f l =
traverse (f ∘ (extract ∘ pair (length l))) l
  rewrite Writer.extract_pair.
A, B: Type
f: A -> B
l: list A
Map_list A B f l = traverse (f ∘ id) l
  change (?f ∘ id) with f.
A, B: Type
f: A -> B
l: list A
Map_list A B f l = traverse f l
  rewrite <- map_to_traverse.
A, B: Type
f: A -> B
l: list A
Map_list A B f l = map f l
  reflexivity.
Qed.

#[export] Instance ToCtxlist_List_Full:
  ToCtxlist nat list := ToCtxlist_Mapdt.

#[export] Instance ToCtxset_List_Full:
  ToCtxset nat list := ToCtxset_Mapdt.

#[export] Instance Compat_ToSubset_ToCtxset_List_Full:
  @Compat_ToSubset_ToCtxset
    nat list ToCtxset_List_Full ToSubset_list.
Compat_ToSubset_ToCtxset nat list
Proof.
Compat_ToSubset_ToCtxset nat list
  apply Compat_ToSubset_ToCtxset_Traverse.
Qed.