we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v
deleted file mode 100644 (file)
index 8b2fd47..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v
+++ /dev/null
@@ -1,74 +0,0 @@
-(*#* #stop file *)
-
-Require subst0_confluence.
-Require drop_props.
-Require pr0_subst0.
-Require pr0_confluence.
-Require pr2_defs.
-
-   Section pr2_confluence. (*************************************************)
-
-(* case 1.1 : pr2_free pr2_free *********************************************)
-
-      Remark pr2_free_free: (c:?; t0,t1,t2:?)
-                            (pr0 t0 t1) -> (pr0 t0 t2) ->
-                            (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
-      Intros; Pr0Confluence; XEAuto.
-      Qed.
-
-(* case 1.2 : pr2_free pr2_delta ********************************************)
-
-      Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
-                             (pr0 t0 t1) ->
-                             (drop i (0) c (CTail d (Bind Abbr) u)) ->
-                             (pr0 t0 t4) ->
-                            (subst0 i u t4 t2) ->
-                             (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
-      Intros; Pr0Confluence; Pr0Subst0; XEAuto.
-      Qed.
-
-(* case 2.2 : pr2_delta pr2_delta *******************************************)
-
-      Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
-                              (drop i (0) c (CTail d (Bind Abbr) u)) ->
-                              (pr0 t0 t3) ->
-                             (subst0 i u t3 t1) ->
-                              (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
-                              (pr0 t0 t4) ->
-                             (subst0 i0 u0 t4 t2) ->
-                              (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
-      Intros; Pr0Confluence; Repeat Pr0Subst0;
-      [ XEAuto | XEAuto | XEAuto | Idtac ].
-      Apply (neq_eq_e i i0); Intros.
-(* case 1 : i != i0 *)
-      Subst0Confluence; XEAuto.
-(* case 2 : i = i0 *)
-      Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i.
-      DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u.
-      Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ].
-      Qed.
-
-(* main *********************************************************************)
-
-      Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc.
-
-(*#* #caption "confluence with itself: Church-Rosser property" *)
-(*#* #cap #cap c, t0, t1, t2, t *)
-
-      Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
-                              (t2:?) (pr2 c t0 t2) ->
-                              (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
-      Intros; Inversion H; Inversion H0; XDEAuto 3.
-      Qed.
-
-   End pr2_confluence.
-
-      Tactic Definition Pr2Confluence :=
-         Match Context With
-            | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
-               LApply (pr2_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
-               XElim H1; Intros
-            | _ -> Pr0Confluence.
-
-(*#* #single *)