contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_props.v b/helm/coq-contribs/LAMBDA-TYPES/lift_props.v
new file mode 100644 (file)
index 0000000..5d5d7d0
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_props.v
@@ -0,0 +1,43 @@
+(*#* #stop file *)
+
+Require lift_defs.
+
+   Section lift_props. (*****************************************************)
+
+      Theorem lift_free: (t:?; h,k,d,e:?) (le e (plus d h)) -> (le d e) ->
+                         (lift k e (lift h d t)) = (lift (plus k h) d t).
+      XElim t; Intros.
+(* case 1: TSort *)
+      Repeat Rewrite lift_sort; XAuto.
+(* case 2: TBRef n *)
+      Apply (lt_le_e n d); Intros.
+(* case 2.1: n < d *)
+      Repeat Rewrite lift_bref_lt; XEAuto.
+(* case 2.2: n >= d *)
+      Repeat Rewrite lift_bref_ge; XEAuto.
+(* case 3: TTail k *)
+      LiftTailRw; XAuto.
+      Qed.
+
+      Theorem lift_d : (t:?; h,k,d,e:?) (le e d) ->
+                       (lift h (plus k d) (lift k e t)) = (lift k e (lift h d t)).
+      XElim t; Intros.
+(* case 1: TSort *)
+      Repeat Rewrite lift_sort; XAuto.
+(* case 2: TBRef n *)
+      Apply (lt_le_e n e); Intros.
+(* case 2.1: n < e *)
+      Cut (lt n d); Intros; Repeat Rewrite lift_bref_lt; XEAuto.
+(* case 2.2: n >= e *)
+      Rewrite lift_bref_ge; [ Idtac | XAuto ].
+      Rewrite plus_sym; Apply (lt_le_e n d); Intros.
+(* case 2.2.1: n < d *)
+      Do 2 (Rewrite lift_bref_lt; [ Idtac | XAuto ]).
+      Rewrite lift_bref_ge; XAuto.
+(* case 2.2.2: n >= d *)
+      Repeat Rewrite lift_bref_ge; XAuto.
+(* case 3: TTail k *)
+      LiftTailRw; SRw; XAuto.
+      Qed.
+
+   End lift_props.