we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v
deleted file mode 100644 (file)
index ebe6bfc..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v
+++ /dev/null
@@ -1,65 +0,0 @@
-Require lift_props.
-Require drop_props.
-Require pc3_props.
-Require ty0_defs.
-
-(*#* #caption "main properties of typing" #clauses ty0_props *)
-
-   Section ty0_lift. (*******************************************************)
-
-(*#* #caption "lift preserves types" *)
-(*#* #cap #cap t1, t2 #alpha c in C1, e in C2, d in i *)
-
-      Theorem ty0_lift : (g:?; e:?; t1,t2:?) (ty0 g e t1 t2) ->
-                         (c:?) (wf0 g c) -> (d,h:?) (drop h d c e) ->
-                         (ty0 g c (lift h d t1) (lift h d t2)).
-
-(*#* #stop file *)
-
-      Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
-      XEAuto.
-(* case 2 : ty0_sort *)
-      Repeat Rewrite lift_sort; XAuto.
-(* case 3 : ty0_abbr *)
-      Apply (lt_le_e n d0); Intros; DropDis.
-(* case 3.1 : n < d0 *)
-      Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
-      DropGenBase; Rewrite H4 in H0; Clear H4 x.
-      Rewrite lift_lref_lt; [ Idtac | XAuto ].
-      Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
-      EApply ty0_abbr; XEAuto.
-(* case 3.2 : n >= d0 *)
-      Rewrite lift_lref_ge; [ Idtac | XAuto ].
-      Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
-      Rewrite (plus_sym h (S n)); Simpl; XEAuto.
-(* case 4: ty0_abst *)
-      Apply (lt_le_e n d0); Intros; DropDis.
-(* case 4.1 : n < d0 *)
-      Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
-      DropGenBase; Rewrite H4 in H0; Clear H4 x.
-      Rewrite lift_lref_lt; [ Idtac | XAuto ].
-      Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
-      EApply ty0_abst; XEAuto.
-(* case 4.2 : n >= d0 *)
-      Rewrite lift_lref_ge; [ Idtac | XAuto ].
-      Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
-      Rewrite (plus_sym h (S n)); Simpl; XEAuto.
-(* case 5: ty0_bind *)
-      LiftTailRw; Simpl; EApply ty0_bind; XEAuto.
-(* case 6: ty0_appl *)
-      LiftTailRw; Simpl; EApply ty0_appl; [ Idtac | Rewrite <- lift_bind ]; XEAuto.
-(* case 7: ty0_cast *)
-      LiftTailRw; XEAuto.
-      Qed.
-
-   End ty0_lift.
-
-      Hints Resolve ty0_lift : ltlc.
-
-      Tactic Definition Ty0Lift b u :=
-         Match Context With
-            [ H: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
-               LApply (ty0_lift ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
-               LApply (H_x (CTail ?2 (Bind b) u)); [ Clear H_x; Intros H_x | XEAuto ];
-               LApply (H_x (0) (1)); [ Clear H_x; Intros | XAuto ].