matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_1.etc

   1 include "ground/arith/nat_le_plus.ma".
   2 include "ground/arith/nat_le_pred.ma".
   3
   4 lemma tls_succ_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
   5       q ϵ 𝐂❨o,n❩ →
   6       ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
   7 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
   8 qed-.
   9
  10 lemma xap_le_unwind2_rmap_append_closed_dx (o) (f) (p) (q) (n):
  11       q ϵ 𝐂❨o,n❩ → ∀m. m ≤ n →
  12       ▶[f]q＠❨m❩ = ▶[f](p●q)＠❨m❩.
  13 #o #f #p #q #n #Hq elim Hq -q -n
  14 [|*: #q #n [ #k #_ ] #_ #IH ] #m #Hm
  15 [ <(nle_inv_zero_dx … Hm) -m //
  16 | <unwind2_rmap_d_dx <unwind2_rmap_d_dx
  17   <tr_compose_xap <tr_compose_xap
  18   @IH -IH (**) (* auto too slow *)
  19   @nle_trans [| @tr_uni_xap ]
  20   /2 width=1 by nle_plus_bi_dx/
  21 | <unwind2_rmap_m_dx <unwind2_rmap_m_dx
  22   /2 width=2 by/
  23 | <unwind2_rmap_L_dx <unwind2_rmap_L_dx
  24   elim (nle_inv_succ_dx … Hm) -Hm // * #Hm #H0
  25   >H0 -H0 <tr_xap_push <tr_xap_push
  26   /3 width=2 by eq_f/
  27 | <unwind2_rmap_A_dx <unwind2_rmap_A_dx
  28   /2 width=2 by/
  29 | <unwind2_rmap_S_dx <unwind2_rmap_S_dx
  30   /2 width=2 by/
  31 ]
  32 qed-.
  33
  34 lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
  35       q ϵ 𝐂❨o,n❩ →
  36       ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
  37 #o #f #p #q #n #Hq
  38 lapply (pcc_L_sn … Hq) -Hq #Hq
  39 lapply (xap_le_unwind2_rmap_append_closed_dx o f p … Hq (↑n) ?) -Hq //
  40 <tr_xap_succ_nap <tr_xap_succ_nap #Hq
  41 /2 width=1 by eq_inv_nsucc_bi/
  42 qed-.
  43
  44 lemma nap_unwind2_rmap_push_closed_depth (o) (f) (q) (n):
  45       q ϵ 𝐂❨o,n❩ →
  46       ♭q = ▶[⫯f]q＠§❨n❩.
  47 #o #f #q #n #Hq elim Hq -q -n
  48 [|*: #q #n [ #k #_ ] #_ #IH ] //
  49 <unwind2_rmap_d_dx <tr_compose_nap //
  50 qed-.
  51
  52 lemma nap_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (n):
  53       q ϵ 𝐂❨o,n❩ →
  54       ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
  55 #o #f #p #q #n #Hq
  56 <nap_unwind2_rmap_append_closed_Lq_dx //
  57 /2 width=2 by nap_unwind2_rmap_push_closed_depth/
  58 qed-.
  59
  60 lemma xap_unwind2_rmap_append_closed_true_dx_depth (f) (p) (q) (n):
  61       q ϵ 𝐂❨Ⓣ,n❩ → ♭q = ▶[f](p●q)＠❨n❩.
  62 #f #p #q #n #Hq elim Hq -q -n //
  63 #q #n #k #Ho #_ #IH
  64 <unwind2_rmap_d_dx <tr_compose_xap
  65 >Ho // <tr_uni_xap_succ <Ho //
  66 qed-.
  67
  68 lemma tls_plus_unwind2_rmap_closed_true (f) (q) (n):
  69       q ϵ 𝐂❨Ⓣ,n❩ →
  70       ∀m. ⇂*[m]f ≗ ⇂*[m+n]▶[f]q.
  71 #f #q #n #Hq elim Hq -q -n //
  72 #q #n #k #Ho #_ #IH #m
  73 >Ho // <nplus_succ_dx
  74 @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
  75 >nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold
  76 >nplus_succ_dx <Ho //
  77 qed-.
  78
  79 lemma tls_unwind2_rmap_append_closed_true_dx (f) (p) (q) (n):
  80       q ϵ 𝐂❨Ⓣ,n❩ →
  81       ▶[f]p ≗ ⇂*[n]▶[f](p●q).
  82 /2 width=1 by tls_plus_unwind2_rmap_closed_true/
  83 qed-.
  84
  85 lemma nap_plus_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (m) (n):
  86       q ϵ 𝐂❨o,n❩ →
  87       ▶[f]p＠❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
  88 #o #f #p #q #m #n #Hq
  89 <tr_nap_plus @eq_f2
  90 [ <(tr_xap_eq_repl … (tls_succ_unwind2_rmap_append_closed_Lq_dx …)) //
  91 | /2 width=2 by nap_unwind2_rmap_append_closed_Lq_dx_depth/
  92 ]
  93 qed-.
  94
  95 lemma nap_plus_unwind2_rmap_append_closed_bLq_dx_depth (o) (f) (p) (b) (q) (m) (n):
  96       b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
  97       ♭b+♭q = ▶[f](p●b●𝗟◗q)＠§❨m+n❩.
  98 #o #f #p #b #q #m #n #Hb #Hq
  99 >(xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb
 100 >(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq //
 101 qed-.
 102
 103 lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n):
 104       b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
 105       ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q).
 106 #o #f #p #b #q #m #n #Hb #Hq
 107 >nplus_succ_dx <stream_tls_plus >list_append_assoc
 108 @(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb
 109 /3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/
 110 qed-.