Tealeaves.Examples.LambdaNominal.Categorical

(*|
#################### Lambda Calculus With Nominal Variables ####################
|*)

From Tealeaves Require Export
  Examples.LambdaNominal.Syntax
  Classes.Categorical.DecoratedMonad (shift).

From Tealeaves Require
  Classes.Categorical.DecoratedTraversableMonadPoly.

Import List.ListNotations.

#[local] Generalizable Variables G.

(*|
***********************************************
Bifunctor Instance
***********************************************
|*)

Fixpoint map2_term {B1 V1 B2 V2: Type}
  (ρ: B1 → B2) (σ: V1 → V2)
  (t: term B1 V1): term B2 V2 :=
  match t with
  | tvar v ⇒ (@tvar B2 V2) (σ v)
  | lam v body ⇒ lam (ρ v) (map2_term ρ σ body)
  | tap t1 t2 ⇒ tap (map2_term ρ σ t1) (map2_term ρ σ t2)
  end.

Lemma map2_id_term: ∀ (B1 V1: Type),
    map2_term (@id B1) (@id V1) = @id (term B1 V1).
Proof.
  intros. ext t. induction t.
  - reflexivity.
  - cbn. now rewrite IHt.
  - cbn. now rewrite IHt1, IHt2.
Qed.

Lemma map2_map2_term:
  ∀ (B1 V1 B2 V2 b3 v3: Type)
    (ρ1: B1 → B2) (σ1: V1 → V2) (ρ2: B2 → b3) (σ2: V2 → v3),
    map2_term ρ2 σ2 ∘ map2_term ρ1 σ1 = map2_term (ρ2 ∘ ρ1) (σ2 ∘ σ1).
Proof.
  intros. ext t. induction t.
  - reflexivity.
  - cbn. compose near t on left. now rewrite IHt.
  - cbn.
    compose near t1 on left. rewrite IHt1.
    compose near t2 on left. rewrite IHt2.
    reflexivity.
Qed.

#[export] Instance Map2_term: Map2 term.
Proof.
  intros A1 B1 A2 B2 f1 f2.
  apply (map2_term f1 f2).
Defined.

(*|
Rewriting Principles
========================
|*)

Section map_term_rewriting.

  Context
    {B1 V1 B2 V2: Type}
    (ρ: B1 → B2)
    (σ: V1 → V2).

  Lemma map2_term_rw1: ∀ (v: V1),
      map2 ρ σ (tvar (B := B1) v) = tvar (σ v).
  Proof.
    reflexivity.
  Qed.

  Lemma map2_term_rw2: ∀ (b: B1) (body: term B1 V1),
      map2 ρ σ (lam b body) = lam (ρ b) (map2 ρ σ body).
  Proof.
    reflexivity.
  Qed.

  Lemma map2_term_rw3: ∀ (t1 t2: term B1 V1),
      map2 ρ σ (tap t1 t2) = tap (map2 ρ σ t1) (map2 ρ σ t2).
  Proof.
    reflexivity.
  Qed.

End map_term_rewriting.

(*|
Functor Laws
=====================
|*)

#[export] Instance Functor2_term: Functor2 term.
Proof.
  constructor.
  - intros. ext t. induction t.
    + reflexivity.
    + rewrite map2_term_rw2.
      now rewrite IHt.
    + rewrite map2_term_rw3.
      rewrite IHt1.
      rewrite IHt2.
      reflexivity.
  - intros. unfold compose. ext t.
    induction t.
    + reflexivity.
    + rewrite map2_term_rw2.
      rewrite map2_term_rw2.
      rewrite IHt.
      reflexivity.
    + rewrite map2_term_rw3.
      rewrite map2_term_rw3.
      rewrite IHt1.
      rewrite IHt2.
      reflexivity.
Qed.

(*|
***********************************************
Polymorphic Decoration
***********************************************
|*)

