Tealeaves.Backends.DB.Simplification

Extra lemmas

Section db_simplification_lemmas.

  Context
    `{ret_inst : Return T}
      `{Map_T_inst : Map T}
      `{Mapd_T_inst : Mapd T}
      `{Traverse_T_inst : Traverse T}
      `{Bind_T_inst : Bind T T}
      `{Mapdt_T_inst : Mapdt T}
      `{Bindd_T_inst : Bindd T T}
      `{Bindt_T_inst : Bindt T T}
      `{Binddt_T_inst : Binddt T T}
      `{! Compat_Map_Binddt nat T T}
      `{! Compat_Mapd_Binddt nat T T}
      `{! Compat_Traverse_Binddt nat T T}
      `{! Compat_Bind_Binddt nat T T}
      `{! Compat_Mapdt_Binddt nat T T}
      `{! Compat_Bindd_Binddt nat T T}
      `{! Compat_Bindt_Binddt nat T T}
      `{Monad_inst : ! DecoratedTraversableMonad T}.

  Context
    `{Map_U_inst : Map U}
      `{Mapd_U_inst : Mapd U}
      `{Traverse_U_inst : Traverse U}
      `{Bind_U_inst : Bind T U}
      `{Mapdt_U_inst : Mapdt U}
      `{Bindd_U_inst : Bindd T U}
      `{Bindt_U_inst : Bindt T U}
      `{Binddt_U_inst : Binddt T U}
      `{! Compat_Map_Binddt nat T U}
      `{! Compat_Mapd_Binddt nat T U}
      `{! Compat_Traverse_Binddt nat T U}
      `{! Compat_Bind_Binddt nat T U}
      `{! Compat_Mapdt_Binddt nat T U}
      `{! Compat_Bindd_Binddt nat T U}
      `{! Compat_Bindt_Binddt nat T U}
      `{Module_inst : ! DecoratedTraversableRightPreModule T U
                        (unit := Monoid_unit_zero)
                        (op := Monoid_op_plus)}.

  Lemma subst_id_Applied: t,
      subst (@ret T _ ) t = t.
  Proof.
    now rewrite subst_id.
  Qed.


  (* used for simpl_db *)
  Lemma subst_compose_ret_assoc {X: Type}: (f: T X) σ,
    (f subst σ) ret = f σ.
  Proof.
    intros.
    change_left (f (subst σ ret)).
    rewrite subst_compose_ret.
    reflexivity.
  Qed.


  (* Autosubst: subst_compR *)
  Lemma subst_subst_R {X}: (f: U X) (σ2 σ1: T ),
      (f subst σ2) subst σ1 = f subst (T := T) (subst σ2 σ1).
  Proof.
    intros.
    reassociateon left.
    rewrite subst_subst.
    reflexivity.
  Qed.


  (* Autosubst: subst_compI *)
  Lemma subst_subst_applied: (σ2 σ1: T ) (t: U ),
      subst σ2 (subst σ1 t) = subst (T := T) (subst σ2 σ1) t.
  Proof.
    intros.
    compose near t on left.
    rewrite subst_subst.
    reflexivity.
  Qed.


End db_simplification_lemmas.

Unfolding up


Ltac unfold_up :=
  rewrite ?up__sub_unfold;
  (* up__sub σ = ret 0 ⋅ (subst (ret ∘ (+1)) ∘ σ). *)
  unfold up__ren.

Simplifying renaming via unfolding

Lemma local__ren_zero_comp_alt {X Y Z: Type} {f: × X Y} {g: Y Z} {n}:
  (g f) (0, n) = g (f (0, n)).
  reflexivity.
Qed.

Lemma local__ren_zero_comp {X:Type} {f: X} {ρ n}:
    (f local__ren ρ) (0, n) = f (ρ n).
Proof.
  unfold compose.
  intros.
  rewrite local__ren_zero.
  conclude.
Qed.


Ltac rw_local__ren :=
  rewrite ?local__ren_zero, ?local__ren_zero_comp, ?local__ren_zero_comp_alt,
    ?local__sub_zero.

Ltac rw_db_local :=
  unfold_ops @Monoid_op_plus @Monoid_unit_zero;
  repeat rw_local__ren;
  normalize_all_ret.

Lemma rename_to_mapd {T} `{Mapd nat T}: (ρ: ),
    rename ρ = mapd (local__ren ρ).
