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/functions/cocompose_2.ma".
16 include "ground_2/relocation/rtmap_coafter.ma".
18 (* RELOCATION N-STREAM ******************************************************)
20 rec definition fun0 (n1:nat) on n1: rtmap → nat.
22 #f2 cases n1 -n1 [ @0 ]
26 rec definition fun2 (n1:nat) on n1: rtmap → rtmap.
27 * * [ | #n2 #f2 @(n2⨮f2) ]
28 #f2 cases n1 -n1 [ @f2 ]
32 rec definition fun1 (n1:nat) (f1:rtmap) on n1: rtmap → rtmap.
33 * * [ | #n2 #f2 @(n1⨮f1) ]
34 #f2 cases n1 -n1 [ @f1 ]
38 corec definition cocompose: rtmap → rtmap → rtmap.
39 #f2 * #n1 #f1 @(seq … (fun0 n1 f2)) @(cocompose (fun2 n1 f2) (fun1 n1 f1 f2))
42 interpretation "functional co-composition (nstream)"
43 'CoCompose f1 f2 = (cocompose f1 f2).
45 (* Basic properties on funs *************************************************)
47 (* Note: we need theese since matita blocks recursive δ when ι is blocked *)
48 lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (↑f2).
52 lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (↑f2).
56 lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1⨮f1.
60 (* Basic properies on cocompose *********************************************)
62 lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)⨮(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1⨮f1).
63 #f2 #f1 #n1 <(stream_rew … (f2~∘(n1⨮f1))) normalize //
66 (* Basic inversion lemmas on compose ****************************************)
68 lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f →
71 <cocompose_rew #H destruct
72 normalize /2 width=1 by conj/
75 lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ (↑n1⨮f1) = x⨮f →
76 ∃∃n. ↑n = x & f2 ~∘ (n1⨮f1) = n⨮f.
78 <cocompose_rew #H destruct
79 @(ex2_intro … (fun0 n1 f2)) // <cocompose_rew
83 lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1⨮f1) = x⨮f →
84 0 = x ∧ f2 ~∘ (n1⨮f1) = f.
86 <cocompose_rew #H destruct
90 (* Specific properties on coafter *******************************************)
92 corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≘ f.
93 * #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
95 [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
96 | #n1 #H cases (cocompose_inv_pnx … H) -H /3 width=7 by coafter_push/
98 | #n2 >next_rew #H cases (cocompose_inv_nxx … H) -H /3 width=5 by coafter_next/
102 theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1.
103 /2 width=1 by coafter_total_aux/ qed.