]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / drops.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/xoa/ex_1_2.ma".
16 include "ground/xoa/ex_4_3.ma".
17 include "ground/relocation/rtmap_coafter.ma".
18 include "static_2/notation/relations/rdropstar_4.ma".
19 include "static_2/notation/relations/rdrop_3.ma".
20 include "static_2/relocation/seq.ma".
21 include "static_2/relocation/lifts_bind.ma".
22
23 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
24
25 (* Basic_1: includes: drop_skip_bind drop1_skip_bind *)
26 (* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip
27                         drop_refl_atom_O2 drop_drop_lt drop_skip_lt
28 *)
29 inductive drops (b:bool): pr_map → relation lenv ≝
30 | drops_atom: ∀f. (b = Ⓣ → 𝐈❨f❩) → drops b (f) (⋆) (⋆)
31 | drops_drop: ∀f,I,L1,L2. drops b f L1 L2 → drops b (↑f) (L1.ⓘ[I]) L2
32 | drops_skip: ∀f,I1,I2,L1,L2.
33               drops b f L1 L2 → ⇧*[f] I2 ≘ I1 →
34               drops b (⫯f) (L1.ⓘ[I1]) (L2.ⓘ[I2])
35 .
36
37 interpretation "generic slicing (local environment)"
38    'RDropStar b f L1 L2 = (drops b f L1 L2).
39
40 interpretation "uniform slicing (local environment)"
41    'RDrop i L1 L2 = (drops true (pr_uni i) L1 L2).
42
43 definition d_liftable1: predicate (relation2 lenv term) ≝
44                         λR. ∀K,T. R K T → ∀b,f,L. ⇩*[b,f] L ≘ K →
45                         ∀U. ⇧*[f] T ≘ U → R L U.
46
47 definition d_liftable1_isuni: predicate (relation2 lenv term) ≝
48                               λR. ∀K,T. R K T → ∀b,f,L. ⇩*[b,f] L ≘ K → 𝐔❨f❩ →
49                               ∀U. ⇧*[f] T ≘ U → R L U.
50
51 definition d_deliftable1: predicate (relation2 lenv term) ≝
52                           λR. ∀L,U. R L U → ∀b,f,K. ⇩*[b,f] L ≘ K →
53                           ∀T. ⇧*[f] T ≘ U → R K T.
54
55 definition d_deliftable1_isuni: predicate (relation2 lenv term) ≝
56                                 λR. ∀L,U. R L U → ∀b,f,K. ⇩*[b,f] L ≘ K → 𝐔❨f❩ →
57                                 ∀T. ⇧*[f] T ≘ U → R K T.
58
59 definition d_liftable2_sn: ∀C:Type[0]. ∀S:?→relation C.
60                            predicate (lenv→relation C) ≝
61                            λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⇩*[b,f] L ≘ K →
62                            ∀U1. S f T1 U1 →
63                            ∃∃U2. S f T2 U2 & R L U1 U2.
64
65 definition d_deliftable2_sn: ∀C:Type[0]. ∀S:?→relation C.
66                              predicate (lenv→relation C) ≝
67                              λC,S,R. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⇩*[b,f] L ≘ K →
68                              ∀T1. S f T1 U1 →
69                              ∃∃T2. S f T2 U2 & R K T1 T2.
70
71 definition d_liftable2_bi: ∀C:Type[0]. ∀S:?→relation C.
72                            predicate (lenv→relation C) ≝
73                            λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⇩*[b,f] L ≘ K →
74                            ∀U1. S f T1 U1 →
75                            ∀U2. S f T2 U2 → R L U1 U2.
76
77 definition d_deliftable2_bi: ∀C:Type[0]. ∀S:?→relation C.
78                              predicate (lenv→relation C) ≝
79                              λC,S,R. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⇩*[b,f] L ≘ K →
80                              ∀T1. S f T1 U1 →
81                              ∀T2. S f T2 U2 → R K T1 T2.
82
83 definition co_dropable_sn: predicate (?→relation lenv) ≝
84                            λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → 𝐔❨f❩ →
85                            ∀f2,L2. R f2 L1 L2 → ∀f1. f ~⊚ f1 ≘ f2 →
86                            ∃∃K2. R f1 K1 K2 & ⇩*[b,f] L2 ≘ K2.
87
88 definition co_dropable_dx: predicate (?→relation lenv) ≝
89                            λR. ∀f2,L1,L2. R f2 L1 L2 →
90                            ∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❨f❩ →
91                            ∀f1. f ~⊚ f1 ≘ f2 →
92                            ∃∃K1. ⇩*[b,f] L1 ≘ K1 & R f1 K1 K2.
93
94 definition co_dedropable_sn: predicate (?→relation lenv) ≝
95                              λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → ∀f1,K2. R f1 K1 K2 →
96                              ∀f2. f ~⊚ f1 ≘ f2 →
97                              ∃∃L2. R f2 L1 L2 & ⇩*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
98
99 (* Basic properties *********************************************************)
100
101 lemma drops_atom_F: ∀f. ⇩*[Ⓕ,f] ⋆ ≘ ⋆.
102 #f @drops_atom #H destruct
103 qed.
104
105 lemma drops_eq_repl_back: ∀b,L1,L2. pr_eq_repl_back … (λf. ⇩*[b,f] L1 ≘ L2).
106 #b #L1 #L2 #f1 #H elim H -f1 -L1 -L2
107 [ /4 width=3 by drops_atom, pr_isi_eq_repl_back/
108 | #f1 #I #L1 #L2 #_ #IH #f2 #H elim (eq_inv_nx … H) -H
109   /3 width=3 by drops_drop/
110 | #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H elim (eq_inv_px … H) -H
111   /3 width=3 by drops_skip, liftsb_eq_repl_back/
112 ]
113 qed-.
114
115 lemma drops_eq_repl_fwd: ∀b,L1,L2. pr_eq_repl_fwd … (λf. ⇩*[b,f] L1 ≘ L2).
116 #b #L1 #L2 @pr_eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *)
117 qed-.
118
119 (* Basic_2A1: includes: drop_FT *)
120 lemma drops_TF: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → ⇩*[Ⓕ,f] L1 ≘ L2.
121 #f #L1 #L2 #H elim H -f -L1 -L2
122 /3 width=1 by drops_atom, drops_drop, drops_skip/
123 qed.
124
125 (* Basic_2A1: includes: drop_gen *)
126 lemma drops_gen: ∀b,f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → ⇩*[b,f] L1 ≘ L2.
127 * /2 width=1 by drops_TF/
128 qed-.
129
130 (* Basic_2A1: includes: drop_T *)
131 lemma drops_F: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → ⇩*[Ⓕ,f] L1 ≘ L2.
132 * /2 width=1 by drops_TF/
133 qed-.
134
135 lemma d_liftable2_sn_bi: ∀C,S. (∀f,c. is_mono … (S f c)) →
136                          ∀R. d_liftable2_sn C S R → d_liftable2_bi C S R.
137 #C #S #HS #R #HR #K #T1 #T2 #HT12 #b #f #L #HLK #U1 #HTU1 #U2 #HTU2
138 elim (HR … HT12 … HLK … HTU1) -HR -K -T1 #X #HTX #HUX
139 <(HS … HTX … HTU2) -T2 -U2 -b -f //
140 qed-.
141
142 lemma d_deliftable2_sn_bi: ∀C,S. (∀f. is_inj2 … (S f)) →
143                            ∀R. d_deliftable2_sn C S R → d_deliftable2_bi C S R.
144 #C #S #HS #R #HR #L #U1 #U2 #HU12 #b #f #K #HLK #T1 #HTU1 #T2 #HTU2
145 elim (HR … HU12 … HLK … HTU1) -HR -L -U1 #X #HUX #HTX
146 <(HS … HUX … HTU2) -U2 -T2 -b -f //
147 qed-.
148
149 (* Basic inversion lemmas ***************************************************)
150
151 fact drops_inv_atom1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → X = ⋆ →
152                           Y = ⋆ ∧ (b = Ⓣ → 𝐈❨f❩).
153 #b #f #X #Y * -f -X -Y
154 [ /3 width=1 by conj/
155 | #f #I #L1 #L2 #_ #H destruct
156 | #f #I1 #I2 #L1 #L2 #_ #_ #H destruct
157 ]
158 qed-.
159
160 (* Basic_1: includes: drop_gen_sort *)
161 (* Basic_2A1: includes: drop_inv_atom1 *)
162 lemma drops_inv_atom1: ∀b,f,Y. ⇩*[b,f] ⋆ ≘ Y → Y = ⋆ ∧ (b = Ⓣ → 𝐈❨f❩).
163 /2 width=3 by drops_inv_atom1_aux/ qed-.
164
165 fact drops_inv_drop1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I,K. X = K.ⓘ[I] → f = ↑g →
166                           ⇩*[b,g] K ≘ Y.
167 #b #f #X #Y * -f -X -Y
168 [ #f #Hf #g #J #K #H destruct
169 | #f #I #L1 #L2 #HL #g #J #K #H1 #H2 <(eq_inv_pr_next_bi … H2) -g destruct //
170 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J #K #_ #H2 elim (eq_inv_pr_push_next … H2)
171 ]
172 qed-.
173
174 (* Basic_1: includes: drop_gen_drop *)
175 (* Basic_2A1: includes: drop_inv_drop1_lt drop_inv_drop1 *)
176 lemma drops_inv_drop1: ∀b,f,I,K,Y. ⇩*[b,↑f] K.ⓘ[I] ≘ Y → ⇩*[b,f] K ≘ Y.
177 /2 width=6 by drops_inv_drop1_aux/ qed-.
178
179 fact drops_inv_skip1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I1,K1. X = K1.ⓘ[I1] → f = ⫯g →
180                           ∃∃I2,K2. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & Y = K2.ⓘ[I2].
181 #b #f #X #Y * -f -X -Y
182 [ #f #Hf #g #J1 #K1 #H destruct
183 | #f #I #L1 #L2 #_ #g #J1 #K1 #_ #H2 elim (eq_inv_pr_next_push … H2)
184 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct
185   /2 width=5 by ex3_2_intro/
186 ]
187 qed-.
188
189 (* Basic_1: includes: drop_gen_skip_l *)
190 (* Basic_2A1: includes: drop_inv_skip1 *)
191 lemma drops_inv_skip1: ∀b,f,I1,K1,Y. ⇩*[b,⫯f] K1.ⓘ[I1] ≘ Y →
192                        ∃∃I2,K2. ⇩*[b,f] K1 ≘ K2 & ⇧*[f] I2 ≘ I1 & Y = K2.ⓘ[I2].
193 /2 width=5 by drops_inv_skip1_aux/ qed-.
194
195 fact drops_inv_skip2_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I2,K2. Y = K2.ⓘ[I2] → f = ⫯g →
196                           ∃∃I1,K1. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & X = K1.ⓘ[I1].
197 #b #f #X #Y * -f -X -Y
198 [ #f #Hf #g #J2 #K2 #H destruct
199 | #f #I #L1 #L2 #_ #g #J2 #K2 #_ #H2 elim (eq_inv_pr_next_push … H2)
200 | #f #I1 #I2 #L1 #L2 #HL #HV #g #J2 #K2 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct
201   /2 width=5 by ex3_2_intro/
202 ]
203 qed-.
204
205 (* Basic_1: includes: drop_gen_skip_r *)
206 (* Basic_2A1: includes: drop_inv_skip2 *)
207 lemma drops_inv_skip2: ∀b,f,I2,X,K2. ⇩*[b,⫯f] X ≘ K2.ⓘ[I2] →
208                        ∃∃I1,K1. ⇩*[b,f] K1 ≘ K2 & ⇧*[f] I2 ≘ I1 & X = K1.ⓘ[I1].
209 /2 width=5 by drops_inv_skip2_aux/ qed-.
210
211 (* Basic forward lemmas *****************************************************)
212
213 fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⇩*[b,f2] X ≘ Y → ∀I,K. Y = K.ⓘ[I] →
214                           ∃∃f1,f. 𝐈❨f1❩ & f2 ⊚ ↑f1 ≘ f & ⇩*[b,f] X ≘ K.
215 #b #f2 #X #Y #H elim H -f2 -X -Y
216 [ #f2 #Hf2 #J #K #H destruct
217 | #f2 #I #L1 #L2 #_ #IHL #J #K #H elim (IHL … H) -IHL
218   /3 width=7 by pr_after_next, ex3_2_intro, drops_drop/
219 | #f2 #I1 #I2 #L1 #L2 #HL #_ #_ #J #K #H destruct
220   lapply (pr_after_isi_dx 𝐢 … f2) /3 width=9 by pr_after_push, ex3_2_intro, drops_drop/
221 ]
222 qed-.
223
224 lemma drops_fwd_drop2: ∀b,f2,I,X,K. ⇩*[b,f2] X ≘ K.ⓘ[I] →
225                        ∃∃f1,f. 𝐈❨f1❩ & f2 ⊚ ↑f1 ≘ f & ⇩*[b,f] X ≘ K.
226 /2 width=4 by drops_fwd_drop2_aux/ qed-.
227
228 (* Properties with test for identity ****************************************)
229
230 (* Basic_2A1: includes: drop_refl *)
231 lemma drops_refl: ∀b,L,f. 𝐈❨f❩ → ⇩*[b,f] L ≘ L.
232 #b #L elim L -L /2 width=1 by drops_atom/
233 #L #I #IHL #f #Hf elim (pr_isi_inv_gen … Hf) -Hf
234 /3 width=1 by drops_skip, liftsb_refl/
235 qed.
236
237 (* Forward lemmas test for identity *****************************************)
238
239 (* Basic_1: includes: drop_gen_refl *)
240 (* Basic_2A1: includes: drop_inv_O2 *)
241 lemma drops_fwd_isid: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → 𝐈❨f❩ → L1 = L2.
242 #b #f #L1 #L2 #H elim H -f -L1 -L2 //
243 [ #f #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) //
244 | /5 width=5 by pr_isi_inv_push, liftsb_fwd_isid, eq_f2, sym_eq/
245 ]
246 qed-.
247
248 lemma drops_after_fwd_drop2: ∀b,f2,I,X,K. ⇩*[b,f2] X ≘ K.ⓘ[I] →
249                              ∀f1,f. 𝐈❨f1❩ → f2 ⊚ ↑f1 ≘ f → ⇩*[b,f] X ≘ K.
250 #b #f2 #I #X #K #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H
251 #g1 #g #Hg1 #Hg #HK lapply (pr_after_mono_eq … Hg … Hf ??) -Hg -Hf
252 /3 width=5 by drops_eq_repl_back, pr_isi_inv_eq_repl, pr_eq_next/
253 qed-.
254
255 (* Forward lemmas with test for finite colength *****************************)
256
257 lemma drops_fwd_isfin: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐅❨f❩.
258 #f #L1 #L2 #H elim H -f -L1 -L2
259 /3 width=1 by pr_isf_next, pr_isf_push, pr_isf_isi/
260 qed-.
261
262 (* Properties with test for uniformity **************************************)
263
264 lemma drops_isuni_ex: ∀f. 𝐔❨f❩ → ∀L. ∃K. ⇩*[Ⓕ,f] L ≘ K.
265 #f #H elim H -f /4 width=2 by drops_refl, drops_TF, ex_intro/
266 #f #_ #g #H #IH destruct * /2 width=2 by ex_intro/
267 #L #I elim (IH L) -IH /3 width=2 by drops_drop, ex_intro/
268 qed-.
269
270 (* Inversion lemmas with test for uniformity ********************************)
271
272 lemma drops_inv_isuni: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐔❨f❩ →
273                        (𝐈❨f❩ ∧ L1 = L2) ∨
274                        ∃∃g,I,K. ⇩*[Ⓣ,g] K ≘ L2 & 𝐔❨g❩ & L1 = K.ⓘ[I] & f = ↑g.
275 #f #L1 #L2 * -f -L1 -L2
276 [ /4 width=1 by or_introl, conj/
277 | /4 width=7 by pr_isu_inv_next, ex4_3_intro, or_intror/
278 | /7 width=6 by drops_fwd_isid, liftsb_fwd_isid, pr_isu_inv_push, pr_isi_push, or_introl, conj, eq_f2, sym_eq/
279 ]
280 qed-.
281
282 (* Basic_2A1: was: drop_inv_O1_pair1 *)
283 lemma drops_inv_bind1_isuni: ∀b,f,I,K,L2. 𝐔❨f❩ → ⇩*[b,f] K.ⓘ[I] ≘ L2 →
284                              (𝐈❨f❩ ∧ L2 = K.ⓘ[I]) ∨
285                              ∃∃g. 𝐔❨g❩ & ⇩*[b,g] K ≘ L2 & f = ↑g.
286 #b #f #I #K #L2 #Hf #H elim (pr_isu_split … Hf) -Hf * #g #Hg #H0 destruct
287 [ lapply (drops_inv_skip1 … H) -H * #Z #Y #HY #HZ #H destruct
288   <(drops_fwd_isid … HY Hg) -Y >(liftsb_fwd_isid … HZ Hg) -Z
289   /4 width=3 by pr_isi_push, or_introl, conj/
290 | lapply (drops_inv_drop1 … H) -H /3 width=4 by ex3_intro, or_intror/
291 ]
292 qed-.
293
294 (* Basic_2A1: was: drop_inv_O1_pair2 *)
295 lemma drops_inv_bind2_isuni: ∀b,f,I,K,L1. 𝐔❨f❩ → ⇩*[b,f] L1 ≘ K.ⓘ[I] →
296                              (𝐈❨f❩ ∧ L1 = K.ⓘ[I]) ∨
297                              ∃∃g,I1,K1. 𝐔❨g❩ & ⇩*[b,g] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1] & f = ↑g.
298 #b #f #I #K *
299 [ #Hf #H elim (drops_inv_atom1 … H) -H #H destruct
300 | #L1 #I1 #Hf #H elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
301   [ #Hf #H destruct /3 width=1 by or_introl, conj/
302   | /3 width=7 by ex4_3_intro, or_intror/
303   ]
304 ]
305 qed-.
306
307 lemma drops_inv_bind2_isuni_next: ∀b,f,I,K,L1. 𝐔❨f❩ → ⇩*[b,↑f] L1 ≘ K.ⓘ[I] →
308                                   ∃∃I1,K1. ⇩*[b,f] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1].
309 #b #f #I #K #L1 #Hf #H elim (drops_inv_bind2_isuni … H) -H /2 width=3 by pr_isu_next/ -Hf *
310 [ #H elim (pr_isi_inv_next … H) -H //
311 | /2 width=4 by ex2_2_intro/
312 ]
313 qed-.
314
315 fact drops_inv_TF_aux: ∀f,L1,L2. ⇩*[Ⓕ,f] L1 ≘ L2 → 𝐔❨f❩ →
316                        ∀I,K. L2 = K.ⓘ[I] → ⇩*[Ⓣ,f] L1 ≘ K.ⓘ[I].
317 #f #L1 #L2 #H elim H -f -L1 -L2
318 [ #f #_ #_ #J #K #H destruct
319 | #f #I #L1 #L2 #_ #IH #Hf #J #K #H destruct
320   /4 width=3 by drops_drop, pr_isu_inv_next/
321 | #f #I1 #I2 #L1 #L2 #HL12 #HI21 #_ #Hf #J #K #H destruct
322   lapply (pr_isu_inv_push … Hf ??) -Hf [1,2: // ] #Hf
323   <(drops_fwd_isid … HL12) -K // <(liftsb_fwd_isid … HI21) -I1
324   /3 width=3 by drops_refl, pr_isi_push/
325 ]
326 qed-.
327
328 (* Basic_2A1: includes: drop_inv_FT *)
329 lemma drops_inv_TF: ∀f,I,L,K. ⇩*[Ⓕ,f] L ≘ K.ⓘ[I] → 𝐔❨f❩ → ⇩*[Ⓣ,f] L ≘ K.ⓘ[I].
330 /2 width=3 by drops_inv_TF_aux/ qed-.
331
332 (* Basic_2A1: includes: drop_inv_gen *)
333 lemma drops_inv_gen: ∀b,f,I,L,K. ⇩*[b,f] L ≘ K.ⓘ[I] → 𝐔❨f❩ → ⇩*[Ⓣ,f] L ≘ K.ⓘ[I].
334 * /2 width=1 by drops_inv_TF/
335 qed-.
336
337 (* Basic_2A1: includes: drop_inv_T *)
338 lemma drops_inv_F: ∀b,f,I,L,K. ⇩*[Ⓕ,f] L ≘ K.ⓘ[I] → 𝐔❨f❩ → ⇩*[b,f] L ≘ K.ⓘ[I].
339 * /2 width=1 by drops_inv_TF/
340 qed-.
341
342 (* Forward lemmas with test for uniformity **********************************)
343
344 (* Basic_1: was: drop_S *)
345 (* Basic_2A1: was: drop_fwd_drop2 *)
346 lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K. 𝐔❨f❩ → ⇩*[b,f] X ≘ K.ⓘ[I] → ⇩*[b,↑f] X ≘ K.
347 /3 width=7 by drops_after_fwd_drop2, pr_after_isu_isi_next/ qed-.
348
349 (* Inversion lemmas with uniform relocations ********************************)
350
351 lemma drops_inv_atom2: ∀b,L,f. ⇩*[b,f] L ≘ ⋆ →
352                        ∃∃n,f1. ⇩*[b,𝐔❨n❩] L ≘ ⋆ & 𝐔❨n❩ ⊚ f1 ≘ f.
353 #b #L elim L -L
354 [ /3 width=4 by drops_atom, pr_after_isi_sn, ex2_2_intro/
355 | #L #I #IH #f #H elim (pr_map_split_tl f) * #g #H0 destruct
356   [ elim (drops_inv_skip1 … H) -H #J #K #_ #_ #H destruct
357   | lapply (drops_inv_drop1 … H) -H #HL
358     elim (IH … HL) -IH -HL /3 width=8 by drops_drop, pr_after_next, ex2_2_intro/
359   ]
360 ]
361 qed-.
362
363 lemma drops_inv_succ: ∀L1,L2,i. ⇩[↑i] L1 ≘ L2 →
364                       ∃∃I,K. ⇩[i] K ≘ L2 & L1 = K.ⓘ[I].
365 #L1 #L2 #i #H elim (drops_inv_isuni … H) -H // *
366 [ #H elim (pr_isi_inv_next … H) -H //
367 | /2 width=4 by ex2_2_intro/
368 ]
369 qed-.
370
371 (* Properties with uniform relocations **************************************)
372
373 lemma drops_F_uni: ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ ∨ ∃∃I,K. ⇩[i] L ≘ K.ⓘ[I].
374 #L elim L -L /2 width=1 by or_introl/
375 #L #I #IH * /4 width=3 by drops_refl, ex1_2_intro, or_intror/
376 #i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/
377 * /4 width=3 by drops_drop, ex1_2_intro, or_intror/
378 qed-.
379
380 (* Basic_2A1: includes: drop_split *)
381 lemma drops_split_trans: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → ∀f1,f2. f1 ⊚ f2 ≘ f → 𝐔❨f1❩ →
382                          ∃∃L. ⇩*[b,f1] L1 ≘ L & ⇩*[b,f2] L ≘ L2.
383 #b #f #L1 #L2 #H elim H -f -L1 -L2
384 [ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom
385   #H lapply (H0f H) -b
386   #H elim (pr_after_inv_isi … Hf H) -f //
387 | #f #I #L1 #L2 #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (pr_after_inv_next … Hf) -Hf [1,3: * |*: // ]
388   [ #g1 #g2 #Hf #H1 #H2 destruct
389     lapply (pr_isu_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1
390     elim (IHL12 … Hf) -f
391     /4 width=5 by drops_drop, drops_skip, liftsb_refl, pr_isu_isi, ex2_intro/
392   | #g1 #Hf #H destruct elim (IHL12 … Hf) -f
393     /3 width=5 by ex2_intro, drops_drop, pr_isu_inv_next/
394   ]
395 | #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #f1 #f2 #Hf #Hf1 elim (pr_after_inv_push … Hf) -Hf [2,3: // ]
396   #g1 #g2 #Hf #H1 #H2 destruct elim (liftsb_split_trans … HI21 … Hf) -HI21
397   elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, pr_isu_fwd_push/
398 ]
399 qed-.
400
401 lemma drops_split_div: ∀b,f1,L1,L. ⇩*[b,f1] L1 ≘ L → ∀f2,f. f1 ⊚ f2 ≘ f → 𝐔❨f2❩ →
402                        ∃∃L2. ⇩*[Ⓕ,f2] L ≘ L2 & ⇩*[Ⓕ,f] L1 ≘ L2.
403 #b #f1 #L1 #L #H elim H -f1 -L1 -L
404 [ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct
405 | #f1 #I #L1 #L #HL1 #IH #f2 #f #Hf #Hf2 elim (pr_after_inv_next_sn … Hf) -Hf [2,3: // ]
406   #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/
407 | #f1 #I1 #I #L1 #L #HL1 #HI1 #IH #f2 #f #Hf #Hf2
408   elim (pr_after_inv_push_sn … Hf) -Hf [1,3: * |*: // ]
409   #g2 #g #Hg #H2 #H0 destruct
410   [ lapply (pr_isu_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
411     lapply (pr_after_isi_inv_dx … Hg … Hg2) -Hg #Hg
412     /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, pr_isi_push, ex2_intro/
413   | lapply (pr_isu_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1
414     elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/
415   ]
416 ]
417 qed-.
418
419 (* Properties with application **********************************************)
420
421 lemma drops_tls_at: ∀f,i1,i2. @❨i1,f❩ ≘ i2 →
422                     ∀b,L1,L2. ⇩*[b,⫰*[i2]f] L1 ≘ L2 →
423                     ⇩*[b,⫯⫰*[↑i2]f] L1 ≘ L2.
424 /3 width=3 by drops_eq_repl_fwd, pr_pat_inv_succ_dx_tls/ qed-.
425
426 lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❨O,f❩ ≘ i →
427                                ∃∃J,K. ⇩[i]L ≘ K.ⓘ[J] & ⇩*[b,⫰*[↑i]f] K ≘ K0 & ⇧*[⫰*[↑i]f] I ≘ J.
428 #b #f #I #L #K0 #H #i #Hf
429 elim (drops_split_trans … H) -H [ |5: @(pr_after_nat_uni … Hf) |2,3: skip ] /2 width=1 by pr_after_isi_dx/ #Y #HLY #H
430 lapply (drops_tls_at … Hf … H) -H #H
431 elim (drops_inv_skip2 … H) -H #J #K #HK0 #HIJ #H destruct
432 /3 width=5 by drops_inv_gen, ex3_2_intro/
433 qed-.
434
435 (* Properties with context-sensitive equivalence for terms ******************)
436
437 lemma ceq_lift_sn: d_liftable2_sn … liftsb ceq_ext.
438 #K #I1 #I2 #H <(ceq_ext_inv_eq … H) -I2
439 /2 width=3 by ex2_intro/ qed-.
440
441 lemma ceq_inv_lift_sn: d_deliftable2_sn … liftsb ceq_ext.
442 #L #J1 #J2 #H <(ceq_ext_inv_eq … H) -J2
443 /2 width=3 by ex2_intro/ qed-.
444
445 (* Note: d_deliftable2_sn cfull does not hold *)
446 lemma cfull_lift_sn: d_liftable2_sn … liftsb cfull.
447 #K #I1 #I2 #_ #b #f #L #_ #J1 #_ -K -I1 -b
448 elim (liftsb_total I2 f) /2 width=3 by ex2_intro/
449 qed-.
450
451 (* Basic_2A1: removed theorems 12:
452               drops_inv_nil drops_inv_cons d1_liftable_liftables
453               drop_refl_atom_O2 drop_inv_pair1
454               drop_inv_Y1 drop_Y1 drop_O_Y drop_fwd_Y2
455               drop_fwd_length_minus2 drop_fwd_length_minus4
456 *)
457 (* Basic_1: removed theorems 53:
458             drop1_gen_pnil drop1_gen_pcons drop1_getl_trans
459             drop_ctail drop_skip_flat
460             cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
461             drop_clear drop_clear_O drop_clear_S
462             clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r
463             clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle
464             getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans
465             getl_clear_bind getl_clear_conf getl_dec getl_drop getl_drop_conf_lt
466             getl_drop_conf_ge getl_conf_ge_drop getl_drop_conf_rev
467             drop_getl_trans_lt drop_getl_trans_le drop_getl_trans_ge
468             getl_drop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O
469             getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le
470             getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono
471 *)