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/substitution/tps_lift.ma".
16 include "Basic_2/unfold/tpss.ma".
18 (* PARTIAL UNFOLD ON TERMS **************************************************)
20 (* Advanced properties ******************************************************)
22 lemma tpss_subst: ∀L,K,V,U1,i,d,e.
24 ⇩[0, i] L ≡ K. 𝕓{Abbr} V → K ⊢ V [0, d + e - i - 1] ▶* U1 →
25 ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ▶* U2.
26 #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
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 (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
33 lapply (tps_weak … HU02 d e ? ?) -HU02 [ >minus_plus >commutative_plus /2 width=1/ | /2 width=1/ | /2 width=3/ ]
37 (* Advanced inverion lemmas *************************************************)
39 lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ▶* T2 →
41 ∃∃K,V1,V2,i. d ≤ i & i < d + e &
42 ⇩[O, i] L ≡ K. 𝕓{Abbr} V1 &
43 K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
46 #L #T2 #I #d #e #H @(tpss_ind … H) -T2
50 elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
51 | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
52 lapply (ldrop_fwd_ldrop2 … HLK) #H
53 elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
54 @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
59 lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶* T2 →
61 ∃∃K,V1,V2. d ≤ i & i < d + e &
62 ⇩[O, i] L ≡ K. 𝕓{Abbr} V1 &
63 K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
66 elim (tpss_inv_atom1 … H) -H /2 width=1/
67 * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
70 lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 →
71 ∀K,V. ⇩[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
72 #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
73 #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
76 (* Relocation properties ****************************************************)
78 lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
79 ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
80 ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
81 L ⊢ U1 [dt, et] ▶* U2.
82 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
83 [ #U2 #H >(lift_mono … HTU1 … H) -H //
84 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
85 elim (lift_total T d e) #U #HTU
86 lapply (IHT … HTU) -IHT #HU1
87 lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
91 lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
92 ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
93 ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
94 ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ▶* U2.
95 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2
96 [ #U2 #H >(lift_mono … HTU1 … H) -H //
97 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
98 elim (lift_total T d e) #U #HTU
99 lapply (IHT … HTU) -IHT #HU1
100 lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
104 lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
105 ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
106 ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
107 L ⊢ U1 [dt + e, et] ▶* U2.
108 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2
109 [ #U2 #H >(lift_mono … HTU1 … H) -H //
110 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
111 elim (lift_total T d e) #U #HTU
112 lapply (IHT … HTU) -IHT #HU1
113 lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
117 lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
118 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
120 ∃∃T2. K ⊢ T1 [dt, et] ▶* T2 & ⇧[d, e] T2 ≡ U2.
121 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
123 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
124 elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
128 lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
129 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
130 dt ≤ d → d + e ≤ dt + et →
131 ∃∃T2. K ⊢ T1 [dt, et - e] ▶* T2 & ⇧[d, e] T2 ≡ U2.
132 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
134 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
135 elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
139 lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
140 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
142 ∃∃T2. K ⊢ T1 [dt - e, et] ▶* T2 & ⇧[d, e] T2 ≡ U2.
143 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
145 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
146 elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
150 lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
151 L ⊢ U1 [d, e] ▶* U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
152 #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
153 #U #U2 #_ #HU2 #IHU destruct
154 <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
157 lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
158 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
159 dt ≤ d → dt + et ≤ d + e →
160 ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2.
161 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
163 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
164 elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/