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ᴿ) →
  26       ↳[↑[q●p]f＠❨n❩](↑[↑[q]f]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
  38       <(IH … H0) in ⊢ (???%); -IH -H0 <tr_xap_plus //
  39     | <reverse_rcons <path_head_m_sn #H0
  40       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  41       <list_append_assoc <lift_rmap_m_dx <lift_path_m_dx <reverse_rcons
  42       <tr_xap_succ_nap <path_head_m_sn
  43       <(IH … H0) in ⊢ (???%); -IH -H0 //
  44     | <reverse_rcons <path_head_L_sn #H0
  45       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  46       <list_append_assoc <lift_rmap_L_dx <lift_path_L_dx <reverse_rcons
  47       <tr_xap_succ_nap <path_head_L_sn
  48       <(IH … H0) in ⊢ (???%); -IH -H0 //
  49     | <reverse_rcons <path_head_A_sn #H0
  50       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  51       <list_append_assoc <lift_rmap_A_dx <lift_path_A_dx <reverse_rcons
  52       <tr_xap_succ_nap <path_head_A_sn
  53       <(IH … H0) in ⊢ (???%); -IH -H0 //
  54     | <reverse_rcons <path_head_S_sn #H0
  55       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  56       <list_append_assoc <lift_rmap_S_dx <lift_path_S_dx <reverse_rcons
  57       <tr_xap_succ_nap <path_head_S_sn
  58       <(IH … H0) in ⊢ (???%); -IH -H0 //
  59     ]
  60   ]
  61 ]
  62 qed.