matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.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/syntax/path_structure.ma".
  16 include "delayed_updating/substitution/lift_eq.ma".
  17
  18 (* LIFT FOR PATH ***********************************************************)
  19
  20 (* Constructions with structure ********************************************)
  21
  22 lemma lift_d_empty_dx (n) (p) (f):
  23       (⊗p)◖𝗱❨(↑[p◖𝗱❨n❩]f)@❨n❩❩ = ↑[f](p◖𝗱❨n❩).
  24 #n #p elim p -p
  25 [| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
  26 [ //
  27 | <list_cons_shift <list_cons_comm <list_cons_comm //
  28 | <lift_d_lcons_sn <lift_d_lcons_sn //
  29 | <lift_L_sn <lift_L_sn <lift_lcons <IH //
  30 | <lift_A_sn <lift_A_sn <lift_lcons <IH //
  31 | <lift_S_sn <lift_S_sn <lift_lcons <IH //
  32 ]
  33 qed.
  34
  35 lemma lift_L_dx (p) (f):
  36       (⊗p)◖𝗟 = ↑[f](p◖𝗟).
  37 #p elim p -p
  38 [| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
  39 [ //
  40 | //
  41 | <lift_d_lcons_sn //
  42 | <lift_L_sn <lift_lcons //
  43 | <lift_A_sn <lift_lcons //
  44 | <lift_S_sn <lift_lcons //
  45 ]
  46 qed.
  47
  48 lemma lift_A_dx (p) (f):
  49       (⊗p)◖𝗔 = ↑[f](p◖𝗔).
  50 #p elim p -p
  51 [| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
  52 [ //
  53 | //
  54 | <lift_d_lcons_sn //
  55 | <lift_L_sn <lift_lcons //
  56 | <lift_A_sn <lift_lcons //
  57 | <lift_S_sn <lift_lcons //
  58 ]
  59 qed.
  60
  61 lemma lift_S_dx (p) (f):
  62       (⊗p)◖𝗦 = ↑[f](p◖𝗦).
  63 #p elim p -p
  64 [| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
  65 [ //
  66 | //
  67 | <lift_d_lcons_sn //
  68 | <lift_L_sn <lift_lcons //
  69 | <lift_A_sn <lift_lcons //
  70 | <lift_S_sn <lift_lcons //
  71 ]
  72 qed.
  73
  74 lemma structure_lift (p) (f):
  75       ⊗p = ⊗↑[f]p.
  76 #p elim p -p
  77 [| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
  78 [ //
  79 | //
  80 | //
  81 | <lift_L_sn <lift_lcons //
  82 | <lift_A_sn <lift_lcons //
  83 | <lift_S_sn <lift_lcons //
  84 ]
  85 qed.
  86
  87 lemma lift_structure (p) (f):
  88       ⊗p = ↑[f]⊗p.
  89 #p elim p -p
  90 [| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
  91 [ //
  92 | //
  93 | //
  94 | <structure_L_sn <lift_L_sn <lift_lcons //
  95 | <structure_A_sn <lift_A_sn <lift_lcons //
  96 | <structure_S_sn <lift_S_sn <lift_lcons //
  97 ]
  98 qed.