1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/unfold/tpss_lift.ma".
16 include "basic_2/unfold/delift.ma".
18 (* INVERSE BASIC TERM RELOCATION *******************************************)
20 (* Advanced properties ******************************************************)
22 lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
23 ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, d + e - i - 1] ≡ V2 →
24 ⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2.
25 #L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
26 elim (lift_total V 0 (i+1)) #U #HVU
27 lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m
28 /2 width=1/ /3 width=6/
31 (* Advanced inversion lemmas ************************************************)
33 lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
34 #L #U2 #i #d #e * #U #HU #HU2 #Hid
35 elim (tpss_inv_lref1 … HU) -HU
36 [ #H destruct >(lift_inv_lref2_lt … HU2) //
38 lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
39 elim (lt_refl_false … Hi)
43 lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
45 ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
46 K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
48 #L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
49 elim (tpss_inv_lref1 … HU) -HU
50 [ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //
51 | * #K #V1 #V #_ #_ #HLK #HV1 #HVU
52 elim (lift_div_be … HVU … HU2 ? ?) -U // /2 width=1/ /3 width=6/
56 lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
57 d + e ≤ i → U2 = #(i - e).
58 #L #U2 #i #d #e * #U #HU #HU2 #Hdei
59 elim (tpss_inv_lref1 … HU) -HU
60 [ #H destruct >(lift_inv_lref2_ge … HU2) //
61 | * #K #V1 #V2 #_ #Hide
62 lapply (lt_to_le_to_lt … Hide Hdei) -Hide -Hdei #Hi
63 elim (lt_refl_false … Hi)
67 lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
69 | (∃∃K,V1,V2. d ≤ i & i < d + e &
71 K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
74 | (d + e ≤ i ∧ U2 = #(i - e)).
76 elim (lt_or_ge i d) #Hdi
77 [ elim (delift_inv_lref1_lt … H Hdi) -H /3 width=1/
78 | elim (lt_or_ge i (d+e)) #Hide
79 [ elim (delift_inv_lref1_be … H Hdi Hide) -H /3 width=6/
80 | elim (delift_inv_lref1_ge … H Hide) -H /3 width=1/
85 (* Properties on basic term relocation **************************************)
87 lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
88 ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
89 ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 →
91 #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2
92 elim (lift_total T d e) #U #HTU
93 lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
94 elim (lift_trans_ge … HT2 … HTU ?) -T // -Hdetd #T #HT2 #HTU
95 >(lift_mono … HTU2 … HT2) -T2 /2 width=3/
98 lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
99 ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
100 ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
101 L ⊢ U1 [dt, et + e] ≡ T2.
102 #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1
103 elim (lift_total T d e) #U #HTU
104 lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
105 lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/
108 lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
109 ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
110 ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
111 L ⊢ U1 [dt + e, et] ≡ U2.
112 #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2
113 elim (lift_total T d e) #U #HTU
114 lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
115 elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU
116 >(lift_mono … HTU2 … HT2) -T2 /2 width=3/