From Tealeaves Require Export
  Examples.STLC.Syntax
  Backends.DB.

Import STLC.Syntax.TermNotations.
Import DB.Simplification.
Import DB.AutosubstShim.Notations.

(** * Simplification Tests for the De Bruijn Backend *)
(**********************************************************************)

(** ** Rewriting Lemmas for <<rename>> *)
(**********************************************************************)
Section rename.

  Context (ρ: nat -> nat).

  Theorem term_rename1: forall n,
      rename ρ (tvar n: Lam nat) = tvar (ρ n).
ρ: nat -> nat
forall n : nat,
rename ρ (tvar n : Lam nat) = tvar (ρ n)
  Proof.
ρ: nat -> nat
forall n : nat,
rename ρ (tvar n : Lam nat) = tvar (ρ n)
    intros.
ρ: nat -> nat
n: nat
rename ρ (tvar n : Lam nat) = tvar (ρ n)
    simplify_rename.
ρ: nat -> nat
n: nat
ret (ρ n) = ret (ρ n)
    conclude.
  Qed.

  Theorem term_rename2: forall (t1 t2: Lam nat) (n: nat),
      rename ρ (app t1 t2: Lam nat) = app (rename ρ t1) (rename ρ t2).
ρ: nat -> nat
forall t1 t2 : Lam nat,
nat ->
rename ρ (⟨ t1 ⟩ (t2) : Lam nat) =
(⟨ rename ρ t1 ⟩ (rename ρ t2))
  Proof.
ρ: nat -> nat
forall t1 t2 : Lam nat,
nat ->
rename ρ (⟨ t1 ⟩ (t2) : Lam nat) =
(⟨ rename ρ t1 ⟩ (rename ρ t2))
    intros.
ρ: nat -> nat
t1, t2: Lam nat
n: nat
rename ρ (⟨ t1 ⟩ (t2) : Lam nat) =
(⟨ rename ρ t1 ⟩ (rename ρ t2))
    simplify_rename.
ρ: nat -> nat
t1, t2: Lam nat
n: nat
(⟨ rename ρ t1 ⟩ (rename ρ t2)) =
(⟨ rename ρ t1 ⟩ (rename ρ t2))
    conclude.
  Qed.

  Theorem term_rename3: forall (τ: typ) (t: Lam nat),
      rename ρ (lam τ t: Lam nat) = lam τ (rename (up__ren ρ) t).
ρ: nat -> nat
forall (τ : typ) (t : Lam nat),
rename ρ ((λ) τ t : Lam nat) =
(λ) τ (rename (up__ren ρ) t)
  Proof.
ρ: nat -> nat
forall (τ : typ) (t : Lam nat),
rename ρ ((λ) τ t : Lam nat) =
(λ) τ (rename (up__ren ρ) t)
    intros.
ρ: nat -> nat
τ: typ
t: Lam nat
rename ρ ((λ) τ t : Lam nat) =
(λ) τ (rename (up__ren ρ) t)
    simplify_rename.
ρ: nat -> nat
τ: typ
t: Lam nat
(λ) τ (rename (up__ren ρ) t) =
(λ) τ (rename (up__ren ρ) t)
    conclude.
  Qed.

End rename.

Section subst.

  Context (σ: nat -> Lam nat).

  Theorem term_subst1: forall n,
      subst σ (tvar n: Lam nat) = σ n.
σ: nat -> Lam nat
forall n : nat, (tvar n : Lam nat).[σ] = σ n
  Proof.
σ: nat -> Lam nat
forall n : nat, (tvar n : Lam nat).[σ] = σ n
    intros.
σ: nat -> Lam nat
n: nat
(tvar n : Lam nat).[σ] = σ n
    simplify_subst.
σ: nat -> Lam nat
n: nat
σ n = σ n
    conclude.
  Qed.

  Theorem term_subst2: forall (t1 t2: Lam nat),
      subst σ (app t1 t2: Lam nat) = app (subst σ t1) (subst σ t2).
σ: nat -> Lam nat
forall t1 t2 : Lam nat,
(⟨ t1 ⟩ (t2) : Lam nat).[σ] = (⟨ t1.[σ] ⟩ (t2.[σ]))
  Proof.
