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

   1 (*#* #stop file *)
   2
   3 Require lift_defs.
   4
   5    Section lift_props. (*****************************************************)
   6
   7       Theorem lift_free: (t:?; h,k,d,e:?) (le e (plus d h)) -> (le d e) ->
   8                          (lift k e (lift h d t)) = (lift (plus k h) d t).
   9       XElim t; Intros.
  10 (* case 1: TSort *)
  11       Repeat Rewrite lift_sort; XAuto.
  12 (* case 2: TLRef n *)
  13       Apply (lt_le_e n d); Intros.
  14 (* case 2.1: n < d *)
  15       Repeat Rewrite lift_lref_lt; XEAuto.
  16 (* case 2.2: n >= d *)
  17       Repeat Rewrite lift_lref_ge; XEAuto.
  18 (* case 3: TTail k *)
  19       LiftTailRw; XAuto.
  20       Qed.
  21
  22       Theorem lift_d : (t:?; h,k,d,e:?) (le e d) ->
  23                        (lift h (plus k d) (lift k e t)) = (lift k e (lift h d t)).
  24       XElim t; Intros.
  25 (* case 1: TSort *)
  26       Repeat Rewrite lift_sort; XAuto.
  27 (* case 2: TLRef n *)
  28       Apply (lt_le_e n e); Intros.
  29 (* case 2.1: n < e *)
  30       Cut (lt n d); Intros; Repeat Rewrite lift_lref_lt; XEAuto.
  31 (* case 2.2: n >= e *)
  32       Rewrite lift_lref_ge; [ Idtac | XAuto ].
  33       Rewrite plus_sym; Apply (lt_le_e n d); Intros.
  34 (* case 2.2.1: n < d *)
  35       Do 2 (Rewrite lift_lref_lt; [ Idtac | XAuto ]).
  36       Rewrite lift_lref_ge; XAuto.
  37 (* case 2.2.2: n >= d *)
  38       Repeat Rewrite lift_lref_ge; XAuto.
  39 (* case 3: TTail k *)
  40       LiftTailRw; SRw; XAuto.
  41       Qed.
  42
  43    End lift_props.