X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fdelift_lift.ma;h=a7f31fb809643badd7894803607de1d22ed3d1d1;hb=fc5a0d62ece398d8547dda0f429b9f1e24bca306;hp=5ae82271da24e8ef08b4d09746d9d96f198a2334;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
index 5ae82271d..a7f31fb80 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
@@ -15,11 +15,22 @@
 include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/delift.ma".
 
-(* DELIFT ON TERMS **********************************************************)
+(* INVERSE TERM RELOCATION  *************************************************)
 
+(* Advanced properties ******************************************************)
+
+lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
+                      ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, d + e - i - 1] ≡ V2 →
+                      ⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2.
+#L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
+elim (lift_total V 0 (i+1)) #U #HVU
+lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m
+/2 width=1/ /3 width=6/
+qed.
+ 
 (* Advanced forward lemmas **************************************************)
 
-lemma delift_fwd_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
+lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
 #L #U2 #i #d #e * #U #HU #HU2 #Hid
 elim (tpss_inv_lref1 … HU) -HU
 [ #H destruct >(lift_inv_lref2_lt … HU2) //
@@ -29,7 +40,7 @@ elim (tpss_inv_lref1 … HU) -HU
 ]
 qed-.
 
-lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
+lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
                            d ≤ i → i < d + e →
                            ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
                                       K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
@@ -42,7 +53,7 @@ elim (tpss_inv_lref1 … HU) -HU
 ]
 qed-.
 
-lemma delift_fwd_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
+lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
                            d + e ≤ i → U2 = #(i - e).
 #L #U2 #i #d #e * #U #HU #HU2 #Hdei
 elim (tpss_inv_lref1 … HU) -HU
@@ -52,3 +63,55 @@ elim (tpss_inv_lref1 … HU) -HU
   elim (lt_refl_false … Hi)
 ]
 qed-.
+
+lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
+                        ∨∨ (i < d ∧ U2 = #i) 
+                        |  (∃∃K,V1,V2. d ≤ i & i < d + e &
+                                       ⇩[0, i] L ≡ K. ⓓV1 &
+                                       K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
+                                       ⇧[0, d] V2 ≡ U2
+                           )
+                        |  (d + e ≤ i ∧ U2 = #(i - e)).
+#L #U2 #i #d #e #H
+elim (lt_or_ge i d) #Hdi
+[ elim (delift_inv_lref1_lt … H Hdi) -H /3 width=1/
+| elim (lt_or_ge i (d+e)) #Hide
+  [ elim (delift_inv_lref1_be … H Hdi Hide) -H /3 width=6/
+  | elim (delift_inv_lref1_ge … H Hide) -H /3 width=1/
+  ]
+]
+qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+                      ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
+                      ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 →
+                      L ⊢ U1 [dt, et] ≡ U2.
+#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2
+elim (lift_total T d e) #U #HTU
+lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
+elim (lift_trans_ge … HT2 … HTU ?) -T // -Hdetd #T #HT2 #HTU
+>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
+qed.
+
+lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+                      ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
+                      ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
+                      L ⊢ U1 [dt, et + e] ≡ T2.
+#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1
+elim (lift_total T d e) #U #HTU
+lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
+lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/
+qed.
+
+lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+                      ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
+                      ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+                      L ⊢ U1 [dt + e, et] ≡ U2.
+#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2
+elim (lift_total T d e) #U #HTU
+lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
+elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU
+>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
+qed.