matita/matita/contribs/lambdadelta/ground/relocation/pstream_basic.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/arith/nat_lt_plus.ma".
  16 include "ground/relocation/rtmap_basic_at.ma".
  17 include "ground/relocation/pstream_after.ma".
  18
  19 (* RELOCATION N-STREAM ******************************************************)
  20
  21 (* Specific properties on basic relocation **********************************)
  22
  23 lemma apply_basic_lt: ∀m,n,i. ninj i ≤ m → 𝐁❨m,n❩@❨i❩ = i.
  24 /3 width=1 by at_inv_total, at_basic_lt/ qed-.
  25
  26 lemma apply_basic_ge: ∀m,n,i. m < ninj i → 𝐁❨m,n❩@❨i❩ = i+n.
  27 /3 width=1 by at_inv_total, at_basic_ge/ qed-.
  28
  29 (* Specific main properties on basic relocation *****************************)
  30
  31 theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
  32                     ∀h1,h2. 𝐁❨d2,h2❩∘𝐁❨d1,h1❩ ≡ 𝐁❨d1+h2,h1❩∘𝐁❨d2,h2❩.
  33 #d1 #d2 #Hd21 #h1 #h2
  34 @nstream_inv_eq
  35 @nstream_eq_inv_ext #i
  36 <compose_apply <compose_apply
  37 elim (nat_split_lt_ge d2 i) #Hd2
  38 [ elim (nat_split_lt_ge d1 i) -Hd21 #Hd1
  39   [ >(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2) >apply_basic_ge
  40     [ >apply_basic_ge // >nrplus_inj_sn /2 width=1 by nlt_plus_bi_sn/
  41     | >nrplus_inj_sn /2 width=2 by nlt_plus_dx_dx/
  42     ]
  43   | >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2)
  44     >apply_basic_lt // >nrplus_inj_sn /2 width=1 by nle_plus_bi_dx/
  45   ]
  46 | lapply (nle_trans … Hd2 … Hd21) -Hd21 #Hd1
  47   >(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2)
  48   >apply_basic_lt /2 width=1 by nle_plus_dx_dx/
  49 ]
  50 qed-.