(****************************************************************************) (* *) (* 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_lift. Require subst1_defs. Section subst1_lift. (****************************************************) Lemma subst1_lift_lt: (t1,t2,u:?; i:?) (subst1 i u t1 t2) -> (d:?) (lt i d) -> (h:?) (subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)). Proof. Intros until 1; XElim H; Clear t2; XAuto. Qed. Lemma subst1_lift_ge: (t1,t2,u:?; i,h:?) (subst1 i u t1 t2) -> (d:?) (le d i) -> (subst1 (plus i h) u (lift h d t1) (lift h d t2)). Proof. Intros until 1; XElim H; Clear t2; XAuto. Qed. Hint discr : ld := Extern 4 (subst1 ? ? ? ?) Rewrite lift_sort. Hint discr : ld := Extern 4 (subst1 ? ? ? ?) Rewrite lift_lref_lt. Hint discr : ld := Extern 4 (subst1 ? ? ? ?) Rewrite lift_lref_gt. Hint discr : ld := Extern 4 (subst1 ? ? ? ?) Rewrite lift_free; Simpl. Hint discr : ld := Extern 4 (subst1 ? ? ? ?) Rewrite lift_head. Lemma subst1_ex: (u,t1:?; d:?) (EX t2 | (subst1 d u t1 (lift (1) d t2))). Proof. XElim t1; Intros. (* case 1: TSort *) XDEAuto 3. (* case 2: TLRef n *) Apply (lt_eq_gt_e n d); Intros; Subst; XDEAuto 4. (* case 2: THead k *) XDecomPose '(H d); XDecomPose '(H0 (s k d)); XDEAuto 4. Qed. Hints Resolve le_S_n le_trans : ld. Lemma subst1_lift_S: (u:?; i,h:?) (le h i) -> (subst1 i (TLRef h) (lift (S h) (S i) u) (lift (S h) i u) ). Proof. XElim u; Intros. (* case 1: TSort *) Repeat Rewrite lift_sort; XAuto. (* case 2: TLRef n *) Apply (lt_eq_gt_e n i); Intros; Subst. (* case 2.1: n < i *) Repeat Rewrite lift_lref_lt; XAuto. (* case 2.1: n = i *) Rewrite lift_lref_lt; [ Idtac | XAuto ]. Rewrite lift_lref_ge; [ Idtac | XAuto ]. Arith11 n h. Rewrite <- lift_lref_ge with d:=O; XAuto. (* case 2.1: n > i *) Repeat Rewrite lift_lref_ge; XAuto. (* case 3: Thead k *) Repeat Rewrite lift_head. Apply subst1_head; SRw; XDEAuto 3. Qed. End subst1_lift. Hints Resolve subst1_lift_lt subst1_lift_ge : ld.