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/notation/functions/atsection_2.ma".
   5 include "ground/arith/nat_lt.ma".
   6 include "ground/arith/nat_plus_rplus.ma".
   7 include "ground/arith/nat_pred_succ.ma".
   8
   9 lemma nlt_npsucc_bi (n1) (n2):
  10       n1 < n2 → npsucc n1 < npsucc n2.
  11 #n1 #n2 #Hn elim Hn -n2 //
  12 #n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
  13 qed.
  14
  15 definition tr_nap (f) (l:nat): nat ≝
  16            ↓(f＠⧣❨↑l❩).
  17
  18 interpretation
  19   "functional non-negative application (total relocation maps)"
  20   'AtSection f l = (tr_nap f l).
  21
  22 lemma tr_nap_unfold (f) (l):
  23       ↓(f＠⧣❨↑l❩) = f＠§❨l❩.
  24 // qed.
  25
  26 lemma tr_pap_succ_nap (f) (l):
  27       ↑(f＠§❨l❩) = f＠⧣❨↑l❩.
  28 // qed.
  29
  30 lemma tr_compose_nap (f2) (f1) (l):
  31       f2＠§❨f1＠§❨l❩❩ = (f2∘f1)＠§❨l❩.
  32 #f2 #f1 #l
  33 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
  34 <tr_compose_pap <npsucc_pred //
  35 qed.
  36
  37 lemma tr_uni_nap (n) (m):
  38       m + n = 𝐮❨n❩＠§❨m❩.
  39 #n #m
  40 <tr_nap_unfold
  41 <tr_uni_pap <nrplus_npsucc_sn //
  42 qed.
  43
  44 lemma tr_nap_push (f):
  45       ∀l. ↑(f＠§❨l❩) = (⫯f)＠§❨↑l❩.
  46 #f #l
  47 <tr_nap_unfold <tr_nap_unfold
  48 <tr_pap_push <pnpred_psucc //
  49 qed.
  50
  51 lemma tr_nap_pushs_lt (f) (n) (m):
  52       m < n → m = (⫯*[n]f)＠§❨m❩.
  53 #f #n #m #Hmn
  54 <tr_nap_unfold <tr_pap_pushs_le
  55 /2 width=1 by nlt_npsucc_bi/
  56 qed-.
  57
  58 theorem tr_nap_eq_repl (i):
  59         stream_eq_repl … (λf1,f2. f1＠§❨i❩ = f2＠§❨i❩).
  60 #i #f1 #f2 #Hf
  61 <tr_nap_unfold <tr_nap_unfold
  62 /3 width=1 by tr_pap_eq_repl, eq_f/
  63 qed.