LN.v

From Tealeaves.Theory Require Export
  DecoratedTraversableMonad.
From Tealeaves.Backends.Common Require Export
  Names AtomSet AssocList.
From Tealeaves.Backends.LN Require Export
  LN Simplification.

From Tealeaves.Simplification Require Export
  Simplification.

Import DecoratedTraversableMonad.UsefulInstances.
Import Classes.Kleisli.Theory.DecoratedTraversableMonad.

Module Notations.
  Export Categorical.Applicative.Notations. (* <⋆> *)
  Export Kleisli.Comonad.Notations.
  (* Export Kleisli.DecoratedFunctor.Notations. *)
  Export Kleisli.DecoratedMonad.Notations.
  Export Kleisli.TraversableFunctor.Notations.
  Export Kleisli.TraversableMonad.Notations.
  Export Kleisli.DecoratedTraversableFunctor.Notations.
  Export Kleisli.DecoratedTraversableMonad.Notations.
  Export Kleisli.DecoratedContainerFunctor.Notations. (* ∈d *)
  (* Export Kleisli.DecoratedContainerMonad.Notations. *)
  Export Categorical.ContainerFunctor.Notations. (* ∈ *)

  Export Product.Notations. (* × *)
  Export Monoid.Notations. (* Ƶ and ● *)
  Export Subset.Notations. (* ∪ *)
  Export List.ListNotations. (* [] :: *)

  (* Export LN.OpNotations. (* operations *) *)
  Export Common.AtomSet.Notations.
  Export Common.AssocList.Notations. (* one, ~ *)
End Notations.


Module Type SyntaxSIGHetero.
  Parameter (iterm oterm : Type).
  Parameter (T U : Type -> Type).
  Parameter ret_inst: Return T.
  Parameter binddt_T_inst: Binddt nat T T.
  Parameter binddt_U_inst: Binddt nat T U.
  Parameter module_inst:
    DecoratedTraversableRightModule nat T U
      (Return_inst := ret_inst)
      (Bindd_T_inst := binddt_T_inst)
      (Bindd_U_inst := binddt_U_inst)
      (unit := Monoid_unit_zero)
      (op := Monoid_op_plus).
  Parameter to_T:  iterm -> T LN.
  Parameter to_T_inv: T LN -> iterm.
  Parameter to_U: oterm -> U LN.
  Parameter to_U_inv: U LN -> oterm.
  Parameter to_T_iso : forall (t : iterm), to_T_inv (to_T t) = t.
  Parameter to_U_iso : forall (t : oterm), to_U_inv (to_U t) = t.
  Parameter to_T_iso_inv : forall (t : T LN), to_T (to_T_inv t) = t.
  Parameter to_U_iso_inv : forall (t : U LN), to_U (to_U_inv t) = t.
  Parameter from_atom: atom -> iterm.
  Parameter from_ix: nat -> iterm.
  Parameter from_atom_Ret:
    from_atom = to_T_inv ○ @ret T ret_inst LN ○ Fr.
  Parameter from_ix_Ret:
    from_ix = to_T_inv ○ @ret T ret_inst LN ○ Bd.
End SyntaxSIGHetero.

Module Type TheorySIG.
  Parameters iterm oterm : Type.
  Parameters
    (open : iterm -> oterm -> oterm)
    (close : atom -> oterm -> oterm)
    (subst : atom -> iterm -> oterm -> oterm)
    (LCb : oterm -> bool).
End TheorySIG.

