]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_sor.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_sor.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/notation/relations/runion_3.ma".
16 include "ground/xoa/or_3.ma".
17 include "ground/xoa/ex_3_2.ma".
18 include "ground/relocation/pr_tl.ma".
19
20 (* RELATIONAL UNION FOR PARTIAL RELOCATION MAPS *****************************)
21
22 (*** sor *)
23 coinductive pr_sor: relation3 pr_map pr_map pr_map ≝
24 (*** sor_pp *)
25 | pr_sor_push_bi (f1) (f2) (f) (g1) (g2) (g):
26   pr_sor f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → pr_sor g1 g2 g
27 (*** sor_np *)
28 | pr_sor_next_push (f1) (f2) (f) (g1) (g2) (g):
29   pr_sor f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → pr_sor g1 g2 g
30 (*** sor_pn *)
31 | pr_sor_push_next (f1) (f2) (f) (g1) (g2) (g):
32   pr_sor f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → pr_sor g1 g2 g
33 (*** sor_nn *)
34 | pr_sor_next_bi (f1) (f2) (f) (g1) (g2) (g):
35   pr_sor f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → pr_sor g1 g2 g
36 .
37
38 interpretation
39   "relational union (partial relocation maps)"
40   'RUnion f1 f2 f = (pr_sor f1 f2 f).
41
42 (* Basic constructions ******************************************************)
43
44 (*** sor_idem *)
45 corec lemma pr_sor_idem:
46             ∀f. f ⋓ f ≘ f.
47 #f cases (pr_map_split_tl f) #H
48 [ @(pr_sor_push_bi … H H H)
49 | @(pr_sor_next_bi … H H H)
50 ] -H //
51 qed.
52
53 (*** sor_comm *)
54 corec lemma pr_sor_comm:
55             ∀f1,f2,f. f1 ⋓ f2 ≘ f → f2 ⋓ f1 ≘ f.
56 #f1 #f2 #f * -f1 -f2 -f
57 #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
58 [ @pr_sor_push_bi | @pr_sor_push_next | @pr_sor_next_push | @pr_sor_next_bi ] /2 width=7 by/
59 qed-.
60
61 (* Basic inversions *********************************************************)
62
63 (*** sor_inv_ppx *)
64 lemma pr_sor_inv_push_bi:
65       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 →
66       ∃∃f. f1 ⋓ f2 ≘ f & ⫯f = g.
67 #g1 #g2 #g * -g1 -g2 -g
68 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
69 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
70 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
71 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
72 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
73 /2 width=3 by ex2_intro/
74 qed-.
75
76 (*** sor_inv_npx *)
77 lemma pr_sor_inv_next_push:
78       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 →
79       ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
80 #g1 #g2 #g * -g1 -g2 -g
81 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
82 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
83 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
84 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
85 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
86 /2 width=3 by ex2_intro/
87 qed-.
88
89 (*** sor_inv_pnx *)
90 lemma pr_sor_inv_push_next:
91       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 →
92       ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
93 #g1 #g2 #g * -g1 -g2 -g
94 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
95 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
96 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
97 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
98 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
99 /2 width=3 by ex2_intro/
100 qed-.
101
102 (*** sor_inv_nnx *)
103 lemma pr_sor_inv_next_bi:
104       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 →
105       ∃∃f. f1 ⋓ f2 ≘ f & ↑f = g.
106 #g1 #g2 #g * -g1 -g2 -g
107 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct
108 try (>(eq_inv_pr_push_bi … Hx1) -x1) try (>(eq_inv_pr_next_bi … Hx1) -x1)
109 try elim (eq_inv_pr_push_next … Hx1) try elim (eq_inv_pr_next_push … Hx1)
110 try (>(eq_inv_pr_push_bi … Hx2) -x2) try (>(eq_inv_pr_next_bi … Hx2) -x2)
111 try elim (eq_inv_pr_push_next … Hx2) try elim (eq_inv_pr_next_push … Hx2)
112 /2 width=3 by ex2_intro/
113 qed-.
114
115 (* Advanced inversions ******************************************************)
116
117 (*** sor_inv_ppn *)
118 lemma pr_sor_inv_push_bi_next:
119       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
120       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
121 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
122 elim (pr_sor_inv_push_bi … H … H1 H2) -g1 -g2 #x #_ #H destruct
123 /2 width=3 by eq_inv_pr_push_next/
124 qed-.
125
126 (*** sor_inv_nxp *)
127 lemma pr_sor_inv_next_sn_push:
128       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
129       ∀f1,f. ↑f1 = g1 → ⫯f = g → ⊥.
130 #g1 #g2 #g #H #f1 #f #H1 #H0
131 elim (pr_map_split_tl g2) #H2
132 [ elim (pr_sor_inv_next_push … H … H1 H2)
133 | elim (pr_sor_inv_next_bi … H … H1 H2)
134 ] -g1 #x #H
135 /2 width=3 by eq_inv_pr_next_push/
136 qed-.
137
138 (*** sor_inv_xnp *)
139 lemma pr_sor_inv_next_dx_push:
140       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
141       ∀f2,f. ↑f2 = g2 → ⫯f = g → ⊥.
142 #g1 #g2 #g #H #f2 #f #H2 #H0
143 elim (pr_map_split_tl g1) #H1
144 [ elim (pr_sor_inv_push_next … H … H1 H2)
145 | elim (pr_sor_inv_next_bi … H … H1 H2)
146 ] -g2 #x #H
147 /2 width=3 by eq_inv_pr_next_push/
148 qed-.
149
150 (*** sor_inv_ppp *)
151 lemma pr_sor_inv_push_bi_push:
152       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
153       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ⋓ f2 ≘ f.
154 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
155 elim (pr_sor_inv_push_bi … H … H1 H2) -g1 -g2 #x #Hx #H destruct
156 <(eq_inv_pr_push_bi … H) -f //
157 qed-.
158
159 (*** sor_inv_npn *)
160 lemma pr_sor_inv_next_push_next:
161       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
162       ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
163 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
164 elim (pr_sor_inv_next_push … H … H1 H2) -g1 -g2 #x #Hx #H destruct
165 <(eq_inv_pr_next_bi … H) -f //
166 qed-.
167
168 (*** sor_inv_pnn *)
169 lemma pr_sor_inv_push_next_next:
170       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
171       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
172 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
173 elim (pr_sor_inv_push_next … H … H1 H2) -g1 -g2 #x #Hx #H destruct
174 <(eq_inv_pr_next_bi … H) -f //
175 qed-.
176
177 (*** sor_inv_nnn *)
178 lemma pr_sor_inv_next_bi_next:
179       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
180       ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⋓ f2 ≘ f.
181 #g1 #g2 #g #H #f1 #f2 #f #H1 #H2 #H0
182 elim (pr_sor_inv_next_bi … H … H1 H2) -g1 -g2 #x #Hx #H destruct
183 <(eq_inv_pr_next_bi … H) -f //
184 qed-.
185
186 (*** sor_inv_pxp *)
187 lemma pr_sor_inv_push_sn_push:
188       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
189       ∀f1,f. ⫯f1 = g1 → ⫯f = g →
190       ∃∃f2. f1 ⋓ f2 ≘ f & ⫯f2 = g2.
191 #g1 #g2 #g #H #f1 #f #H1 #H0
192 elim (pr_map_split_tl g2) #H2
193 [ /3 width=7 by pr_sor_inv_push_bi_push, ex2_intro/
194 | elim (pr_sor_inv_next_dx_push … H … H2 H0)
195 ]
196 qed-.
197
198 (*** sor_inv_xpp *)
199 lemma pr_sor_inv_push_dx_push:
200       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
201       ∀f2,f. ⫯f2 = g2 → ⫯f = g →
202       ∃∃f1. f1 ⋓ f2 ≘ f & ⫯f1 = g1.
203 #g1 #g2 #g #H #f2 #f #H2 #H0
204 elim (pr_map_split_tl g1) #H1
205 [ /3 width=7 by pr_sor_inv_push_bi_push, ex2_intro/
206 | elim (pr_sor_inv_next_sn_push … H … H1 H0)
207 ]
208 qed-.
209
210 (*** sor_inv_pxn *)
211 lemma pr_sor_inv_push_sn_next:
212       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
213       ∀f1,f. ⫯f1 = g1 → ↑f = g →
214       ∃∃f2. f1 ⋓ f2 ≘ f & ↑f2 = g2.
215 #g1 #g2 #g #H #f1 #f #H1 #H0
216 elim (pr_map_split_tl g2) #H2
217 [ elim (pr_sor_inv_push_bi_next … H … H1 H2 H0)
218 | /3 width=7 by pr_sor_inv_push_next_next, ex2_intro/
219 ]
220 qed-.
221
222 (*** sor_inv_xpn *)
223 lemma pr_sor_inv_push_dx_next:
224       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
225       ∀f2,f. ⫯f2 = g2 → ↑f = g →
226       ∃∃f1. f1 ⋓ f2 ≘ f & ↑f1 = g1.
227 #g1 #g2 #g #H #f2 #f #H2 #H0
228 elim (pr_map_split_tl g1) #H1
229 [ elim (pr_sor_inv_push_bi_next … H … H1 H2 H0)
230 | /3 width=7 by pr_sor_inv_next_push_next, ex2_intro/
231 ]
232 qed-.
233
234 (*** sor_inv_xxp *)
235 lemma pr_sor_inv_push:
236       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ⫯f = g →
237       ∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫯f1 = g1 & ⫯f2 = g2.
238 #g1 #g2 #g #H #f #H0
239 elim (pr_map_split_tl g1) #H1
240 [ elim (pr_sor_inv_push_sn_push … H … H1 H0) -g /2 width=5 by ex3_2_intro/
241 | elim (pr_sor_inv_next_sn_push … H … H1 H0)
242 ]
243 qed-.
244
245 (*** sor_inv_nxn *)
246 lemma pr_sor_inv_next_sn_next:
247       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
248       ∀f1,f. ↑f1 = g1 → ↑f = g →
249       ∨∨ ∃∃f2. f1 ⋓ f2 ≘ f & ⫯f2 = g2
250        | ∃∃f2. f1 ⋓ f2 ≘ f & ↑f2 = g2.
251 #g1 #g2 elim (pr_map_split_tl g2)
252 /4 width=7 by pr_sor_inv_next_push_next, pr_sor_inv_next_bi_next, ex2_intro, or_intror, or_introl/
253 qed-.
254
255 (*** sor_inv_xnn *)
256 lemma pr_sor_inv_next_dx_next:
257       ∀g1,g2,g. g1 ⋓ g2 ≘ g →
258       ∀f2,f. ↑f2 = g2 → ↑f = g →
259       ∨∨ ∃∃f1. f1 ⋓ f2 ≘ f & ⫯f1 = g1
260        | ∃∃f1. f1 ⋓ f2 ≘ f & ↑f1 = g1.
261 #g1 elim (pr_map_split_tl g1)
262 /4 width=7 by pr_sor_inv_push_next_next, pr_sor_inv_next_bi_next, ex2_intro, or_intror, or_introl/
263 qed-.
264
265 (*** sor_inv_xxn *)
266 lemma pr_sor_inv_next:
267       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
268       ∨∨ ∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫯f2 = g2
269        | ∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫯f1 = g1 & ↑f2 = g2
270        | ∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ↑f2 = g2.
271 #g1 #g2 #g #H #f #H0
272 elim (pr_map_split_tl g1) #H1
273 [ elim (pr_sor_inv_push_sn_next … H … H1 H0) -g
274   /3 width=5 by or3_intro1, ex3_2_intro/
275 | elim (pr_sor_inv_next_sn_next … H … H1 H0) -g *
276   /3 width=5 by or3_intro0, or3_intro2, ex3_2_intro/
277 ]
278 qed-.
279
280 (* Constructions with pr_tl *************************************************)
281
282 (*** sor_tl *)
283 lemma pr_sor_tl:
284       ∀f1,f2,f. f1 ⋓ f2 ≘ f → ⫰f1 ⋓ ⫰f2 ≘ ⫰f.
285 #f1 cases (pr_map_split_tl f1) #H1
286 #f2 cases (pr_map_split_tl f2) #H2
287 #f #Hf
288 [ cases (pr_sor_inv_push_bi … Hf … H1 H2)
289 | cases (pr_sor_inv_push_next … Hf … H1 H2)
290 | cases (pr_sor_inv_next_push … Hf … H1 H2)
291 | cases (pr_sor_inv_next_bi … Hf … H1 H2)
292 ] -Hf #g #Hg #H destruct //
293 qed.
294
295 (*** sor_xxn_tl *)
296 lemma pr_sor_next_tl:
297       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
298       (∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫰g2 = f2) ∨
299       (∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫰g1 = f1 & ↑f2 = g2).
300 #g1 #g2 #g #H #f #H0 elim (pr_sor_inv_next … H … H0) -H -H0 *
301 /3 width=5 by ex3_2_intro, or_introl, or_intror/
302 qed-.
303
304 (*** sor_xnx_tl *)
305 lemma pr_sor_next_dx_tl:
306       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f2. ↑f2 = g2 →
307       ∃∃f1,f. f1 ⋓ f2 ≘ f & ⫰g1 = f1 & ↑f = g.
308 #g1 elim (pr_map_split_tl g1) #H1 #g2 #g #H #f2 #H2
309 [ elim (pr_sor_inv_push_next … H … H1 H2)
310 | elim (pr_sor_inv_next_bi … H … H1 H2)
311 ] -g2
312 /3 width=5 by ex3_2_intro/
313 qed-.
314
315 (*** sor_nxx_tl *)
316 lemma pr_sor_next_sn_tl:
317       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1. ↑f1 = g1 →
318       ∃∃f2,f. f1 ⋓ f2 ≘ f & ⫰g2 = f2 & ↑f = g.
319 #g1 #g2 elim (pr_map_split_tl g2) #H2 #g #H #f1 #H1
320 [ elim (pr_sor_inv_next_push … H … H1 H2)
321 | elim (pr_sor_inv_next_bi … H … H1 H2)
322 ] -g1
323 /3 width=5 by ex3_2_intro/
324 qed-.
325
326 (* Inversions with pr_tl ****************************************************)
327
328 (*** sor_inv_tl_sn *)
329 lemma pr_sor_inv_tl_sn:
330       ∀f1,f2,f. ⫰f1 ⋓ f2 ≘ f → f1 ⋓ ↑f2 ≘ ↑f.
331 #f1 #f2 #f elim (pr_map_split_tl f1)
332 /2 width=7 by pr_sor_push_next, pr_sor_next_bi/
333 qed-.
334
335 (*** sor_inv_tl_dx *)
336 lemma pr_sor_inv_tl_dx:
337       ∀f1,f2,f. f1 ⋓ ⫰f2 ≘ f → ↑f1 ⋓ f2 ≘ ↑f.
338 #f1 #f2 #f elim (pr_map_split_tl f2)
339 /2 width=7 by pr_sor_next_push, pr_sor_next_bi/
340 qed-.