contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
new file mode 100644 (file)
index 0000000..f3dc1c5
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
@@ -0,0 +1,39 @@
+Require lift_props.
+Require subst0_lift.
+Require pr0_defs.
+
+(*#* #caption "main properties of predicate \\texttt{pr0}" *)
+(*#* #clauses pr0_props *)
+
+   Section pr0_lift. (*******************************************************)
+
+(*#* #caption "conguence with lift" *)
+(*#* #cap #cap t1,t2 #alpha d in i *)
+
+      Theorem pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
+                        (h,d:?) (pr0 (lift h d t1) (lift h d t2)).
+
+(*#* #stop file *)
+
+      Intros until 1; XElim H; Intros.
+(* case 1: pr0_refl *)
+      XAuto.
+(* case 2: pr0_cong *)
+      LiftTailRw; XAuto.
+(* case 3 : pr0_beta *)
+      LiftTailRw; XAuto.
+(* case 4: pr0_gamma *)
+      LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
+(* case 5: pr0_delta *)
+      LiftTailRw; Simpl.
+      EApply pr0_delta; [ XAuto | Apply H2 | Idtac ].
+      LetTac d' := (S d); Arith10 d; Unfold d'; XAuto.
+(* case 6: pr0_zeta *)
+      LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
+(* case 7: pr0_epsilon *)
+      LiftTailRw; XAuto.
+      Qed.
+
+   End pr0_lift.
+
+      Hints Resolve pr0_lift : ltlc.