we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v
deleted file mode 100644 (file)
index 8a27227..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v
+++ /dev/null
@@ -1,88 +0,0 @@
-(*#* #stop file *)
-
-Require lift_gen.
-Require pr3_props.
-Require pr3_gen.
-Require pc3_defs.
-Require pc3_props.
-
-   Section pc3_gen. (********************************************************)
-
-      Theorem pc3_gen_sort: (c:?; m,n:?) (pc3 c (TSort m) (TSort n)) -> m = n.
-      Intros; Pc3Unfold; Repeat Pr3GenBase.
-      Rewrite H0 in H; Clear H0 x c.
-      TGenBase; XAuto.
-      Qed.
-
-      Theorem pc3_gen_abst: (c:?; u1,u2,t1,t2:?)
-                            (pc3 c (TTail (Bind Abst) u1 t1)
-                                   (TTail (Bind Abst) u2 t2)
-                            ) ->
-                            (pc3 c u1 u2) /\
-                            (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
-      Intros.
-      Pc3Unfold; Repeat Pr3GenBase; Rewrite H1 in H; Clear H1 x.
-      TGenBase; Rewrite H1 in H4; Rewrite H6 in H5.
-      XEAuto.
-      Qed.
-
-      Theorem pc3_gen_lift: (c:?; t1,t2:?; h,d:?)
-                            (pc3 c (lift h d t1) (lift h d t2)) ->
-                            (e:?) (drop h d c e) ->
-                            (pc3 e t1 t2).
-      Intros.
-      Pc3Unfold; Repeat Pr3Gen; Rewrite H2 in H; Clear H2 x.
-      LiftGen; Rewrite H in H4; XEAuto.
-      Qed.
-
-      Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
-                                (pc3 c (TTail (Bind b) u1 t1)
-                                       (TTail (Bind Abst) u2 t2)
-                                ) ->
-                                (pc3 (CTail c (Bind b) u1) t1
-                                     (lift (1) (0) (TTail (Bind Abst) u2 t2))
-                                ).
-      XElim b; Intros;
-      Try EqFalse; Pc3Unfold; Repeat Pr3Gen;
-      Try (Rewrite H0 in H3; TGenBase);
-      Rewrite H1 in H0; Clear H H1 x;
-      EApply pc3_pr3_t; XEAuto.
-      Qed.
-
-      Theorem pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?)
-                                 (pc3 c (lift h d t)
-                                        (TTail (Bind Abst) u2 t2)
-                                 ) ->
-                                 (e:?) (drop h d c e) ->
-                                 (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
-                                             (pr3 c u2 (lift h d u1)) &
-                                             (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
-                                 ).
-      Intros.
-      Pc3Unfold; Repeat Pr3Gen; Rewrite H1 in H; Clear H1 x.
-      LiftGenBase; Rewrite H in H3; Rewrite H1 in H4; Rewrite H2 in H5; XEAuto.
-      Qed.
-
-   End pc3_gen.
-
-      Tactic Definition Pc3Gen :=
-         Match Context With
-           | [H: (pc3 ?1 (TSort ?2) (TSort ?3)) |- ? ] ->
-              LApply (pc3_gen_sort ?1 ?2 ?3); [ Clear H; Intros | XAuto ]
-            | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5));
-                _: (drop ?2 ?3 ?1 ?6) |- ? ] ->
-               LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ];
-               LApply (H_x ?6); [ Clear H_x; Intros | XAuto ]
-            | [ H: (pc3 ?1 (TTail (Bind Abst) ?2 ?3) (TTail (Bind Abst) ?4 ?5)) |- ? ] ->
-               LApply (pc3_gen_abst ?1 ?2 ?4 ?3 ?5);[ Clear H; Intros H | XAuto ];
-               XElim H; Intros
-            | [ H: (pc3 ?1 (TTail (Bind ?2) ?3 ?4) (TTail (Bind Abst) ?5 ?6));
-                _: ~ ?2 = Abst |- ? ] ->
-               LApply (pc3_gen_not_abst ?2); [ Intros H_x | XAuto ];
-               LApply (H_x ?1 ?4 ?6 ?3 ?5); [ Clear H H_x; Intros | XAuto ]
-            | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (TTail (Bind Abst) ?5 ?6));
-                _: (drop ?2 ?3 ?1 ?7) |- ? ] ->
-               LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
-               LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];
-               XElim H_x; Intros
-           | _ -> Pr3Gen.