(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require lift_props. Require subst0_defs. Section subst0_lift. (****************************************************) Lemma subst0_lift_lt: (t1,t2,u:?; i:?) (subst0 i u t1 t2) -> (d:?) (lt i d) -> (h:?) (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)). Proof. Intros until 1; XElim H; Intros. (* case 1: subst0_lref *) Rewrite lift_lref_lt; [ Idtac | XAuto ]. LetTac w := (minus d (S i0)). Arith8 d '(S i0); Rewrite lift_d; XAuto. (* case 2: subst0_fst *) LiftHeadRw; XAuto. (* case 3: subst0_snd *) SRwBackIn H0; LiftHeadRw; Rewrite <- (minus_s_s k); XAuto. (* case 4: subst0_both *) SRwBackIn H2; LiftHeadRw. Apply subst0_both; [ Idtac | Rewrite <- (minus_s_s k) ]; XAuto. Qed. Lemma subst0_lift_ge: (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) -> (d:?) (le d i) -> (subst0 (plus i h) u (lift h d t1) (lift h d t2)). Proof. Intros until 1; XElim H; Intros. (* case 1: subst0_lref *) Rewrite lift_lref_ge; [ Idtac | XAuto ]. Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ]. Arith5'c h i0; XAuto. (* case 2: subst0_fst *) LiftHeadRw; XAuto. (* case 3: subst0_snd *) SRwBackIn H0; LiftHeadRw; XAuto. (* case 4: subst0_snd *) SRwBackIn H2; LiftHeadRw; XAuto. Qed. Lemma subst0_lift_ge_S: (t1,t2,u:?; i:?) (subst0 i u t1 t2) -> (d:?) (le d i) -> (subst0 (S i) u (lift (1) d t1) (lift (1) d t2)). Proof. Intros; Arith7 i; Apply subst0_lift_ge; XAuto. Qed. Lemma subst0_lift_ge_s: (t1,t2,u:?; i:?) (subst0 i u t1 t2) -> (d:?) (le d i) -> (b:?) (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)). Proof. Intros; Simpl; Apply subst0_lift_ge_S; XAuto. Qed. End subst0_lift. Hints Resolve subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s : ld.