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

   1 (**) (* reverse include *)
   2 include "ground/relocation/tr_pn_eq.ma".
   3 include "ground/relocation/tr_compose_pn.ma".
   4 include "ground/relocation/nap.ma".
   5 include "ground/notation/functions/at_2.ma".
   6
   7 definition tr_xap (f) (l:nat): nat ≝
   8            (⫯f)＠§❨l❩.
   9
  10 interpretation
  11   "functional extended application (total relocation maps)"
  12   'At 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.
  72
  73 theorem tr_xap_eq_repl (i):
  74         stream_eq_repl … (λf1,f2. f1＠❨i❩ = f2＠❨i❩).
  75 #i #f1 #f2 #Hf
  76 <tr_xap_unfold <tr_xap_unfold
  77 /3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
  78 qed.
  79
  80 lemma tr_nap_plus_dx_xap (f) (m) (n):
  81       ⇂*[↑n]f＠❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
  82 /2 width=1 by tr_nap_eq_repl/
  83 qed.
  84
  85 lemma tr_nap_plus_sn_xap (f) (m) (n):
  86       ⇂*[n]f＠§❨m❩+f＠❨n❩ = f＠§❨m+n❩.
  87 // qed.
  88
  89 lemma tr_xap_pos (f) (n):
  90       n = ↑↓n → f＠❨n❩=↑↓(f＠❨n❩).
  91 #f #n #H0 >H0 -H0
  92 <tr_xap_ninj <nsucc_pnpred //
  93 qed.