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 (* TAILED UNWIND FOR RELOCATION MAP *****************************************)
  23
  24 (* Constructions with path_head *********************************************)
  25
  26 lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (m):
  27       q = ↳[n]q → m ≤ n →
  28       ▶[f](p●q)＠❨m❩ = ▶[f]↳[n](p●q)＠❨m❩.
  29 #f #p #q elim q -q
  30 [ #n #m #Hq
  31   <(eq_inv_path_empty_head … Hq) -n #Hm
  32   <(nle_inv_zero_dx … Hm) -m //
  33 | #l #q #IH #n @(nat_ind_succ … n) -n
  34   [ #m #_ #Hm <(nle_inv_zero_dx … Hm) -m -IH //
  35   | #n #_ #m cases l [ #k ]
  36     [ <path_head_d_dx #Hq #Hm
  37       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  38       <unwind2_rmap_d_dx <unwind2_rmap_d_dx
  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_dx #Hq #Hm
  44       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  45       <unwind2_rmap_m_dx <unwind2_rmap_m_dx
  46       /2 width=2 by/
  47     | <path_head_L_dx #Hq
  48       @(nat_ind_succ … m) -m // #m #_ #Hm
  49       lapply (nle_inv_succ_bi … Hm) -Hm #Hm
  50       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  51       <unwind2_rmap_L_dx <unwind2_rmap_L_dx
  52       <tr_xap_push <tr_xap_push
  53       /3 width=2 by eq_f/
  54     | <path_head_A_dx #Hq #Hm
  55       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  56       <unwind2_rmap_A_dx <unwind2_rmap_A_dx
  57       /2 width=2 by/
  58     | <path_head_S_dx #Hq #Hm
  59       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  60       <unwind2_rmap_S_dx <unwind2_rmap_S_dx
  61       /2 width=2 by/
  62     ]
  63   ]
  64 ]
  65 qed-.
  66
  67 lemma unwind2_rmap_head_xap_closed (f) (p) (q) (n):
  68       q = ↳[n]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 [ #k ]
  80   [ <unwind2_rmap_d_dx <path_head_d_dx <height_d_dx
  81     <nplus_comm in ⊢ (??(??%)?); <nplus_assoc
  82     >IH -IH <tr_compose_xap <tr_uni_xap_succ //
  83   | <unwind2_rmap_m_dx <path_head_m_dx <height_m_dx //
  84   | <unwind2_rmap_L_dx <path_head_L_dx <height_L_dx
  85     <tr_xap_push <npred_succ <nplus_succ_sn //
  86   | <unwind2_rmap_A_dx <path_head_A_dx <height_A_dx //
  87   | <unwind2_rmap_S_dx <path_head_S_dx <height_S_dx //
  88   ]
  89 ]
  90 qed.
  91
  92 lemma unwind2_rmap_append_pap_closed (f) (p) (q) (h:pnat):
  93       q = ↳[h]q →
  94       ♭q = ninj (▶[f](p●q)＠⧣❨h❩).
  95 #f #p #q #h #Hh
  96 >tr_xap_ninj >(path_head_refl_append_sn p … Hh) in ⊢ (??%?);
  97 >(unwind2_rmap_head_xap_closed … Hh) -Hh
  98 <path_head_depth //
  99 qed.
 100
 101 lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (m):
 102       q = ↳[n]q →
 103       ⇂*[m]▶[f]p ≗ ⇂*[n+m]▶[f](p●q).
 104 #f #p #q elim q -q
 105 [ #n #m #Hq
 106   <(eq_inv_path_empty_head … Hq) -n //
 107 | #l #q #IH #n @(nat_ind_succ … n) -n //
 108   #n #_ #m cases l [ #k ]
 109   [ <path_head_d_dx #Hq
 110     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq <nrplus_inj_sn
 111     @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
 112     >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
 113     /2 width=1 by/
 114   | <path_head_m_dx #Hq
 115     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 116     <unwind2_rmap_m_sn /2 width=1 by/
 117   | <path_head_L_dx #Hq
 118     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 119     <unwind2_rmap_L_dx <nplus_succ_sn /2 width=1 by/
 120   | <path_head_A_dx #Hq
 121     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 122     <unwind2_rmap_A_dx /2 width=2 by/
 123   | <path_head_S_dx #Hq
 124     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
 125     <unwind2_rmap_S_dx /2 width=2 by/
 126   ]
 127 ]
 128 qed-.
 129
 130 lemma tls_unwind2_rmap_closed (f) (p) (q) (n):
 131       q = ↳[n]q →
 132       ▶[f]p ≗ ⇂*[n]▶[f](p●q).
 133 /2 width=1 by tls_unwind2_rmap_plus_closed/
 134 qed.