contribution about \lambda-\delta

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / subst0_lift.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v
new file mode 100644 (file)
index 0000000..d4ce741
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v
@@ -0,0 +1,49 @@
+(*#* #stop file *)
+
+Require lift_props.
+Require subst0_defs.
+
+   Section subst0_lift. (****************************************************)
+
+      Theorem subst0_lift_lt : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+                               (d:?) (lt i d) -> (h:?)
+                               (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
+       Intros until 1; XElim H; Intros.
+(* case 1: subst0_bref *)
+       Rewrite lift_bref_lt; [ Idtac | XAuto ].
+       LetTac w := (minus d (S i0)).
+       Arith8 d '(S i0); Rewrite lift_d; XAuto.
+(* case 2: subst0_fst *)
+       LiftTailRw; XAuto.
+(* case 3: subst0_snd *)
+       SRwBackIn H0; LiftTailRw; Rewrite <- (minus_s_s k); XAuto.
+(* case 4: subst0_both *)
+       SRwBackIn H2; LiftTailRw.
+       Apply subst0_both; [ Idtac | Rewrite <- (minus_s_s k) ]; XAuto.
+       Qed.
+
+      Theorem subst0_lift_ge : (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
+                               (d:?) (le d i) ->
+                               (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
+      Intros until 1; XElim H; Intros.
+(* case 1: subst0_bref *)
+      Rewrite lift_bref_ge; [ Idtac | XAuto ].
+      Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
+      Arith5'c h i0; XAuto.
+(* case 2: subst0_fst *)
+      LiftTailRw; XAuto.
+(* case 3: subst0_snd *)
+      SRwBackIn H0; LiftTailRw; XAuto.
+(* case 4: subst0_snd *)
+      SRwBackIn H2; LiftTailRw; XAuto.
+      Qed.
+
+      Theorem subst0_lift_ge_S : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+                                 (d:?) (le d i) -> (b:?)
+                                 (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
+      Intros; Simpl; Arith7 i; Apply subst0_lift_ge; XAuto.
+      Qed.
+
+   End subst0_lift.
+
+      Hints Resolve subst0_lift_lt subst0_lift_ge subst0_lift_ge_S : ltlc.