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/relations/rat_3.ma".
16 include "ground_2/relocation/trace.ma".
18 (* RELOCATION TRACE *********************************************************)
20 inductive at: trace → relation nat ≝
21 | at_empty: at (◊) 0 0
22 | at_zero : ∀cs. at (Ⓣ @ cs) 0 0
23 | at_succ : ∀cs,i1,i2. at cs i1 i2 → at (Ⓣ @ cs) (⫯i1) (⫯i2)
24 | at_false: ∀cs,i1,i2. at cs i1 i2 → at (Ⓕ @ cs) i1 (⫯i2).
26 interpretation "relocation (trace)"
27 'RAt i1 cs i2 = (at cs i1 i2).
29 (* Basic inversion lemmas ***************************************************)
31 fact at_inv_empty_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = 0 ∧ i2 = 0.
32 #cs #i1 #i2 * -cs -i1 -i2 /2 width=1 by conj/
33 #cs #i1 #i2 #_ #H destruct
36 lemma at_inv_empty: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = 0 ∧ i2 = 0.
37 /2 width=5 by at_inv_empty_aux/ qed-.
39 lemma at_inv_empty_zero_sn: ∀i. @⦃0, ◊⦄ ≡ i → i = 0.
40 #i #H elim (at_inv_empty … H) -H //
43 lemma at_inv_empty_zero_dx: ∀i. @⦃i, ◊⦄ ≡ 0 → i = 0.
44 #i #H elim (at_inv_empty … H) -H //
47 lemma at_inv_empty_succ_sn: ∀i1,i2. @⦃⫯i1, ◊⦄ ≡ i2 → ⊥.
48 #i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
51 lemma at_inv_empty_succ_dx: ∀i1,i2. @⦃i1, ◊⦄ ≡ ⫯i2 → ⊥.
52 #i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
55 fact at_inv_true_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓣ @ tl →
57 ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, tl⦄ ≡ j2.
58 #cs #i1 #i2 * -cs -i1 -i2
59 [2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
60 /3 width=5 by ex3_2_intro, or_introl, or_intror, conj/
63 lemma at_inv_true: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ i2 →
65 ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, cs⦄ ≡ j2.
66 /2 width=3 by at_inv_true_aux/ qed-.
68 lemma at_inv_true_zero_sn: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ i → i = 0.
69 #cs #i #H elim (at_inv_true … H) -H * //
73 lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0.
74 #cs #i #H elim (at_inv_true … H) -H * //
75 #j1 #j2 #_ #H destruct
78 lemma at_inv_true_succ_sn: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ i2 →
79 ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
80 #cs #i1 #i2 #H elim (at_inv_true … H) -H *
82 | #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
86 lemma at_inv_true_succ_dx: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
87 ∃∃j1. i1 = ⫯j1 & @⦃j1, cs⦄ ≡ i2.
88 #cs #i1 #i2 #H elim (at_inv_true … H) -H *
90 | #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
94 lemma at_inv_true_succ: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
96 #cs #i1 #i2 #H elim (at_inv_true … H) -H *
98 | #j1 #j2 #H1 #H2 destruct //
102 lemma at_inv_true_O_S: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ ⫯i → ⊥.
103 #cs #i #H elim (at_inv_true … H) -H *
105 | #j1 #j2 #H destruct
109 lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥.
110 #cs #i #H elim (at_inv_true … H) -H *
112 | #j1 #j2 #_ #H destruct
116 fact at_inv_false_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓕ @ tl →
117 ∃∃j2. i2 = ⫯j2 & @⦃i1, tl⦄ ≡ j2.
118 #cs #i1 #i2 * -cs -i1 -i2
119 [2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
120 /2 width=3 by ex2_intro/
123 lemma at_inv_false: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
124 ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
125 /2 width=3 by at_inv_false_aux/ qed-.
127 lemma at_inv_false_S: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ ⫯i2 → @⦃i1, cs⦄ ≡ i2.
128 #cs #i1 #i2 #H elim (at_inv_false … H) -H
132 lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥.
133 #cs #i #H elim (at_inv_false … H) -H
137 lemma at_inv_le: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ ∥cs∥ ∧ i2 ≤ |cs|.
138 #cs #i1 #i2 #H elim H -cs -i1 -i2 /2 width=1 by conj/
139 #cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/
142 lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥ < i1 → ⊥.
143 #cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
146 lemma at_inv_gt2: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → |cs| < i2 → ⊥.
147 #cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
150 (* Basic properties *********************************************************)
152 (* Note: lemma 250 *)
153 lemma at_le: ∀cs,i1. i1 ≤ ∥cs∥ →
154 ∃∃i2. @⦃i1, cs⦄ ≡ i2 & i2 ≤ |cs|.
156 [ #i1 #H <(le_n_O_to_eq … H) -i1 /2 width=3 by at_empty, ex2_intro/
158 [ * /2 width=3 by at_zero, ex2_intro/
159 #i1 #H lapply (le_S_S_to_le … H) -H
160 #H elim (IH … H) -IH -H /3 width=3 by at_succ, le_S_S, ex2_intro/
161 | #i1 #H elim (IH … H) -IH -H /3 width=3 by at_false, le_S_S, ex2_intro/
166 lemma at_top: ∀cs. @⦃∥cs∥, cs⦄ ≡ |cs|.
167 #cs elim cs -cs // * /2 width=1 by at_succ, at_false/
170 lemma at_monotonic: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀j1. j1 < i1 →
171 ∃∃j2. @⦃j1, cs⦄ ≡ j2 & j2 < i2.
172 #cs #i1 #i2 #H elim H -cs -i1 -i2
173 [ #j1 #H elim (lt_zero_false … H)
174 | #cs #j1 #H elim (lt_zero_false … H)
175 | #cs #i1 #i2 #Hij #IH * /2 width=3 by ex2_intro, at_zero/
176 #j1 #H lapply (lt_S_S_to_lt … H) -H
178 #j2 #Hj12 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
179 | #cs #i1 #i2 #_ #IH #j1 #H elim (IH … H) -i1
180 /3 width=3 by le_S_S, ex2_intro, at_false/
184 lemma at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
185 #cs elim cs -cs [ | * #cs #IH ]
186 [ * [2: #i1 ] * [2,4: #i2 ]
187 [4: /2 width=1 by at_empty, or_introl/
188 |*: @or_intror #H elim (at_inv_empty … H) #H1 #H2 destruct
190 | * [2: #i1 ] * [2,4: #i2 ]
191 [ elim (IH i1 i2) -IH
192 /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/
193 | -IH /3 width=3 by at_inv_true_O_S, or_intror/
194 | -IH /3 width=3 by at_inv_true_S_O, or_intror/
195 | -IH /2 width=1 by or_introl, at_zero/
198 [ elim (IH i1 i2) -IH
199 /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/
200 | -IH /3 width=3 by at_inv_false_O, or_intror/
205 lemma is_at_dec: ∀cs,i2. Decidable (∃i1. @⦃i1, cs⦄ ≡ i2).
207 [ * /3 width=2 by ex_intro, or_introl/
208 #i2 @or_intror * /2 width=3 by at_inv_empty_succ_dx/
209 | * #cs #IH * [2,4: #i2 ]
211 [ * /4 width=2 by at_succ, ex_intro, or_introl/
212 | #H @or_intror * #x #Hx
213 elim (at_inv_true_succ_dx … Hx) -Hx
214 /3 width=2 by ex_intro/
217 [ * /4 width=2 by at_false, ex_intro, or_introl/
218 | #H @or_intror * /4 width=2 by at_inv_false_S, ex_intro/
220 | /3 width=2 by at_zero, ex_intro, or_introl/
221 | @or_intror * /2 width=3 by at_inv_false_O/
226 (* Basic forward lemmas *****************************************************)
228 lemma at_increasing: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ i2.
229 #cs #i1 elim i1 -i1 //
230 #j1 #IHi #i2 #H elim (at_monotonic … H j1) -H
231 /3 width=3 by le_to_lt_to_lt/
234 lemma at_increasing_strict: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
235 i1 < i2 ∧ @⦃i1, cs⦄ ≡ ⫰i2.
236 #cs #i1 #i2 #H elim (at_inv_false … H) -H
237 #j2 #H #Hj2 destruct /4 width=2 by conj, at_increasing, le_S_S/
240 (* Main properties **********************************************************)
242 theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
243 #cs #i #i1 #H elim H -cs -i -i1
244 [2,3,4: #cs [2,3: #i #i1 #_ #IH ] ] #i2 #H
245 [ elim (at_inv_true_succ_sn … H) -H
246 #j2 #H destruct #H >(IH … H) -cs -i -i1 //
247 | elim (at_inv_false … H) -H
248 #j2 #H destruct #H >(IH … H) -cs -i -i1 //
249 | /2 width=2 by at_inv_true_zero_sn/
250 | /2 width=1 by at_inv_empty_zero_sn/
254 theorem at_inj: ∀cs,i1,i. @⦃i1, cs⦄ ≡ i → ∀i2. @⦃i2, cs⦄ ≡ i → i1 = i2.
255 #cs #i1 #i #H elim H -cs -i1 -i
256 [2,3,4: #cs [ |2,3: #i1 #i #_ #IH ] ] #i2 #H
257 [ /2 width=2 by at_inv_true_zero_dx/
258 | elim (at_inv_true_succ_dx … H) -H
259 #j2 #H destruct #H >(IH … H) -cs -i1 -i //
260 | elim (at_inv_false … H) -H
261 #j #H destruct #H >(IH … H) -cs -i1 -j //
262 | /2 width=1 by at_inv_empty_zero_dx/