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 let corec compose: rtmap → rtmap → rtmap ≝ ?.
21 #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2
25 interpretation "functional composition (nstream)"
26 'compose f1 f2 = (compose f1 f2).
28 (* Basic properies on compose ***********************************************)
30 lemma compose_rew: ∀f1,f2,n2. f1@❴n2❵@(↓*[⫯n2]f1)∘f2 = f1∘(n2@f2).
31 #f1 #f2 #n2 <(stream_rew … (f1∘(n2@f2))) normalize //
34 lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f.
35 #f1 * #n2 #f2 #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: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f →
42 f1@❴n2❵ = n ∧ (↓*[⫯n2]f1)∘f2 = f.
43 #f1 #f2 #f #n2 #n <(stream_rew … (f1∘(n2@f2))) normalize
44 #H destruct /2 width=1 by conj/
47 lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f →
49 #f1 #f2 #f #n1 #n <compose_rew
50 #H destruct /2 width=1 by conj/
53 lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f →
54 ⫯(n1+f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
55 #f1 #f2 #f #n1 #n2 #n <compose_rew
56 #H destruct <tls_S1 /2 width=1 by conj/
59 lemma compose_inv_S1: ∀f1,f2,f,n2,n. (⫯f1)∘(n2@f2) = n@f →
60 ⫯(f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
61 #f1 #f2 #f #n2 #n <compose_rew
62 #H destruct <tls_S1 /2 width=1 by conj/
65 (* Specific properties ******************************************************)
67 lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
69 #f1 #f2 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
72 lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f →
73 ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f.
74 #f1 #f2 #f #n2 #n #Hf #n1 elim n1 -n1 /2 width=7 by after_next, after_push/
77 lemma after_apply: ∀n2,f1,f2,f. (↓*[⫯n2] f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
79 [ * /2 width=1 by after_O2/
80 | #n2 #IH * /3 width=1 by after_S2/
84 let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?.
85 * #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1
87 [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
88 | #n2 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
90 | #n1 >next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=7 by after_next/
94 theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2.
95 /2 width=1 by after_total_aux/ qed.
97 (* Specific inversion lemmas ************************************************)
99 lemma after_inv_xpx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ↑f2 = g2 →
100 f1 ⊚ f2 ≡ f ∧ n1 = n.
101 #f1 #g2 #f #n1 elim n1 -n1
102 [ #n #Hf #f2 #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 | #n1 #IH #n #Hf #f2 #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: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ⫯f2 = g2 →
112 ∃∃m. f1 ⊚ f2 ≡ m@f & ⫯(n1+m) = n.
113 #f1 #g2 #f #n1 elim n1 -n1
114 [ #n #Hf #f2 #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 | #n1 #IH #n #Hf #f2 #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: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ 0 = n2.
125 #f1 #f2 #f #n2 #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 (* Specific forward lemmas **************************************************)
134 lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n.
135 #f1 #f2 #f #n2 #n #H lapply (after_fwd_at ? n2 0 … H) -H [1,2,3: // ]
136 /3 width=2 by at_inv_O1, sym_eq/
139 lemma after_fwd_tls: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f →
141 #f #f2 #n2 elim n2 -n2
142 [ #f1 #n1 #n #H elim (after_inv_xpx … H) -H //
143 | #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
144 #m #Hm #H destruct /2 width=3 by/
148 lemma after_inv_apply: ∀f1,f2,f,n1,n2,n. n1@f1 ⊚ n2@f2 ≡ n@f →
149 (n1@f1)@❴n2❵ = n ∧ (↓*[n2]f1) ⊚ f2 ≡ f.
150 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.