Fixpoint dec2_term_rec {B V: Type} (ctx: list B)
  (t: term B V): term (list B × B) (list B × V) :=
  match t with
  | tvar v ⇒ tvar (ctx, v)
  | lam b body ⇒ lam (ctx, b) (dec2_term_rec (ctx ++ [b]) body)
  | tap t1 t2 ⇒ tap (dec2_term_rec ctx t1) (dec2_term_rec ctx t2)
  end.

Definition dec2_term {B V: Type}:
  term B V →
  term (list B × B) (list B × V) :=
  dec2_term_rec nil.

#[export] Instance DecoratePoly_term: DecoratePoly term := @dec2_term.

(*|
The ``shift2`` operation
==========================
|*)

Lemma dec2_term_rec_app_shift {B V: Type}:
  ∀ (ctx1 ctx2: list B) (t: term B V),
    dec2_term_rec (ctx1 ++ ctx2) t =
      shift2 (ctx1, dec2_term_rec ctx2 t).
Proof.
  intros.
  generalize dependent ctx1.
  generalize dependent ctx2.
  induction t; intros.
  - cbn.
    reflexivity.
  - cbn.
    rewrite <- List.app_assoc.
    rewrite IHt.
    reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite IHt2.
    reflexivity.
Qed.

Lemma dec2_term_rec_shift {B V: Type}:
  ∀ (ctx: list B) (t: term B V),
    dec2_term_rec ctx t =
      shift2 (ctx, dec2_term t).
Proof.
  intros.
  rewrite <- (List.app_nil_r ctx) at 1.
  rewrite dec2_term_rec_app_shift.
  reflexivity.
Qed.

(*|
Rewriting Principles
=======================
|*)

Section dec2_term_rewriting.

  Context (B V: Type) (ctx: list B).

  Lemma dec2_term_rec_rw1: ∀ (v: V),
      dec2_term_rec ctx (tvar v) = tvar (ctx, v).
  Proof.
    reflexivity.
  Qed.

  Lemma dec2_term_rec_rw2: ∀ (b: B) (body: term B V),
      dec2_term_rec ctx (lam b body) =
        lam (ctx, b) (dec2_term_rec (ctx ++ [b]) body).
  Proof.
    reflexivity.
  Qed.

  Lemma dec2_term_rec_rw3: ∀ (t1 t2: term B V),
      dec2_term_rec ctx (tap t1 t2) =
        tap (dec2_term_rec ctx t1) (dec2_term_rec ctx t2).
  Proof.
    reflexivity.
  Qed.

  Lemma dec2_term_rw1: ∀ (v: V),
      decp (tvar (B := B) v) = tvar ([], v).
  Proof.
    cbn.
    reflexivity.
  Qed.

  Lemma dec2_term_rw2: ∀ (b: B) (body: term B V),
      decp (lam b body) = lam ([], b) (shift2 ([b], decp body)).
  Proof.
    intros. cbn.
    rewrite dec2_term_rec_shift.
    reflexivity.
  Qed.

  Lemma dec2_term_rw2': ∀ (b: B) (body: term B V),
      decp (lam b body) = lam ([], b) (dec2_term_rec [b] body).
  Proof.
    reflexivity.
  Qed.

  Lemma dec2_term_rw3: ∀ (t1 t2: term B V),
      decp (tap t1 t2) = tap (decp t1) (decp t2).
  Proof.
    reflexivity.
  Qed.

End dec2_term_rewriting.

(*|
Decoration Laws
=======================

Naturality
-----------------------
|*)

Lemma map_dec2_rec_spec:
  ∀ (B1 V1 B2 V2: Type)
    (ρ: list B1 × B1 → B2) (σ: list B1 × V1 → V2) (ctx: list B1),
    map2 ρ σ ∘ dec2_term_rec ctx =
      map2 (ρ ⦿ ctx) (σ ⦿ ctx) ∘ dec2_term.
