matita/matita/contribs/lambdadelta/ground/relocation/xap.ma

   1 include "ground/arith/nat_rplus_pplus.ma".
   2 include "ground/relocation/nap.ma".
   3 include "ground/notation/functions/apply_2.ma".
   4 include "ground/relocation/tr_compose_pn.ma".
   5 include "ground/relocation/tr_pap_tls.ma".
   6
   7 definition tr_xap (f) (l:nat): nat ≝
   8            (⫯f)@↑❨l❩.
   9
  10 interpretation
  11   "functional extended application (total relocation maps)"
  12   'Apply f l = (tr_xap f l).
  13
  14 lemma tr_xap_unfold (f) (l):
  15       (⫯f)@↑❨l❩ = f＠❨l❩.
  16 // qed.
  17
  18 lemma tr_xap_zero (f):
  19       (𝟎) = f＠❨𝟎❩.
  20 // qed.
  21
  22 lemma tr_xap_ninj (f) (p):
  23       ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
  24 // qed.
  25
  26 lemma tr_xap_succ_nap (f) (n):
  27       ↑(f@↑❨n❩) = f＠❨↑n❩.
  28 #f #n
  29 <tr_xap_ninj //
  30 qed.
  31
  32 lemma tr_compose_xap (f2) (f1) (l):
  33       f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
  34 #f2 #f1 #l
  35 <tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
  36 >tr_compose_nap >tr_compose_push_bi //
  37 qed.
  38
  39 lemma tr_uni_xap_succ (n) (m):
  40       ↑m + n = 𝐮❨n❩＠❨↑m❩.
  41 #n #m
  42 <tr_xap_unfold
  43 <tr_nap_push <tr_uni_nap //
  44 qed.
  45
  46 lemma tr_uni_xap (n) (m):
  47       𝐮❨n❩＠❨m❩ ≤ m+n.
  48 #n #m @(nat_ind_succ … m) -m //
  49 qed.
  50
  51 lemma tr_xap_push (f) (l):
  52       ↑(f＠❨l❩) = (⫯f)＠❨↑l❩.
  53 #f #l
  54 <tr_xap_unfold <tr_xap_unfold
  55 <tr_nap_push //
  56 qed.
  57
  58 lemma tr_xap_pushs_le (f) (n) (m):
  59       m ≤ n → m = (⫯*[n]f)＠❨m❩.
  60 #f #n #m #Hmn
  61 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
  62 /2 width=1 by nlt_succ_dx/
  63 qed-.
  64
  65 lemma tr_xap_plus (n1) (n2) (f):
  66       (⇂*[n2]f)＠❨n1❩+f＠❨n2❩ = f＠❨n1+n2❩.
  67 * [| #n1 ] // * [| #n2 ] // #f
  68 <nrplus_inj_sn <nrplus_inj_dx
  69 <nrplus_inj_sn <nrplus_inj_dx
  70 >tr_pap_plus //
  71 qed.