]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_coafter.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/rcoafter_3.ma".
16 include "ground/xoa/ex_3_2.ma".
17 include "ground/relocation/pr_tl.ma".
18
19 (* RELATIONAL CO-COMPOSITION FOR PARTIAL RELOCATION MAPS ********************)
20
21 (*** coafter *)
22 coinductive pr_coafter: relation3 pr_map pr_map pr_map ≝
23 (*** coafter_refl *)
24 | pr_coafter_refl (f1) (f2) (f) (g1) (g2) (g):
25   pr_coafter f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → pr_coafter g1 g2 g
26 (*** coafter_push *)
27 | pr_coafter_push (f1) (f2) (f) (g1) (g2) (g):
28   pr_coafter f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → pr_coafter g1 g2 g
29 (*** coafter_next *)
30 | pr_coafter_next (f1) (f2) (f) (g1) (g):
31   pr_coafter f1 f2 f → ↑f1 = g1 → ⫯f = g → pr_coafter g1 f2 g
32 .
33
34 interpretation
35   "relational co-composition (partial relocation maps)"
36   'RCoAfter f1 f2 f = (pr_coafter f1 f2 f).
37
38 (* Basic inversions *********************************************************)
39
40 (*** coafter_inv_ppx *)
41 lemma pr_coafter_inv_push_bi:
42       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 →
43       ∃∃f. f1 ~⊚ f2 ≘ f & ⫯f = g.
44 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
45 [ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct
46   >(eq_inv_pr_push_bi … Hx1) >(eq_inv_pr_push_bi … Hx2) -x2 -x1
47   /2 width=3 by ex2_intro/
48 | #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
49   elim (eq_inv_pr_push_next … Hx2)
50 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
51   elim (eq_inv_pr_push_next … Hx1)
52 ]
53 qed-.
54
55 (*** coafter_inv_pnx *)
56 lemma pr_coafter_inv_push_next:
57       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 →
58       ∃∃f. f1 ~⊚ f2 ≘ f & ↑f = g.
59 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
60 [ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
61   elim (eq_inv_pr_next_push … Hx2)
62 | #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct
63   >(eq_inv_pr_push_bi … Hx1) >(eq_inv_pr_next_bi … Hx2) -x2 -x1
64   /2 width=3 by ex2_intro/
65 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
66   elim (eq_inv_pr_push_next … Hx1)
67 ]
68 qed-.
69
70 (*** coafter_inv_nxx *)
71 lemma pr_coafter_inv_next_sn:
72       ∀g1,f2,g. g1 ~⊚ f2 ≘ g → ∀f1. ↑f1 = g1 →
73       ∃∃f. f1 ~⊚ f2 ≘ f & ⫯f = g.
74 #g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1
75 [ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
76   elim (eq_inv_pr_next_push … Hx1)
77 | #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
78   elim (eq_inv_pr_next_push … Hx1)
79 | #g #Hf #H1 #H #x1 #Hx1 destruct
80   >(eq_inv_pr_next_bi … Hx1) -x1
81   /2 width=3 by ex2_intro/
82 ]
83 qed-.
84
85 (* Advanced inversions ******************************************************)
86
87 (*** coafter_inv_ppp *)
88 lemma pr_coafter_inv_push_bi_push:
89       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
90       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ~⊚ f2 ≘ f.
91 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H
92 elim (pr_coafter_inv_push_bi … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
93 <(eq_inv_pr_push_bi … Hx) -f //
94 qed-.
95
96 (*** coafter_inv_ppn *)
97 lemma pr_coafter_inv_push_bi_next:
98       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
99       ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
100 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H
101 elim (pr_coafter_inv_push_bi … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
102 elim (eq_inv_pr_push_next … Hx)
103 qed-.
104
105 (*** coafter_inv_pnn *)
106 lemma pr_coafter_inv_push_next_next:
107       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
108       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ~⊚ f2 ≘ f.
109 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H
110 elim (pr_coafter_inv_push_next … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
111 <(eq_inv_pr_next_bi … Hx) -f //
112 qed-.
113
114 (*** coafter_inv_pnp *)
115 lemma pr_coafter_inv_push_next_push:
116       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
117       ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ⫯f = g → ⊥.
118 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H
119 elim (pr_coafter_inv_push_next … Hg … H1 H2) -g1 -g2 #x #Hf #Hx destruct
120 elim (eq_inv_pr_next_push … Hx)
121 qed-.
122
123 (*** coafter_inv_nxp *)
124 lemma pr_coafter_inv_next_sn_push:
125       ∀g1,f2,g. g1 ~⊚ f2 ≘ g →
126       ∀f1,f. ↑f1 = g1 → ⫯f = g → f1 ~⊚ f2 ≘ f.
127 #g1 #f2 #g #Hg #f1 #f #H1 #H
128 elim (pr_coafter_inv_next_sn … Hg … H1) -g1 #x #Hf #Hx destruct
129 <(eq_inv_pr_push_bi … Hx) -f //
130 qed-.
131
132 (*** coafter_inv_nxn *)
133 lemma pr_coafter_inv_next_sn_next:
134       ∀g1,f2,g. g1 ~⊚ f2 ≘ g →
135       ∀f1,f. ↑f1 = g1 → ↑f = g → ⊥.
136 #g1 #f2 #g #Hg #f1 #f #H1 #H
137 elim (pr_coafter_inv_next_sn … Hg … H1) -g1 #x #Hf #Hx destruct
138 elim (eq_inv_pr_push_next … Hx)
139 qed-.
140
141 (*** coafter_inv_pxp *)
142 lemma pr_coafter_inv_push_sn_push:
143       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
144       ∀f1,f. ⫯f1 = g1 → ⫯f = g →
145       ∃∃f2. f1 ~⊚ f2 ≘ f & ⫯f2 = g2.
146 #g1 #g2 #g #Hg #f1 #f #H1 #H
147 elim (pr_map_split_tl g2) #H2
148 [ lapply (pr_coafter_inv_push_bi_push … Hg … H1 H2 H) -g1 -g
149   /2 width=3 by ex2_intro/
150 | elim (pr_coafter_inv_push_next_push … Hg … H1 H2 H)
151 ]
152 qed-.
153
154 (*** coafter_inv_pxn *)
155 lemma pr_coafter_inv_push_sn_next:
156       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
157       ∀f1,f. ⫯f1 = g1 → ↑f = g →
158       ∃∃f2. f1 ~⊚ f2 ≘ f & ↑f2 = g2.
159 #g1 #g2 #g #Hg #f1 #f #H1 #H
160 elim (pr_map_split_tl g2) #H2
161 [ elim (pr_coafter_inv_push_bi_next … Hg … H1 H2 H)
162 | lapply (pr_coafter_inv_push_next_next … Hg … H1 … H) -g1 -g
163   /2 width=3 by ex2_intro/
164 ]
165 qed-.
166
167 (*** coafter_inv_xxn *)
168 lemma pr_coafter_inv_next:
169       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f. ↑f = g →
170       ∃∃f1,f2. f1 ~⊚ f2 ≘ f & ⫯f1 = g1 & ↑f2 = g2.
171 #g1 #g2 #g #Hg #f #H
172 elim (pr_map_split_tl g1) #H1
173 [ elim (pr_coafter_inv_push_sn_next … Hg … H1 H) -g
174   /2 width=5 by ex3_2_intro/
175 | elim (pr_coafter_inv_next_sn_next … Hg … H1 H)
176 ]
177 qed-.
178
179 (*** coafter_inv_xnn *)
180 lemma pr_coafter_inv_next_dx_next:
181       ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
182       ∀f2,f. ↑f2 = g2 → ↑f = g →
183       ∃∃f1. f1 ~⊚ f2 ≘ f & ⫯f1 = g1.
184 #g1 #g2 #g #Hg #f2 #f #H2 destruct #H
185 elim (pr_coafter_inv_next … Hg … H) -g #z1 #z2 #Hf #H1 #H2 destruct
186 /2 width=3 by ex2_intro/
187 qed-.
188
189 (*** coafter_inv_xxp *)
190 lemma pr_coafter_inv_push:
191       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f. ⫯f = g →
192       ∨∨ ∃∃f1,f2. f1 ~⊚ f2 ≘ f & ⫯f1 = g1 & ⫯f2 = g2
193        | ∃∃f1. f1 ~⊚ g2 ≘ f & ↑f1 = g1.
194 #g1 #g2 #g #Hg #f #H
195 elim (pr_map_split_tl g1) #H1
196 [ elim (pr_coafter_inv_push_sn_push … Hg … H1 H) -g
197   /3 width=5 by or_introl, ex3_2_intro/
198 | /4 width=5 by pr_coafter_inv_next_sn_push, or_intror, ex2_intro/
199 ]
200 qed-.
201
202 (*** coafter_inv_pxx *)
203 lemma pr_coafter_inv_push_sn:
204       ∀g1,g2,g. g1 ~⊚ g2 ≘ g → ∀f1. ⫯f1 = g1 →
205       ∨∨ ∃∃f2,f. f1 ~⊚ f2 ≘ f & ⫯f2 = g2 & ⫯f = g
206        | ∃∃f2,f. f1 ~⊚ f2 ≘ f & ↑f2 = g2 & ↑f = g.
207 #g1 #g2 #g #Hg #f1 #H1
208 elim (pr_map_split_tl g2) #H2
209 [ elim (pr_coafter_inv_push_bi … Hg … H1 H2) -g1
210   /3 width=5 by or_introl, ex3_2_intro/
211 | elim (pr_coafter_inv_push_next … Hg … H1 H2) -g1
212   /3 width=5 by or_intror, ex3_2_intro/
213 ]
214 qed-.
215
216 (* Inversions with pr_tl ****************************************************)
217
218 (*** coafter_inv_tl1 *)
219 lemma pr_coafter_inv_tl_dx:
220       ∀g2,g1,g. g2 ~⊚ ⫰g1 ≘ g →
221       ∃∃f. ⫯g2 ~⊚ g1 ≘ f & ⫰f = g.
222 #g2 #g1 #g
223 elim (pr_map_split_tl g1) #H1 #H2
224 [ /3 width=7 by pr_coafter_refl, ex2_intro/
225 | @(ex2_intro … (↑g)) /2 width=7 by pr_coafter_push/ (* * full auto fails *)
226 ]
227 qed-.
228
229 (*** coafter_inv_tl0 *)
230 lemma pr_coafter_inv_tl:
231       ∀g2,g1,g. g2 ~⊚ g1 ≘ ⫰g →
232       ∃∃f1. ⫯g2 ~⊚ f1 ≘ g & ⫰f1 = g1.
233 #g2 #g1 #g
234 elim (pr_map_split_tl g) #H1 #H2
235 [ /3 width=7 by pr_coafter_refl, ex2_intro/
236 | @(ex2_intro … (↑g1)) /2 width=7 by pr_coafter_push/ (* * full auto fails *)
237 ]
238 qed-.