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/relocation/cpy_lift.ma".
16 include "basic_2/substitution/cpys.ma".
18 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
20 (* Advanced properties ******************************************************)
22 lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e.
23 d ≤ yinj i → i < d + e →
24 ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ⫰(d+e-i)] U1 →
25 ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, e] U2.
26 #I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1
27 [ /3 width=5 by cpy_cpys, cpy_subst/
28 | #U #U1 #_ #HU1 #IHU #U2 #HU12
29 elim (lift_total U 0 (i+1)) #U0 #HU0
30 lapply (IHU … HU0) -IHU #H
31 lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
32 lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
33 lapply (cpy_weak … HU02 d e ? ?) -HU02
34 [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
35 >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/
39 lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d.
41 ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ∞] U1 →
42 ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, ∞] U2.
43 #I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12
44 @(cpys_subst … HLK … HU12) >yminus_Y_inj //
47 (* Advanced inverion lemmas *************************************************)
49 lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 →
51 ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e &
52 ⇩[O, i] L ≡ K.ⓑ{J}V1 &
53 ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 &
56 #I #G #L #T2 #d #e #H @(cpys_ind … H) -T2
57 [ /2 width=1 by or_introl/
60 elim (cpy_inv_atom1 … HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ]
61 | * #J #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
62 lapply (ldrop_fwd_ldrop2 … HLK) #H
63 elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT
64 [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ]
65 /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
70 lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
72 ∃∃I,K,V1,V2. d ≤ i & i < d + e &
73 ⇩[O, i] L ≡ K.ⓑ{I}V1 &
74 ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 &
76 #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
77 * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/
80 lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
81 ∀I,K,V1. ⇩[O, i] L ≡ K.ⓑ{I}V1 →
82 ∀V2. ⇧[O, i+1] V2 ≡ T2 →
83 ∧∧ ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2
86 #G #L #T2 #i #d #e #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H
87 [ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK //
88 | * #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2
89 lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct
90 lapply (ldrop_mono … HLY … HLK) -L #H destruct
91 /2 width=1 by and3_intro/
95 (* Relocation properties ****************************************************)
97 lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
98 ∀L,U1,d,e. dt + et ≤ yinj d → ⇩[d, e] L ≡ K →
99 ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
100 ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2.
101 #G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2
102 [ #U2 #H >(lift_mono … HTU1 … H) -H //
103 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
104 elim (lift_total T d e) #U #HTU
105 lapply (IHT … HTU) -IHT #HU1
106 lapply (cpy_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
110 lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
111 ∀L,U1,d,e. dt ≤ yinj d → d ≤ dt + et →
112 ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
113 ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*×[dt, et + e] U2.
114 #G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2
115 [ #U2 #H >(lift_mono … HTU1 … H) -H //
116 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
117 elim (lift_total T d e) #U #HTU
118 lapply (IHT … HTU) -IHT #HU1
119 lapply (cpy_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
123 lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
124 ∀L,U1,d,e. yinj d ≤ dt → ⇩[d, e] L ≡ K →
125 ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
126 ⦃G, L⦄ ⊢ U1 ▶*×[dt+e, et] U2.
127 #G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2
128 [ #U2 #H >(lift_mono … HTU1 … H) -H //
129 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
130 elim (lift_total T d e) #U #HTU
131 lapply (IHT … HTU) -IHT #HU1
132 lapply (cpy_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
136 lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
137 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
139 ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 & ⇧[d, e] T2 ≡ U2.
140 #G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2
141 [ /2 width=3 by ex2_intro/
142 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
143 elim (cpy_inv_lift1_le … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
147 lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
148 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
149 dt ≤ d → d + e ≤ dt + et →
150 ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
151 #G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2
152 [ /2 width=3 by ex2_intro/
153 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
154 elim (cpy_inv_lift1_be … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
158 lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
159 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
161 ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
162 #G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2
163 [ /2 width=3 by ex2_intro/
164 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
165 elim (cpy_inv_lift1_ge … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
169 lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat.
170 ⦃G, L⦄ ⊢ U1 ▶*×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
171 #G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2 //
172 #U #U2 #_ #HU2 #IHU destruct
173 <(cpy_inv_lift1_eq … HTU1 … HU2) -HU2 -HTU1 //
176 lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
177 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
178 d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
179 ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 &
181 #G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2
182 [ /2 width=3 by ex2_intro/
183 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
184 elim (cpy_inv_lift1_ge_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
188 lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
189 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
190 dt ≤ d → dt + et ≤ d + e →
191 ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
192 #G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2
193 [ /2 width=3 by ex2_intro/
194 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
195 elim (cpy_inv_lift1_be_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
199 lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
200 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
201 dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
202 ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
203 #G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2
204 [ /2 width=3 by ex2_intro/
205 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
206 elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/