matita/matita/contribs/lambdadelta/ground/etc/relocation/trace_at.etc

   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/rat_3.ma".
  16 include "ground_2/relocation/trace.ma".
  17
  18 (* RELOCATION TRACE *********************************************************)
  19
  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).
  25
  26 interpretation "relocation (trace)"
  27    'RAt i1 cs i2 = (at cs i1 i2).
  28
  29 (* Basic inversion lemmas ***************************************************)
  30
  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
  34 qed-.
  35
  36 lemma at_inv_empty: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = 0 ∧ i2 = 0.
  37 /2 width=5 by at_inv_empty_aux/ qed-.
  38
  39 lemma at_inv_empty_zero_sn: ∀i. @⦃0, ◊⦄ ≡ i → i = 0.
  40 #i #H elim (at_inv_empty … H) -H //
  41 qed-.
  42
  43 lemma at_inv_empty_zero_dx: ∀i. @⦃i, ◊⦄ ≡ 0 → i = 0.
  44 #i #H elim (at_inv_empty … H) -H //
  45 qed-.
  46
  47 lemma at_inv_empty_succ_sn: ∀i1,i2. @⦃⫯i1, ◊⦄ ≡ i2 → ⊥.
  48 #i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
  49 qed-.
  50
  51 lemma at_inv_empty_succ_dx: ∀i1,i2. @⦃i1, ◊⦄ ≡ ⫯i2 → ⊥.
  52 #i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
  53 qed-.
  54
  55 fact at_inv_true_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓣ @ tl →
  56                       (i1 = 0 ∧ i2 = 0) ∨
  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/
  61 qed-.
  62
  63 lemma at_inv_true: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ i2 →
  64                    (i1 = 0 ∧ i2 = 0) ∨
  65                    ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, cs⦄ ≡ j2.
  66 /2 width=3 by at_inv_true_aux/ qed-.
  67
  68 lemma at_inv_true_zero_sn: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ i → i = 0.
  69 #cs #i #H elim (at_inv_true … H) -H * //
  70 #j1 #j2 #H destruct
  71 qed-.
  72
  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
  76 qed-.
  77
  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 *
  81 [ #H destruct
  82 | #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
  83 ]
  84 qed-.
  85
  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 *
  89 [ #_ #H destruct
  90 | #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
  91 ]
  92 qed-.
  93
  94 lemma at_inv_true_succ: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
  95                         @⦃i1, cs⦄ ≡ i2.
  96 #cs #i1 #i2 #H elim (at_inv_true … H) -H *
  97 [ #H destruct
  98 | #j1 #j2 #H1 #H2 destruct //
  99 ]
 100 qed-.
 101
 102 lemma at_inv_true_O_S: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ ⫯i → ⊥.
 103 #cs #i #H elim (at_inv_true … H) -H *
 104 [ #_ #H destruct
 105 | #j1 #j2 #H destruct
 106 ]
 107 qed-.
 108
 109 lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥.
 110 #cs #i #H elim (at_inv_true … H) -H *
 111 [ #H destruct
 112 | #j1 #j2 #_ #H destruct
 113 ]
 114 qed-.
 115
 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/
 121 qed-.
 122
 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-.
 126
 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
 129 #j2 #H destruct //
 130 qed-.
 131
 132 lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥.
 133 #cs #i #H elim (at_inv_false … H) -H
 134 #j2 #H destruct
 135 qed-.
 136
 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/
 140 qed-.
 141
 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/
 144 qed-.
 145
 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/
 148 qed-.
 149
 150 (* Basic properties *********************************************************)
 151
 152 (* Note: lemma 250 *)
 153 lemma at_le: ∀cs,i1. i1 ≤ ∥cs∥ →
 154              ∃∃i2. @⦃i1, cs⦄ ≡ i2 & i2 ≤ |cs|.
 155 #cs elim cs -cs
 156 [ #i1 #H <(le_n_O_to_eq … H) -i1 /2 width=3 by at_empty, ex2_intro/
 157 | * #cs #IH
 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/
 162   ]
 163 ]
 164 qed-.
 165
 166 lemma at_top: ∀cs. @⦃∥cs∥, cs⦄ ≡ |cs|.
 167 #cs elim cs -cs // * /2 width=1 by at_succ, at_false/
 168 qed.
 169
 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
 177   #H elim (IH … H) -i1
 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/
 181 ]
 182 qed-.
 183
 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
 189   ]
 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/
 196   ]
 197 | #i1 * [2: #i2 ]
 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/
 201   ]
 202 ]
 203 qed-.
 204
 205 lemma is_at_dec: ∀cs,i2. Decidable (∃i1. @⦃i1, cs⦄ ≡ i2).
 206 #cs elim cs -cs
 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 ]
 210   [ elim (IH i2) -IH
 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/
 215     ]
 216   | elim (IH i2) -IH
 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/
 219     ]
 220   | /3 width=2 by at_zero, ex_intro, or_introl/
 221   | @or_intror * /2 width=3 by at_inv_false_O/
 222   ]
 223 ]
 224 qed-.
 225
 226 (* Basic forward lemmas *****************************************************)
 227
 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/
 232 qed-.
 233
 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/
 238 qed-.
 239
 240 (* Main properties **********************************************************)
 241
 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/
 251 ]
 252 qed-.
 253
 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/
 263 ]
 264 qed-.