matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_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.tcs.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/rtmap_id.ma".
  17
  18 (* RELOCATION MAP ***********************************************************)
  19
  20 coinductive at: rtmap → relation nat ≝
  21 | at_refl: ∀f,g,j1,j2. ↑f = g → 0 = j1 → 0 = j2 → at g j1 j2
  22 | at_push: ∀f,i1,i2. at f i1 i2 → ∀g,j1,j2. ↑f = g → ⫯i1 = j1 → ⫯i2 = j2 → at g j1 j2
  23 | at_next: ∀f,i1,i2. at f i1 i2 → ∀g,j2. ⫯f = g → ⫯i2 = j2 → at g i1 j2
  24 .
  25
  26 interpretation "relational application (rtmap)"
  27    'RAt i1 f i2 = (at f i1 i2).
  28
  29 (* Basic inversion lemmas ***************************************************)
  30
  31 lemma at_inv_ppx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. 0 = i1 → ↑g = f → 0 = i2.
  32 #f #i1 #i2 * -f -i1 -i2 //
  33 [ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
  34 | #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (discr_push_next … H)
  35 ]
  36 qed-.
  37
  38 lemma at_inv_npx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j1. ⫯j1 = i1 → ↑g = f →
  39                   ∃∃j2. @⦃j1, g⦄ ≡ j2 & ⫯j2 = i2.
  40 #f #i1 #i2 * -f -i1 -i2
  41 [ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
  42 | #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/
  43 | #f #i1 #i2 #_ #g #j2 * #_ #x #x1 #_ #H elim (discr_push_next … H)
  44 ]
  45 qed-.
  46
  47 lemma at_inv_xnx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ⫯g = f →
  48                   ∃∃j2. @⦃i1, g⦄ ≡ j2 & ⫯j2 = i2.
  49 #f #i1 #i2 * -f -i1 -i2
  50 [ #f #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
  51 | #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
  52 | #f #i1 #i2 #Hi #g #j2 * * #x #H >(injective_next … H) -g /2 width=3 by ex2_intro/
  53 ]
  54 qed-.
  55
  56 (* Advanced inversion lemmas ************************************************)
  57
  58 lemma at_inv_ppn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
  59                   ∀g,j2. 0 = i1 → ↑g = f → ⫯j2 = i2 → ⊥.
  60 #f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2
  61 #H destruct
  62 qed-.
  63
  64 lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
  65                   ∀g,j1. ⫯j1 = i1 → ↑g = f → 0 = i2 → ⊥.
  66 #f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
  67 #x2 #Hg * -i2 #H destruct
  68 qed-.
  69
  70 lemma at_inv_npn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
  71                   ∀g,j1,j2. ⫯j1 = i1 → ↑g = f → ⫯j2 = i2 → @⦃j1, g⦄ ≡ j2.
  72 #f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
  73 #x2 #Hg * -i2 #H destruct //
  74 qed-.
  75
  76 lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
  77                   ∀g. ⫯g = f → 0 = i2 → ⊥.
  78 #f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
  79 #x2 #Hg * -i2 #H destruct
  80 qed-.
  81
  82 lemma at_inv_xnn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
  83                   ∀g,j2. ⫯g = f → ⫯j2 = i2 → @⦃i1, g⦄ ≡ j2.
  84 #f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xnx … Hf … H) -f
  85 #x2 #Hg * -i2 #H destruct //
  86 qed-.
  87
  88 lemma at_inv_pxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i1 → 0 = i2 → ∃g. ↑g = f.
  89 #f elim (pn_split … f) * /2 width=2 by ex_intro/
  90 #g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
  91 qed-.
  92
  93 lemma at_inv_pxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. 0 = i1 → ⫯j2 = i2 →
  94                   ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f.
  95 #f elim (pn_split … f) *
  96 #g #H #i1 #i2 #Hf #j2 #H1 #H2
  97 [ elim (at_inv_ppn … Hf … H1 H H2)
  98 | /3 width=5 by at_inv_xnn, ex2_intro/
  99 ]
 100 qed-.
 101
 102 lemma at_inv_nxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
 103                   ∀j1. ⫯j1 = i1 → 0 = i2 → ⊥.
 104 #f elim (pn_split f) *
 105 #g #H #i1 #i2 #Hf #j1 #H1 #H2
 106 [ elim (at_inv_npp … Hf … H1 H H2)
 107 | elim (at_inv_xnp … Hf … H H2)
 108 ]
 109 qed-.
 110
 111 lemma at_inv_nxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j1,j2. ⫯j1 = i1 → ⫯j2 = i2 →
 112                   (∃∃g. @⦃j1, g⦄ ≡ j2 & ↑g = f) ∨
 113                   ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f.
 114 #f elim (pn_split f) *
 115 /4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/
 116 qed-.
 117
 118 (* Note: the following inversion lemmas must be checked *)
 119 lemma at_inv_xpx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f →
 120                   (0 = i1 ∧ 0 = i2) ∨
 121                   ∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ⫯j2 = i2.
 122 #f * [2: #i1 ] #i2 #Hf #g #H
 123 [ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 124 | >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
 125 ]
 126 qed-.
 127
 128 lemma at_inv_xpp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f → 0 = i2 → 0 = i1.
 129 #f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * //
 130 #j1 #j2 #_ #_ * -i2 #H destruct
 131 qed-.
 132
 133 lemma at_inv_xpn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j2. ↑g = f → ⫯j2 = i2 →
 134                   ∃∃j1. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1.
 135 #f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xpx … Hf … H) -f *
 136 [ #_ * -i2 #H destruct
 137 | #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
 138 ]
 139 qed-.
 140
 141 lemma at_inv_xxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i2 →
 142                   ∃∃g. 0 = i1 & ↑g = f.
 143 #f elim (pn_split f) *
 144 #g #H #i1 #i2 #Hf #H2
 145 [ /3 width=6 by at_inv_xpp, ex2_intro/
 146 | elim (at_inv_xnp … Hf … H H2)
 147 ]
 148 qed-.
 149
 150 lemma at_inv_xxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2.  ⫯j2 = i2 →
 151                   (∃∃g,j1. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ↑g = f) ∨
 152                   ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f.
 153 #f elim (pn_split f) *
 154 #g #H #i1 #i2 #Hf #j2 #H2
 155 [ elim (at_inv_xpn … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/
 156 | lapply (at_inv_xnn … Hf … H H2) -i2 /3 width=3 by or_intror, ex2_intro/
 157 ]
 158 qed-.
 159
 160 (* Basic forward lemmas *****************************************************)
 161
 162 lemma at_increasing: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2.
 163 #i2 elim i2 -i2
 164 [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf //
 165 | #i2 #IH * //
 166   #i1 #f #Hf elim (at_inv_nxn … Hf) -Hf [1,4: * |*: // ]
 167   /3 width=2 by le_S_S, le_S/
 168 ]
 169 qed-.
 170
 171 lemma at_increasing_strict: ∀g,i1,i2. @⦃i1, g⦄ ≡ i2 → ∀f. ⫯f = g →
 172                             i1 < i2 ∧ @⦃i1, f⦄ ≡ ⫰i2.
 173 #g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H
 174 /4 width=2 by conj, at_increasing, le_S_S/
 175 qed-.
 176
 177 lemma at_fwd_id_ex: ∀f,i. @⦃i, f⦄ ≡ i → ∃g. ↑g = f.
 178 #f elim (pn_split f) * /2 width=2 by ex_intro/
 179 #g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H
 180 #j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg
 181 #H elim (lt_le_false … H) -H //
 182 qed-.
 183
 184 (* Basic properties *********************************************************)
 185
 186 corec lemma at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2).
 187 #i1 #i2 #f1 #H1 cases H1 -f1 -i1 -i2
 188 [ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /2 width=2 by at_refl/
 189 | #f1 #i1 #i2 #Hf1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /3 width=7 by at_push/
 190 | #f1 #i1 #i2 #Hf1 #g1 #j2 #H #H2 #f2 #H12 cases (eq_inv_nx … H12 … H) -g1 /3 width=5 by at_next/
 191 ]
 192 qed-.
 193
 194 lemma at_eq_repl_fwd: ∀i1,i2. eq_repl_fwd (λf. @⦃i1, f⦄ ≡ i2).
 195 #i1 #i2 @eq_repl_sym /2 width=3 by at_eq_repl_back/
 196 qed-.
 197
 198 lemma at_le_ex: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀i1. i1 ≤ i2 →
 199                 ∃∃j1. @⦃i1, f⦄ ≡ j1 & j1 ≤ j2.
 200 #j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
 201 [ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
 202   #g [ #x2 ] #Hg [ #H2 ] #H0
 203   [ * /3 width=3 by at_refl, ex2_intro/
 204     #i1 #Hi12 destruct lapply (le_S_S_to_le … Hi12) -Hi12
 205     #Hi12 elim (IH … Hg … Hi12) -x2 -IH
 206     /3 width=7 by at_push, ex2_intro, le_S_S/
 207   | #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2
 208     /3 width=5 by at_next, ex2_intro, le_S_S/
 209   ]
 210 | elim (at_inv_xxp … Hf) -Hf //
 211   #g * -i2 #H2 #i1 #Hi12 <(le_n_O_to_eq … Hi12)
 212   /3 width=3 by at_refl, ex2_intro/
 213 ]
 214 qed-.
 215
 216 lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1.
 217 #i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
 218 #f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/
 219 qed-.
 220
 221 (* Main properties **********************************************************)
 222
 223 theorem at_monotonic: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀j1,i1. @⦃i1, f⦄ ≡ j1 →
 224                       i1 < i2 → j1 < j2.
 225 #j2 elim j2 -j2
 226 [ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f //
 227   #g #H21 #_ #j1 #i1 #_ #Hi elim (lt_le_false … Hi) -Hi //
 228 | #j2 #IH #i2 #f #H2f * //
 229   #j1 #i1 #H1f #Hi elim (lt_inv_gen … Hi)
 230   #x2 #_ #H21 elim (at_inv_nxn … H2f … H21) -H2f [1,3: * |*: // ]
 231   #g #H2g #H
 232   [ elim (at_inv_xpn … H1f … H) -f
 233     /4 width=8 by lt_S_S_to_lt, lt_S_S/
 234   | /4 width=8 by at_inv_xnn, lt_S_S/
 235   ]
 236 ]
 237 qed-.
 238
 239 theorem at_inv_monotonic: ∀j1,i1,f. @⦃i1, f⦄ ≡ j1 → ∀j2,i2. @⦃i2, f⦄ ≡ j2 →
 240                           j1 < j2 → i1 < i2.
 241 #j1 elim j1 -j1
 242 [ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f //
 243   #g * -i1 #H #j2 #i2 #H2f #Hj elim (lt_inv_O1 … Hj) -Hj
 244   #x2 #H22 elim (at_inv_xpn … H2f … H H22) -f //
 245 | #j1 #IH *
 246   [ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ]
 247     #g #H1g #H #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
 248     /3 width=7 by at_inv_xnn/
 249   | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
 250     #y2 #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ]
 251     #g #Hg #H
 252     [ elim (at_inv_xpn … H2f … H H22) -f -H22
 253       /3 width=7 by lt_S_S/
 254     | /3 width=7 by at_inv_xnn/
 255     ]
 256   ]
 257 ]
 258 qed-.
 259
 260 theorem at_mono: ∀f,i,i1. @⦃i, f⦄ ≡ i1 → ∀i2. @⦃i, f⦄ ≡ i2 → i2 = i1.
 261 #f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
 262 #Hi elim (lt_le_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
 263 qed-.
 264
 265 theorem at_inj: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀i2. @⦃i2, f⦄ ≡ i → i1 = i2.
 266 #f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
 267 #Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
 268 qed-.
 269
 270 (* Properties on tls ********************************************************)
 271
 272 lemma at_pxx_tls: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, ⫱*[n]f⦄ ≡ 0.
 273 #n elim n -n //
 274 #n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/
 275 qed.
 276
 277 lemma at_tls: ∀i2,f. ↑⫱*[⫯i2]f ≗ ⫱*[i2]f → ∃i1. @⦃i1, f⦄ ≡ i2.
 278 #i2 elim i2 -i2
 279 [ /4 width=4 by at_eq_repl_back, at_refl, ex_intro/
 280 | #i2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
 281   elim (IH … H) -IH -H #i1 #Hf
 282   elim (pn_split f) * #g #Hg destruct /3 width=8 by at_push, at_next, ex_intro/
 283 ]
 284 qed-.
 285
 286 (* Inversion lemmas with tls ************************************************)
 287
 288 lemma at_inv_tls: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → ↑⫱*[⫯i2]f ≗ ⫱*[i2]f.
 289 #i2 elim i2 -i2
 290 [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
 291   /2 width=1 by eq_refl/
 292 | #i2 #IH #i1 #f #Hf elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] /2 width=2 by/
 293 ]
 294 qed-.
 295
 296 (* Advanced inversion lemmas on isid ****************************************)
 297
 298 lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
 299 #i elim i -i
 300 [ #f #H elim (isid_inv_gen … H) -H /2 width=2 by at_refl/
 301 | #i #IH #f #H elim (isid_inv_gen … H) -H /3 width=7 by at_push/
 302 ]
 303 qed.
 304
 305 lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
 306 /3 width=6 by isid_inv_at, at_mono/ qed-.
 307
 308 (* Advanced properties on isid **********************************************)
 309
 310 corec lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄.
 311 #f #Hf lapply (Hf 0)
 312 #H cases (at_fwd_id_ex … H) -H
 313 #g #H @(isid_push … H) /3 width=7 by at_inv_npn/
 314 qed-.
 315
 316 (* Advanced properties on id ************************************************)
 317
 318 lemma id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈𝐝 ≗ f.
 319 /3 width=1 by isid_at, eq_id_inv_isid/ qed-.
 320
 321 lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
 322 /2 width=1 by isid_inv_at/ qed.