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

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