Proof.
  intros. ext t. unfold compose.
  generalize dependent ctx.
  generalize dependent σ.
  generalize dependent ρ.
  induction t; intros ρ σ ctx.
  - cbn. unfold preincr, compose, incr.
    change (@nil B1) with (Ƶ: list B1).
    rewrite monoid_id_r.
    reflexivity.
  - cbn.
    rewrite IHt.
    rewrite IHt.
    fequal.
    + unfold preincr, incr, compose, monoid_op, Monoid_op_list.
      rewrite List.app_nil_r.
      reflexivity.
    + rewrite preincr_preincr.
      rewrite preincr_preincr.
      reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite IHt2.
    reflexivity.
Qed.

Lemma dec2_rec_spec:
  ∀ (B V: Type) (ctx: list B),
    dec2_term_rec ctx =
      map2 (incr ctx) (incr ctx) ∘ dec2_term (V := V).
Proof.
  intros.
  change_left (id ∘ dec2_term_rec ctx (V := V)).
  rewrite <- fun2_map_id.
  rewrite map_dec2_rec_spec.
  reflexivity.
Qed.

Section naturality.

  Context {B1 V1 B2 V2: Type}
    (ρ: B1 → B2) (σ: V1 → V2).

  Lemma dec2_rec_map: ∀ (ctx: list B1),
      dec2_term_rec (map ρ ctx) ∘ map2 ρ σ =
        map2 (map_pair (map (F := list) ρ) ρ)
          (map_pair (map (F := list) ρ) σ) ∘ dec2_term_rec ctx.
  Proof.
    intros. ext t. unfold compose.
    generalize dependent ρ; clear ρ.
    generalize dependent σ; clear σ.
    generalize dependent ctx.
    induction t as [v | b body IHbody | t1 IHt1 t2 IHt2];
      intros.
    - reflexivity.
    - cbn.
      fequal.
      replace (map ρ ctx ++ [ρ b])
        with (map ρ (ctx ++ [b])) by now rewrite map_list_app.
      rewrite IHbody.
      reflexivity.
    - cbn.
      rewrite IHt1.
      rewrite IHt2.
      reflexivity.
  Qed.

  Lemma dec_map:
    dec2_term ∘ map2 ρ σ =
      map2 (map_pair (map (F := list) ρ) ρ)
        (map_pair (map (F := list) ρ) σ) ∘ dec2_term.
  Proof.
    unfold dec2_term.
    change (@nil B2) with (map ρ nil).
    rewrite dec2_rec_map.
    reflexivity.
  Qed.

End naturality.

(*|
Counit Law
-----------------------
|*)

Lemma dec2_rec_extract_term: ∀ (B V: Type) (ctx: list B),
    map2 (extract_L) (extract_L) ∘ dec2_term_rec ctx = @id (term B V).
Proof.
  intros. ext t. unfold compose.
  generalize dependent ctx. induction t; intro ctx.
  - reflexivity.
  - cbn. now rewrite IHt.
  - cbn. now rewrite IHt1, IHt2.
Qed.

Lemma dec_extract_term: ∀ (B V: Type),
    map2 (extract_L) (extract_L) ∘ dec2_term = @id (term B V).
Proof.
  intros. unfold dec2_term. apply dec2_rec_extract_term.
Qed.

(*|
Cojoin Law
-----------------------
|*)

Lemma dec2_rec_dec2_rec_term: ∀ (B V: Type) (ctx: list B),
    dec2_term_rec (decorate_prefix_list ctx) ∘ dec2_term_rec ctx =
      map2 (cojoin_L) (cojoin_L) ∘ dec2_term_rec ctx (B := B) (V := V).
Proof.
  intros. ext t. unfold compose.
  generalize dependent ctx.
  induction t; intro ctx.
  - reflexivity.
  - cbn.
    rewrite <- IHt.
    rewrite decorate_prefix_list_rw_app.
    cbn. change (@nil B) with (Ƶ: list B).
    rewrite monoid_id_r.
    reflexivity.
  - cbn. now rewrite IHt1, IHt2.
Qed.

