contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
new file mode 100644 (file)
index 0000000..87bf9c8
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
@@ -0,0 +1,62 @@
+(*#* #stop file *)
+
+Require tlt_defs.
+Require lift_tlt.
+Require subst0_defs.
+
+   Section subst0_tlt_props. (***********************************************)
+
+      Theorem subst0_weight_le : (u,t,z:?; d:?) (subst0 d u t z) ->
+                                 (f,g:?) ((m:?) (le (f m) (g m))) ->
+                                 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
+                                 (le (weight_map f z) (weight_map g t)).
+      Intros until 1; XElim H.
+(* case 1: subst0_bref *)
+      Intros; XAuto.
+(* case 2: subst0_fst *)
+      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
+(* case 3: subst0_snd *)
+      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
+(* case 4: subst0_both *)
+      XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
+      Qed.
+
+      Theorem subst0_weight_lt : (u,t,z:?; d:?) (subst0 d u t z) -> (f,g:?)
+                                 ((m:?) (le (f m) (g m))) ->
+                                 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
+                                 (lt (weight_map f z) (weight_map g t)).
+      Intros until 1; XElim H.
+(* case 1: subst0_bref *)
+      Intros; XAuto.
+(* case 2: subst0_fst *)
+      XElim k; [ XElim b | Idtac ]; Simpl; Intros;
+      Apply lt_n_S; (Apply lt_le_plus_plus; [ XAuto | Idtac ]); (**)
+      [ Auto 6 with ltlc (**) | XAuto | XAuto | XAuto ].
+(* case 3: subst0_snd *)
+      XElim k; [ XElim b | Idtac ]; Simpl;
+      [ Auto 8 with ltlc | Auto 6 with ltlc | Auto 6 with ltlc | XAuto ]. (**)
+(* case 3: subst0_both *)
+      XElim k; [ XElim b | Idtac ]; Simpl;
+      Intros; Apply lt_n_S; [ Apply lt_le_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus ]; XAuto.
+      EApply subst0_weight_le; [ XEAuto | XAuto | XAuto ].
+      Qed.
+
+      Theorem subst0_tlt_tail: (u,t,z:?) (subst0 (0) u t z) ->
+                               (tlt (TTail (Bind Abbr) u z)
+                                    (TTail (Bind Abbr) u t)
+                               ).
+      Unfold tlt weight; Intros; Simpl.
+      Apply lt_n_S; Apply le_lt_plus_plus; [ XAuto | Idtac ].
+      EApply subst0_weight_lt; [ XEAuto | XAuto | XAuto ].
+      Qed.
+
+      Theorem subst0_tlt: (u,t,z:?) (subst0 (0) u t z) ->
+                          (tlt z (TTail (Bind Abbr) u t)).
+      Intros.
+      EApply tlt_trans; [ Idtac | Apply subst0_tlt_tail; XEAuto].
+      XAuto.
+      Qed.
+
+   End subst0_tlt_props.
+
+      Hints Resolve subst0_tlt : ltlc.