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/ltpss_sn.ma".
18 (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
20 lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
21 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
22 d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
23 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
24 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
26 | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
27 elim (le_inv_plus_l … He12) #_ #He2
28 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
29 lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
30 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
31 elim (le_inv_plus_l … Hd1e2) #_ #He2
32 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
33 lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
37 lemma ltpss_sn_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
38 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
39 d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
40 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
41 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
43 | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
44 elim (le_inv_plus_l … He12) #_ #He2
45 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
46 lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
47 | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
48 elim (le_inv_plus_l … Hd1e2) #_ #He2
49 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
50 lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
54 lemma ltpss_sn_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
55 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
56 ∃∃L. L2 ⊢ ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
57 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
58 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
59 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
60 lapply (le_n_O_to_eq … He2) -He2 #H destruct
61 lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
62 | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
63 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
64 [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
65 | -HK01 -HV01 <minus_le_minus_minus_comm //
66 elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
68 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
69 elim (le_inv_plus_l … Hd1e2) #_ #He2
70 <minus_le_minus_minus_comm //
71 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
72 elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
76 lemma ltpss_sn_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
77 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
78 ∃∃L. L ⊢ ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
79 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
80 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
81 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
82 lapply (le_n_O_to_eq … He2) -He2 #H destruct
83 lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
84 | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
85 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
86 [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
87 | -HK10 -HV10 <minus_le_minus_minus_comm //
88 elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
90 | #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
91 elim (le_inv_plus_l … Hd1e2) #_ #He2
92 <minus_le_minus_minus_comm //
93 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
94 elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
98 lemma ltpss_sn_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
99 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
100 ∃∃L. L2 ⊢ ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
101 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
102 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
104 | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
105 lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
106 lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
107 | #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
108 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
109 [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
110 | -HK01 -HV01 <minus_le_minus_minus_comm //
111 elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
116 lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
117 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
118 ∃∃L. L ⊢ ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
119 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
120 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
122 | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
123 lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
124 lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
125 | #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
126 lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
127 [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
128 | -HK10 -HV10 <minus_le_minus_minus_comm //
129 elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
134 lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
135 ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
136 d2 ≤ d1 → d1 ≤ d2 + e2 →
137 ∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 &
139 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
140 [ #d1 #e1 #K2 #d2 #e2 #H #_ #_
141 >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
142 | #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_
143 lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
144 | #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2
145 elim (IHLK1 … HK12 H1 H2) -K1 -H2
146 lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/
147 | #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12
148 elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct
149 [ lapply (le_n_O_to_eq … Hd12) -Hd12 <plus_n_Sm #H destruct
150 | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
151 elim (IHLK1 … HK12 …) -IHLK1 // /2 width=1/ >plus_minus_commutative // #L2 #HL12 #HLK2
152 elim (lift_total W2 d1 e1) #V2 #HWV2
153 lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // /2 width=1/
154 >plus_minus // >commutative_plus /4 width=5/
155 | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
156 elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2
157 elim (lift_total W2 d1 e1) #V2 #HWV2
158 lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // ] /2 width=1/
159 >commutative_plus /3 width=5/
164 lemma ldrop_ltpss_sn_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
165 ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d2 + e2 ≤ d1 →
166 ∃∃L2. L1 ⊢ ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
167 #L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
168 [ #d1 #e1 #K2 #d2 #e2 #H #_
169 >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
170 | #K1 #I #V1 #K2 #d2 #e2 #HK12 #H
171 elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/
172 | #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H
173 elim (IHLK1 … HK12 H) -K1
174 elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12
175 >(ltpss_sn_inv_refl_O2 … HL12) -L1 /3 width=5/
176 | #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21
177 elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct
178 [ -IHLK1 -Hd21 <(ltpss_sn_inv_refl_O2 … H) -X /3 width=5/
179 | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
180 elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2
181 elim (lift_total W2 d1 e1) #V2 #HWV2
182 lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 /2 width=1/ /3 width=5/
183 | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
184 elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2
185 elim (lift_total W2 d1 e1) #V2 #HWV2
186 lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/