Lemma dec_dec2_term: ∀ (B V: Type),
    dec2_term ∘ dec2_term (B := B) (V := V) =
      map2 (cojoin_L) (cojoin_L) ∘ dec2_term.
Proof.
  intros. unfold dec2_term.
  change (@nil (list B × B)) with (decorate_prefix_list (@nil B)).
  apply dec2_rec_dec2_rec_term.
Qed.

(*|
Typeclass Instance
====================
|*)

#[export] Instance: DecoratedFunctorPoly term.
Proof.
  constructor.
  - typeclasses eauto.
  - unfold PolyDecorateNatural.
    intros.
    setoid_rewrite dec_map.
    fequal.
    fequal.
    now ext [ctx a].
  - intros.
    rewrite dec_dec2_term.
    reflexivity.
  - intros.
    rewrite dec_extract_term.
    reflexivity.
Qed.

(*|
***********************************************
Applicative distribution
***********************************************
|*)

Fixpoint dist2_term
  {G: Type → Type} `{Map G} `{Pure G} `{Mult G}
  {B V: Type}
  (t: term (G B) (G V)): G (term B V) :=
  match t with
  | tvar vr ⇒ map (@tvar B V) vr
  | lam bin body ⇒ pure (@lam B V)
                   <⋆> bin
                   <⋆> dist2_term body
  | tap t1 t2 ⇒ pure (@tap B V)
                <⋆> dist2_term t1
                <⋆> dist2_term t2
  end.

#[export] Instance term_dist2: ApplicativeDist2 term := @dist2_term.

(*|
Distribution Laws
============================

Applicative Homomorphisms
----------------------------
|*)

Lemma dist2_term_morph:
  ∀ (G1 G2: Type → Type)
    `{Map G1} `{Mult G1} `{Pure G1}
    `{Map G2} `{Mult G2} `{Pure G2}
    (ϕ: ∀ (A: Type), G1 A → G2 A),
    ApplicativeMorphism G1 G2 ϕ →
    ∀ (B V: Type),
      dist2 (G := G2) ∘ map2 (ϕ B) (ϕ V) =

        ϕ (term B V) ∘ dist2 (G := G1) (B := B) (A := V).
Proof.
  intros. ext t. unfold compose.
  induction t.
  - cbn.
    rewrite appmor_natural.
    reflexivity.
  - cbn.
    rewrite IHt.
    rewrite ap_morphism_1.
    rewrite ap_morphism_1.
    rewrite appmor_pure.
    reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite IHt2.
    rewrite ap_morphism_1.
    rewrite ap_morphism_1.
    rewrite appmor_pure.
    reflexivity.
Qed.

(*|
Identity Applicative
----------------------------
|*)

Lemma dist2_term_identity:
  ∀ (B V: Type),
    dist2_term (G := fun A ⇒ A) (B := B) (V := V) = @id (term B V).
Proof.
  intros. ext t. unfold id. induction t.
  reflexivity.
  cbn. rewrite IHt. reflexivity.
  cbn. rewrite IHt1, IHt2. reflexivity.
Qed.

(*|
Linearity
----------------------------
|*)

Lemma dist2_term_linear:
  ∀ (G1 G2: Type → Type)
    `{Map G1} `{Mult G1} `{Pure G1} `{! Applicative G1}
    `{Map G2} `{Mult G2} `{Pure G2} `{! Applicative G2},
  ∀ (B V: Type),
    dist2 (G := G1 ∘ G2) =
    map (F := G1) (dist2 (G := G2)) ∘
      dist2 (T := term) (G := G1) (B := G2 B) (A := G2 V).
Proof.
  intros. ext t. unfold compose at 4.
  induction t.
  - cbn. compose near v on right.
    rewrite fun_map_map.
    reflexivity.
  - cbn.
    rewrite IHt.
    unfold_ops @Pure_compose.
    rewrite (ap_compose2 G2 G1).
    rewrite (ap_compose2 G2 G1).
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite app_pure_natural.
    rewrite <- ap_map.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite IHt2.
    unfold_ops @Pure_compose.
    rewrite (ap_compose2 G2 G1).
    rewrite (ap_compose2 G2 G1).
    rewrite map_ap.
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite app_pure_natural.
    rewrite app_pure_natural.
    rewrite <- ap_map.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite <- ap_map.
    rewrite app_pure_natural.
    reflexivity.
Qed.

(*|
Naturality
----------------------------
|*)

Section naturality.

  Context {B1 V1 B2 V2: Type}
    (ρ: B1 → B2) (σ: V1 → V2).

  Lemma dist_map `{Applicative G}:
    map (map2 ρ σ) ∘ dist2_term (G := G) =
      dist2_term ∘ map2 (map ρ) (map σ).
  Proof.
    intros. ext t. unfold compose.
    induction t as [v | b body IHbody | t1 IHt1 t2 IHt2];
      change (@nil B2) with (map ρ nil).
    - cbn.
      compose near v on left.
      rewrite fun_map_map.
      compose near v on right.
      rewrite fun_map_map.
      reflexivity.
    - cbn.
      rewrite map_ap.
      rewrite map_ap.
      rewrite app_pure_natural.
      rewrite <- ap_map.
      rewrite app_pure_natural.
      rewrite <- IHbody.
      rewrite <- ap_map.
      rewrite map_ap.
      rewrite app_pure_natural.
      reflexivity.
    - cbn.
      rewrite map_ap.
      rewrite map_ap.
      rewrite app_pure_natural.
      rewrite <- IHt1.
      rewrite <- ap_map.
      rewrite app_pure_natural.
      rewrite <- IHt2.
      rewrite <- ap_map.
      rewrite map_ap.
      rewrite app_pure_natural.
      reflexivity.
  Qed.
