matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_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/substitution/lift_gen_eq.ma".
  16 include "delayed_updating/syntax/path_head.ma".
  17 include "delayed_updating/syntax/path_reverse.ma".
  18 include "ground/relocation/xap.ma".
  19
  20 (* LIFT FOR PATH ************************************************************)
  21
  22 (* Constructions with head for path *****************************************)
  23
  24 lemma lift_path_head (f) (p) (q) (n):
  25       pᴿ = ↳[n](pᴿ●qᴿ) →
  26       ↳[↑[q●p]f＠❨n❩](↑[f](q●p))ᴿ = (↑[↑[q]f]p)ᴿ.
  27 #f #p @(list_ind_rcons … p) -p
  28 [ #q #n #H0
  29   <(eq_inv_path_empty_head … H0) -H0
  30   <path_head_zero //
  31 | #p #l #IH #q #n @(nat_ind_succ …n) -n [| #m #_ ]
  32   [ <reverse_rcons <path_head_zero #H0 destruct
  33   | cases l [ #n ]
  34     [ <reverse_rcons <path_head_d_sn #H0
  35       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  36       <list_append_assoc <lift_rmap_d_dx <lift_path_d_dx <reverse_rcons
  37       <tr_xap_succ_nap <path_head_d_sn >tr_xap_succ_nap
  38       <lift_path_d_dx >lift_rmap_append <reverse_rcons
  39       <(IH … H0) -IH -H0 <tr_xap_plus //
  40     | <reverse_rcons <path_head_m_sn #H0
  41       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  42       <list_append_assoc <lift_rmap_m_dx <lift_path_m_dx <reverse_rcons
  43       <tr_xap_succ_nap <path_head_m_sn >tr_xap_succ_nap
  44       <lift_path_m_dx <reverse_rcons
  45       <(IH … H0) -IH -H0 //
  46     | <reverse_rcons <path_head_L_sn #H0
  47       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  48       <list_append_assoc <lift_rmap_L_dx <lift_path_L_dx <reverse_rcons
  49       <tr_xap_succ_nap <path_head_L_sn >tr_xap_succ_nap
  50       <lift_path_L_dx <reverse_rcons
  51       <(IH … H0) -IH -H0 //
  52     | <reverse_rcons <path_head_A_sn #H0
  53       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  54       <list_append_assoc <lift_rmap_A_dx <lift_path_A_dx <reverse_rcons
  55       <tr_xap_succ_nap <path_head_A_sn >tr_xap_succ_nap
  56       <lift_path_A_dx <reverse_rcons
  57       <(IH … H0) -IH -H0 //
  58     | <reverse_rcons <path_head_S_sn #H0
  59       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  60       <list_append_assoc <lift_rmap_S_dx <lift_path_S_dx <reverse_rcons
  61       <tr_xap_succ_nap <path_head_S_sn >tr_xap_succ_nap
  62       <lift_path_S_dx <reverse_rcons
  63       <(IH … H0) -IH -H0 //
  64     ]
  65   ]
  66 ]
  67 qed.