(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require tlt_defs. Require lift_tlt. Require subst0_defs. Section subst0_tlt_props. (***********************************************) Hints Resolve le_S_n : ld. Hint discr : ld := Extern 4 (lt (weight_map (wadd ? ?) (lift (S ?) ? ?)) (wadd ? ? ?)) Simpl; Rewrite <- lift_weight_add_O. Lemma subst0_weight_le: (u,t,z:?; d:?) (subst0 d u t z) -> (f,g:?) ((m:?) (le (f m) (g m))) -> (lt (weight_map f (lift (S d) (0) u)) (g d)) -> (le (weight_map f z) (weight_map g t)). Proof. Intros until 1; XElim H. (* case 1: subst0_lref *) Intros; XAuto. (* case 2: subst0_fst *) XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ld (**) | XAuto | XAuto | XAuto ]. (* case 3: subst0_snd *) XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ld (**) | XAuto | XAuto | XAuto ]. (* case 4: subst0_both *) XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ld (**) | XAuto | XAuto | XAuto ]. Qed. Lemma subst0_weight_lt: (u,t,z:?; d:?) (subst0 d u t z) -> (f,g:?) ((m:?) (le (f m) (g m))) -> (lt (weight_map f (lift (S d) (0) u)) (g d)) -> (lt (weight_map f z) (weight_map g t)). Proof. Intros until 1; XElim H. (* case 1: subst0_lref *) Intros; XAuto. (* case 2: subst0_fst *) XElim k; [ XElim b | Idtac ]; Simpl; Intros; Apply lt_n_S; (Apply lt_le_plus_plus; [ XAuto | Idtac ]); (**) [ Auto 6 with ld (**) | XAuto | XAuto | XAuto ]. (* case 3: subst0_snd *) XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 8 with ld | Auto 6 with ld | Auto 6 with ld | XAuto ]. (**) (* case 3: subst0_both *) XElim k; [ XElim b | Idtac ]; Simpl; Intros; Apply lt_n_S; [ Apply lt_le_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus ]; XAuto. EApply subst0_weight_le; [ XDEAuto 2 | XAuto | XAuto ]. Qed. Hint discr : ld := Extern 4 (lt (weight_map ? (lift (0) (0) ?)) ?) Rewrite lift_r. Lemma subst0_tlt_head: (u,t,z:?) (subst0 (0) u t z) -> (tlt (THead (Bind Abbr) u z) (THead (Bind Abbr) u t) ). Proof. Unfold tlt weight; Intros; Simpl. Apply lt_n_S; Apply le_lt_plus_plus; [ XAuto | Idtac ]. EApply subst0_weight_lt; [ XDEAuto 2 | XAuto | XAuto ]. Qed. Lemma subst0_tlt: (u,t,z:?) (subst0 (0) u t z) -> (tlt z (THead (Bind Abbr) u t)). Proof. Intros. EApply tlt_trans; [ Idtac | Apply subst0_tlt_head; XDEAuto 2 ]. XAuto. Qed. End subst0_tlt_props.