contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst1_gen.v b/helm/coq-contribs/LAMBDA-TYPES/subst1_gen.v
new file mode 100644 (file)
index 0000000..0b2d4a1
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst1_gen.v
@@ -0,0 +1,44 @@
+(*#* #stop file *)
+
+Require subst0_gen.
+Require subst1_defs.
+
+   Section subst1_gen_lift. (************************************************)
+
+      Theorem subst1_gen_lift_lt : (u,t1,x:?; i,h,d:?) (subst1 i (lift h d u) (lift h (S (plus i d)) t1) x) ->
+                                   (EX t2 | x = (lift h (S (plus i d)) t2) & (subst1 i u t1 t2)).
+      Intros; XElim H; Clear x; Intros;
+      Try Subst0Gen; XEAuto.
+      Qed.
+
+      Theorem subst1_gen_lift_eq : (t,u,x:?; h,d,i:?)
+                                   (le d i) -> (lt i (plus d h)) ->
+                                   (subst1 i u (lift h d t) x) ->
+                                   x = (lift h d t).
+      Intros; XElim H1; Clear x; Intros;
+      Try Subst0Gen; XAuto.
+      Qed.
+
+      Theorem subst1_gen_lift_ge : (u,t1,x:?; i,h,d:?) (subst1 i u (lift h d t1) x) ->
+                                   (le (plus d h) i) ->
+                                   (EX t2 | x = (lift h d t2) & (subst1 (minus i h) u t1 t2)).
+      Intros; XElim H; Clear x; Intros;
+      Try Subst0Gen; XEAuto.
+      Qed.
+
+   End subst1_gen_lift.
+
+      Tactic Definition Subst1Gen :=
+         Match Context With
+            | [ H: (subst1 ?0 (lift ?1 ?2 ?3) (lift ?1 (S (plus ?0 ?2)) ?4) ?5) |- ? ] ->
+               LApply (subst1_gen_lift_lt ?3 ?4 ?5 ?0 ?1 ?2); [ Clear H; Intros H | XAuto ];
+               XElim H; Intros
+            | [ H: (subst1 ?0 ?1 (lift (1) ?0 ?2) ?3) |- ? ] ->
+               LApply (subst1_gen_lift_eq ?2 ?1 ?3 (1) ?0 ?0); [ Intros H_x | XAuto ];
+               LApply H_x; [ Clear H_x; Intros H_x | Rewrite plus_sym; XAuto ];
+               LApply H_x; [ Clear H H_x; Intros | XAuto ]
+            | [ H0: (subst1 ?0 ?1 (lift (1) ?4 ?2) ?3); H1: (lt ?4 ?0) |- ? ] ->
+               LApply (subst1_gen_lift_ge ?1 ?2 ?3 ?0 (1) ?4); [ Clear H0; Intros H0 | XAuto ];
+               LApply H0; [ Clear H0; Intros H0 | Rewrite plus_sym; XAuto ];
+               XElim H0; Intros
+            | _ -> Subst1GenBase.