Proof.
  reflexivity.
Qed.


Ltac simplify_rename :=
  rewrite ?rename_to_mapd;
  simplify_mapd;
  rewrite ?local__ren_preincr_1;
  rewrite ?rename_to_mapd;
  rw_db_local.

Simplifying substitution via unfolding

Ltac tealeaves_unfold :=
  rewrite ?rename_to_subst.

Lemma subst_to_bindd {T U} `{Return T} `{Mapd nat T} `{Bindd nat T U}: (σ: T ),
    subst (T := T) (U := U) σ = bindd (local__sub σ).
Proof.
  reflexivity.
Qed.


(* Simplify by unfolding *)
Ltac simplify_subst :=
  rewrite ?subst_to_bindd;
  simplify_bindd;
  rewrite ?local__sub_preincr_1;
  rewrite ?subst_to_bindd;
  rw_db_local.

Simplifying substitution a la Autosubst

Ltac simplify_subst_id :=
  rewrite
    ?subst_id_Applied,
    ?subst_id.

Ltac simplify_subst_ret :=
  rewrite
    ?subst_ret,
    ?subst_compose_ret,
    ?subst_compose_ret_assoc.

Ltac simplify_subst_subst :=
  rewrite
    ?subst_subst_applied,
    ?subst_subst_R,
    ?subst_subst.

Ltac normalize_rename_to_subst :=
  rewrite ?rename_to_subst.

Ltac normalize_rename_to_subst_in_all :=
  rewrite ?rename_to_subst in ×.

(* unfold some operations to reduce the number that must be considered *)
Ltac simplify_db_unfold_phase :=
  unfold_up;
  normalize_rename_to_subst.

Ltac simplify_db_end_phase :=
  idtac.

Ltac simplify_db_core_phase :=
  simplify_subst_id;
  simplify_subst_ret;
  simplify_subst_subst;
  try simplify_subst;
  rewrite ?cons_compose.

Ltac simplify_db :=
  simplify_db_unfold_phase;
  repeat (progress simplify_db_core_phase);
  simplify_db_end_phase.

Ltac simplify_like_autosubst_core :=
  progress
    rewrite
    ?subst_compose_ret,
    ?subst_id,
    ?subst_subst,
    ?subst_compose_ret_assoc,
    ?subst_subst_applied,
    ?subst_ret,
    ?subst_id_Applied.

Ltac normalize_functions :=
  ltac_trace "normalize_functions";
  match goal with
  | |- context[?f id] ⇒
      change (f id) with f
  | |- context[(id ?f)] ⇒
      change (id f) with f
  | |- context[(?f (?g ?h))] ⇒
      change (f (g h)) with (f g h)
  end.

Lemma cons_compose_S {X}: (x: X) (σ: X) (n: ),
    (x σ) (+ (S n)) = σ (+n).
Proof.
  reflexivity.
Qed.


Ltac simplify_cons :=
  match goal with
  | |- context[(?x ) (+ (S ?n))] ⇒
     rewrite (cons_compose_S x σ n)
  | |- context[?x ( (+ (S ?n)))] ⇒
      change x withn);
      rewrite (cons_eta σ n)
  | _progress (rewrite ?cons_compose, ?lift_eta)
  end.

Ltac factor_out_ret :=
  repeat match goal with
    | |- context[((ret (T := ?T) (A := ?A) ?f) ?g)]
        change ((ret (T := T) (A := A) f) g)
        with (ret (T := T) (A := A) (f g))
    end;
  rewrite ?cons_compose.

Ltac simplify_db_like_autosubst :=
  repeat (progress simplify_subst); (* in place of cbn *)
  simplify_db_unfold_phase;
  repeat (first
            [ simplify_like_autosubst_core
            | simplify_cons
            | simplify_lift
            | normalize_functions
    ]);
  factor_out_ret;
  simplify_db_end_phase.