+++ /dev/null
-(*#* #stop file *)
-
-Require tlt_defs.
-Require lift_defs.
-
- Hint discr : ltlc := Extern 4 (lt (weight_map (wadd ? ?) (lift (S ?) ? ?)) (wadd ? ? ?))
- Simpl; Rewrite <- lift_weight_add_O.
-
- Hint discr : ltlc := Extern 4 (lt (weight_map ? (lift (0) (0) ?)) ?)
- Rewrite lift_r.
-
- Section lift_tlt_props. (*************************************************)
-
- Theorem lift_weight_map: (t:?; h,d:?; f:?)
- ((m:?) (le d m) -> (f m)=(0)) ->
- (weight_map f (lift h d t)) = (weight_map f t).
- XElim t; Intros.
-(* case 1: TSort *)
- XAuto.
-(* case 2: TLRef n *)
- Apply (lt_le_e n d); Intros.
-(* case 2.1: n < d *)
- Rewrite lift_lref_lt; XAuto.
-(* case 2.2: n >= d *)
- Rewrite lift_lref_ge; [ Simpl | XAuto ].
- Rewrite (H n); XAuto.
-(* case 3: TTail k *)
- XElim k; Intros; LiftTailRw; Simpl.
-(* case 3.1: Bind *)
- XElim b; [ Rewrite H; [ Idtac | XAuto ] | Idtac | Idtac ];
- Rewrite H0; Intros; Try (LeLtGen; Rewrite H2; Simpl); XAuto.
-(* case 3.2: Flat *)
- XAuto.
- Qed.
-
- Hints Resolve lift_weight_map : ltlc.
-
- Theorem lift_weight : (t:?; h,d:?) (weight (lift h d t)) = (weight t).
- Unfold weight; XAuto.
- Qed.
-
- Theorem lift_weight_add : (w:?; t:?; h,d:?; f,g:?)
- ((m:?) (lt m d) -> (g m) = (f m)) ->
- (g d) = w ->
- ((m:?) (le d m) -> (g (S m)) = (f m)) ->
- (weight_map f (lift h d t)) =
- (weight_map g (lift (S h) d t)).
- XElim t; Intros.
-(* case 1: TSort *)
- XAuto.
-(* case 2: TLRef *)
- Apply (lt_le_e n d); Intros.
-(* case 2.1: n < d *)
- Repeat Rewrite lift_lref_lt; Simpl; XAuto.
-(* case 2.2: n >= d *)
- Repeat Rewrite lift_lref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
-(* case 3: TTail k *)
- XElim k; Intros; LiftTailRw; Simpl.
-(* case 1 : bind b *)
- XElim b; Simpl;
- Apply (f_equal nat);
- (Apply (f_equal2 nat nat); [ XAuto | Idtac ]);
- ( Apply H0; Simpl; Intros; Try (LeLtGen; Rewrite H4; Simpl); XAuto).
-(* case 2 : Flat *)
- XAuto.
- Qed.
-
- Theorem lift_weight_add_O: (w:?; t:?; h:?; f:?)
- (weight_map f (lift h (0) t)) =
- (weight_map (wadd f w) (lift (S h) (0) t)).
- Intros.
- EApply lift_weight_add; XAuto.
- Intros; Inversion H.
- Qed.
-
- Theorem lift_tlt_dx: (k:?; u,t:?; h,d:?)
- (tlt t (TTail k u (lift h d t))).
- Unfold tlt; Intros.
- Rewrite <- (lift_weight t h d).
- Fold (tlt (lift h d t) (TTail k u (lift h d t))); XAuto.
- Qed.
-
- End lift_tlt_props.
-
- Hints Resolve lift_tlt_dx : ltlc.
-
-(*#* #single *)