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

   1 (*#* #stop file *)
   2
   3 Require lift_props.
   4 Require subst0_defs.
   5
   6    Section subst0_lift. (****************************************************)
   7
   8       Theorem subst0_lift_lt : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
   9                                (d:?) (lt i d) -> (h:?)
  10                                (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
  11        Intros until 1; XElim H; Intros.
  12 (* case 1: subst0_bref *)
  13        Rewrite lift_bref_lt; [ Idtac | XAuto ].
  14        LetTac w := (minus d (S i0)).
  15        Arith8 d '(S i0); Rewrite lift_d; XAuto.
  16 (* case 2: subst0_fst *)
  17        LiftTailRw; XAuto.
  18 (* case 3: subst0_snd *)
  19        SRwBackIn H0; LiftTailRw; Rewrite <- (minus_s_s k); XAuto.
  20 (* case 4: subst0_both *)
  21        SRwBackIn H2; LiftTailRw.
  22        Apply subst0_both; [ Idtac | Rewrite <- (minus_s_s k) ]; XAuto.
  23        Qed.
  24
  25       Theorem subst0_lift_ge : (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
  26                                (d:?) (le d i) ->
  27                                (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
  28       Intros until 1; XElim H; Intros.
  29 (* case 1: subst0_bref *)
  30       Rewrite lift_bref_ge; [ Idtac | XAuto ].
  31       Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
  32       Arith5'c h i0; XAuto.
  33 (* case 2: subst0_fst *)
  34       LiftTailRw; XAuto.
  35 (* case 3: subst0_snd *)
  36       SRwBackIn H0; LiftTailRw; XAuto.
  37 (* case 4: subst0_snd *)
  38       SRwBackIn H2; LiftTailRw; XAuto.
  39       Qed.
  40
  41       Theorem subst0_lift_ge_S : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
  42                                  (d:?) (le d i) -> (b:?)
  43                                  (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
  44       Intros; Simpl; Arith7 i; Apply subst0_lift_ge; XAuto.
  45       Qed.
  46
  47    End subst0_lift.
  48
  49       Hints Resolve subst0_lift_lt subst0_lift_ge subst0_lift_ge_S : ltlc.