contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v
new file mode 100644 (file)
index 0000000..222a08c
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v
@@ -0,0 +1,64 @@
+Require pr0_confluence.
+Require pr1_defs.
+
+(*#* #caption "main properties of predicate \\texttt{pr1}" *)
+(*#* #clauses pr1_props *)
+
+   Section pr1_confluence. (*************************************************)
+
+(*#* #caption "confluence with single step reduction: strip lemma" *)
+(*#* #cap #cap t0, t1, t2, t *)
+
+      Theorem pr1_strip : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr0 t0 t2) ->
+                          (EX t | (pr1 t1 t) & (pr1 t2 t)).
+
+(*#* #stop proof *)
+
+      Intros until 1; XElim H; Intros.
+(* case 1 : pr1_r *)
+      XEAuto.
+(* case 2 : pr1_u *)
+      Pr0Confluence.
+      LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
+      XElim H1; Intros; XEAuto.
+      Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "confluence with itself: Church-Rosser property" *)
+(*#* #cap #cap t0, t1, t2, t *)
+
+      Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
+                               (EX t | (pr1 t1 t) & (pr1 t2 t)).
+
+(*#* #stop file *)
+
+      Intros until 1; XElim H; Intros.
+(* case 1 : pr1_r *)
+      XEAuto.
+(* case 2 : pr1_u *)
+      LApply (pr1_strip t3 t5); [ Clear H2; Intros H2 | XAuto ].
+      LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
+      XElim H; Intros.
+      LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
+      XElim H1; Intros; XEAuto.
+      Qed.
+
+   End pr1_confluence.
+
+      Tactic Definition Pr1Confluence :=
+         Match Context With
+            | [ H1: (pr1 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] ->
+               LApply (pr1_strip ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
+               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
+               XElim H1; Intros
+            | [ H1: (pr1 ?1 ?2); H2: (pr1 ?1 ?3) |-? ] ->
+               LApply (pr1_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
+               LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
+               XElim H1; Intros
+            | _ -> Pr0Confluence.
+
+(*#* #start file *)
+
+(*#* #single *)
+