σ: nat -> Lam nat
forall t1 t2 : Lam nat,
(⟨ t1 ⟩ (t2) : Lam nat).[σ] = (⟨ t1.[σ] ⟩ (t2.[σ]))
    intros.
σ: nat -> Lam nat
t1, t2: Lam nat
(⟨ t1 ⟩ (t2) : Lam nat).[σ] = (⟨ t1.[σ] ⟩ (t2.[σ]))
    simplify_subst.
σ: nat -> Lam nat
t1, t2: Lam nat
(⟨ t1.[σ] ⟩ (t2.[σ])) = (⟨ t1.[σ] ⟩ (t2.[σ]))
    conclude.
  Qed.

  Theorem term_subst3: forall (τ: typ) (t: Lam nat),
      subst σ (lam τ t: Lam nat) = lam τ (subst (up__sub σ) t).
σ: nat -> Lam nat
forall (τ : typ) (t : Lam nat),
((λ) τ t : Lam nat).[σ] = (λ) τ t.[up__sub σ]
  Proof.
σ: nat -> Lam nat
forall (τ : typ) (t : Lam nat),
((λ) τ t : Lam nat).[σ] = (λ) τ t.[up__sub σ]
    intros.
σ: nat -> Lam nat
τ: typ
t: Lam nat
((λ) τ t : Lam nat).[σ] = (λ) τ t.[up__sub σ]
    simplify_subst.
σ: nat -> Lam nat
τ: typ
t: Lam nat
(λ) τ t.[up__sub σ] = (λ) τ t.[up__sub σ]
    conclude.
  Qed.

End subst.

(** ** Rewriting Lemmas for <<subst>> *)
(**********************************************************************)
Section subst.

  Context (σ: nat -> Lam nat).

  Goal subst ret = id.
σ: nat -> Lam nat
subst ret = id
  Proof.
σ: nat -> Lam nat
subst ret = id
    simplify_db.
σ: nat -> Lam nat
id = id
    conclude.
  Qed.

  Goal forall t, subst ret t = t.
σ: nat -> Lam nat
forall t : Lam nat, t.[ret] = t
  Proof.
σ: nat -> Lam nat
forall t : Lam nat, t.[ret] = t
    intros.
σ: nat -> Lam nat
t: Lam nat
t.[ret] = t
    simplify_db.
σ: nat -> Lam nat
t: Lam nat
t = t
    conclude.
  Qed.

  Goal forall (t1 t2: Lam nat),
      subst σ (app t1 t2) =
        app (subst σ t1) (subst σ t2).
σ: nat -> Lam nat
forall t1 t2 : Lam nat,
(⟨ t1 ⟩ (t2)).[σ] = (⟨ t1.[σ] ⟩ (t2.[σ]))
  Proof.
σ: nat -> Lam nat
forall t1 t2 : Lam nat,
(⟨ t1 ⟩ (t2)).[σ] = (⟨ t1.[σ] ⟩ (t2.[σ]))
    intros.
σ: nat -> Lam nat
t1, t2: Lam nat
(⟨ t1 ⟩ (t2)).[σ] = (⟨ t1.[σ] ⟩ (t2.[σ]))
    simplify_db.
σ: nat -> Lam nat
t1, t2: Lam nat
(⟨ t1.[σ] ⟩ (t2.[σ])) = (⟨ t1.[σ] ⟩ (t2.[σ]))
    conclude.
  Qed.

  Goal forall (τ: typ) (t: Lam nat),
      subst σ (lam τ t: Lam nat) = lam τ (subst (up__sub σ) t).
σ: nat -> Lam nat
forall (τ : typ) (t : Lam nat),
((λ) τ t : Lam nat).[σ] = (λ) τ t.[up__sub σ]
  Proof.
σ: nat -> Lam nat
forall (τ : typ) (t : Lam nat),
((λ) τ t : Lam nat).[σ] = (λ) τ t.[up__sub σ]
    intros.
σ: nat -> Lam nat
τ: typ
t: Lam nat
((λ) τ t : Lam nat).[σ] = (λ) τ t.[up__sub σ]
    simplify_db_like_autosubst.
σ: nat -> Lam nat
τ: typ
t: Lam nat
(λ) τ t.[ret 0 .: σ >>> subst ((+1) >>> ret)] =
(λ) τ t.[ret 0 .: σ >>> subst ((+1) >>> ret)]
    conclude.
  Qed.

End subst.