Formalizing variadic syntax with Tealeaves

let with no pairwise binding

To illustrate the use of the traversal representation theorem, we consider an example where the syntax has no mutual binding structure.

From Tealeaves Require Export
  Examples.VariadicLet.Terms
  Functors.List_Telescoping.

(*
  Adapters.Compositions.DecoratedTraversableModule.
*)
#[local] Generalizable Variables G A B C.
#[local] Set Implicit Arguments.
#[local] Open Scope nat_scope.

Fixpoint binddt_term
  (G : Type -> Type) `{Map G} `{Pure G} `{Mult G}
  {v1 v2 : Type}
  (f : nat * v1 -> G (term v2))
  (t : term v1) : G (term v2) :=
  match t with
  | tvar v => f (0, v)
  | abs body => pure (@abs v2) <⋆> binddt_term (f ⦿ 1) body
  | letin defs body =>
      pure (@letin v2) <⋆>
        ((fix F ls :=
            match ls with
            | nil => pure nil
            | cons d drest =>
                pure cons <⋆> binddt_term f d <⋆> F drest
            end) defs) <⋆> binddt_term (f ⦿ length defs) body
  | app t1 t2 =>
      pure (@app v2) <⋆> binddt_term f t1 <⋆> binddt_term f t2
  end.

#[export] Instance Binddt_term: Binddt nat term term
  := @binddt_term.

#[export] Instance Map_term: Map term
  := DerivedOperations.Map_Binddt nat term term.
#[export] Instance Mapd_term: Mapd nat term
  := DerivedOperations.Mapd_Binddt nat term term.
#[export] Instance Traverse_term: Traverse term
  := DerivedOperations.Traverse_Binddt nat term term.
#[export] Instance Mapdt_term: Mapdt nat term
  := DerivedOperations.Mapdt_Binddt nat term term.
#[export] Instance Bind_term: Bind term term
  := DerivedOperations.Bind_Binddt nat term term.
#[export] Instance Bindd_term: Bindd nat term term
  := DerivedOperations.Bindd_Binddt nat term term.
#[export] Instance Bindt_term: Bindt term term
  := DerivedOperations.Bindt_Binddt nat term term.
#[export] Instance ToSubset_term: ToSubset term
  := ToSubset_Traverse.
#[export] Instance ToBatch_term: ToBatch term
  := DerivedOperations.ToBatch_Traverse.

Section rewriting.

  Section pointful.

    Context
      `{Applicative G}
      (v1 v2 : Type)
      (f : nat * v1 -> G (term v2)).

    (** ** Rewriting Laws *)
    (******************************************************************************)
    Lemma binddt_term_rw1: forall (v: v1),
        binddt f (tvar v) = f (0, v).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall v : v1, binddt f (tvar v) = f (0, v)
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall v : v1, binddt f (tvar v) = f (0, v)
      reflexivity.
    Qed.

    Lemma binddt_term_rw2: forall (t: term v1),
        binddt f (abs t) =
          pure (@abs v2) <⋆> binddt (f ⦿ 1) t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t : term v1,
binddt f (abs t) =
pure (abs (v:=v2)) <⋆> binddt (f ⦿ 1) t
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t : term v1,
binddt f (abs t) =
pure (abs (v:=v2)) <⋆> binddt (f ⦿ 1) t
      reflexivity.
    Qed.

    Lemma binddt_term_rw3: forall (l : list (term v1)) (body: term v1),
        binddt f (letin l body) =
          pure (@letin v2) <⋆> traverse (binddt f) l <⋆>
            binddt (f ⦿ length l) body.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall (l : list (term v1)) (body : term v1),
binddt f (letin l body) =
pure (letin (v:=v2)) <⋆> traverse (binddt f) l <⋆>
binddt (f ⦿ length l) body
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall (l : list (term v1)) (body : term v1),
binddt f (letin l body) =
pure (letin (v:=v2)) <⋆> traverse (binddt f) l <⋆>
binddt (f ⦿ length l) body
      intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
