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

   1 Require lift_props.
   2 Require subst0_lift.
   3 Require pr0_defs.
   4
   5 (*#* #caption "main properties of the relation $\\PrZ{}{}$" *)
   6 (*#* #clauses pr0_props *)
   7
   8 (*#* #stop file *)
   9
  10    Section pr0_lift. (*******************************************************)
  11
  12 (*#* #caption "conguence with lift" *)
  13 (*#* #cap #cap t1,t2 #alpha d in i *)
  14
  15       Theorem pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
  16                         (h,d:?) (pr0 (lift h d t1) (lift h d t2)).
  17
  18       Intros until 1; XElim H; Intros.
  19 (* case 1: pr0_refl *)
  20       XAuto.
  21 (* case 2: pr0_cong *)
  22       LiftTailRw; XAuto.
  23 (* case 3 : pr0_beta *)
  24       LiftTailRw; XAuto.
  25 (* case 4: pr0_upsilon *)
  26       LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
  27 (* case 5: pr0_delta *)
  28       LiftTailRw; Simpl.
  29       EApply pr0_delta; [ XAuto | Apply H2 | Idtac ].
  30       LetTac d' := (S d); Arith10 d; Unfold d'; XAuto.
  31 (* case 6: pr0_zeta *)
  32       LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
  33 (* case 7: pr0_epsilon *)
  34       LiftTailRw; XAuto.
  35       Qed.
  36
  37    End pr0_lift.
  38
  39       Hints Resolve pr0_lift : ltlc.