End naturality.

#[export] Instance Natural_dist2_term:
  ∀ (G: Type → Type) (Map_G: Map G) (Pure_G: Pure G) (Mult_G: Mult G),
    Applicative G → Natural2 (@dist2 term term_dist2 G Map_G Pure_G Mult_G).
Proof.
  intros.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - intros. apply dist_map.
    auto.
Qed.

(*|
Typeclass Instance
============================
|*)

#[export] Instance TraversableFunctor2_term: TraversableFunctor2 term.
Proof.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - apply dist2_term_morph.
  - apply dist2_term_identity.
  - intros. apply dist2_term_linear; auto.
Qed.

(*|
***********************************************
Monad
***********************************************
|*)

Fixpoint join_term {B V: Type} (t: term B (term B V)): term B V :=
  match t with
  | tvar v ⇒ v
  | lam b body ⇒ lam b (join_term body)
  | tap t1 t2 ⇒ tap (join_term t1) (join_term t2)
  end.

#[export] Instance Join_lambda_term: ∀ B, Join (term B) :=
  @join_term.

(*|
Rewriting Principles
============================
|*)

Section join_term_rewriting.

  Context (B V: Type).

  Lemma join_term_rw1: ∀ (v: term B V),
      join (tvar (B := B) v) = v.
  Proof.
    reflexivity.
  Qed.

  Lemma join_term_rw2: ∀ (b: B) (body: term B (term B V)),
      join (lam b body) = lam b (join body).
  Proof.
    reflexivity.
  Qed.

  Lemma join_term_rw3: ∀ (t1 t2: term B (term B V)),
      join (tap t1 t2) = tap (join t1) (join t2).
  Proof.
    reflexivity.
  Qed.

End join_term_rewriting.

(*|
Monad Laws
============================
|*)

(*|
Left Unit Law
--------------------
|*)

Lemma join_ret_term {B V: Type}:
  join_term ∘ ret (A := term B V) = @id (term B V).
Proof.
  reflexivity.
Qed.

(*|
Right Unit Law
--------------------
|*)

