matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.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/rat_3.ma".
  16 include "ground_2/relocation/trace.ma".
  17
  18 (* RELOCATION TRACE *********************************************************)
  19
  20 inductive at: trace → relation nat ≝
  21    | at_zero : ∀cs. at (Ⓣ @ cs) 0 0
  22    | at_succ : ∀cs,i,j. at cs i j → at (Ⓣ @ cs) (⫯i) (⫯j)
  23    | at_false: ∀cs,i,j. at cs i j → at (Ⓕ @ cs) i (⫯j).
  24
  25 interpretation "relocation (trace)"
  26    'RAt i1 cs i2 = (at cs i1 i2).
  27
  28 (* Basic inversion lemmas ***************************************************)
  29
  30 fact at_inv_empty_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → cs = ◊ → ⊥.
  31 #cs #i #j * -cs -i -j
  32 #cs [2,3: #i #j #_ ] #H destruct
  33 qed-.
  34
  35 lemma at_inv_empty: ∀i,j. @⦃i, ◊⦄ ≡ j → ⊥.
  36 /2 width=5 by at_inv_empty_aux/ qed-.
  37
  38 fact at_inv_true_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓣ @ tl →
  39                       (i = 0 ∧ j = 0) ∨
  40                       ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, tl⦄ ≡ j0.
  41 #cs #i #j * -cs -i -j
  42 #cs [2,3: #i #j #Hij ] #tl #H destruct
  43 /3 width=5 by ex3_2_intro, or_introl, or_intror, conj/
  44 qed-.
  45
  46 lemma at_inv_true: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ j →
  47                    (i = 0 ∧ j = 0) ∨
  48                    ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, cs⦄ ≡ j0.
  49 /2 width=3 by at_inv_true_aux/ qed-.
  50
  51 lemma at_inv_true_zero_sn: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ j → j = 0.
  52 #cs #j #H elim (at_inv_true … H) -H * //
  53 #i0 #j0 #H destruct
  54 qed-.
  55
  56 lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0.
  57 #cs #i #H elim (at_inv_true … H) -H * //
  58 #i0 #j0 #_ #H destruct
  59 qed-.
  60
  61 lemma at_inv_true_succ_sn: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ j →
  62                            ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0.
  63 #cs #i #j #H elim (at_inv_true … H) -H *
  64 [ #H destruct
  65 | #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/
  66 ]
  67 qed-.
  68
  69 lemma at_inv_true_succ_dx: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ ⫯j →
  70                            ∃∃i0. i = ⫯i0 & @⦃i0, cs⦄ ≡ j.
  71 #cs #i #j #H elim (at_inv_true … H) -H *
  72 [ #_ #H destruct
  73 | #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/
  74 ]
  75 qed-.
  76
  77 lemma at_inv_true_succ: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ ⫯j →
  78                         @⦃i, cs⦄ ≡ j.
  79 #cs #i #j #H elim (at_inv_true … H) -H *
  80 [ #H destruct
  81 | #i0 #j0 #H1 #H2 destruct //
  82 ]
  83 qed-.
  84
  85 lemma at_inv_true_O_S: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ ⫯j → ⊥.
  86 #cs #j #H elim (at_inv_true … H) -H *
  87 [ #_ #H destruct
  88 | #i0 #j0 #H1 destruct
  89 ]
  90 qed-.
  91
  92 lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥.
  93 #cs #i #H elim (at_inv_true … H) -H *
  94 [ #H destruct
  95 | #i0 #j0 #_ #H1 destruct
  96 ]
  97 qed-.
  98
  99 fact at_inv_false_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓕ @ tl →
 100                        ∃∃j0. j = ⫯j0 & @⦃i, tl⦄ ≡ j0.
 101 #cs #i #j * -cs -i -j
 102 #cs [2,3: #i #j #Hij ] #tl #H destruct
 103 /2 width=3 by ex2_intro/
 104 qed-.
 105
 106 lemma at_inv_false: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ j →
 107                     ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0.
 108 /2 width=3 by at_inv_false_aux/ qed-.
 109
 110 lemma at_inv_false_S: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ ⫯j → @⦃i, cs⦄ ≡ j.
 111 #cs #i #j #H elim (at_inv_false … H) -H
 112 #j0 #H destruct //
 113 qed-.
 114
 115 lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥.
 116 #cs #i #H elim (at_inv_false … H) -H
 117 #j0 #H destruct
 118 qed-.
 119
 120 (* Basic properties *********************************************************)
 121
 122 lemma at_monotonic: ∀cs,i2,j2. @⦃i2, cs⦄ ≡ j2 → ∀i1. i1 < i2 →
 123                     ∃∃j1. @⦃i1, cs⦄ ≡ j1 & j1 < j2.
 124 #cs #i2 #j2 #H elim H -cs -i2 -j2
 125 [ #cs #i1 #H elim (lt_zero_false … H)
 126 | #cs #i #j #Hij #IH * /2 width=3 by ex2_intro, at_zero/
 127   #i1 #H lapply (lt_S_S_to_lt … H) -H
 128   #H elim (IH … H) -i
 129   #j1 #Hij1 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
 130 | #cs #i #j #_ #IH #i1 #H elim (IH … H) -i
 131   /3 width=3 by le_S_S, ex2_intro, at_false/
 132 ]
 133 qed-.
 134
 135 lemma at_at_dec: ∀cs,i,j. Decidable (@⦃i, cs⦄ ≡ j).
 136 #cs elim cs -cs [ | * #cs #IH ]
 137 [ /3 width=3 by at_inv_empty, or_intror/
 138 | * [2: #i ] * [2,4: #j ]
 139   [ elim (IH i j) -IH
 140     /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/
 141   | -IH /3 width=3 by at_inv_true_O_S, or_intror/
 142   | -IH /3 width=3 by at_inv_true_S_O, or_intror/
 143   | -IH /2 width=1 by or_introl, at_zero/
 144   ]
 145 | #i * [2: #j ]
 146   [ elim (IH i j) -IH
 147     /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/
 148   | -IH /3 width=3 by at_inv_false_O, or_intror/
 149   ]
 150 ]
 151 qed-.
 152
 153 (* Basic forward lemmas *****************************************************)
 154
 155 lemma at_increasing: ∀cs,i,j. @⦃i, cs⦄ ≡ j → i ≤ j.
 156 #cs #i elim i -i //
 157 #i0 #IHi #j #H elim (at_monotonic … H i0) -H
 158 /3 width=3 by le_to_lt_to_lt/
 159 qed-.
 160
 161 lemma at_length_lt: ∀cs,i,j. @⦃i, cs⦄ ≡ j → j < |cs|.
 162 #cs elim cs -cs [ | * #cs #IH ] #i #j #H normalize
 163 [ elim (at_inv_empty … H)
 164 | elim (at_inv_true … H) * -H //
 165   #i0 #j0 #H1 #H2 #Hij0 destruct /3 width=2 by le_S_S/
 166 | elim (at_inv_false … H) -H
 167   #j0 #H #H0 destruct /3 width=2 by le_S_S/
 168 ]
 169 qed-.
 170
 171 (* Main properties **********************************************************)
 172
 173 theorem at_mono: ∀cs,i,j1. @⦃i, cs⦄ ≡ j1 → ∀j2. @⦃i, cs⦄ ≡ j2 → j1 = j2.
 174 #cs #i #j1 #H elim H -cs -i -j1
 175 #cs [ |2,3: #i #j1 #_ #IH ] #j2 #H
 176 [ lapply (at_inv_true_zero_sn … H) -H //
 177 | elim (at_inv_true_succ_sn … H) -H
 178   #j0 #H destruct #H >(IH … H) -cs -i -j1 //
 179 | elim (at_inv_false … H) -H
 180   #j0 #H destruct #H >(IH … H) -cs -i -j1 //
 181 ]
 182 qed-.
 183
 184 theorem at_inj: ∀cs,i1,j. @⦃i1, cs⦄ ≡ j → ∀i2. @⦃i2, cs⦄ ≡ j → i1 = i2.
 185 #cs #i1 #j #H elim H -cs -i1 -j
 186 #cs [ |2,3: #i1 #j #_ #IH ] #i2 #H
 187 [ lapply (at_inv_true_zero_dx … H) -H //
 188 | elim (at_inv_true_succ_dx … H) -H
 189   #i0 #H destruct #H >(IH … H) -cs -i1 -j //
 190 | elim (at_inv_false … H) -H
 191   #j0 #H destruct #H >(IH … H) -cs -i1 -j0 //
 192 ]
 193 qed-.