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.