Module MakeTheory_Hetero
  (Syntax: SyntaxSIGHetero) <: TheorySIG.
  Import Syntax.

  Definition iterm := Syntax.iterm.
  Definition oterm := Syntax.oterm.

  Import DecoratedTraversableMonad.UsefulInstances.

  #[local] Existing Instance Syntax.ret_inst.
  #[local] Existing Instance Syntax.binddt_T_inst.
  #[local] Existing Instance Syntax.binddt_U_inst.
  #[local] Existing Instance Syntax.module_inst.
  #[local] Existing Instance Map_Binddt.
  #[local] Existing Instance Mapd_Binddt.
  #[local] Existing Instance Traverse_Binddt.
  #[local] Existing Instance Mapdt_Binddt.
  #[local] Existing Instance Bind_Binddt.
  #[local] Existing Instance Bindt_Binddt.
  #[local] Existing Instance Bindd_Binddt.
  #[local] Existing Instance ToBatch_Traverse.
  #[local] Existing Instance ToSubset_Traverse.

  Import AtomSet.Notations.

  Coercion to_T : Syntax.iterm >-> T.
  Coercion to_U : Syntax.oterm >-> U.

  Definition open : iterm -> oterm -> oterm :=
    fun t u => to_U_inv (open (T := T) (U := U) t u).

  Definition close : atom -> oterm -> oterm :=
    fun x u => to_U_inv (close (U := U) x u).

  Definition subst : atom -> iterm -> oterm -> oterm :=
    fun x t u => to_U_inv (subst (T := T) (U := U) x t u).

  Definition free : oterm -> list atom :=
    fun u => free (U := U) u.

  Definition FV : oterm -> AtomSet.t :=
    fun u => FV (U := U) u.

  Definition LC : oterm -> Prop :=
    fun u => LC (U := U) u.

  Definition LCb : oterm -> bool :=
    fun u => LCb (U := U) u.

  Definition scoped : oterm -> AtomSet.t -> Prop :=
    fun t γ => FV t ⊆ γ.

  Definition subst_i : atom -> iterm -> iterm -> iterm :=
    fun x t u => to_T_inv (LN.subst (T := T) (U := T) x t u).

  Definition FV_i : iterm -> AtomSet.t :=
    fun t => LN.FV (U := T) t.

  Definition LC_i : iterm -> Prop :=
    fun u => LN.LC (U := T) u.

  Module Notations.
    Notation "t '{ x ~> u }" := (subst x u t) (at level 35).
    Notation "t '( u )" := (open u t) (at level 35).
    Notation "'[ x ] t" := (close x t) (at level 35).
  End Notations.

  Import Notations.

  Coercion from_atom : atom >-> Syntax.iterm.
  Coercion from_ix : nat >-> Syntax.iterm.

  Implicit Types (x y: atom) (t: iterm) (u: oterm).

  Theorem open_lc: forall t u,
    LC u -> u '(t) = u.forall t u, LC u -> u '( t) = u
  Proof.forall t u, LC u -> u '( t) = u
    intros.t: iterm
u: oterm
H: LC u
u '( t) = u
    unfold LC.t: iterm
u: oterm
H: LC u
u '( t) = u
    unfold open.t: iterm
u: oterm
H: LC u
to_U_inv (LN.open t u) = u
    rewrite open_lc.t: iterm
u: oterm
H: LC u
to_U_inv u = u
t: iterm
u: oterm
H: LC u
LN.LC u
    -t: iterm
u: oterm
H: LC u
to_U_inv u = u apply to_U_iso.
    -t: iterm
