Library Subst

Require Export Equality.

Internalized Substitution


Definition Subst := R (.\"Subst", "s", "k", "u"; "s" (.\"n"; !EqN "n" "k" "u" (!Var "n"))
                                                     (.\"s1", "s2"; !App ("Subst" "s1" "k" "u") ("Subst" "s2" "k" "u"))
                                                     (.\"s1"; !Lam ("Subst" "s1" (!Succ "k") "u")) ).


Lemma Subst_correct s k u :
  Subst (tenc s) (enc k) (tenc u) == tenc (subst s k u).

Proof.

  revert k u; induction s; intros k u.

  - transitivity (EqN (enc n) (enc k) (tenc u) (Var (enc n))).
crush.
    destruct (EqN_correct n k) as [[A H] | [A H]].

    + subst.
rewrite H.
      simpl.
decide (k = k). crush. tauto.
    + simpl.
decide (n = k); try omega.
      rewrite H.
crush.
  - transitivity (App ((((lam (Subst #0)) (tenc s1)) (enc k)) (tenc u)) ((((lam (Subst #0)) (tenc s2)) (enc k)) (tenc u))).
crush.
    cbv; now rewrite !Eta, IHs1, IHs2; value; crush.

  - transitivity (Lam ((((lam (Subst #0)) (tenc s)) (Succ (enc k))) (tenc u))).
crush.
    rewrite Eta, Succ_correct, IHs; value.
crush.
Qed.