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 "basic_2/substitution/gr2.ma".
17 (* GENERIC RELOCATION WITH PAIRS ********************************************)
19 inductive minuss: nat → relation (list2 nat nat) ≝
20 | minuss_nil: ∀i. minuss i ⟠ ⟠
21 | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
22 minuss i ({d, e} @ des1) ({d - i, e} @ des2)
23 | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
24 minuss i ({d, e} @ des1) des2
27 interpretation "minus (generic relocation with pairs)"
28 'RMinus des1 i des2 = (minuss i des1 des2).
30 (* Basic inversion lemmas ***************************************************)
32 fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠.
33 #des1 #des2 #i * -des1 -des2 -i
35 | #des1 #des2 #d #e #i #_ #_ #H destruct
36 | #des1 #des2 #d #e #i #_ #_ #H destruct
40 lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠.
43 fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
44 ∀d,e,des. des1 = {d, e} @ des →
45 d ≤ i ∧ des ▭ e + i ≡ des2 ∨
46 ∃∃des0. i < d & des ▭ i ≡ des0 &
47 des2 = {d - i, e} @ des0.
48 #des1 #des2 #i * -des1 -des2 -i
49 [ #i #d #e #des #H destruct
50 | #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/
51 | #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1/
55 lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
56 d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨
57 ∃∃des. i < d & des1 ▭ i ≡ des &
58 des2 = {d - i, e} @ des.
61 lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
62 d ≤ i → des1 ▭ e + i ≡ des2.
63 #des1 #des2 #d #e #i #H
64 elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi
65 lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
66 elim (lt_refl_false … Hi)
69 lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
71 ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des.
72 #des1 #des2 #d #e #i #H
73 elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid
74 lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
75 elim (lt_refl_false … Hi)