helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v

   1 (*#* #stop file *)
   2
   3 Require tlt_defs.
   4 Require lift_tlt.
   5 Require subst0_defs.
   6
   7    Section subst0_tlt_props. (***********************************************)
   8
   9       Theorem subst0_weight_le : (u,t,z:?; d:?) (subst0 d u t z) ->
  10                                  (f,g:?) ((m:?) (le (f m) (g m))) ->
  11                                  (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
  12                                  (le (weight_map f z) (weight_map g t)).
  13       Intros until 1; XElim H.
  14 (* case 1: subst0_lref *)
  15       Intros; XAuto.
  16 (* case 2: subst0_fst *)
  17       XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
  18 (* case 3: subst0_snd *)
  19       XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
  20 (* case 4: subst0_both *)
  21       XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
  22       Qed.
  23
  24       Theorem subst0_weight_lt : (u,t,z:?; d:?) (subst0 d u t z) -> (f,g:?)
  25                                  ((m:?) (le (f m) (g m))) ->
  26                                  (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
  27                                  (lt (weight_map f z) (weight_map g t)).
  28       Intros until 1; XElim H.
  29 (* case 1: subst0_lref *)
  30       Intros; XAuto.
  31 (* case 2: subst0_fst *)
  32       XElim k; [ XElim b | Idtac ]; Simpl; Intros;
  33       Apply lt_n_S; (Apply lt_le_plus_plus; [ XAuto | Idtac ]); (**)
  34       [ Auto 6 with ltlc (**) | XAuto | XAuto | XAuto ].
  35 (* case 3: subst0_snd *)
  36       XElim k; [ XElim b | Idtac ]; Simpl;
  37       [ Auto 8 with ltlc | Auto 6 with ltlc | Auto 6 with ltlc | XAuto ]. (**)
  38 (* case 3: subst0_both *)
  39       XElim k; [ XElim b | Idtac ]; Simpl;
  40       Intros; Apply lt_n_S; [ Apply lt_le_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus ]; XAuto.
  41       EApply subst0_weight_le; [ XEAuto | XAuto | XAuto ].
  42       Qed.
  43
  44       Theorem subst0_tlt_tail: (u,t,z:?) (subst0 (0) u t z) ->
  45                                (tlt (TTail (Bind Abbr) u z)
  46                                     (TTail (Bind Abbr) u t)
  47                                ).
  48       Unfold tlt weight; Intros; Simpl.
  49       Apply lt_n_S; Apply le_lt_plus_plus; [ XAuto | Idtac ].
  50       EApply subst0_weight_lt; [ XEAuto | XAuto | XAuto ].
  51       Qed.
  52
  53       Theorem subst0_tlt: (u,t,z:?) (subst0 (0) u t z) ->
  54                           (tlt z (TTail (Bind Abbr) u t)).
  55       Intros.
  56       EApply tlt_trans; [ Idtac | Apply subst0_tlt_tail; XEAuto].
  57       XAuto.
  58       Qed.
  59
  60    End subst0_tlt_props.
  61
  62       Hints Resolve subst0_tlt : ltlc.