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/relocation/nstream_istot.ma".
16 include "ground_2/relocation/rtmap_after.ma".
18 (* RELOCATION N-STREAM ******************************************************)
20 corec definition compose: rtmap → rtmap → rtmap.
21 #f2 * #n1 #f1 @(seq … (f2@❴n1❵)) @(compose ? f1) -compose -f1
25 interpretation "functional composition (nstream)"
26 'compose f2 f1 = (compose f2 f1).
28 (* Basic properies on compose ***********************************************)
30 lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵@(↓*[⫯n1]f2)∘f1 = f2∘(n1@f1).
31 #f2 #f1 #n1 <(stream_rew … (f2∘(n1@f1))) normalize //
34 lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (⫯f2)∘f1 = ⫯f.
35 #f2 * #n1 #f1 #f <compose_rew <compose_rew
36 * -f <tls_S1 /2 width=1 by eq_f2/
39 (* Basic inversion lemmas on compose ****************************************)
41 lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1@f1) = n@f →
42 f2@❴n1❵ = n ∧ (↓*[⫯n1]f2)∘f1 = f.
43 #f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1@f1))) normalize
44 #H destruct /2 width=1 by conj/
47 lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2@f2)∘(↑f1) = n@f →
49 #f2 #f1 #f #n2 #n <compose_rew
50 #H destruct /2 width=1 by conj/
53 lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2@f2)∘(⫯n1@f1) = n@f →
54 ⫯(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
55 #f2 #f1 #f #n2 #n1 #n <compose_rew
56 #H destruct <tls_S1 /2 width=1 by conj/
59 lemma compose_inv_S1: ∀f2,f1,f,n1,n. (⫯f2)∘(n1@f1) = n@f →
60 ⫯(f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
61 #f2 #f1 #f #n1 #n <compose_rew
62 #H destruct <tls_S1 /2 width=1 by conj/
65 (* Specific properties on after *********************************************)
67 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
69 #f2 #f1 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
72 lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≘ n@f →
73 ∀n2. n2@f2 ⊚ ⫯n1@f1 ≘ ⫯(n2+n)@f.
74 #f2 #f1 #f #n1 #n #Hf #n2 elim n2 -n2 /2 width=7 by after_next, after_push/
77 lemma after_apply: ∀n1,f2,f1,f. (↓*[⫯n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1@f1 ≘ f2@❴n1❵@f.
79 [ * /2 width=1 by after_O2/
80 | #n1 #IH * /3 width=1 by after_S2/
84 corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
85 * #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
87 [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
88 | #n1 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
90 | #n2 >next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=5 by after_next/
94 theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
95 /2 width=1 by after_total_aux/ qed.
97 (* Specific inversion lemmas on after ***************************************)
99 lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ↑f1 = g2 →
100 f2 ⊚ f1 ≘ f ∧ n2 = n.
101 #f2 #g2 #f #n2 elim n2 -n2
102 [ #n #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ]
103 #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
104 | #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
105 #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
106 #x #Hx #H destruct elim (IH … Hg) [2,3: // ] -IH -Hg
107 #H destruct /2 width=1 by conj/
111 lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ⫯f1 = g2 →
112 ∃∃m. f2 ⊚ f1 ≘ m@f & ⫯(n2+m) = n.
113 #f2 #g2 #f #n2 elim n2 -n2
114 [ #n #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ]
115 #g #Hf #H elim (next_inv_seq_dx … H) -H
116 #x #Hx #Hg destruct /2 width=3 by ex2_intro/
117 | #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
118 #g #Hg #H elim (next_inv_seq_dx … H) -H
119 #x #Hx #H destruct elim (IH … Hg) -IH -Hg [2,3: // ]
120 #m #Hf #Hm destruct /2 width=3 by ex2_intro/
124 lemma after_inv_const: ∀f2,f1,f,n1,n. n@f2 ⊚ n1@f1 ≘ n@f → f2 ⊚ f1 ≘ f ∧ 0 = n1.
125 #f2 #f1 #f #n1 #n elim n -n
126 [ #H elim (after_inv_pxp … H) -H [ |*: // ]
127 #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
128 | #n #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/
132 lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≗ f.
133 /2 width=4 by after_mono/ qed-.
135 (* Specific forward lemmas on after *****************************************)
137 lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≘ n@f → f2@❴n1❵ = n.
138 #f2 #f1 #f #n1 #n #H lapply (after_fwd_at ? n1 0 … H) -H [1,2,3: // ]
139 /3 width=2 by at_inv_O1, sym_eq/
142 lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≘ n@f →
144 #f #f1 #n1 elim n1 -n1
145 [ #f2 #n2 #n #H elim (after_inv_xpx … H) -H //
146 | #n1 #IH * #m1 #f2 #n2 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
147 #m #Hm #H destruct /2 width=3 by/
151 lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2@f2 ⊚ n1@f1 ≘ n@f →
152 (n2@f2)@❴n1❵ = n ∧ (↓*[n1]f2) ⊚ f1 ≘ f.
153 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.