binddt f (letin l body) =
pure (letin (v:=v2)) <⋆> traverse (binddt f) l <⋆>
binddt (f ⦿ length l) body cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
pure (letin (v:=v2)) <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l <⋆> binddt (f ⦿ length l) body =
pure (letin (v:=v2)) <⋆> traverse (binddt f) l <⋆>
binddt (f ⦿ length l) body
      do 2 fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l = traverse (binddt f) l
      unfold traverse.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
Traverse_list G Map_G Pure_G Mult_G (term v1)
  (term v2) (binddt f) l
      unfold Traverse_list.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
traverse_list G (term v1) (term v2) (binddt f) l
      unfold traverse_list.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
l: list (term v1)
body: term v1
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
(fix traverse_list
   (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A B : Type) (f : A -> G B)
   (l : list A) {struct l} : G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G (term v1) (term v2)
  (binddt f) l
      induction l.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
body: term v1
pure [] = pure []
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
a: term v1
l: list (term v1)
body: term v1
IHl: (fix F (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
(fix traverse_list
   (G : Type -> Type) (H : Map G) 
   (H0 : Pure G) (H1 : Mult G) 
   (A B : Type) (f : A -> G B) 
   (l : list A) {struct l} : 
 G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G 
  (term v1) (term v2) (binddt f) l
pure cons <⋆> binddt f a <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
pure cons <⋆> binddt f a <⋆>
(fix traverse_list
   (G : Type -> Type) (H : Map G) 
   (H0 : Pure G) (H1 : Mult G) 
   (A B : Type) (f : A -> G B) 
   (l : list A) {struct l} : 
 G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G 
  (term v1) (term v2) (binddt f) l
      -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
body: term v1
pure [] = pure [] cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
body: term v1
pure [] = pure []
        reflexivity.
      -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
a: term v1
l: list (term v1)
body: term v1
IHl: (fix F (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
(fix traverse_list
   (G : Type -> Type) (H : Map G) 
   (H0 : Pure G) (H1 : Mult G) 
   (A B : Type) (f : A -> G B) 
   (l : list A) {struct l} : 
 G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G 
  (term v1) (term v2) (binddt f) l
pure cons <⋆> binddt f a <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
pure cons <⋆> binddt f a <⋆>
(fix traverse_list
   (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A B : Type) (f : A -> G B)
   (l : list A) {struct l} : G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G (term v1) (term v2)
  (binddt f) l cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
a: term v1
l: list (term v1)
body: term v1
IHl: (fix F (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
(fix traverse_list
   (G : Type -> Type) (H : Map G) 
   (H0 : Pure G) (H1 : Mult G) 
   (A B : Type) (f : A -> G B) 
   (l : list A) {struct l} : 
 G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G 
  (term v1) (term v2) (binddt f) l
pure cons <⋆> binddt f a <⋆>
(fix F (ls : list (term v1)) : G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
pure cons <⋆> binddt f a <⋆>
(fix traverse_list
   (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A B : Type) (f : A -> G B)
   (l : list A) {struct l} : G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G (term v1) (term v2)
  (binddt f) l
        rewrite IHl.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
a: term v1
l: list (term v1)
body: term v1
IHl: (fix F (ls : list (term v1)) :
     G (list (term v2)) :=
   match ls with
   | [] => pure []
   | d :: drest =>
       pure cons <⋆> binddt f d <⋆> F drest
   end) l =
(fix traverse_list
   (G : Type -> Type) (H : Map G) 
   (H0 : Pure G) (H1 : Mult G) 
   (A B : Type) (f : A -> G B) 
   (l : list A) {struct l} : 
 G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G 
  (term v1) (term v2) (binddt f) l
pure cons <⋆> binddt f a <⋆>
(fix traverse_list
   (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A B : Type) (f : A -> G B)
   (l : list A) {struct l} : G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G (term v1) (term v2)
  (binddt f) l =
pure cons <⋆> binddt f a <⋆>
(fix traverse_list
   (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A B : Type) (f : A -> G B)
   (l : list A) {struct l} : G (list B) :=
   match l with
   | [] => pure []
   | x :: xs =>
       pure cons <⋆> f x <⋆>
       traverse_list G H H0 H1 A B f xs
   end) G Map_G Pure_G Mult_G (term v1) (term v2)
  (binddt f) l
        reflexivity.
    Qed.

    Lemma binddt_term_rw4: forall (t1 t2: term v1),
        binddt f (app t1 t2) =
          pure (@app v2) <⋆> binddt f t1 <⋆> binddt f t2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t1 t2 : term v1,
binddt f (app t1 t2) =
pure (app (v:=v2)) <⋆> binddt f t1 <⋆> binddt f t2
    Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
v1, v2: Type
f: nat * v1 -> G (term v2)
forall t1 t2 : term v1,
binddt f (app t1 t2) =
pure (app (v:=v2)) <⋆> binddt f t1 <⋆> binddt f t2
      reflexivity.
    Qed.

  End pointful.

  (** ** Point-free Rewriting Laws *)
  (******************************************************************************)
  Section pointfree.

    Context
      `{Applicative G2}
      {B C: Type}
      (g : nat * B -> G2 (term C)).

    Lemma binddt_pointfree_letin_defs: forall l,
        binddt g ∘ letin (v:=B) l =
          (precompose (binddt (g ⦿ length l)) ∘ ap G2)
            (pure (letin (v:=C)) <⋆> (traverse (binddt g) l)).G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall l : list (term B),
binddt g ∘ letin l =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> traverse (binddt g) l)
    Proof.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall l : list (term B),
binddt g ∘ letin l =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> traverse (binddt g) l)
      intros l.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
binddt g ∘ letin l =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> traverse (binddt g) l)
      ext body.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
body: term B
(binddt g ∘ letin l) body =
(precompose (binddt (g ⦿ length l)) ∘ ap G2)
  (pure (letin (v:=C)) <⋆> traverse (binddt g) l) body
      unfold precompose, compose.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
body: term B
binddt g (letin l body) =
pure (letin (v:=C)) <⋆> traverse (binddt g) l <⋆>
binddt (g ⦿ length l) body
      rewrite binddt_term_rw3.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
l: list (term B)
body: term B
pure (letin (v:=C)) <⋆> traverse (binddt g) l <⋆>
binddt (g ⦿ length l) body =
pure (letin (v:=C)) <⋆> traverse (binddt g) l <⋆>
binddt (g ⦿ length l) body
      reflexivity.
    Qed.

    Lemma binddt_pointfree_letin: forall `(l:list A),
        compose (binddt g) ∘ letin (v := B) ∘ trav_make (T := list) l (B := term B) =
          ((compose (precompose (binddt (g ⦿ length l)) ∘ ap G2) ∘
              precompose (traverse (T := list) (binddt g)) ∘
              ap G2 ∘ pure (F := G2)) (letin (v:=C))) ∘ trav_make l (B := term B).G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall (A : Type) (l : list A),
compose (binddt g) ∘ letin (v:=B) ∘ trav_make l =
(compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (traverse (binddt g)) ∘ ap G2 ∘ pure)
  (letin (v:=C)) ∘ trav_make l
    Proof.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
forall (A : Type) (l : list A),
compose (binddt g) ∘ letin (v:=B) ∘ trav_make l =
(compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (traverse (binddt g)) ∘ ap G2 ∘ pure)
  (letin (v:=C)) ∘ trav_make l
      intros A l.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
compose (binddt g) ∘ letin (v:=B) ∘ trav_make l =
(compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
 ∘ precompose (traverse (binddt g)) ∘ ap G2 ∘ pure)
  (letin (v:=C)) ∘ trav_make l
      ext l' body.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
(compose (binddt g) ∘ letin (v:=B) ∘ trav_make l) l'
  body =
((compose (precompose (binddt (g ⦿ length l)) ∘ ap G2)
  ∘ precompose (traverse (binddt g)) ∘ ap G2 ∘ pure)
   (letin (v:=C)) ∘ trav_make l) l' body
      unfold precompose, compose.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
binddt g (letin (trav_make l l') body) =
pure (letin (v:=C)) <⋆>
traverse (binddt g) (trav_make l l') <⋆>
binddt (g ⦿ length l) body
      rewrite binddt_term_rw3.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
pure (letin (v:=C)) <⋆>
traverse (binddt g) (trav_make l l') <⋆>
binddt (g ⦿ length (trav_make l l')) body =
pure (letin (v:=C)) <⋆>
traverse (binddt g) (trav_make l l') <⋆>
binddt (g ⦿ length l) body
      do 2 rewrite <- list_plength_length.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
pure (letin (v:=C)) <⋆>
traverse (binddt g) (trav_make l l') <⋆>
binddt (g ⦿ plength (trav_make l l')) body =
pure (letin (v:=C)) <⋆>
traverse (binddt g) (trav_make l l') <⋆>
binddt (g ⦿ plength l) body
      rewrite <- plength_trav_make.G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
B, C: Type
g: nat * B -> G2 (term C)
A: Type
l: list A
l': Vector (plength l) (term B)
body: term B
pure (letin (v:=C)) <⋆>
traverse (binddt g) (trav_make l l') <⋆>
binddt (g ⦿ plength l) body =
pure (letin (v:=C)) <⋆>
traverse (binddt g) (trav_make l l') <⋆>
binddt (g ⦿ plength l) body
      reflexivity.
    Qed.

  End pointfree.

End rewriting.

Ltac simplify_binddt_letin :=
  ltac_trace "simplify_binddt_letin";
  match goal with
  | |- context[binddt ?f (tvar ?y)] =>
      rewrite binddt_term_rw1
  | |- context[((binddt ?f) (abs ?body))] =>
      rewrite binddt_term_rw2
  | |- context[((binddt ?f) (letin ?l ?body))] =>
      rewrite binddt_term_rw3
  | |- context[((binddt ?f) (app ?t1 ?t2))] =>
      rewrite binddt_term_rw4
  end.

Ltac cbn_binddt ::=
  simplify_binddt_letin.

DTM laws

Theorem dtm1_term:
  forall `{Applicative G} (A B : Type),
  forall f : nat * A -> G (term B),
    binddt f ∘ ret  = f ∘ ret (T := (nat ×)).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 (term B)),
binddt f ∘ ret = f ∘ ret
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 (term B)),
binddt f ∘ ret = f ∘ ret
  reflexivity.
Qed.

Theorem dtm2_term : forall A : Type,
    binddt (T := term) (U := term)
      (G := fun A => A) (ret (T := term) ∘ extract (W := (nat ×))) = @id (term A).forall A : Type, binddt (ret ∘ extract) = id
Proof.forall A : Type, binddt (ret ∘ extract) = id
  derive_dtm2.A: Type
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs -> binddt (ret ∘ extract) t = t
IHt: binddt (ret ∘ extract) t = t
traverse (binddt (ret ∘ extract)) defs = defs
  apply traverse_respectful_id; auto.
Qed.

Theorem dtm3_term:
  forall `{Applicative G1} `{Applicative G2},
  forall `(g : nat * B -> G2 (term C)) `(f : nat * A -> G1 (term B)),
    map (binddt g) ∘ binddt f = binddt (G := G1 ∘ G2) (g ⋆7 f).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 (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
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 (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
  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
B, C: Type
g: nat * B -> G2 (term C)
A: Type
f: nat * A -> G1 (term B)
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
  derive_dtm3.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure (compose (binddt g) ∘ letin (v:=B)) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
  (* TODO investigate how to stop ^^^ from unfold Pure_compose in traverse *)
  progress binddt_typeclass_normalize.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure (compose (binddt g) ∘ letin (v:=B)) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
  (* ^ Hence necessity to repair the damage so rewrite <- IHdefs' works below *)
  { (* left hand side *)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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure (compose (binddt g) ∘ letin (v:=B)) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    rewrite traverse_repr 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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure (compose (binddt g) ∘ letin (v:=B)) <⋆>
map (trav_make defs)
  (forwards
     (traverse (mkBackwards ∘ binddt f)
        (trav_contents defs))) <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    dtm3_push_map_right_to_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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure
  (precompose (trav_make defs)
     (compose (binddt g) ∘ letin (v:=B))) <⋆>
forwards
  (traverse (mkBackwards ∘ binddt f)
     (trav_contents defs)) <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    repeat change (precompose ?f ?g) with (g ∘ f).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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure
  (compose (binddt g) ∘ letin (v:=B) ∘ trav_make defs) <⋆>
forwards
  (traverse (mkBackwards ∘ binddt f)
     (trav_contents defs)) <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    rewrite binddt_pointfree_letin.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C)) ∘ 
   trav_make defs) <⋆>
forwards
  (traverse (mkBackwards ∘ binddt f)
     (trav_contents defs)) <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    change (?g ∘ ?trav_make defs) with (precompose (trav_make defs) g).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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure
  (precompose (trav_make defs)
     ((compose
         (precompose (binddt (g ⦿ length defs))
          ∘ ap G2) ∘ precompose (traverse (binddt g))
       ∘ ap G2 ∘ pure) (letin (v:=C)))) <⋆>
forwards
  (traverse (mkBackwards ∘ binddt f)
     (trav_contents defs)) <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    rewrite <- app_pure_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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
map (precompose (trav_make defs))
  (pure
     ((compose
         (precompose (binddt (g ⦿ length defs))
          ∘ ap G2) ∘ precompose (traverse (binddt g))
       ∘ ap G2 ∘ pure) (letin (v:=C)))) <⋆>
forwards
  (traverse (mkBackwards ∘ binddt f)
     (trav_contents defs)) <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    rewrite ap_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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
map (trav_make defs)
  (forwards
     (traverse (mkBackwards ∘ binddt f)
        (trav_contents defs))) <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    rewrite <- traverse_repr.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    (* right hand side *)
    assert (IHdefs':
             traverse (G := G1 ∘ G2) (map (binddt g) ∘ binddt f) defs =
               traverse (G := G1 ∘ G2)
                 (binddt (G := G1 ∘ G2) (g ⋆7 f)) defs).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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    {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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs apply traverse_respectful; try typeclasses eauto.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
forall a : term A,
a ∈ defs ->
(map (binddt g) ∘ binddt f) a = binddt (g ⋆7 f) a
      intros t' t'_in.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
t': term A
t'_in: t' ∈ defs
(map (binddt g) ∘ binddt f) t' = binddt (g ⋆7 f) t'
      unfold compose 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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
t': term A
t'_in: t' ∈ defs
map (binddt g) (binddt f t') = binddt (g ⋆7 f) t'
      apply (IHdefs t' t'_in g f). }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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt (g ⋆7 f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    rewrite <- IHdefs'.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (map (binddt g) ∘ binddt f) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    change (map ?g ∘ ?f) with (g ⋆2 f).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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
traverse (binddt g ⋆2 binddt f) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    rewrite <- trf_traverse_traverse.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
(map (traverse (binddt g)) ∘ traverse (binddt f)) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    change ((?g ∘ ?f) defs) with (g (f defs)).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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure (pure (letin (v:=C))) <⋆>
map (traverse (binddt g)) (traverse (binddt f) defs) <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    dtm3_rhs_one_constructor.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure
  (precompose (traverse (binddt g))
     (ap G2 (pure (letin (v:=C))))) <⋆>
traverse (binddt f) defs <⋆>
map (binddt (g ⦿ length defs))
  (binddt (f ⦿ length defs) t)
    dtm3_rhs_one_constructor.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
B, C, A: Type
H1: Functor G2
H2: Functor G1
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) =
binddt (g ⋆7 f) t
IHt: forall (g : nat * B -> G2 (term C))
  (f : nat * A -> G1 (term B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (term C)
f: nat * A -> G1 (term B)
IHdefs': traverse (map (binddt g) ∘ binddt f) defs =
traverse (binddt (g ⋆7 f)) defs
pure
  ((compose
      (precompose (binddt (g ⦿ length defs)) ∘ ap G2)
    ∘ precompose (traverse (binddt g)) ∘ 
    ap G2 ∘ pure) (letin (v:=C))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t =
pure
  (precompose (binddt (g ⦿ length defs))
   ∘ (ap G2
      ∘ precompose (traverse (binddt g))
          (ap G2 (pure (letin (v:=C)))))) <⋆>
traverse (binddt f) defs <⋆>
binddt (f ⦿ length defs) t
    reflexivity.
  }
Qed.

Theorem dtm4_term :
  forall (G1 G2 : Type -> Type)
    (H1 : Map G1) (H2 : Mult G1) (H3 : Pure G1)
    (H4 : Map G2) (H5 : Mult G2) (H6 : Pure G2)
    (ϕ : forall A : Type, G1 A -> G2 A),
    ApplicativeMorphism G1 G2 ϕ ->
    forall (A B : Type) (f : nat * A -> G1 (term B)),
      ϕ (term B) ∘ binddt f = binddt (ϕ (term B) ∘ f).forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H2 : Mult G1) (H3 : Pure G1) (H4 : Map G2)
  (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (term B)),
ϕ (term B) ∘ binddt f = binddt (ϕ (term B) ∘ f)
Proof.forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H2 : Mult G1) (H3 : Pure G1) (H4 : Map G2)
  (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (term B)),
ϕ (term B) ∘ binddt f = binddt (ϕ (term B) ∘ f)
  intros.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 (term B)
ϕ (term B) ∘ binddt f = binddt (ϕ (term B) ∘ f)
  derive_dtm4.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
ϕ (list (term B)) (traverse (binddt f) defs) =
traverse (binddt (ϕ (term B) ∘ f)) defs
  compose near defs on left.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
(ϕ (list (term B)) ∘ traverse (binddt f)) defs =
traverse (binddt (ϕ (term B) ∘ f)) defs
  rewrite (trf_traverse_morphism).G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
traverse (ϕ (term B) ∘ binddt f) defs =
traverse (binddt (ϕ (term B) ∘ f)) defs
  apply traverse_respectful.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
forall a : term A,
a ∈ defs ->
(ϕ (term B) ∘ binddt f) a = binddt (ϕ (term B) ∘ f) a
  unfold compose.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
forall a : term A,
a ∈ defs ->
ϕ (term B) (binddt f a) = binddt (ϕ (term B) ○ f) a
  intros t' t'_in.G1, G2: Type -> Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A, B: Type
H0: Applicative G1
H7: Functor G1
H8: Applicative G2
H9: Functor G2
defs: list (term A)
t: term A
IHdefs: forall t : term A,
t ∈ defs ->
forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
IHt: forall f : nat * A -> G1 (term B),
ϕ (term B) (binddt f t) =
binddt (ϕ (term B) ∘ f) t
f: nat * A -> G1 (term B)
t': term A
t'_in: t' ∈ defs
ϕ (term B) (binddt f t') = binddt (ϕ (term B) ○ f) t'
  apply (IHdefs t' t'_in f).
Qed.

#[export] Instance DTM_LetIn: DecoratedTraversableMonad nat term.DecoratedTraversableMonad nat term
Proof.DecoratedTraversableMonad nat term
  constructor.Monoid nat
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 (term B)),
binddt f ∘ ret = f ∘ ret
DecoratedTraversableRightPreModule nat term term
  -Monoid nat typeclasses eauto.
  -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 (term B)),
binddt f ∘ ret = f ∘ ret 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 (term B)
binddt f ∘ ret = f ∘ ret apply dtm1_term.
  -DecoratedTraversableRightPreModule nat term term constructor.forall A : Type, binddt (ret ∘ extract) = id
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 (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 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 : nat * A -> G1 (term B)),
ϕ (term B) ∘ binddt f = binddt (ϕ (term B) ∘ f)
    +forall A : Type, binddt (ret ∘ extract) = id apply dtm2_term.
    +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 (B C : Type) (g : nat * B -> G2 (term C))
  (A : Type) (f : nat * A -> G1 (term B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 f) 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
B, C: Type
g: nat * B -> G2 (term C)
A: Type
f: nat * A -> G1 (term B)
map (binddt g) ∘ binddt f = binddt (g ⋆7 f) apply dtm3_term.
    +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 : nat * A -> G1 (term B)),
ϕ (term B) ∘ binddt f = binddt (ϕ (term B) ∘ f) apply dtm4_term.
Qed.