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

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