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

   1 include "ground/relocation/tr_uni_pap.ma".
   2 include "ground/relocation/tr_compose_pap.ma".
   3 include "ground/relocation/tr_pap_eq.ma".
   4 include "ground/relocation/tr_pap_hdtl_eq.ma".
   5 include "ground/notation/functions/atsection_2.ma".
   6 include "ground/arith/nat_lt.ma".
   7 include "ground/arith/nat_plus_pplus.ma".
   8 include "ground/arith/nat_pred_succ.ma".
   9
  10 lemma nlt_npsucc_bi (n1) (n2):
  11       n1 < n2 → npsucc n1 < npsucc n2.
  12 #n1 #n2 #Hn elim Hn -n2 //
  13 #n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
  14 qed.
  15
  16 definition tr_nap (f) (l:nat): nat ≝
  17            ↓(f＠⧣❨↑l❩).
  18
  19 interpretation
  20   "functional non-negative application (total relocation maps)"
  21   'AtSection f l = (tr_nap f l).
  22
  23 lemma tr_nap_unfold (f) (l):
  24       ↓(f＠⧣❨↑l❩) = f＠§❨l❩.
  25 // qed.
  26
  27 lemma tr_pap_succ_nap (f) (l):
  28       ↑(f＠§❨l❩) = f＠⧣❨↑l❩.
  29 // qed.
  30
  31 lemma tr_compose_nap (f2) (f1) (l):
  32       f2＠§❨f1＠§❨l❩❩ = (f2∘f1)＠§❨l❩.
  33 #f2 #f1 #l
  34 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
  35 <tr_compose_pap <npsucc_pred //
  36 qed.
  37
  38 lemma tr_uni_nap (n) (m):
  39       m + n = 𝐮❨n❩＠§❨m❩.
  40 #n #m
  41 <tr_nap_unfold
  42 <tr_uni_pap <nrplus_npsucc_sn //
  43 qed.
  44
  45 lemma tr_nap_push (f):
  46       ∀l. ↑(f＠§❨l❩) = (⫯f)＠§❨↑l❩.
  47 #f #l
  48 <tr_nap_unfold <tr_nap_unfold
  49 <tr_pap_push <pnpred_psucc //
  50 qed.
  51
  52 lemma tr_nap_pushs_lt (f) (n) (m):
  53       m < n → m = (⫯*[n]f)＠§❨m❩.
  54 #f #n #m #Hmn
  55 <tr_nap_unfold <tr_pap_pushs_le
  56 /2 width=1 by nlt_npsucc_bi/
  57 qed-.
  58
  59 theorem tr_nap_eq_repl (i):
  60         stream_eq_repl … (λf1,f2. f1＠§❨i❩ = f2＠§❨i❩).
  61 #i #f1 #f2 #Hf
  62 <tr_nap_unfold <tr_nap_unfold
  63 /3 width=1 by tr_pap_eq_repl, eq_f/
  64 qed.
  65
  66 lemma tr_eq_inv_nap_zero_tl_bi (f1) (f2):
  67       f1＠§❨𝟎❩ = f2＠§❨𝟎❩ → ⇂f1 ≗ ⇂f2 → f1 ≗ f2.
  68 #f1 #f2
  69 <tr_nap_unfold <tr_nap_unfold #H1 #H2
  70 /3 width=1 by tr_eq_inv_pap_unit_tl_bi, eq_inv_pnpred_bi/
  71 qed-.
  72
  73 lemma tr_nap_plus_sn (f) (m) (n):
  74       (⫯⇂*[↑n]f)＠§❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
  75 #f #m @(nat_ind_succ … m) -m [| #m #_ ] #n
  76 [ <nplus_zero_sn <nplus_zero_sn //
  77 | <tr_nap_push <nplus_comm in ⊢ (???%);
  78   <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
  79   <nsucc_pnpred <nrplus_inj_sn <nrplus_pnpred_dx
  80   >nrplus_npsucc_sn <nrplus_inj_dx
  81   <pplus_comm in ⊢ (???%); <tr_pap_plus //
  82 ]
  83 qed.
  84
  85 lemma tr_nap_plus_dx (f) (m) (n):
  86       ⇂*[n]f＠§❨m❩+(⫯f)＠§❨n❩ = f＠§❨m+n❩.
  87 #f #m #n @(nat_ind_succ … n) -n [| #n #_ ]
  88 [ //
  89 | <tr_nap_push
  90   <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
  91   <nsucc_pnpred <nplus_pnpred_sn
  92   >nrplus_npsucc_sn <nrplus_inj_dx
  93   <tr_pap_plus //
  94 ]
  95 qed.