- functional properties of lift closed!

- the proof of a main property of lift was lost due to a segmentation
fault of auto :-((

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
index ee54dede2e11dce091eecdc18dd3d3579ed3e1ef..0044de7f1c1d4ef744782ba586c4e23b705787bc 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
@@ -16,10 +16,46 @@ include "lambda-delta/substitution/lift_defs.ma".
 
 (* RELOCATION ***************************************************************)
 
-(* the functional properties **************************************************)
+(* the functional properties ************************************************)
 
-axiom lift_total: ∀d,e,T1. ∃T2. ↑[d,e] T1 ≡ T2.
+lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
+#T1 elim T1 -T1
+[ /2/
+| #i #d #e elim (lt_or_ge i d) /3/
+| * #I #V1 #T1 #IHV1 #IHT1 #d #e
+  elim (IHV1 d e) -IHV1 #V2 #HV12
+  [ elim (IHT1 (d+1) e) -IHT1 /3/
+  | elim (IHT1 d e) -IHT1 /3/
+  ]
+]
+qed.
 
-axiom lift_mono:  ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
+lemma lift_mono:  ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
+#d #e #T #U1 #H elim H -H d e T U1
+[ #k #d #e #X #HX
+  lapply (lift_inv_sort1 … HX) -HX //
+| #i #d #e #Hid #X #HX 
+  lapply (lift_inv_lref1_lt … HX ?) -HX //
+| #i #d #e #Hdi #X #HX 
+  lapply (lift_inv_lref1_ge … HX ?) -HX //
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+]
+qed.
 
-axiom lift_inj:  ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2.
+lemma lift_inj:  ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2.
+#d #e #T1 #U #H elim H -H d e T1 U
+[ #k #d #e #X #HX
+  lapply (lift_inv_sort2 … HX) -HX //
+| #i #d #e #Hid #X #HX 
+  lapply (lift_inv_lref2_lt … HX ?) -HX //
+| #i #d #e #Hdi #X #HX 
+  lapply (lift_inv_lref2_ge … HX ?) -HX /2/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+  elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
+]
+qed.

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
index ba74cf7b2507e8bd8d182ff19772354688c288d7..ff9b05b752631a1094359d6aca5eae781c02a309 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/lift_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
@@ -18,10 +18,10 @@ include "lambda-delta/substitution/lift_defs.ma".
 
 (* the main properies *******************************************************)
 
-theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
-                     ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
-                     d1 ≤ d2 →
-                     ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1.
+lemma lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+                   ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
+                   d1 ≤ d2 →
+                   ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1.
 #d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
 [ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
   lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/
@@ -48,9 +48,9 @@ theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
 ]
 qed.
 
-theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
-                                 d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
-                                 ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2.
+lemma lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
+                               d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
+                               ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2.
 #d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
 [ /3/
 | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
@@ -67,9 +67,9 @@ theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
 ]
 qed.
 
-theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
-                       ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 →
-                       d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2.
+lemma lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+                     ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 →
+                     d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2.
 #d1 #e1 #T1 #T #H elim H -d1 e1 T1 T
 [ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_
   >(lift_inv_sort1 … HT2) -HT2 //