Lemma join_map_ret_term {B V: Type}:
  join_term ∘ map2 (@id B) (ret (A := V)) = @id (term B V).
Proof.
  ext t. unfold compose. induction t.
  - reflexivity.
  - cbn. rewrite IHt. reflexivity.
  - cbn. rewrite IHt1, IHt2. reflexivity.
Qed.

(*|
Associativity Law
--------------------
|*)

Lemma join_join_term {B V: Type}:
  join_term ∘ join_term (B := B) (V := term B V) =
    join_term ∘ map2 id (join_term).
Proof.
  intros. ext t.
  unfold compose.
  induction t as [v | b body IHbody | t1 IHt1 t2 IHt2].
  - reflexivity.
  - cbn.
    rewrite IHbody.
    reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite IHt2.
    reflexivity.
Qed.

(*|
Naturality
--------------------
|*)

Section naturality.

  Context {B1 V1 B2 V2: Type}
    (ρ: B1 → B2) (σ: V1 → V2).

  Lemma join_map:
    join (T := term B2) ∘ map2 ρ (map2 ρ σ) =
      map2 ρ σ ∘ (join (T := term B1) (A := V1)).
  Proof.
    ext t. unfold compose.
    induction t as [v | b body IHbody | t1 IHt1 t2 IHt2].
    - reflexivity.
    - cbn.
      rewrite IHbody.
      reflexivity.
    - cbn.
      rewrite IHt1.
      rewrite IHt2.
      reflexivity.
  Qed.

End naturality.

(*|
Typeclass Instance
=====================
|*)

#[export] Instance Monad_term: ∀ B, Monad (term B).
Proof.
  constructor.
  - typeclasses eauto.
  - constructor; try typeclasses eauto.
    intros. reflexivity.
  - constructor; try typeclasses eauto.
    intros. unfold map, Map2_1.
    rewrite <- join_map.
    reflexivity.
  - intros. reflexivity.
  - intros. unfold map, Map2_1.
    apply join_map_ret_term.
  - intros. unfold map, Map2_1.
    apply join_join_term.
Qed.

#[export] Instance Monad2_term: Monad2 term.
Proof.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - reflexivity.
  - intros.
    intros. unfold map, Map2_1.
    rewrite <- join_map.
    reflexivity.
Qed.

(*|
***********************************************
Relating Decoration and Traversal
***********************************************
|*)

Lemma dist_dec2_rec_commute:
  ∀ (B V: Type)
    `{ApplicativeCommutativeIdempotent G}
    (ctx: list (G B))
    (t: term (G B) (G V)),
    dist2 (T := term) (G := G) (map2 dist_Z dist2_L (dec2_term_rec ctx t)) =
      pure (dec2_term_rec (B := B) (V := V)) <⋆> (dist list G ctx)
        <⋆> (dist2 (T := term) (G := G) t).
Proof.
  intros.
  generalize dependent ctx.
  induction t; intro ctx.
  - cbn.
    (* LHS *)
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    (* RHS *)
    rewrite map_to_ap.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    reflexivity.
  - cbn.
    (* LHS *)
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite IHt.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite dist_list_app.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite dist_list_one.
    rewrite <- ap_map.
    rewrite map_ap.
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite (ap_flip_x3 (lhs := b) (rhs := dist list G ctx)).
    rewrite app_pure_natural.
    rewrite ap_contract.
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite ap_contract.
    rewrite app_pure_natural.
    (* RHS *)
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite IHt2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    (* RHS *)
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite ap3.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite <- ap4; repeat rewrite ap2.
    rewrite (ap_flip_x3 (G := G)
               (lhs := dist2 (T := term) (G := G) t1)
               (rhs := dist list G ctx)).
    rewrite app_pure_natural.
    rewrite ap_contract.
    rewrite app_pure_natural.
    rewrite ap3.
    rewrite <- ap4; repeat rewrite ap2.
    reflexivity.
Qed.

Lemma dist_dec_commute:
  ∀ (B V: Type)
    `{ApplicativeCommutativeIdempotent G}
    (t: term (G B) (G V)),
    dist2 (T := term) (G := G) (map2 dist_Z dist2_L (dec2_term t)) =
      pure (dec2_term (B := B) (V := V)) <⋆> (dist2 (T := term) (G := G) t).
