Tealeaves.Examples.RecBag.Syntax

From Tealeaves Require Export
  Classes.Categorical.ApplicativeCommutativeIdempotent
  Classes.Categorical.TraversableFunctor
  Classes.Kleisli.DecoratedTraversableCommIdemFunctor
  Classes.Kleisli.DecoratedTraversableMonadPoly
  Functors.List
  Backends.Common.Names
  Functors.List.

Import Product.Notations.
Import Monoid.Notations.
Import List.ListNotations.
Import DecoratedTraversableCommIdemFunctor.Notations.
Import Applicative.Notations.

#[local] Generalizable Variables G ϕ.
#[local] Set Implicit Arguments.

Definition dist_pair
  {b1 v1: Type}
  `{Map G} `{Mult G} `{Pure G}:
  list (G b1) × G v1 → G (list b1 × v1) :=
  fun '(x, y) ⇒ pure (@pair (list b1) v1) <⋆> dist list G x <⋆> y.

Definition dec_bag: ∀ (A: Type), list A → list (list A × A) :=
  fun A l ⇒ map (pair l) l.

Section lfg.

  Context `{ApplicativeCommutativeIdempotent G} (A: Type).

  Lemma map_dist_pair_nil: ∀ (ctx: list (G A)) (l: list (G A)),
      l = nil →
      dist list G (A := (list A) × A) (map (F := list) dist_pair (map (F := list) (pair ctx) l))
      = pure (F := G) (A := list (list A × A)) (@nil (list A × A)).
  Proof.
    intros. subst. reflexivity.
  Qed.

  Lemma map_dist_pair: ∀ (ctx: list (G A)) (l: list (G A)),
      l ≠ nil →
      dist list G (A := (list A) × A) (map (F := list) dist_pair (map (F := list) (pair ctx) l))
      =
        pure (F := G) (fun ctx ⇒ map (F := list) (pair ctx))
          <⋆> (dist list G ctx)
          <⋆> dist list G l.
  Proof.
    intros. destruct l.
    - contradiction.
    - clear H0.
      generalize dependent g.
      induction l; intro g.
      + cbn.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
      (* RHS *)
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        reflexivity.
      + rewrite map_list_cons.
        rewrite map_list_cons.
        rewrite dist_list_cons_1.
        rewrite IHl.
        cbn.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        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 <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite (ap_flip1 (G := G) (lhs := dist list G ctx) (rhs := g)).
        rewrite app_pure_natural.
        rewrite ap_contract.
        rewrite map_ap.
        rewrite app_pure_natural.
        rewrite (ap_flip1 (G := G) (B := list A) (A := A) (lhs := g) (rhs := dist list G ctx)).
        rewrite app_pure_natural.
        (* RHS *)
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        reflexivity.
  Qed.

  Lemma informative_list_nilb: ∀ (l: list (G A)),
      {l = nil} + {l ≠ nil}.
  Proof.
    intros. destruct l.
    - now left.
    - now right.
  Defined.

  Lemma decorate_commute: ∀ (l: list (G A)),
      map (dec_bag (A := A)) (dist list G l) =
        dist list G (map (F := list) dist_pair (dec_bag l)).
  Proof.
    intros. induction l.
    - cbn.
      rewrite app_pure_natural.
      reflexivity.
    - cbn.
      rewrite map_ap.
      rewrite map_ap.
      rewrite app_pure_natural.
      (* RHS *)
      rewrite <- ap4.
      rewrite ap2.
      rewrite <- ap4.
      rewrite ap2.
      rewrite ap2.
      rewrite <- ap4.
      rewrite ap2.
      rewrite <- ap4.
      rewrite ap2.
      rewrite ap2.
      destruct (informative_list_nilb l).
      + subst.
        cbn.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite ap_contract.
        rewrite app_pure_natural.
        reflexivity.
      + rewrite map_dist_pair; auto.
        rewrite (ap_flip1 (A := A) (B := list A) (f := pure (compose (compose cons ∘ pair) ∘ cons))
                   (lhs := a) (rhs := dist list G l)).
        rewrite app_pure_natural.
        rewrite ap_contract.
        rewrite map_ap.
        rewrite app_pure_natural.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap3.
        rewrite <- ap4.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite <- ap4.
        rewrite ap2.
        rewrite ap2.
        rewrite dist_list_cons_1.
        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 ap_contract.
        rewrite map_ap.
        rewrite map_ap.
        rewrite map_ap.
        rewrite app_pure_natural.
        rewrite ap_contract.
        rewrite map_ap.
        rewrite app_pure_natural.
        rewrite (ap_flip1 (G := G) (A := list A) (B := A)
                   (f := pure
                      (double_input
                         ∘ (compose (compose double_input)
                              ∘ (compose (evalAt cons)
                                   ∘ (compose (compose ∘ compose)
                                        ∘ (compose (evalAt (map ○ pair)) ∘ compose (compose ∘ compose)
                                             ∘ (double_input ∘ flip (compose (compose cons ∘ pair) ∘ cons))))))))
                   (lhs := dist list G l) (rhs := a)).
        rewrite app_pure_natural.
        rewrite ap_contract.
        rewrite map_ap.
        rewrite app_pure_natural.
        reflexivity.
  Qed.

End lfg.

Section mapci.

End mapci.