contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
new file mode 100644 (file)
index 0000000..1d67abf
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
@@ -0,0 +1,75 @@
+(*#* #stop file *)
+
+Require Export pr1_defs.
+Require Export pr2_defs.
+
+      Inductive pr3 [c:C] : T -> T -> Prop :=
+         | pr3_r : (t:?) (pr3 c t t)
+         | pr3_u : (t2,t1:?) (pr2 c t1 t2) ->
+                   (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
+
+      Hint pr3: ltlc := Constructors pr3.
+
+   Section pr3_props. (******************************************************)
+
+      Theorem pr3_pr2 : (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
+      XEAuto.
+      Qed.
+
+      Theorem pr3_t : (t2,t1,c:?) (pr3 c t1 t2) ->
+                      (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
+      Intros until 1; XElim H; XEAuto.
+      Qed.
+
+      Theorem pr3_tail_1 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
+                           (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
+      Intros until 1; XElim H; Intros.
+(* case 1 : pr3_r *)
+      XAuto.
+(* case 2 : pr3_u *)
+      EApply pr3_u; [ Apply pr2_tail_1; Apply H | XAuto ].
+      Qed.
+
+      Theorem pr3_tail_2 : (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
+                           (pr3 c (TTail k u t1) (TTail k u t2)).
+      Intros until 1; XElim H; Intros.
+(* case 1 : pr3_r *)
+      XAuto.
+(* case 2 : pr3_u *)
+      EApply pr3_u; [ Apply pr2_tail_2; Apply H | XAuto ].
+      Qed.
+
+      Hints Resolve pr3_tail_1 pr3_tail_2 : ltlc.
+
+      Theorem pr3_tail_21 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
+                            (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
+                            (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
+      Intros.
+      EApply pr3_t; [ Apply pr3_tail_2 | Apply pr3_tail_1 ]; XAuto.
+      Qed.
+
+      Theorem pr3_tail_12 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
+                            (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
+                            (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
+      Intros.
+      EApply pr3_t; [ Apply pr3_tail_1 | Apply pr3_tail_2 ]; XAuto.
+      Qed.
+
+      Theorem pr3_shift : (h:?; c,e:?) (drop h (0) c e) ->
+                          (t1,t2:?) (pr3 c t1 t2) ->
+                          (pr3 e (app c h t1) (app c h t2)).
+      Intros until 2; XElim H0; Clear t1 t2; Intros.
+(* case 1 : pr3_r *)
+      XAuto.
+(* case 2 : pr3_u *)
+      XEAuto.
+      Qed.
+
+      Theorem pr3_pr1: (t1,t2:?) (pr1 t1 t2) -> (c:?) (pr3 c t1 t2).
+      Intros until 1; XElim H; XEAuto.
+      Qed.
+
+   End pr3_props.
+
+      Hints Resolve pr3_pr2 pr3_t pr3_pr1
+                    pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.