Proof.
  intros.
  unfold dec2_term.
  rewrite dist_dec2_rec_commute; auto.
  rewrite dist_list_nil.
  rewrite ap2.
  reflexivity.
Qed.

Lemma dist_dec_commute2:
  ∀ (B V: Type)
    `{ApplicativeCommutativeIdempotent G},
    dist2 (T := term) (G := G) ∘ map2 (dist_Z (G := G)) (dist2_L (G := G)) ∘ dec2_term =
      map (dec2_term (B := B) (V := V)) ∘
        (dist2 (T := term) (G := G) (B := B) (A := V)).
Proof.
  intros.
  ext t.
  unfold compose.
  rewrite dist_dec_commute; auto.
  rewrite <- map_to_ap.
  reflexivity.
Qed.

Import Adapters.PolyToMono.Categorical.DecoratedFunctor.ToMono1.
Import Adapters.PolyToMono.Categorical.TraversableFunctor.ToMono.

Lemma fun2_map_map_pw:
  ∀ (B1 A1 B2 A2 B3 A3: Type)
    (g2: B2 → B3) (f2: A2 → A3)
    (g1: B1 → B2) (f1: A1 → A2) (t: term B1 A1),
    map2 g2 f2 (map2 g1 f1 t) = map2 (g2 ∘ g1) (f2 ∘ f1) t.
Proof.
  intros. compose near t on left.
  now rewrite fun2_map_map.
Qed.

Ltac simplify_id :=
  repeat (change (?f ∘ id) with f || change (id ∘ ?f) with f).

#[export] Instance Single_DTF: ∀ (B: Type), DecoratedTraversableFunctor (list B) (term B).
Proof.
  intros.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - intros. unfold compose. ext t.
    unfold_ops @Map2_1.
    unfold_ops @Dist2_1.
    unfold compose at 1.
    unfold compose at 1.
    rewrite fun2_map_map_pw.
    simplify_id.
    unfold dec, VDec.
    unfold compose at 1.
    rewrite fun2_map_map_pw.
    simplify_id.
    unfold decp.
    unfold DecoratePoly_term.
    unfold dec2_term.
    generalize (@nil B).
    induction t; intro ctx.
    + cbn. unfold id.
      compose near v.
      rewrite (fun_map_map).
      rewrite (fun_map_map).
      reflexivity.
    + cbn in ×.
      rewrite IHt.
      unfold compose at 1.
      rewrite ap2.
      rewrite <- ap_map.
      rewrite app_pure_natural.
      (* RHS *)
      rewrite ap2.
      rewrite map_ap.
      rewrite app_pure_natural.
      reflexivity.
    + cbn in ×.
      rewrite IHt1.
      rewrite <- ap_map.
      rewrite app_pure_natural.
      rewrite IHt2.
      rewrite <- ap_map.
      rewrite map_ap.
      rewrite app_pure_natural.
      (* RHS *)
      rewrite map_ap.
      rewrite map_ap.
      rewrite app_pure_natural.
      reflexivity.
Qed.

Lemma dist_dec2_rec_commute_map:
  ∀ (B1 V1 B2 V2: Type)
    `{Applicative G}
    (ctx: list (G B1))
    (t: term (G B1) (G V1))
    (ρ: list B1 × B1 → G B2)
    (σ: list B1 × V1 → G V2),
    True.
Proof.
  intros.
Abort.

(*|
Typeclass Instance
=======================
|*)
#[export] Instance: DecoratedTraversableFunctorPoly term.
Proof.
  constructor; try typeclasses eauto.
  intros.
  rewrite dist_dec_commute2.
  - reflexivity.
  - assumption.
