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_2/notation/relations/rafter_3.ma".
16 include "ground_2/lib/streams_hdtl.ma".
17 include "ground_2/relocation/nstream_at.ma".
19 (* RELOCATION N-STREAM ******************************************************)
21 let corec compose: rtmap → rtmap → rtmap ≝ ?.
22 #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2
26 interpretation "functional composition (nstream)"
27 'compose f1 f2 = (compose f1 f2).
29 coinductive after: relation3 rtmap rtmap rtmap ≝
30 | after_refl: ∀f1,f2,f,g1,g2,g.
31 after f1 f2 f → g1 = ↑f1 → g2 = ↑f2 → g = ↑f → after g1 g2 g
32 | after_push: ∀f1,f2,f,g1,g2,g.
33 after f1 f2 f → g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → after g1 g2 g
34 | after_next: ∀f1,f2,f,g1,g.
35 after f1 f2 f → g1 = ⫯f1 → g = ⫯f → after g1 f2 g
38 interpretation "relational composition (nstream)"
39 'RAfter f1 f2 f = (after f1 f2 f).
41 (* Basic properies on compose ***********************************************)
43 lemma compose_unfold: ∀f1,f2,n2. f1∘(n2@f2) = f1@❴n2❵@tln … (⫯n2) f1∘f2.
44 #f1 #f2 #n2 >(stream_expand … (f1∘(n2@f2))) normalize //
47 lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f.
48 * #n1 #f1 * #n2 #f2 #f >compose_unfold >compose_unfold
49 #H destruct normalize //
52 (* Basic inversion lemmas on compose ****************************************)
54 lemma compose_inv_unfold: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f →
55 f1@❴n2❵ = n ∧ tln … (⫯n2) f1∘f2 = f.
56 #f1 #f2 #f #n2 #n >(stream_expand … (f1∘(n2@f2))) normalize
57 #H destruct /2 width=1 by conj/
60 lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f →
62 #f1 #f2 #f #n1 #n >compose_unfold
63 #H destruct /2 width=1 by conj/
66 lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f →
67 n = ⫯(n1+f1@❴n2❵) ∧ f1∘(n2@f2) = f1@❴n2❵@f.
68 #f1 #f2 #f #n1 #n2 #n >compose_unfold
69 #H destruct /2 width=1 by conj/
72 lemma compose_inv_S1: ∀f1,f2,f,n1,n2,n. (⫯n1@f1)∘(n2@f2) = n@f →
73 n = ⫯((n1@f1)@❴n2❵) ∧ (n1@f1)∘(n2@f2) = (n1@f1)@❴n2❵@f.
74 #f1 #f2 #f #n1 #n2 #n >compose_unfold
75 #H destruct /2 width=1 by conj/
78 (* Basic properties on after ************************************************)
80 lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
82 #f1 #f2 #f #Ht #n elim n -n /2 width=7 by after_refl, after_next/
85 lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f →
86 ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f.
87 #f1 #f2 #f #n2 #n #Ht #n1 elim n1 -n1 /2 width=7 by after_next, after_push/
90 lemma after_apply: ∀n2,f1,f2,f. (tln … (⫯n2) f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
92 [ * /2 width=1 by after_O2/
93 | #n2 #IH * /3 width=1 by after_S2/
97 let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?.
98 * #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1
100 [ #H cases (compose_inv_O2 … H) -H
101 /3 width=7 by after_refl, eq_f2/
102 | #n2 #H cases (compose_inv_S2 … H) -H
103 /3 width=7 by after_push/
105 | #n1 #H cases (compose_inv_S1 … H) -H
106 /4 width=7 by after_next, next_rew_sn/
110 theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2.
111 /2 width=1 by after_total_aux/ qed.
113 (* Basic inversion lemmas on after ******************************************)
115 fact after_inv_OOx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ↑f2 →
116 ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
117 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
118 [ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct
119 <(injective_push … Hx1) <(injective_push … Hx2) -x2 -x1
120 /2 width=3 by ex2_intro/
121 | #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
122 elim (discr_next_push … Hx2)
123 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
124 elim (discr_next_push … Hx1)
128 lemma after_inv_OOx: ∀f1,f2,g. ↑f1 ⊚ ↑f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f.
129 /2 width=5 by after_inv_OOx_aux/ qed-.
131 fact after_inv_OSx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ⫯f2 →
132 ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
133 #g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
134 [ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
135 elim (discr_push_next … Hx2)
136 | #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct
137 <(injective_push … Hx1) <(injective_next … Hx2) -x2 -x1
138 /2 width=3 by ex2_intro/
139 | #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
140 elim (discr_next_push … Hx1)
144 lemma after_inv_OSx: ∀f1,f2,g. ↑f1 ⊚ ⫯f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
145 /2 width=5 by after_inv_OSx_aux/ qed-.
147 fact after_inv_Sxx_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. g1 = ⫯f1 →
148 ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
149 #g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1
150 [ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
151 elim (discr_push_next … Hx1)
152 | #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
153 elim (discr_push_next … Hx1)
154 | #g #Hf #H1 #H #x1 #Hx1 destruct
155 <(injective_next … Hx1) -x1
156 /2 width=3 by ex2_intro/
160 lemma after_inv_Sxx: ∀f1,f2,g. ⫯f1 ⊚ f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f.
161 /2 width=5 by after_inv_Sxx_aux/ qed-.
163 (* Advanced inversion lemmas on after ***************************************)
165 fact after_inv_OOO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
166 ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ↑f → f1 ⊚ f2 ≡ f.
167 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
168 #x #Hf #Hx destruct >(injective_push … Hx) -f //
171 fact after_inv_OOS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
172 ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ⫯f → ⊥.
173 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
174 #x #Hf #Hx destruct elim (discr_next_push … Hx)
177 fact after_inv_OSS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
178 ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → f1 ⊚ f2 ≡ f.
179 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
180 #x #Hf #Hx destruct >(injective_next … Hx) -f //
183 fact after_inv_OSO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
184 ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ↑f → ⊥.
185 #g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
186 #x #Hf #Hx destruct elim (discr_push_next … Hx)
189 fact after_inv_SxS_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
190 ∀f1,f. g1 = ⫯f1 → g = ⫯f → f1 ⊚ f2 ≡ f.
191 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
192 #x #Hf #Hx destruct >(injective_next … Hx) -f //
195 fact after_inv_SxO_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
196 ∀f1,f. g1 = ⫯f1 → g = ↑f → ⊥.
197 #g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1
198 #x #Hf #Hx destruct elim (discr_push_next … Hx)
201 fact after_inv_OxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
202 ∀f1,f. g1 = ↑f1 → g = ↑f →
203 ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
204 #g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
205 [ elim (after_inv_OSO_aux … Hg … H1 … H) -g1 -g -f1 -f //
206 | lapply (after_inv_OOO_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
210 lemma after_inv_OxO: ∀f1,g2,f. ↑f1 ⊚ g2 ≡ ↑f →
211 ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2.
212 /2 width=5 by after_inv_OxO_aux/ qed-.
214 fact after_inv_OxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
215 ∀f1,f. g1 = ↑f1 → g = ⫯f →
216 ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ⫯f2.
217 #g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
218 [ lapply (after_inv_OSS_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
219 | elim (after_inv_OOS_aux … Hg … H1 … H) -g1 -g -f1 -f //
223 fact after_inv_xxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ↑f →
224 ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
225 * * [2: #m1 ] #g1 #g2 #g #Hg #f #H
226 [ elim (after_inv_SxO_aux … Hg … H) -g2 -g -f //
227 | elim (after_inv_OxO_aux … Hg … H) -g /2 width=5 by ex3_2_intro/
231 lemma after_inv_xxO: ∀g1,g2,f. g1 ⊚ g2 ≡ ↑f →
232 ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2.
233 /2 width=3 by after_inv_xxO_aux/ qed-.
235 fact after_inv_xxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ⫯f →
236 (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
237 ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
238 * * [2: #m1 ] #g1 #g2 #g #Hg #f #H
239 [ /4 width=5 by after_inv_SxS_aux, or_intror, ex2_intro/
240 | elim (after_inv_OxS_aux … Hg … H) -g
241 /3 width=5 by or_introl, ex3_2_intro/
245 lemma after_inv_xxS: ∀g1,g2,f. g1 ⊚ g2 ≡ ⫯f →
246 (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨
247 ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1.
248 /2 width=3 by after_inv_xxS_aux/ qed-.
250 fact after_inv_Oxx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. g1 = ↑f1 →
251 (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨
252 (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f).
253 #g1 * * [2: #m2 ] #g2 #g #Hg #f1 #H
254 [ elim (after_inv_OSx_aux … Hg … H) -g1
255 /3 width=5 by or_intror, ex3_2_intro/
256 | elim (after_inv_OOx_aux … Hg … H) -g1
257 /3 width=5 by or_introl, ex3_2_intro/
261 lemma after_inv_Oxx: ∀f1,g2,g. ↑f1 ⊚ g2 ≡ g →
262 (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨
263 (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f).
264 /2 width=3 by after_inv_Oxx_aux/ qed-.
266 fact after_inv_xOx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ↑f2 →
267 f1 ⊚ f2 ≡ f ∧ n1 = n.
268 #f1 #g2 #f #n1 elim n1 -n1
269 [ #n #Hf #f2 #H2 elim (after_inv_OOx_aux … Hf … H2) -g2 [3: // |2: skip ]
270 #g #Hf #H elim (push_inv_seq_sn … H) -H destruct /2 width=1 by conj/
271 | #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ]
272 #g1 #Hg #H1 elim (next_inv_seq_sn … H1) -H1
273 #x #Hx #H destruct elim (IH … Hg) [2: // |3: skip ] -IH -Hg
274 #H destruct /2 width=1 by conj/
278 lemma after_inv_xOx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ↑f2 ≡ n@f →
279 f1 ⊚ f2 ≡ f ∧ n1 = n.
280 /2 width=3 by after_inv_xOx_aux/ qed-.
282 fact after_inv_xSx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ⫯f2 →
283 ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m).
284 #f1 #g2 #f #n1 elim n1 -n1
285 [ #n #Hf #f2 #H2 elim (after_inv_OSx_aux … Hf … H2) -g2 [3: // |2: skip ]
286 #g #Hf #H elim (next_inv_seq_sn … H) -H
287 #x #Hx #Hg destruct /2 width=3 by ex2_intro/
288 | #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ]
289 #g #Hg #H elim (next_inv_seq_sn … H) -H
290 #x #Hx #H destruct elim (IH … Hg) -IH -Hg [3: // |2: skip ]
291 #m #Hf #Hm destruct /2 width=3 by ex2_intro/
295 lemma after_inv_xSx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ⫯f2 ≡ n@f →
296 ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m).
297 /2 width=3 by after_inv_xSx_aux/ qed-.
299 lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ n2 = 0.
300 #f1 #f2 #f #n2 #n elim n -n
301 [ #H elim (after_inv_OxO … H) -H
302 #g2 #Hf #H elim (push_inv_seq_sn … H) -H /2 width=1 by conj/
303 | #n #IH #H lapply (after_inv_SxS_aux … H ????) -H /2 width=5 by/
307 (* Forward lemmas on application ********************************************)
309 lemma after_at_fwd: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
310 ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i.
311 #f #i1 #i #H elim H -f -i1 -i
312 [ #f #f2 #f1 #H elim (after_inv_xxO … H) -H
313 /2 width=3 by at_refl, ex2_intro/
314 | #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxO … H) -H
315 #g2 #g1 #Hg #H1 #H2 destruct elim (IH … Hg) -f
316 /3 width=3 by at_S1, ex2_intro/
317 | #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxS … H) -H *
318 [ #g2 #g1 #Hg #H2 #H1 destruct elim (IH … Hg) -f
319 /3 width=3 by at_S1, at_next, ex2_intro/
320 | #g1 #Hg #H destruct elim (IH … Hg) -f
321 /3 width=3 by at_next, ex2_intro/
326 lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2,f. f2 ⊚ f1 ≡ f →
327 ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i.
328 #f1 #i1 #i2 #H elim H -f1 -i1 -i2
329 [ #f1 * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H /2 width=3 by ex2_intro/
330 | #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H
331 #Hf #H destruct elim (IH … Hf) -f1 /3 width=3 by at_S1, ex2_intro/
332 | #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xSx … H) -H
333 #m #Hf #Hm destruct elim (IH … Hf) -f1
334 /4 width=3 by at_plus2, at_S1, at_next, ex2_intro/
338 lemma after_fwd_at: ∀f1,f2,i1,i2,i. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i →
339 ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i.
340 #f1 #f2 #i1 #i2 #i #Hi1 #Hi2 #f #Ht elim (after_at1_fwd … Hi1 … Ht) -f1
341 #j #H #Hj >(at_mono … H … Hi2) -i2 //
344 lemma after_fwd_at1: ∀f2,f,i1,i2,i. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i →
345 ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2.
346 #f2 #f #i1 #i2 #i #Hi1 #Hi2 #f1 #Ht elim (after_at_fwd … Hi1 … Ht) -f
347 #j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
350 lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 →
351 ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i.
352 #f #i1 #i #H elim H -f -i1 -i
353 [ #f #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H
354 #g2 #g1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -f -g1 -i2 //
355 | #f #i1 #i #_ #IH #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H
356 #g2 #g1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1
357 /3 width=3 by at_push/
358 | #f #i1 #i #_ #IH #f1 #i2 #Hf1 #f2 #H elim (after_inv_xxS … H) -H *
359 [ #g2 #g1 #Hg #H2 #H1 destruct elim (at_inv_xSx … Hf1) -Hf1
360 /3 width=3 by at_push/
361 | #g2 #Hg #H destruct /3 width=3 by at_next/
366 (* Advanced forward lemmas on after *****************************************)
368 lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → n = f1@❴n2❵.
369 #f1 #f2 #f #n2 #n #H lapply (after_fwd_at … 0 … H) -H [1,4: // |2,3: skip ]
370 /3 width=2 by at_inv_O1, sym_eq/
373 lemma after_fwd_tl: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f →
374 tln … n2 f1 ⊚ f2 ≡ f.
375 #f #f2 #n2 elim n2 -n2
376 [ #f1 #n1 #n #H elim (after_inv_xOx … H) -H //
377 | #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xSx_aux … H ??) -H [3: // |2: skip ]
378 #m #Hm #H destruct /2 width=3 by/
382 lemma after_inv_apply: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f →
383 a = (a1@f1)@❴a2❵ ∧ tln … a2 f1 ⊚ f2 ≡ f.
384 /3 width=3 by after_fwd_tl, after_fwd_hd, conj/ qed-.
386 (* Main properties on after *************************************************)
388 let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
389 ∀f1,f2. f1 ⊚ f2 ≡ f0 →
390 ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?.
391 #f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
392 [ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
393 cases (after_inv_xxO_aux … Hg0 … H0) -g0
395 cases (after_inv_OOx_aux … Hg … H2 H3) -g2 -g3
396 #f #Hf #H /3 width=7 by after_refl/
397 | #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
398 cases (after_inv_xxO_aux … Hg0 … H0) -g0
400 cases (after_inv_OSx_aux … Hg … H2 H3) -g2 -g3
401 #f #Hf #H /3 width=7 by after_push/
402 | #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg
403 cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
404 [ #f1 #f2 #Hf0 #H1 #H2
405 cases (after_inv_Sxx_aux … Hg … H2) -g2
406 #f #Hf #H /3 width=7 by after_push/
407 | #f1 #Hf0 #H1 /3 width=6 by after_next/
412 let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
413 ∀f2, f3. f2 ⊚ f3 ≡ f0 →
414 ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?.
415 #f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
416 [ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
417 cases (after_inv_xxO_aux … Hg0 … H0) -g0
419 cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
420 #f #Hf #H /3 width=7 by after_refl/
421 | #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
422 cases (after_inv_xxS_aux … Hg0 … H0) -g0 *
423 [ #f2 #f3 #Hf0 #H2 #H3
424 cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2
425 #f #Hf #H /3 width=7 by after_push/
427 cases (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2
428 #f #Hf #H /3 width=6 by after_next/
430 | #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg
431 cases (after_inv_Sxx_aux … Hg … H1) -g1
432 #f #Hg #H /3 width=6 by after_next/
436 (* Main inversion lemmas on after *******************************************)
438 let corec after_mono: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
439 f1 ≐ g1 → f2 ≐ g2 → f ≐ g ≝ ?.
440 * #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
441 cases (after_inv_apply … Hf) -Hf #Hn #Hf
442 cases (after_inv_apply … Hg) -Hg #Hm #Hg
443 cases (eq_stream_inv_seq ????? H1) -H1
444 cases (eq_stream_inv_seq ????? H2) -H2
445 /4 width=8 by apply_eq_repl, tln_eq_repl, eq_seq/
448 let corec after_inj: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g →
449 f1 ≐ g1 → f ≐ g → f2 ≐ g2 ≝ ?.
450 * #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2
451 cases (after_inv_apply … Hf) -Hf #Hn #Hf
452 cases (after_inv_apply … Hg) -Hg #Hm #Hg
453 cases (eq_stream_inv_seq ????? H1) -H1 #Hnm1 #Hfg1
454 cases (eq_stream_inv_seq ????? H2) -H2 #Hnm #Hfg
455 lapply (apply_inj_aux … Hn Hm Hnm ?) -n -m
456 /4 width=8 by tln_eq_repl, eq_seq/
459 theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f.
460 /2 width=8 by after_mono/ qed-.
462 (* Properties on after ******************************************************)
464 lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄.
465 #f2 #f1 #f #Ht #H2 @isid_at_total
466 #i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1
467 /3 width=6 by at_inj, eq_stream_sym/
470 lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄.
471 #f2 #f1 #f #Ht #H1 @isid_at_total
472 #i2 #i #Hi2 lapply (at_total i2 f1)
473 #H0 lapply (at_increasing … H0)
474 #Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
475 /3 width=7 by at_eq_repl_back, at_mono, at_id_le/
478 (* Inversion lemmas on after ************************************************)
480 let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
481 * #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H
482 /3 width=7 by after_push, after_refl/
485 let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
487 [ #f1 #H cases (isid_inv_seq … H) -H
488 /3 width=7 by after_refl/
489 | #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/
493 lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f.
494 /3 width=8 by isid_after_sn, after_mono/
497 lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f.
498 /3 width=8 by isid_after_dx, after_mono/
501 axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.