we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
deleted file mode 100644 (file)
index 35b114f..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
+++ /dev/null
@@ -1,84 +0,0 @@
-Require Export pr2_defs.
-Require Export pr3_defs.
-Require Export pc1_defs.
-
-(*#* #caption "the relation $\\PcT{}{}{}$" *)
-(*#* #cap #cap c, t, t1, t2 *)
-
-      Definition pc3 := [c:?; t1,t2:?] (EX t | (pr3 c t1 t) & (pr3 c t2 t)). 
-
-(*#* #stop file *)
-
-      Hints Unfold pc3 : ltlc.
-
-      Tactic Definition Pc3Unfold :=
-         Match Context With
-            [ H: (pc3 ?1 ?2 ?3) |- ? ] -> Unfold pc3 in H; XDecompose H.
-
-   Section pc3_props. (******************************************************)
-
-      Theorem pc3_pr2_r: (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
-      XEAuto.
-      Qed.
-
-      Theorem pc3_pr2_x: (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
-      XEAuto.
-      Qed.
-
-      Theorem pc3_pr3_r: (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
-      XEAuto.
-      Qed.
-
-      Theorem pc3_pr3_x: (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
-      XEAuto.
-      Qed.
-
-      Theorem pc3_pr3_t: (c:?; t1,t0:?) (pr3 c t1 t0) ->
-                         (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
-      XEAuto.
-      Qed.
-
-      Theorem pc3_pr2_u: (c:?; t2,t1:?) (pr2 c t1 t2) ->
-                         (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
-      Intros; Pc3Unfold; XEAuto.
-      Qed.
-      
-      Theorem pc3_refl: (c:?; t:?) (pc3 c t t).
-      XEAuto.
-      Qed.
-
-      Theorem pc3_s: (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
-      Intros; Pc3Unfold; XEAuto.
-      Qed.
-
-      Theorem pc3_thin_dx: (c:? ;t1,t2:?) (pc3 c t1 t2) ->
-                           (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
-                                             (TTail (Flat f) u t2)).
-      Intros; Pc3Unfold; XEAuto.
-      Qed.
-
-      Theorem pc3_tail_1: (c:?; u1,u2:?) (pc3 c u1 u2) ->
-                          (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
-      Intros; Pc3Unfold; XEAuto.
-      Qed.
-
-      Theorem pc3_tail_2: (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
-                          (pc3 c (TTail k u t1) (TTail k u t2)).
-      Intros; Pc3Unfold; XEAuto.
-      Qed.
-
-      Theorem pc3_shift: (h:?; c,e:?) (drop h (0) c e) ->
-                         (t1,t2:?) (pc3 c t1 t2) ->
-                         (pc3 e (app c h t1) (app c h t2)).
-      Intros; Pc3Unfold; XEAuto.
-      Qed.
-
-      Theorem pc3_pc1: (t1,t2:?) (pc1 t1 t2) -> (c:?) (pc3 c t1 t2).
-      Intros; Pc1Unfold; XEAuto.
-      Qed.
-   
-   End pc3_props.
-
-      Hints Resolve pc3_refl pc3_pr2_r pc3_pr2_x pc3_pr3_r pc3_pr3_x
-                    pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
-                    pc3_pr2_u pc3_shift pc3_pc1 : ltlc.