Qed.

(*|
***********************************************
Relating Decoration and Monad
***********************************************
|*)

(*|
Decorated Monad Laws
=======================
|*)

(*|
Return Law
-----------------------
|*)

Lemma decorate_ret_term: ∀ (B V: Type) (V: V),
    dec2_term (ret (T := term B) V) =
      ret ([], V).
Proof.
  reflexivity.
Qed.

(*|
Decorate Join Law
-----------------------
|*)

Lemma decorate_rec_join_term: ∀ (B V: Type) (ctx: list B),
    dec2_term_rec ctx ∘ join (T := term B) (A := V) =
      join (T := term (list B × B))
        ∘ map2 id (shift2 ∘ map_snd dec2_term)
        ∘ dec2_term_rec ctx.
Proof.
  intros. ext t. unfold compose at 1 2 3.
  generalize dependent ctx.
  induction t as [v | b body IHbody | t1 IHt1 t2 IHt2 ]; intro ctx.
  - (* LHS *)
    rewrite join_term_rw1.
    rewrite dec2_rec_spec.
    (* RHS *)
    rewrite dec2_term_rec_rw1.
    unfold compose at 2.
    rewrite map2_term_rw1.
    rewrite join_term_rw1.
    cbn.
    compose near (dec2_term v) on right.
    unfold map2, Map2_term.
    rewrite (map2_map2_term).
    reflexivity.
  - cbn.
    fequal.
    rewrite IHbody.
    reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite IHt2.
    reflexivity.
Qed.

Lemma decorate_join_term: ∀ (B V: Type),
    dec2_term ∘ join (T := term B) (A := V) =
      join (T := term (list B × B)) ∘ map2 id (shift2 ∘ map_snd dec2_term)
        ∘ dec2_term.
Proof.
  intros.
  unfold dec2_term.
  rewrite decorate_rec_join_term.
  reflexivity.
Qed.

(*|
Typeclass Instance
=======================
|*)

#[export] Instance DecoratedMonadPoly_term:
  DecoratedMonadPoly term.
Proof.
  constructor; try typeclasses eauto.
  - reflexivity.
  - apply decorate_join_term.
Qed.

(*|
***********************************************
Relating Monad and Traversal
***********************************************
|*)

(*|
Distribute Join Law
=======================
|*)

(* (t: term (G B) (term (G B) (G V))) *)
Lemma dist_join_term {B V: Type}
  `{Applicative G}:
    dist2 (T := term) (G := G) ∘ join (T := term (G B)) (A := (G V)) =
      map (F := G) join ∘ dist2 (T := term) (G := G)
        ∘ map2 (F := term) id (dist2 (T := term) (G := G)).
Proof.
  intros. ext t. unfold compose.
  induction t as [v | b body IHbody | t1 IHt1 t2 IHt2].
  - cbn. compose near (dist2 v) on right.
    rewrite fun_map_map.
    change (tvar (B := B) (V := term B V)) with
      (ret (T := term B) (A := term B V)).
    setoid_rewrite join_ret_term. (* not sure why setoid_ required here *)
    rewrite fun_map_id.
    reflexivity.
  - cbn.
    rewrite IHbody.
    rewrite <- ap_map.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    reflexivity.
  - cbn.
    rewrite IHt1.
    rewrite <- ap_map.
    rewrite app_pure_natural.
    rewrite IHt2.
    rewrite <- ap_map.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    reflexivity.
Qed.

(*|
Typeclass Instance
=======================
|*)

#[export] Instance TraversableMonad2_term:
  TraversableMonad2 term.
Proof.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - typeclasses eauto.
  - reflexivity.
  - intros. apply dist_join_term.
Qed.

#[export] Instance DecoratedTraversableMonadPoly_term:
  DecoratedTraversableMonadPoly term.
Proof.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - typeclasses eauto.
  - typeclasses eauto.
  - typeclasses eauto.
  - typeclasses eauto.
Qed.