contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v
new file mode 100644 (file)
index 0000000..0dcc0b8
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v
@@ -0,0 +1,79 @@
+(*#* #stop file *)
+
+Require Export pr0_defs.
+
+      Inductive pc0 [t1,t2:T] : Prop :=
+         | pc0_r : (pr0 t1 t2) -> (pc0 t1 t2)
+         | pc0_x : (pr0 t2 t1) -> (pc0 t1 t2).
+
+      Hint pc0 : ltlc := Constructors pc0.
+
+      Inductive pc1 : T -> T -> Prop :=
+         | pc1_r : (t:?) (pc1 t t)
+         | pc1_u : (t2,t1:?) (pc0 t1 t2) -> (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
+
+      Hint pc1 : ltlc := Constructors pc1.
+
+   Section pc0_props. (******************************************************)
+
+      Theorem pc0_s : (t2,t1:?) (pc0 t1 t2) -> (pc0 t2 t1).
+      Intros.
+      Inversion H; XAuto.
+      Qed.
+
+   End pc0_props.
+
+      Hints Resolve pc0_s : ltlc.
+
+   Section pc1_props. (******************************************************)
+
+      Theorem pc1_pr0_r : (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
+      XEAuto.
+      Qed.
+
+      Theorem pc1_pr0_x : (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
+      XEAuto.
+      Qed.
+
+      Theorem pc1_pc0 : (t1,t2:?) (pc0 t1 t2) -> (pc1 t1 t2).
+      XEAuto.
+      Qed.
+
+      Theorem pc1_t : (t2,t1:?) (pc1 t1 t2) ->
+                      (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
+      Intros t2 t1 H; XElim H; XEAuto.
+      Qed.
+
+      Hints Resolve pc1_t : ltlc.
+
+      Theorem pc1_s : (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
+      Intros; XElim H; XEAuto.
+      Qed.
+
+      Theorem pc1_tail_1: (u1,u2:?) (pc1 u1 u2) ->
+                          (t:?; k:?) (pc1 (TTail k u1 t) (TTail k u2 t)).
+      Intros; XElim H; Intros.
+(* case 1: pc1_r *)
+      XAuto.
+(* case 2: pc1_u *)
+      XElim H; Intros; XEAuto.
+      Qed.
+
+      Theorem pc1_tail_2: (t1,t2:?) (pc1 t1 t2) ->
+                          (u:?; k:?) (pc1 (TTail k u t1) (TTail k u t2)).
+      Intros; XElim H; Intros.
+(* case 1: pc1_r *)
+      XAuto.
+(* case 2: pc1_u *)
+      XElim H; Intros; XEAuto.
+      Qed.
+
+      Theorem pc1_tail: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
+                        (k:?) (pc1 (TTail k u1 t1) (TTail k u2 t2)).
+      Intros; EApply pc1_t; [ EApply pc1_tail_1 | EApply pc1_tail_2 ]; XAuto.
+      Qed.
+
+   End pc1_props.
+
+      Hints Resolve pc1_pr0_r pc1_pr0_x pc1_pc0 pc1_t pc1_s
+                    pc1_tail_1 pc1_tail_2 pc1_tail : ltlc.