]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma
78dd6fb9a2465485066d7350f7523636cec39886
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / trace_after.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground_2/notation/relations/rafter_3.ma".
16 include "ground_2/relocation/trace_at.ma".
17
18 (* RELOCATION TRACE *********************************************************)
19
20 inductive after: relation3 trace trace trace ≝
21    | after_empty: after (◊) (◊) (◊)
22    | after_true : ∀cs1,cs2,cs. after cs1 cs2 cs →
23                   ∀b. after (Ⓣ @ cs1) (b @ cs2) (b @ cs)
24    | after_false: ∀cs1,cs2,cs. after cs1 cs2 cs →
25                   after (Ⓕ @ cs1) cs2 (Ⓕ @ cs).
26
27 interpretation "composition (trace)"
28    'RAfter cs1 cs2 cs = (after cs1 cs2 cs).
29
30 (* Basic properties *********************************************************)
31
32 lemma after_length: ∀cs1,cs2. ∥cs1∥ = |cs2| →
33                     ∃∃cs. cs1 ⊚ cs2 ≡ cs & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
34 #cs1 elim cs1 -cs1
35 [ #cs2 #H >(length_inv_zero_sn … H) -cs2 /2 width=4 by after_empty, ex3_intro/
36 | * #cs1 #IH #cs2 #Hcs
37   [ elim (length_inv_succ_sn … Hcs) -Hcs
38     #tl #b #Hcs #H destruct
39   ]
40   elim (IH … Hcs) -IH -Hcs
41   #cs #Hcs #H1 #H2 [ @(ex3_intro … (b@cs)) | @(ex3_intro … (Ⓕ@cs)) ] /2 width=1 by after_true, after_false, colength_cons/
42 ]  
43 qed-.
44
45 (* Basic inversion lemmas ***************************************************)
46
47 fact after_inv_empty1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs1 = ◊ →
48                            cs2 = ◊ ∧ cs = ◊.
49 #cs1 #cs2 #cs * -cs1 -cs2 -cs
50 [ /2 width=1 by conj/
51 | #cs1 #cs2 #cs #_ #b #H destruct
52 | #cs1 #cs2 #cs #_ #H destruct
53 ]
54 qed-.
55
56 lemma after_inv_empty1: ∀cs2,cs. ◊ ⊚ cs2 ≡ cs → cs2 = ◊ ∧ cs = ◊.
57 /2 width=3 by after_inv_empty1_aux/ qed-.
58
59 fact after_inv_true1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓣ @ tl1 →
60                           ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
61 #cs1 #cs2 #cs * -cs1 -cs2 -cs
62 [ #tl1 #H destruct
63 | #cs1 #cs2 #cs #H12 #b #tl1 #H destruct
64   /2 width=6 by ex3_3_intro/
65 | #cs1 #cs2 #cs #_ #tl1 #H destruct
66 ]
67 qed-.
68
69 lemma after_inv_true1: ∀tl1,cs2,cs. (Ⓣ @ tl1) ⊚ cs2 ≡ cs →
70                        ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
71 /2 width=3 by after_inv_true1_aux/ qed-.
72
73 fact after_inv_false1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓕ @ tl1 →
74                            ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
75 #cs1 #cs2 #cs * -cs1 -cs2 -cs
76 [ #tl1 #H destruct
77 | #cs1 #cs2 #cs #_ #b #tl1 #H destruct
78 | #cs1 #cs2 #cs #H12 #tl1 #H destruct
79   /2 width=3 by ex2_intro/
80 ]
81 qed-.
82
83 lemma after_inv_false1: ∀tl1,cs2,cs. (Ⓕ @ tl1) ⊚ cs2 ≡ cs →
84                         ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
85 /2 width=3 by after_inv_false1_aux/ qed-.
86
87 fact after_inv_empty3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs = ◊ →
88                            cs1 = ◊ ∧ cs2 = ◊.
89 #cs1 #cs2 #cs * -cs1 -cs2 -cs
90 [ /2 width=1 by conj/
91 | #cs1 #cs2 #cs #_ #b #H destruct
92 | #cs1 #cs2 #cs #_ #H destruct
93 ]
94 qed-.
95
96 lemma after_inv_empty3: ∀cs1,cs2. cs1 ⊚ cs2 ≡ ◊ → cs1 = ◊ ∧ cs2 = ◊.
97 /2 width=3 by after_inv_empty3_aux/ qed-.
98
99 fact after_inv_inh3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl,b. cs = b @ tl →
100                          (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
101                          ∃∃tl1.  cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
102 #cs1 #cs2 #cs * -cs1 -cs2 -cs
103 [ #tl #b #H destruct
104 | #cs1 #cs2 #cs #H12 #b0 #tl #b #H destruct
105   /3 width=5 by ex3_2_intro, or_introl/
106 | #cs1 #cs2 #cs #H12 #tl #b #H destruct
107   /3 width=3 by ex3_intro, or_intror/
108 ]
109 qed-.
110
111 lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl →
112                       (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
113                       ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
114 /2 width=3 by after_inv_inh3_aux/ qed-.
115
116 lemma after_inv_true3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓣ @ tl →
117                        ∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓣ @ tl2 & tl1 ⊚ tl2 ≡ tl.
118 #cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H // *
119 #tl1 #_ #H destruct
120 qed-. 
121
122 lemma after_inv_false3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓕ @ tl →
123                         (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓕ @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
124                         ∃∃tl1. cs1 = Ⓕ @ tl1 & tl1 ⊚ cs2 ≡ tl.
125 #cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H /2 width=1 by or_introl/ * /3 width=3 by ex2_intro, or_intror/
126 qed-.
127
128 lemma after_inv_length: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs →
129                         ∧∧ ∥cs1∥ = |cs2| & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
130 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by and3_intro/
131 #cs1 #cs2 #cs #_ [ * ] * /2 width=1 by and3_intro/
132 qed-.
133
134 (* Basic forward lemmas *****************************************************)
135
136 lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄ ≡ i →
137                     ∃∃i2. @⦃i1, cs1⦄ ≡ i2 & @⦃i2, cs2⦄ ≡ i.
138 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
139 [ #i1 #i #H elim (at_inv_empty … H) -H
140   #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
141 | #cs1 #cs2 #cs #_ * #IH #i1 #i #H
142   [ elim (at_inv_true … H) -H *
143     [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
144     | #j1 #j #H1 #H2 #Hj1 destruct
145       elim (IH … Hj1) -IH -Hj1 /3 width=3 by at_succ, ex2_intro/
146     ]
147   | elim (at_inv_false … H) -H
148     #j #H #Hj destruct
149     elim (IH … Hj) -IH -Hj /3 width=3 by at_succ, at_false, ex2_intro/
150   ]
151 | #cs1 #cs2 #cs #_ #IH #i1 #i #H elim (at_inv_false … H) -H
152   #j #H #Hj destruct
153   elim (IH … Hj) -IH -Hj /3 width=3 by at_false, ex2_intro/
154 ]
155 qed-.
156
157 lemma after_at1_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
158                      ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
159 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
160 [ #i1 #i2 #H elim (at_inv_empty … H) -H
161   #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
162 | #cs1 #cs2 #cs #_ * #IH #i1 #i2 #H
163   [ elim (at_inv_true … H) -H *
164     [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
165     | #j1 #j2 #H1 #H2 #Hj12 destruct
166       elim (IH … Hj12) -IH -Hj12 /3 width=3 by at_succ, ex2_intro/
167     ]
168   | elim (at_inv_false … H) -H
169     #j2 #H #Hj2 destruct
170     elim (IH … Hj2) -IH -Hj2 /3 width=3 by at_succ, at_false, ex2_intro/
171   ]
172 | #cs1 #cs2 #cs #_ #IH #i1 #i2 #H elim (IH … H) -IH -H
173   /3 width=3 by at_false, ex2_intro/
174 ]
175 qed-.
176
177 lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
178                     ∀i1,i2,i. @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs⦄ ≡ i.
179 #cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at1_fwd … Hcs … Hi1) -cs1
180 #j #H #Hj >(at_mono … Hi2 … H) -i2 //
181 qed-.
182
183 lemma after_fwd_at1: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
184                      ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2.
185 #cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at_fwd … Hcs … Hi1) -cs
186 #j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
187 qed-.
188
189 lemma after_fwd_at2: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
190                      ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i.
191 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
192 [ #i1 #i2 #i #Hi #Hi1 elim (at_inv_empty … Hi1) -Hi1 //
193 | #cs1 #cs2 #cs #_ * #IH #i1 #i2 #i #Hi #Hi1
194   [ elim (at_inv_true … Hi1) -Hi1 *
195     [ -IH #H1 #H2 destruct >(at_inv_true_zero_sn … Hi) -i //
196     | #j1 #j2 #H1 #H2 #Hj12 destruct elim (at_inv_true_succ_sn … Hi) -Hi
197       #j #H #Hj1 destruct /3 width=3 by at_succ/
198     ]
199   | elim (at_inv_false … Hi1) -Hi1
200     #j2 #H #Hj2 destruct elim (at_inv_false … Hi) -Hi
201     #j #H #Hj destruct /3 width=3 by at_succ/
202   ]
203 | #cs1 #cs2 #cs #_ #IH #i1 #i2 #i #Hi #Hi2 elim (at_inv_false … Hi) -Hi
204   #j #H #Hj destruct /3 width=3 by at_false/
205 ]
206 qed-.
207
208 (* Main properties **********************************************************)
209
210 theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 →
211                       ∀cs3, cs4. cs0 ⊚ cs3 ≡ cs4 →
212                       ∃∃cs. cs2 ⊚ cs3 ≡ cs & cs1 ⊚ cs ≡ cs4.
213 #cs1 #cs2 #cs0 #H elim H -cs1 -cs2 -cs0
214 [ #cs3 #cs4 #H elim (after_inv_empty1 … H) -H
215   #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
216 | #cs1 #cs2 #cs0 #_ * #IH #cs3 #cs4 #H
217   [ elim (after_inv_true1 … H) -H
218     #tl3 #tl4 #b #H1 #H2 #Htl destruct
219     elim (IH … Htl) -cs0
220     /3 width=3 by ex2_intro, after_true/
221   | elim (after_inv_false1 … H) -H
222     #tl4 #H #Htl destruct
223     elim (IH … Htl) -cs0
224     /3 width=3 by ex2_intro, after_true, after_false/
225   ]
226 | #cs1 #cs2 #cs0 #_ #IH #cs3 #cs4 #H
227   elim (after_inv_false1 … H) -H
228   #tl4 #H #Htl destruct
229   elim (IH … Htl) -cs0
230   /3 width=3 by ex2_intro, after_false/
231 ]
232 qed-.
233
234 theorem after_trans2: ∀cs1,cs0,cs4. cs1 ⊚ cs0 ≡ cs4 →
235                       ∀cs2, cs3. cs2 ⊚ cs3 ≡ cs0 →
236                       ∃∃cs. cs1 ⊚ cs2 ≡ cs & cs ⊚ cs3 ≡ cs4.
237 #cs1 #cs0 #cs4 #H elim H -cs1 -cs0 -cs4
238 [ #cs2 #cs3 #H elim (after_inv_empty3 … H) -H
239   #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
240 | #cs1 #cs0 #cs4 #_ #b #IH #cs2 #cs3 #H elim (after_inv_inh3 … H) -H *
241   [ #tl2 #tl3 #H1 #H2 #Htl destruct
242     elim (IH … Htl) -cs0
243     /3 width=3 by ex2_intro, after_true/
244   | #tl2 #H1 #H2 #Htl destruct
245     elim (IH … Htl) -cs0
246     /3 width=3 by ex2_intro, after_true, after_false/
247   ]
248 | #cs1 #cs0 #cs4 #_ #IH #cs2 #cs3 #H elim (IH … H) -cs0
249   /3 width=3 by ex2_intro, after_false/
250 ]
251 qed-.
252
253 theorem after_mono: ∀cs1,cs2,x. cs1 ⊚ cs2 ≡ x → ∀y. cs1 ⊚ cs2 ≡ y → x = y.
254 #cs1 #cs2 #x #H elim H -cs1 -cs2 -x
255 [ #y #H elim (after_inv_empty1 … H) -H //
256 | #cs1 #cs #x #_ #b #IH #y #H elim (after_inv_true1 … H) -H
257   #tl #tly #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
258 | #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H
259   #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x //
260 ]
261 qed-.
262
263 theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y.
264 #cs1 #x #cs #H elim H -cs1 -x -cs
265 [ #y #H elim (after_inv_empty1 … H) -H //
266 | #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H
267   #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
268 | #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H
269   #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x //
270 ]
271 qed-.