From Tealeaves.Backends Require Import
  DB.DB
  DB.Simplification.
From Autosubst Require
  Autosubst.

Import DecoratedTraversableMonad.UsefulInstances.

#[local] Generalizable Variables W T U.

Module Autosubst_Instances.
  Import Autosubst.

  Section DTM_to_Autosubst.
    Context
      `{DecoratedTraversableMonad
       (op := Monoid_op_plus) (unit := Monoid_unit_zero) nat T}.

    #[export] Instance Ids_DTM: Ids (T nat) :=
      @ret T _ nat.
    #[export] Instance Rename_DTM: Rename (T nat) :=
      @DB.rename T _.
    #[export] Instance Subst_DTM: Subst (T nat) :=
      @DB.subst T _ _ _ _.

    Lemma rename_subst_DTM:
      forall (xi: nat -> nat) (s: T nat), rename xi s = s.[ren xi].
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall (xi : nat -> nat) (s : T nat),
rename xi s = s.[ren xi]
    Proof.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall (xi : nat -> nat) (s : T nat),
rename xi s = s.[ren xi]
      intros.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
xi: nat -> nat
s: T nat
rename xi s = s.[ren xi]
      unfold_ops @Rename_DTM @Subst_DTM.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
xi: nat -> nat
s: T nat
DB.rename xi s = DB.subst (ren xi) s
      tealeaves_unfold.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
xi: nat -> nat
s: T nat
DB.subst (ret ∘ xi) s = DB.subst (ren xi) s
      reflexivity.
    Qed.

    Lemma subst_id_DTM:
      forall s: T nat, s.[ids] = s.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall s : T nat, s.[ids] = s
    Proof.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall s : T nat, s.[ids] = s
      intros.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
s: T nat
s.[ids] = s
      unfold_ops @Ids_DTM @Subst_DTM.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
s: T nat
DB.subst ret s = s
      simplify_db.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
s: T nat
s = s
      reflexivity.
    Qed.

    Lemma id_subst_DTM: forall (sigma: nat -> T nat) (x: nat),
        (ids x).[sigma] = sigma x.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall (sigma : nat -> T nat) (x : nat),
(ids x).[sigma] = sigma x
    Proof.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall (sigma : nat -> T nat) (x : nat),
(ids x).[sigma] = sigma x
      intros.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
sigma: nat -> T nat
x: nat
(ids x).[sigma] = sigma x
      unfold_ops @Ids_DTM @Subst_DTM.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
sigma: nat -> T nat
x: nat
DB.subst sigma (ret x) = sigma x
      simplify_db.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
sigma: nat -> T nat
x: nat
sigma x = sigma x
      conclude.
    Qed.

    Lemma subst_comp_DTM:
      forall (sigma tau: nat -> T nat) (s: T nat),
        s.[sigma].[tau] = s.[scomp sigma tau].
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall (sigma tau : nat -> T nat) (s : T nat),
s.[sigma].[tau] = s.[sigma >> tau]
    Proof.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
forall (sigma tau : nat -> T nat) (s : T nat),
s.[sigma].[tau] = s.[sigma >> tau]
      intros.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
sigma, tau: nat -> T nat
s: T nat
s.[sigma].[tau] = s.[sigma >> tau]
      unfold_ops @Subst_DTM.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
sigma, tau: nat -> T nat
s: T nat
DB.subst tau (DB.subst sigma s) =
DB.subst (sigma >> tau) s
      compose near s on left.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
sigma, tau: nat -> T nat
s: T nat
(DB.subst tau ∘ DB.subst sigma) s =
DB.subst (sigma >> tau) s
      rewrite subst_subst.
T: Type -> Type
Return_inst: Return T
Bindd_T_inst: Binddt nat T T
H: DecoratedTraversableMonad nat T
sigma, tau: nat -> T nat
s: T nat
DB.subst (DB.subst tau ∘ sigma) s =
DB.subst (sigma >> tau) s
      reflexivity.
    Qed.

    #[export] Instance SubstLemmas_term: SubstLemmas (T nat) :=
      {| rename_subst := rename_subst_DTM;
        subst_id := subst_id_DTM;
        id_subst := id_subst_DTM;
        subst_comp := subst_comp_DTM;
      |}.

  End DTM_to_Autosubst.

  Lemma cons_eq {X:Type}:
    @DB.scons X = Autosubst_Basics.scons.
X: Type
DB.scons = scons
  Proof.
X: Type
DB.scons = scons
    reflexivity.
  Qed.

  Lemma upren_eq {X:Type}:
    up__ren = upren.
X: Type
up__ren = upren
  Proof.
X: Type
up__ren = upren
    reflexivity.
  Qed.

  Lemma up_eq `{Return T} `{Binddt nat T T} {X:Type}:
    up__sub (T := T) = up.
T: Type -> Type
H: Return T
H0: Binddt nat T T
X: Type
up__sub = up
  Proof.
T: Type -> Type
H: Return T
H0: Binddt nat T T
X: Type
up__sub = up
    ext σ ix.
T: Type -> Type
H: Return T
H0: Binddt nat T T
X: Type
σ: nat -> T nat
ix: nat
up__sub σ ix = up σ ix
    unfold up, up__sub.
T: Type -> Type
H: Return T
H0: Binddt nat T T
X: Type
σ: nat -> T nat
ix: nat
DB.scons (ret 0) (DB.rename (DB.lift 1) ∘ σ) ix =
(ids 0 .: σ >>> rename (+1)) ix
    rewrite cons_eq.
T: Type -> Type
H: Return T
H0: Binddt nat T T
X: Type
σ: nat -> T nat
ix: nat
(ret 0 .: DB.rename (DB.lift 1) ∘ σ) ix =
(ids 0 .: σ >>> rename (+1)) ix
    reflexivity.
  Qed.

End Autosubst_Instances.

(** * Autosubst-compatible notations *)
(******************************************************************************)
Module Notations.
  Notation "( + x )" := (lift x) (format "( + x )"): tealeaves_scope.
  Notation "f >>> g" :=
    (compose g f)
      (at level 56, left associativity): tealeaves_scope.
  Notation "s .: sigma" :=
    (scons s sigma)
      (at level 55, sigma at level 56, right associativity): tealeaves_scope.
  Notation "s .[ sigma ]" :=
    (subst sigma s)
      (at level 2, sigma at level 200, left associativity,
        format "s .[ sigma ]" ): tealeaves_scope.
  Notation "s .[ t /]" := (subst (t .: ret) s)
                            (at level 2, t at level 200, left associativity,
                              format "s .[ t /]"): tealeaves_scope.
  Notation "s .[ t1 , t2 , .. , tn /]" :=
    (subst (scons t1 (scons t2 .. (scons tn ret) .. )) s)
      (at level 2, left associativity,
        format "s '[ ' .[ t1 , '/' t2 , '/' .. , '/' tn /] ']'"): tealeaves_scope.
End Notations.