u: oterm
H: LC u
LN.LC u assumption.
  Qed.

  Theorem FV_subst_upper: forall x t u,
      FV (u '{x ~> t}) ⊆ FV u \\ {{x}} ∪ FV_i t.forall x t u,
FV (u '{ x ~> t}) ⊆ FV u \\ {{x}} ∪ FV_i t
  Proof.forall x t u,
FV (u '{ x ~> t}) ⊆ FV u \\ {{x}} ∪ FV_i t
    intros.x: atom
t: iterm
u: oterm
FV (u '{ x ~> t}) ⊆ FV u \\ {{x}} ∪ FV_i t
    unfold FV, FV_i, subst.x: atom
t: iterm
u: oterm
LN.FV (to_U_inv (LN.subst x t u))
⊆ LN.FV u \\ {{x}} ∪ LN.FV t
    rewrite to_U_iso_inv.x: atom
t: iterm
u: oterm
LN.FV (LN.subst x t u) ⊆ LN.FV u \\ {{x}} ∪ LN.FV t
    rewrite FV_subst_upper.x: atom
t: iterm
u: oterm
LN.FV u \\ {{x}} ∪ LN.FV t
⊆ LN.FV u \\ {{x}} ∪ LN.FV t
    reflexivity.
  Qed.

  Theorem FV_subst_lower: forall t u x,
      FV u \\ {{ x }} ⊆ FV (u '{x ~> t}).forall t u x, FV u \\ {{x}} ⊆ FV (u '{ x ~> t})
  Proof.forall t u x, FV u \\ {{x}} ⊆ FV (u '{ x ~> t})
    intros.t: iterm
u: oterm
x: atom
FV u \\ {{x}} ⊆ FV (u '{ x ~> t})
    unfold FV, FV_i, subst.t: iterm
u: oterm
x: atom
LN.FV u \\ {{x}} ⊆ LN.FV (to_U_inv (LN.subst x t u))
    rewrite to_U_iso_inv.t: iterm
u: oterm
x: atom
LN.FV u \\ {{x}} ⊆ LN.FV (LN.subst x t u)
    apply FV_subst_lower.
  Qed.

  Theorem close_open : forall x u,
      ~ x `in` FV u ->
      '[x] (u '(from_atom x)) = u.forall x u, x `notin` FV u -> '[ x] (u '( x)) = u
  Proof.forall x u, x `notin` FV u -> '[ x] (u '( x)) = u
    intros.x: atom
u: oterm
H: x `notin` FV u
'[ x] (u '( x)) = u
    unfold close, open.x: atom
u: oterm
H: x `notin` FV u
to_U_inv (LN.close x (to_U_inv (LN.open x u))) = u
    rewrite from_atom_Ret.x: atom
u: oterm
H: x `notin` FV u
to_U_inv
  (LN.close x
     (to_U_inv (LN.open (to_T_inv (ret (Fr x))) u))) =
u
    rewrite to_U_iso_inv.x: atom
u: oterm
H: x `notin` FV u
to_U_inv
  (LN.close x (LN.open (to_T_inv (ret (Fr x))) u)) = u
    rewrite to_T_iso_inv.x: atom
u: oterm
H: x `notin` FV u
to_U_inv (LN.close x (LN.open (ret (Fr x)) u)) = u
    rewrite close_open.x: atom
u: oterm
H: x `notin` FV u
to_U_inv u = u
x: atom
u: oterm
H: x `notin` FV u
~ element_of x (LN.free u)
    -x: atom
u: oterm
H: x `notin` FV u
to_U_inv u = u rewrite to_U_iso.x: atom
u: oterm
H: x `notin` FV u
u = u
      reflexivity.
    -x: atom
u: oterm
H: x `notin` FV u
~ element_of x (LN.free u) rewrite free_iff_FV.x: atom
u: oterm
H: x `notin` FV u
x `notin` LN.FV u
      assumption.
  Qed.

  Theorem open_close : forall x u,
      ('[x] u) '(x) = u.forall x u, ('[ x] u) '( x) = u
  Proof.forall x u, ('[ x] u) '( x) = u
    intros.x: atom
u: oterm
('[ x] u) '( x) = u
    unfold close, open.x: atom
u: oterm
to_U_inv (LN.open x (to_U_inv (LN.close x u))) = u
    rewrite from_atom_Ret.x: atom
u: oterm
to_U_inv
  (LN.open (to_T_inv (ret (Fr x)))
     (to_U_inv (LN.close x u))) = u
    rewrite to_U_iso_inv.x: atom
u: oterm
to_U_inv
  (LN.open (to_T_inv (ret (Fr x))) (LN.close x u)) = u
    rewrite to_T_iso_inv.x: atom
u: oterm
to_U_inv (LN.open (ret (Fr x)) (LN.close x u)) = u
    rewrite open_close.x: atom
u: oterm
to_U_inv u = u
    rewrite to_U_iso.x: atom
u: oterm
u = u
    reflexivity.
  Qed.

  Theorem subst_open_var : forall u t x y,
      x <> y ->
      LC_i t ->
      u '(from_atom y) '{x ~> t} =
        u '{x ~> t} '(from_atom y).forall u t x y,
x <> y ->
LC_i t -> (u '( y)) '{ x ~> t} = (u '{ x ~> t}) '( y)
  Proof.forall u t x y,
x <> y ->
LC_i t -> (u '( y)) '{ x ~> t} = (u '{ x ~> t}) '( y)
    intros.u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
(u '( y)) '{ x ~> t} = (u '{ x ~> t}) '( y)
    unfold close, open, subst.u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
to_U_inv (LN.subst x t (to_U_inv (LN.open y u))) =
to_U_inv (LN.open y (to_U_inv (LN.subst x t u)))
    rewrite to_U_iso_inv.u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
to_U_inv (LN.subst x t (LN.open y u)) =
to_U_inv (LN.open y (to_U_inv (LN.subst x t u)))
    rewrite to_U_iso_inv.u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
to_U_inv (LN.subst x t (LN.open y u)) =
to_U_inv (LN.open y (LN.subst x t u))
    rewrite from_atom_Ret.u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
to_U_inv
  (LN.subst x t (LN.open (to_T_inv (ret (Fr y))) u)) =
to_U_inv
  (LN.open (to_T_inv (ret (Fr y))) (LN.subst x t u))
    rewrite to_T_iso_inv.u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
to_U_inv (LN.subst x t (LN.open (ret (Fr y)) u)) =
to_U_inv (LN.open (ret (Fr y)) (LN.subst x t u))
    rewrite subst_open_var.u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
to_U_inv (LN.open (ret (Fr y)) (LN.subst x t u)) =
to_U_inv (LN.open (ret (Fr y)) (LN.subst x t u))
u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
x <> y
u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
LN.LC t
    -u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
to_U_inv (LN.open (ret (Fr y)) (LN.subst x t u)) =
to_U_inv (LN.open (ret (Fr y)) (LN.subst x t u)) reflexivity.
    -u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
x <> y assumption.
    -u: oterm
t: iterm
x, y: atom
H: x <> y
H0: LC_i t
LN.LC t assumption.
  Qed.

  Theorem open_spec : forall u t x,
      ~ x `in` FV u ->
      u '(t) = u '(from_atom x) '{x ~> t}.forall u t x,
x `notin` FV u -> u '( t) = (u '( x)) '{ x ~> t}
  Proof.forall u t x,
x `notin` FV u -> u '( t) = (u '( x)) '{ x ~> t}
    intros.u: oterm
t: iterm
x: atom
H: x `notin` FV u
u '( t) = (u '( x)) '{ x ~> t}
    unfold close, open, subst.u: oterm
t: iterm
x: atom
H: x `notin` FV u
to_U_inv (LN.open t u) =
to_U_inv (LN.subst x t (to_U_inv (LN.open x u)))
    rewrite to_U_iso_inv.u: oterm
t: iterm
x: atom
H: x `notin` FV u
to_U_inv (LN.open t u) =
to_U_inv (LN.subst x t (LN.open x u))
    erewrite open_spec.u: oterm
t: iterm
x: atom
H: x `notin` FV u
to_U_inv (LN.subst ?x t (LN.open (ret (Fr ?x)) u)) =
to_U_inv (LN.subst x t (LN.open x u))
u: oterm
t: iterm
x: atom
H: x `notin` FV u
?x `notin` LN.FV u
    -u: oterm
t: iterm
x: atom
H: x `notin` FV u
to_U_inv (LN.subst ?x t (LN.open (ret (Fr ?x)) u)) =
to_U_inv (LN.subst x t (LN.open x u)) rewrite from_atom_Ret.u: oterm
t: iterm
x: atom
H: x `notin` FV u
to_U_inv (LN.subst ?x t (LN.open (ret (Fr ?x)) u)) =
to_U_inv
  (LN.subst x t (LN.open (to_T_inv (ret (Fr x))) u))
      rewrite to_T_iso_inv.u: oterm
t: iterm
x: atom
H: x `notin` FV u
to_U_inv (LN.subst ?x t (LN.open (ret (Fr ?x)) u)) =
to_U_inv (LN.subst x t (LN.open (ret (Fr x)) u))
      reflexivity.
    -u: oterm
t: iterm
x: atom
H: x `notin` FV u
x `notin` LN.FV u assumption.
  Qed.

  Theorem subst_open :  forall t1 t2 u x,
      LC_i t2 ->
      u '(t1) '{x ~> t2} =
        open (subst_i x t2 t1) (u '{x ~> t2}).forall t1 t2 u x,
LC_i t2 ->
(u '( t1)) '{ x ~> t2} =
(u '{ x ~> t2}) '( subst_i x t2 t1)
  Proof.forall t1 t2 u x,
LC_i t2 ->
(u '( t1)) '{ x ~> t2} =
(u '{ x ~> t2}) '( subst_i x t2 t1)
    intros.t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
(u '( t1)) '{ x ~> t2} =
(u '{ x ~> t2}) '( subst_i x t2 t1)
    unfold close, open, subst, subst_i.t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
to_U_inv (LN.subst x t2 (to_U_inv (LN.open t1 u))) =
to_U_inv
  (LN.open (to_T_inv (LN.subst x t2 t1))
     (to_U_inv (LN.subst x t2 u)))
    rewrite to_U_iso_inv.t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
to_U_inv (LN.subst x t2 (LN.open t1 u)) =
to_U_inv
  (LN.open (to_T_inv (LN.subst x t2 t1))
     (to_U_inv (LN.subst x t2 u)))
    rewrite subst_open.t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
to_U_inv
  (LN.open (LN.subst x t2 t1) (LN.subst x t2 u)) =
to_U_inv
  (LN.open (to_T_inv (LN.subst x t2 t1))
     (to_U_inv (LN.subst x t2 u)))
t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
LN.LC t2
    -t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
to_U_inv
  (LN.open (LN.subst x t2 t1) (LN.subst x t2 u)) =
to_U_inv
  (LN.open (to_T_inv (LN.subst x t2 t1))
     (to_U_inv (LN.subst x t2 u))) rewrite to_U_iso_inv.t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
to_U_inv
  (LN.open (LN.subst x t2 t1) (LN.subst x t2 u)) =
to_U_inv
  (LN.open (to_T_inv (LN.subst x t2 t1))
     (LN.subst x t2 u))
      rewrite to_T_iso_inv.t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
to_U_inv
  (LN.open (LN.subst x t2 t1) (LN.subst x t2 u)) =
to_U_inv
  (LN.open (LN.subst x t2 t1) (LN.subst x t2 u))
      reflexivity.
    -t1, t2: iterm
u: oterm
x: atom
H: LC_i t2
LN.LC t2 assumption.
  Qed.

  Theorem FV_open_upper : forall u t,
      FV (u '(t)) ⊆ FV u ∪ FV_i t.forall u t, FV (u '( t)) ⊆ FV u ∪ FV_i t
  Proof.forall u t, FV (u '( t)) ⊆ FV u ∪ FV_i t
    intros.u: oterm
t: iterm
FV (u '( t)) ⊆ FV u ∪ FV_i t
    unfold FV, open.u: oterm
t: iterm
LN.FV (to_U_inv (LN.open t u)) ⊆ LN.FV u ∪ FV_i t
    rewrite to_U_iso_inv.u: oterm
t: iterm
LN.FV (LN.open t u) ⊆ LN.FV u ∪ FV_i t
    rewrite FV_open_upper.u: oterm
t: iterm
LN.FV u ∪ LN.FV t ⊆ LN.FV u ∪ FV_i t
    reflexivity.
  Qed.

  Theorem FV_open_lower : forall t u,
      FV u ⊆ FV (u '(t)).forall t u, FV u ⊆ FV (u '( t))
  Proof.forall t u, FV u ⊆ FV (u '( t))
    intros.t: iterm
u: oterm
FV u ⊆ FV (u '( t))
    unfold FV, open.t: iterm
u: oterm
LN.FV u ⊆ LN.FV (to_U_inv (LN.open t u))
    rewrite to_U_iso_inv.t: iterm
u: oterm
LN.FV u ⊆ LN.FV (LN.open t u)
    rewrite FV_open_lower.t: iterm
u: oterm
LN.FV (LN.open ?Goal0 u) ⊆ LN.FV (LN.open t u)
    reflexivity.
  Qed.

  Theorem FV_close : forall u x,
      FV ('[x] u) [=] FV u \\ {{ x }}.forall u x, FV ('[ x] u) [=] FV u \\ {{x}}
  Proof.forall u x, FV ('[ x] u) [=] FV u \\ {{x}}
    intros.u: oterm
x: atom
FV ('[ x] u) [=] FV u \\ {{x}}
    unfold FV, close.u: oterm
x: atom
LN.FV (to_U_inv (LN.close x u)) [=] LN.FV u \\ {{x}}
    rewrite to_U_iso_inv.u: oterm
x: atom
LN.FV (LN.close x u) [=] LN.FV u \\ {{x}}
    rewrite FV_close.u: oterm
x: atom
LN.FV u \\ {{x}} [=] LN.FV u \\ {{x}}
    reflexivity.
  Qed.

  Theorem nin_FV_close : forall u x,
      ~ x `in` FV ('[x] u).forall u x, x `notin` FV ('[ x] u)
  Proof.forall u x, x `notin` FV ('[ x] u)
    intros.u: oterm
x: atom
x `notin` FV ('[ x] u)
    unfold FV, close.u: oterm
x: atom
x `notin` LN.FV (to_U_inv (LN.close x u))
    rewrite to_U_iso_inv.u: oterm
x: atom
x `notin` LN.FV (LN.close x u)
    apply nin_FV_close.
  Qed.

  Theorem FV_close1 : forall u x y,
      y <> x ->
      y `in` FV ('[x] u) <-> y `in` FV u.forall u x y,
y <> x -> y `in` FV ('[ x] u) <-> y `in` FV u
  Proof.forall u x y,
y <> x -> y `in` FV ('[ x] u) <-> y `in` FV u
    intros.u: oterm
x, y: atom
H: y <> x
y `in` FV ('[ x] u) <-> y `in` FV u
    unfold close, FV.u: oterm
x, y: atom
H: y <> x
y `in` LN.FV (to_U_inv (LN.close x u)) <->
y `in` LN.FV u
    rewrite to_U_iso_inv.u: oterm
x, y: atom
H: y <> x
y `in` LN.FV (LN.close x u) <-> y `in` LN.FV u
    rewrite <- free_iff_FV.u: oterm
x, y: atom
H: y <> x
element_of y (LN.free (LN.close x u)) <->
y `in` LN.FV u
    rewrite in_free_close_iff.u: oterm
x, y: atom
H: y <> x
element_of y (LN.free u) /\ x <> y <-> y `in` LN.FV u
    rewrite <- free_iff_FV.u: oterm
x, y: atom
H: y <> x
element_of y (LN.free u) /\ x <> y <->
element_of y (LN.free u)
    intuition.
  Qed.

End MakeTheory_Hetero.

Module Type SyntaxSIG.
  Parameter (term : Type).
  Parameter (T : Type -> Type).
  Parameter
    (ret_inst : Return T)
    (binddt_inst : Binddt nat T T)
    (monad_inst : DecoratedTraversableMonad nat T
              (unit := Monoid_unit_zero)
              (op := Monoid_op_plus)).
  Parameter to_T:  term -> T LN.
  Parameter to_T_inv: T LN -> term.
  Parameter to_T_iso : forall (t : term), to_T_inv (to_T t) = t.
  Parameter to_T_iso_inv : forall (t : T LN), to_T (to_T_inv t) = t.
  Parameter from_atom: atom -> term.
  Parameter from_ix: nat -> term.
  Parameter from_atom_Ret:
    from_atom = to_T_inv ○ @ret T ret_inst LN ○ Fr.
  Parameter from_ix_Ret:
    from_ix = to_T_inv ○ @ret T ret_inst LN ○ Bd.
End SyntaxSIG.

Module Adapter (M1: SyntaxSIG) <: SyntaxSIGHetero.

  Definition iterm := M1.term.
  Definition oterm := M1.term.
  Definition T := M1.T.
  Definition U := M1.T.
  Definition ret_inst := M1.ret_inst.
  Definition binddt_T_inst := M1.binddt_inst.
  Definition binddt_U_inst := M1.binddt_inst.
  Definition module_inst :=
    @DerivedInstances.DecoratedTraversableRightModule_DecoratedTraversableMonad
      nat T _ _ M1.ret_inst M1.binddt_inst M1.monad_inst.
  Definition to_T := M1.to_T.
  Definition to_T_inv := M1.to_T_inv.
  Definition to_T_iso := M1.to_T_iso.
  Definition to_T_iso_inv := M1.to_T_iso_inv.
  Definition to_U := M1.to_T.
  Definition to_U_inv := M1.to_T_inv.
  Definition to_U_iso := M1.to_T_iso.
  Definition to_U_iso_inv := M1.to_T_iso_inv.
  Definition from_atom := M1.from_atom.
  Definition from_ix := M1.from_ix.
  Definition from_atom_Ret := M1.from_atom_Ret.
  Definition from_ix_Ret := M1.from_ix_Ret.

End Adapter.

Module MakeTheory (Syntax: SyntaxSIG) <:
    (TheorySIG with Definition iterm := Syntax.term
     with Definition oterm := Syntax.term).

  Module Syntax_Hetero <: SyntaxSIGHetero
  := Adapter Syntax.

  Module Theory <:
    (TheorySIG with Definition iterm := Syntax.term
     with Definition oterm := Syntax.term)
    := MakeTheory_Hetero Syntax_Hetero.

  Include Theory.

End MakeTheory.