contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
new file mode 100644 (file)
index 0000000..3a9cb3f
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
@@ -0,0 +1,89 @@
+(*#* #stop file *)
+
+Require tlt_defs.
+Require lift_defs.
+
+      Hint discr : ltlc := Extern 4 (lt (weight_map (wadd ? ?) (lift (S ?) ? ?)) (wadd ? ? ?))
+                           Simpl; Rewrite <- lift_weight_add_O.
+
+      Hint discr : ltlc := Extern 4 (lt (weight_map ? (lift (0) (0) ?)) ?)
+                           Rewrite lift_r.
+
+   Section lift_tlt_props. (*************************************************)
+
+      Theorem lift_weight_map: (t:?; h,d:?; f:?)
+                               ((m:?) (le d m) -> (f m)=(0)) ->
+                               (weight_map f (lift h d t)) = (weight_map f t).
+      XElim t; Intros.
+(* case 1: TSort *)
+      XAuto.
+(* case 2: TBRef n *)
+      Apply (lt_le_e n d); Intros.
+(* case 2.1: n < d *)
+      Rewrite lift_bref_lt; XAuto.
+(* case 2.2: n >= d *)
+      Rewrite lift_bref_ge; [ Simpl | XAuto ].
+      Rewrite (H n); XAuto.
+(* case 3: TTail k *)
+      XElim k; Intros; LiftTailRw; Simpl.
+(* case 3.1: Bind *)
+      XElim b; [ Rewrite H; [ Idtac | XAuto ] | Idtac | Idtac ];
+      Rewrite H0; Intros; Try (LeLtGen; Rewrite H2; Simpl); XAuto.
+(* case 3.2: Flat *)
+      XAuto.
+      Qed.
+
+      Hints Resolve lift_weight_map : ltlc.
+
+      Theorem lift_weight : (t:?; h,d:?) (weight (lift h d t)) = (weight t).
+      Unfold weight; XAuto.
+      Qed.
+
+      Theorem lift_weight_add : (w:?; t:?; h,d:?; f,g:?)
+                                ((m:?) (lt m d) -> (g m) = (f m)) ->
+                                (g d) = w ->
+                                ((m:?) (le d m) -> (g (S m)) = (f m)) ->
+                                (weight_map f (lift h d t)) =
+                                (weight_map g (lift (S h) d t)).
+      XElim t; Intros.
+(* case 1: TSort *)
+      XAuto.
+(* case 2: TBRef *)
+      Apply (lt_le_e n d); Intros.
+(* case 2.1: n < d *)
+      Repeat Rewrite lift_bref_lt; Simpl; XAuto.
+(* case 2.2: n >= d *)
+      Repeat Rewrite lift_bref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
+(* case 3: TTail k *)
+      XElim k; Intros; LiftTailRw; Simpl.
+(* case 1 : bind b *)
+      XElim b; Simpl;
+      Apply (f_equal nat);
+      (Apply (f_equal2 nat nat); [ XAuto | Idtac ]);
+      ( Apply H0; Simpl; Intros; Try (LeLtGen; Rewrite H4; Simpl); XAuto).
+(* case 2 : Flat *)
+      XAuto.
+      Qed.
+
+      Theorem lift_weight_add_O: (w:?; t:?; h:?; f:?)
+                                 (weight_map f (lift h (0) t)) =
+                                 (weight_map (wadd f w) (lift (S h) (0) t)).
+      Intros.
+      EApply lift_weight_add; XAuto.
+      Intros; Inversion H.
+      Qed.
+
+      Theorem lift_tlt_dx: (k:?; u,t:?; h,d:?)
+                           (tlt t (TTail k u (lift h d t))).
+      Unfold tlt; Intros.
+      Rewrite <- (lift_weight t h d).
+      Fold (tlt (lift h d t) (TTail k u (lift h d t))); XAuto.
+      Qed.
+
+   End lift_tlt_props.
+
+      Hints Resolve lift_tlt_dx : ltlc.
+
+(*#* #start file *)
+
+(*#* #single *)