contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v
new file mode 100644 (file)
index 0000000..5c9c2e5
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v
@@ -0,0 +1,55 @@
+(*#* #stop file *)
+
+Require Export lift_defs.
+
+      Inductive subst0 : nat -> T -> T -> T -> Prop :=
+         | subst0_bref : (v:?; i:?) (subst0 i v (TBRef i) (lift (S i) (0) v))
+         | subst0_fst  : (v,w,u:?; i:?) (subst0 i v u w) ->
+                         (t:?; k:?) (subst0 i v (TTail k u t) (TTail k w t))
+         | subst0_snd  : (k:?; v,w,t:?; i:?) (subst0 (s k i) v t w) -> (u:?)
+                         (subst0 i v (TTail k u t) (TTail k u w))
+         | subst0_both : (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
+                         (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
+                         (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
+
+      Hint subst0 : ltlc := Constructors subst0.
+
+   Section subst0_gen_base. (************************************************)
+
+      Theorem subst0_gen_sort : (v,x:?; i,n:?) (subst0 i v (TSort n) x) ->
+                                (P:Prop) P.
+      Intros; Inversion H.
+      Qed.
+
+      Theorem subst0_gen_bref : (v,x:?; i,n:?) (subst0 i v (TBRef n) x) ->
+                                n = i /\ x = (lift (S n) (0) v).
+      Intros; Inversion H; XAuto.
+      Qed.
+
+      Theorem subst0_gen_tail : (k:?; v,u1,t1,x:?; i:?)
+                                (subst0 i v (TTail k u1 t1) x) -> (OR
+                                (EX u2 | x = (TTail k u2 t1) &
+                                        (subst0 i v u1 u2)) |
+                                (EX t2 | x = (TTail k u1 t2) &
+                                         (subst0 (s k i) v t1 t2)) |
+                                (EX u2 t2 | x = (TTail k u2 t2) &
+                                            (subst0 i v u1 u2) &
+                                            (subst0 (s k i) v t1 t2))
+                                ).
+
+      Intros; Inversion H; XEAuto.
+      Qed.
+
+   End subst0_gen_base.
+
+      Tactic Definition Subst0GenBase :=
+         Match Context With
+            | [ H: (subst0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
+               Apply (subst0_gen_sort ?2 ?4 ?1 ?3); Apply H
+            | [ H: (subst0 ?1 ?2 (TBRef ?3) ?4) |- ? ] ->
+               LApply (subst0_gen_bref ?2 ?4 ?1 ?3); [ Clear H; Intros H | XAuto ];
+               XElim H; Intros
+            | [ H: (subst0 ?1 ?2 (TTail ?3 ?4 ?5) ?6) |- ? ] ->
+               LApply (subst0_gen_tail ?3 ?2 ?4 ?5 ?6 ?1); [ Clear H; Intros H | XAuto ];
+               XElim H; Intros H; XElim H; Intros.
+