X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fsubstitution%2Flift.ma;h=340cffccdab53541332f97dbe3ca75612ea83d2d;hb=05959b8deaafaf3aa4ae59296da9c0fbf36c0feb;hp=17ece9a2a1cc644ff78eb416ee5ff4851b964e67;hpb=2af0a3e67ae1a9134102f6a6caf02680a4851312;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma
index 17ece9a2a..340cffccd 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift.ma
@@ -23,3 +23,61 @@ inductive lift: term → nat → nat → term → Prop ≝
 .
 
 interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
+
+(* The basic properties *****************************************************)
+
+lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d,e] #(i - e) ≡ #i.
+#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/
+qed.
+
+(* The basic inversion lemmas ***********************************************)
+
+lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
+#d #e #T1 #T2 #H elim H -H d e T1 T2 //
+   [ #i #d #e #_ #k #H destruct
+   | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+   ]
+qed.
+
+lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
+#d #e #T1 #k #H lapply (lift_inv_sort2_aux … H) /2/
+qed.
+
+lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
+                          (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+   [ #k #d #e #i #H destruct
+   | #j #d #e #Hj #i #Hi destruct /3/
+   | #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
+   | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+   ]
+qed.
+
+lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
+                      (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+#d #e #T1 #i #H lapply (lift_inv_lref2_aux … H) /2/
+qed.
+
+lemma lift_inv_con22_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V2,U2. T2 = ♭I V2.U2 →
+                          ∃V1,U1. ↑[d,e] V1 ≡ V2 ∧ ↑[d+1,e] U1 ≡ U2 ∧
+                                  T1 = ♭I V1.U1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+   [ #k #d #e #I #V2 #U2 #H destruct
+   | #i #d #e #_ #I #V2 #U2 #H destruct
+   | #i #d #e #_ #I #V2 #U2 #H destruct
+   | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /5/
+qed.
+
+lemma lift_inv_con22: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  ♭I V2. U2 →
+                      ∃V1,U1. ↑[d,e] V1 ≡ V2 ∧ ↑[d+1,e] U1 ≡ U2 ∧
+                              T1 = ♭I V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_con22_aux … H) /2/
+qed.
+
+(* the main properies *******************************************************)
+
+axiom lift_trans_rev: ∀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.