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/relocation/pstream_tls.ma".
16 include "ground/relocation/pstream_istot.ma".
17 include "ground/relocation/rtmap_after.ma".
19 (* RELOCATION P-STREAM ******************************************************)
21 corec definition compose: gr_map → gr_map → gr_map.
22 #f2 * #p1 #f1 @(stream_cons … (f2@❨p1❩)) @(compose ? f1) -compose -f1
26 interpretation "functional composition (nstream)"
27 'compose f2 f1 = (compose f2 f1).
29 (* Basic properties on compose ***********************************************)
31 lemma compose_rew: ∀f2,f1,p1. f2@❨p1❩⨮(⫰*[p1]f2)∘f1 = f2∘(p1⨮f1).
32 #f2 #f1 #p1 <(stream_rew … (f2∘(p1⨮f1))) normalize //
35 lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
36 #f2 * #p1 #f1 #f <compose_rew <compose_rew
37 * -f /2 width=1 by eq_f2/
40 (* Basic inversion lemmas on compose ****************************************)
42 lemma compose_inv_rew: ∀f2,f1,f,p1,p. f2∘(p1⨮f1) = p⨮f →
43 f2@❨p1❩ = p ∧ (⫰*[p1]f2)∘f1 = f.
44 #f2 #f1 #f #p1 #p <compose_rew
45 #H destruct /2 width=1 by conj/
48 lemma compose_inv_O2: ∀f2,f1,f,p2,p. (p2⨮f2)∘(⫯f1) = p⨮f →
50 #f2 #f1 #f #p2 #p <compose_rew
51 #H destruct /2 width=1 by conj/
54 lemma compose_inv_S2: ∀f2,f1,f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
55 f2@❨p1❩+p2 = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
56 #f2 #f1 #f #p2 #p1 #p <compose_rew
57 #H destruct >nsucc_inj <stream_tls_swap
61 lemma compose_inv_S1: ∀f2,f1,f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
62 ↑(f2@❨p1❩) = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
63 #f2 #f1 #f #p1 #p <compose_rew
64 #H destruct /2 width=1 by conj/
67 (* Properties on after (specific) *********************************************)
69 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
71 #f2 #f1 #f #Hf #p elim p -p
72 /2 width=7 by gr_after_refl, gr_after_next/
75 lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
76 ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
77 #f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
78 /2 width=7 by gr_after_next, gr_after_push/
81 lemma after_apply: ∀p1,f2,f1,f.
82 (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
84 [ * /2 width=1 by after_O2/
85 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
86 /3 width=1 by after_S2/
90 corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
91 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
93 [ #H cases (compose_inv_O2 … H) -H /3 width=7 by gr_after_refl, eq_f2/
94 | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by gr_after_push/
96 | #p2 >gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold
97 /3 width=5 by gr_after_next/
101 theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
102 /2 width=1 by after_total_aux/ qed.
104 (* Inversion lemmas on after (specific) ***************************************)
106 lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
107 f2 ⊚ f1 ≘ f ∧ p2 = p.
108 #f2 #g2 #f #p2 elim p2 -p2
109 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ]
110 #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
111 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
112 #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
113 #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
114 #H destruct /2 width=1 by conj/
118 lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
119 ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
120 #f2 #g2 #f #p2 elim p2 -p2
121 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ]
122 #g #Hf #H elim (next_inv_seq_dx … H) -H
123 #x #Hx #Hg destruct /2 width=3 by ex2_intro/
124 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
125 #g #Hg #H elim (next_inv_seq_dx … H) -H
126 #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
127 #m #Hf #Hm destruct /2 width=3 by ex2_intro/
131 lemma after_inv_const: ∀f2,f1,f,p1,p.
132 p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
133 #f2 #f1 #f #p1 #p elim p -p
134 [ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ]
135 #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
136 | #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/
140 lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
141 /2 width=4 by gr_after_mono/ qed-.
143 (* Forward lemmas on after (specific) *****************************************)
145 lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
146 #f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
147 /3 width=2 by at_inv_O1, sym_eq/
150 lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
151 (⫰*[↓p1]f2) ⊚ f1 ≘ f.
152 #f #f1 #p1 elim p1 -p1
153 [ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
154 | #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
155 #x #Hx #H destruct /2 width=3 by/
159 lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
160 (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
161 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
163 (* Properties on apply ******************************************************)
165 lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
166 /4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ qed.