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 "ground/notation/relations/rafter_3.ma".
16 include "ground/xoa/ex_3_2.ma".
17 include "ground/relocation/pr_tl.ma".
19 (* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
22 coinductive pr_after: relation3 pr_map pr_map pr_map ≝
24 | pr_after_refl (f1) (f2) (f) (g1) (g2) (g):
25 pr_after f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → pr_after g1 g2 g
27 | pr_after_push (f1) (f2) (f) (g1) (g2) (g):
28 pr_after f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → pr_after g1 g2 g
30 | pr_after_next (f1) (f2) (f) (g1) (g):
31 pr_after f1 f2 f → ↑f1 = g1 → ↑f = g → pr_after g1 f2 g
35 "relational composition (partial relocation maps)"
36 'RAfter f1 f2 f = (pr_after f1 f2 f).
38 (* Basic inversions *********************************************************)
41 lemma pr_after_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)
56 lemma pr_after_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)
71 lemma pr_after_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/
85 (* Advanced inversions ******************************************************)
88 lemma pr_after_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 elim (pr_after_inv_push_bi … Hg … H1 H2) -g1 -g2
92 #x #Hf #Hx destruct <(eq_inv_pr_push_bi … Hx) -f //
96 lemma pr_after_inv_push_bi_next:
97 ∀g1,g2,g. g1 ⊚ g2 ≘ g →
98 ∀f1,f2,f. ⫯f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
99 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (pr_after_inv_push_bi … Hg … H1 H2) -g1 -g2
100 #x #Hf #Hx destruct elim (eq_inv_pr_push_next … Hx)
103 (*** after_inv_pnn *)
104 lemma pr_after_inv_push_next_next:
105 ∀g1,g2,g. g1 ⊚ g2 ≘ g →
106 ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⊚ f2 ≘ f.
107 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (pr_after_inv_push_next … Hg … H1 H2) -g1 -g2
108 #x #Hf #Hx destruct <(eq_inv_pr_next_bi … Hx) -f //
111 (*** after_inv_pnp *)
112 lemma pr_after_inv_push_next_push:
113 ∀g1,g2,g. g1 ⊚ g2 ≘ g →
114 ∀f1,f2,f. ⫯f1 = g1 → ↑f2 = g2 → ⫯f = g → ⊥.
115 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (pr_after_inv_push_next … Hg … H1 H2) -g1 -g2
116 #x #Hf #Hx destruct elim (eq_inv_pr_next_push … Hx)
119 (*** after_inv_nxn *)
120 lemma pr_after_inv_next_sn_next:
121 ∀g1,f2,g. g1 ⊚ f2 ≘ g →
122 ∀f1,f. ↑f1 = g1 → ↑f = g → f1 ⊚ f2 ≘ f.
123 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (pr_after_inv_next_sn … Hg … H1) -g1
124 #x #Hf #Hx destruct <(eq_inv_pr_next_bi … Hx) -f //
127 (*** after_inv_nxp *)
128 lemma pr_after_inv_next_sn_push:
129 ∀g1,f2,g. g1 ⊚ f2 ≘ g →
130 ∀f1,f. ↑f1 = g1 → ⫯f = g → ⊥.
131 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (pr_after_inv_next_sn … Hg … H1) -g1
132 #x #Hf #Hx destruct elim (eq_inv_pr_next_push … Hx)
135 (*** after_inv_pxp *)
136 lemma pr_after_inv_push_sn_push:
137 ∀g1,g2,g. g1 ⊚ g2 ≘ g →
138 ∀f1,f. ⫯f1 = g1 → ⫯f = g →
139 ∃∃f2. f1 ⊚ f2 ≘ f & ⫯f2 = g2.
140 #g1 #g2 elim (pr_map_split_tl g2)
141 #Hg2 #g #Hg #f1 #f #H1 #H
142 [ lapply (pr_after_inv_push_bi_push … Hg … H1 … H) -g1 -g
143 /2 width=3 by ex2_intro/
144 | elim (pr_after_inv_push_next_push … Hg … H1 … H) -g1 -g -f1 -f //
148 (*** after_inv_pxn *)
149 lemma pr_after_inv_push_sn_next:
150 ∀g1,g2,g. g1 ⊚ g2 ≘ g →
151 ∀f1,f. ⫯f1 = g1 → ↑f = g →
152 ∃∃f2. f1 ⊚ f2 ≘ f & ↑f2 = g2.
153 #g1 #g2 elim (pr_map_split_tl g2)
154 #Hg2 #g #Hg #f1 #f #H1 #H
155 [ elim (pr_after_inv_push_bi_next … Hg … H1 … H) -g1 -g -f1 -f //
156 | lapply (pr_after_inv_push_next_next … Hg … H1 … H) -g1 -g
157 /2 width=3 by ex2_intro/
161 (*** after_inv_xxp *)
162 lemma pr_after_inv_push:
163 ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f. ⫯f = g →
164 ∃∃f1,f2. f1 ⊚ f2 ≘ f & ⫯f1 = g1 & ⫯f2 = g2.
165 #g1 elim (pr_map_split_tl g1)
166 #Hg1 #g2 #g #Hg #f #H
167 [ elim (pr_after_inv_push_sn_push … Hg … H) -g /2 width=5 by ex3_2_intro/
168 | elim (pr_after_inv_next_sn_push … Hg … H) -g2 -g -f //
172 (*** after_inv_xxn *)
173 lemma pr_after_inv_next:
174 ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f. ↑f = g →
175 ∨∨ ∃∃f1,f2. f1 ⊚ f2 ≘ f & ⫯f1 = g1 & ↑f2 = g2
176 | ∃∃f1. f1 ⊚ g2 ≘ f & ↑f1 = g1.
177 #g1 elim (pr_map_split_tl g1)
178 #Hg1 #g2 #g #Hg #f #H
179 [ elim (pr_after_inv_push_sn_next … Hg … H) -g
180 /3 width=5 by or_introl, ex3_2_intro/
181 | /4 width=5 by pr_after_inv_next_sn_next, or_intror, ex2_intro/
185 (*** after_inv_pxx *)
186 lemma pr_after_inv_push_sn:
187 ∀g1,g2,g. g1 ⊚ g2 ≘ g → ∀f1. ⫯f1 = g1 →
188 ∨∨ ∃∃f2,f. f1 ⊚ f2 ≘ f & ⫯f2 = g2 & ⫯f = g
189 | ∃∃f2,f. f1 ⊚ f2 ≘ f & ↑f2 = g2 & ↑f = g.
190 #g1 #g2 elim (pr_map_split_tl g2)
192 [ elim (pr_after_inv_push_bi … Hg … H) -g1
193 /3 width=5 by or_introl, ex3_2_intro/
194 | elim (pr_after_inv_push_next … Hg … H) -g1
195 /3 width=5 by or_intror, ex3_2_intro/