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

   1 (*#* #stop file *)
   2
   3 Require tlt_defs.
   4 Require lift_defs.
   5
   6       Hint discr : ltlc := Extern 4 (lt (weight_map (wadd ? ?) (lift (S ?) ? ?)) (wadd ? ? ?))
   7                            Simpl; Rewrite <- lift_weight_add_O.
   8
   9       Hint discr : ltlc := Extern 4 (lt (weight_map ? (lift (0) (0) ?)) ?)
  10                            Rewrite lift_r.
  11
  12    Section lift_tlt_props. (*************************************************)
  13
  14       Theorem lift_weight_map: (t:?; h,d:?; f:?)
  15                                ((m:?) (le d m) -> (f m)=(0)) ->
  16                                (weight_map f (lift h d t)) = (weight_map f t).
  17       XElim t; Intros.
  18 (* case 1: TSort *)
  19       XAuto.
  20 (* case 2: TLRef n *)
  21       Apply (lt_le_e n d); Intros.
  22 (* case 2.1: n < d *)
  23       Rewrite lift_lref_lt; XAuto.
  24 (* case 2.2: n >= d *)
  25       Rewrite lift_lref_ge; [ Simpl | XAuto ].
  26       Rewrite (H n); XAuto.
  27 (* case 3: TTail k *)
  28       XElim k; Intros; LiftTailRw; Simpl.
  29 (* case 3.1: Bind *)
  30       XElim b; [ Rewrite H; [ Idtac | XAuto ] | Idtac | Idtac ];
  31       Rewrite H0; Intros; Try (LeLtGen; Rewrite H2; Simpl); XAuto.
  32 (* case 3.2: Flat *)
  33       XAuto.
  34       Qed.
  35
  36       Hints Resolve lift_weight_map : ltlc.
  37
  38       Theorem lift_weight : (t:?; h,d:?) (weight (lift h d t)) = (weight t).
  39       Unfold weight; XAuto.
  40       Qed.
  41
  42       Theorem lift_weight_add : (w:?; t:?; h,d:?; f,g:?)
  43                                 ((m:?) (lt m d) -> (g m) = (f m)) ->
  44                                 (g d) = w ->
  45                                 ((m:?) (le d m) -> (g (S m)) = (f m)) ->
  46                                 (weight_map f (lift h d t)) =
  47                                 (weight_map g (lift (S h) d t)).
  48       XElim t; Intros.
  49 (* case 1: TSort *)
  50       XAuto.
  51 (* case 2: TLRef *)
  52       Apply (lt_le_e n d); Intros.
  53 (* case 2.1: n < d *)
  54       Repeat Rewrite lift_lref_lt; Simpl; XAuto.
  55 (* case 2.2: n >= d *)
  56       Repeat Rewrite lift_lref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
  57 (* case 3: TTail k *)
  58       XElim k; Intros; LiftTailRw; Simpl.
  59 (* case 1 : bind b *)
  60       XElim b; Simpl;
  61       Apply (f_equal nat);
  62       (Apply (f_equal2 nat nat); [ XAuto | Idtac ]);
  63       ( Apply H0; Simpl; Intros; Try (LeLtGen; Rewrite H4; Simpl); XAuto).
  64 (* case 2 : Flat *)
  65       XAuto.
  66       Qed.
  67
  68       Theorem lift_weight_add_O: (w:?; t:?; h:?; f:?)
  69                                  (weight_map f (lift h (0) t)) =
  70                                  (weight_map (wadd f w) (lift (S h) (0) t)).
  71       Intros.
  72       EApply lift_weight_add; XAuto.
  73       Intros; Inversion H.
  74       Qed.
  75
  76       Theorem lift_tlt_dx: (k:?; u,t:?; h,d:?)
  77                            (tlt t (TTail k u (lift h d t))).
  78       Unfold tlt; Intros.
  79       Rewrite <- (lift_weight t h d).
  80       Fold (tlt (lift h d t) (TTail k u (lift h d t))); XAuto.
  81       Qed.
  82
  83    End lift_tlt_props.
  84
  85       Hints Resolve lift_tlt_dx : ltlc.
  86
  87 (*#* #single *)