matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "delayed_updating/unwind/unwind2_rmap_labels.ma".
  16 include "delayed_updating/unwind/unwind2_rmap_eq.ma".
  17 include "delayed_updating/syntax/path_head_depth.ma".
  18 include "ground/relocation/xap.ma".
  19 include "ground/lib/stream_eq_eq.ma".
  20 include "ground/arith/nat_le_plus.ma".
  21
  22 (* UNWIND MAP FOR PATH ******************************************************)
  23
  24 (* Constructions with path_head *********************************************)
  25
  26 lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k):
  27       p = (↳[n]p)●q → k ≤ n →
  28       (▶[f]p)＠❨k❩ = (▶[f]↳[n]p)＠❨k❩.
  29 #f #p elim p -p
  30 [ #q #n #k #Hq #Hk
  31   elim (eq_inv_list_empty_append … Hq) -Hq * #_ //
  32 | #l #p #IH #q #n @(nat_ind_succ … n) -n
  33   [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH
  34    <path_head_zero <unwind2_rmap_empty //
  35   | #n #_ #k cases l [ #m ]
  36     [ <path_head_d_sn <list_append_lcons_sn #Hq #Hk
  37       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  38       <unwind2_rmap_d_sn <unwind2_rmap_d_sn
  39       <tr_compose_xap <tr_compose_xap
  40       @(IH … Hq) -IH -Hq (**) (* auto too slow *)
  41       @nle_trans [| @tr_uni_xap ]
  42       /2 width=1 by nle_plus_bi_dx/
  43     | <path_head_m_sn <list_append_lcons_sn #Hq #Hk
  44       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  45       <unwind2_rmap_m_sn <unwind2_rmap_m_sn
  46       /2 width=2 by/
  47     | <path_head_L_sn <list_append_lcons_sn #Hq
  48       @(nat_ind_succ … k) -k // #k #_ #Hk
  49       lapply (nle_inv_succ_bi … Hk) -Hk #Hk
  50       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  51       <unwind2_rmap_L_sn <unwind2_rmap_L_sn
  52       <tr_xap_push <tr_xap_push
  53       /3 width=2 by eq_f/
  54     | <path_head_A_sn <list_append_lcons_sn #Hq #Hk
  55       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  56       <unwind2_rmap_A_sn <unwind2_rmap_A_sn
  57       /2 width=2 by/
  58     | <path_head_S_sn <list_append_lcons_sn #Hq #Hk
  59       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  60       <unwind2_rmap_S_sn <unwind2_rmap_S_sn
  61       /2 width=2 by/
  62     ]
  63   ]
  64 ]
  65 qed-.
  66
  67 lemma unwind2_rmap_head_append_xap_closed (f) (p) (q) (n):
  68       p = ↳[n](p●q) →
  69       ▶[f](p●q)＠❨n❩ = ▶[f]↳[n](p●q)＠❨n❩.
  70 /2 width=2 by unwind2_rmap_head_xap_le_closed/
  71 qed-.
  72
  73 lemma unwind2_rmap_head_xap (f) (p) (n):
  74       n + ♯(↳[n]p) = (▶[f]↳[n]p)＠❨n❩.
  75 #f #p elim p -p
  76 [ #n <path_head_empty <unwind2_rmap_labels_L <height_labels_L
  77   <tr_xap_pushs_le //
  78 | #l #p #IH #n @(nat_ind_succ … n) -n //
  79   #n #_ cases l [ #m ]
  80   [ <unwind2_rmap_d_sn <path_head_d_sn <height_d_sn
  81     <nplus_assoc >IH -IH <tr_compose_xap <tr_uni_xap_succ //
  82   | <unwind2_rmap_m_sn <path_head_m_sn <height_m_sn //
  83   | <unwind2_rmap_L_sn <path_head_L_sn <height_L_sn
  84     <tr_xap_push <npred_succ //
  85   | <unwind2_rmap_A_sn <path_head_A_sn <height_A_sn //
  86   | <unwind2_rmap_S_sn <path_head_S_sn <height_S_sn //
  87   ]
  88 ]
  89 qed.
  90
  91 lemma unwind2_rmap_append_pap_closed (f) (p) (q) (n:pnat):
  92       p = ↳[n](p●q) →
  93       ♭p = ninj (▶[f](p●q)＠⧣❨n❩).
  94 #f #p #q #n #Hn
  95 >tr_xap_ninj >Hn in ⊢ (??%?);
  96 >(unwind2_rmap_head_append_xap_closed … Hn) -Hn
  97 <path_head_depth //
  98 qed.
  99
 100 lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (k):
 101       p = (↳[n]p)●q →
 102       ⇂*[k]▶[f]q ≗ ⇂*[n+k]▶[f]p.
 103 #f #p elim p -p
 104 [ #q #n #k #Hq
 105   elim (eq_inv_list_empty_append … Hq) -Hq #Hn #H0 destruct
 106   <path_head_empty in Hn; #Hn
 107   <(eq_inv_empty_labels … Hn) -n //
 108 | #l #p #IH #q #n @(nat_ind_succ … n) -n //
 109   #n #_ #k cases l [ #m ]
 110   [ <path_head_d_sn <list_append_lcons_sn #Hq
 111     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq <nrplus_inj_sn
 112     @(stream_eq_trans … (tls_unwind2_rmap_d_sn …))
 113     >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
 114     /2 width=1 by/
 115   | <path_head_m_sn <list_append_lcons_sn #Hq
 116     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 117     <unwind2_rmap_m_sn /2 width=1 by/
 118   | <path_head_L_sn <list_append_lcons_sn #Hq
 119     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 120     <unwind2_rmap_L_sn <nplus_succ_sn /2 width=1 by/
 121   | <path_head_A_sn <list_append_lcons_sn #Hq
 122     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 123     <unwind2_rmap_A_sn /2 width=2 by/
 124   | <path_head_S_sn <list_append_lcons_sn #Hq
 125     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 126     <unwind2_rmap_S_sn /2 width=2 by/
 127   ]
 128 ]
 129 qed-.
 130
 131 lemma tls_unwind2_rmap_append_closed (f) (p) (q) (n):
 132       p = ↳[n](p●q) →
 133       ▶[f]q ≗ ⇂*[n]▶[f](p●q).
 134 /2 width=1 by tls_unwind2_rmap_plus_closed/
 135 qed.