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/substitution/lift_eq.ma".
  16 include "delayed_updating/syntax/path_structure.ma".
  17 include "delayed_updating/syntax/path_proper.ma".
  18 include "ground/xoa/ex_4_2.ma".
  19
  20 (* LIFT FOR PATH ***********************************************************)
  21
  22 (* Basic constructions with structure **************************************)
  23
  24 lemma structure_lift (p) (f):
  25       ⊗p = ⊗↑[f]p.
  26 #p @(path_ind_lift … p) -p // #p #IH #f
  27 <lift_path_L_sn //
  28 qed.
  29
  30 lemma lift_structure (p) (f):
  31       ⊗p = ↑[f]⊗p.
  32 #p @(path_ind_lift … p) -p //
  33 qed.
  34
  35 (* Destructions with structure **********************************************)
  36
  37 lemma lift_des_structure (q) (p) (f):
  38       ⊗q = ↑[f]p → ⊗q = ⊗p.
  39 // qed-.
  40
  41 (* Constructions with proper condition for path *****************************)
  42
  43 lemma lift_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
  44       (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
  45 #p2 #p1 @(path_ind_lift … p1) -p1 //
  46 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
  47 [ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
  48 | <lift_path_d_lcons_sn <IH //
  49 | <lift_path_m_sn <IH //
  50 | <lift_path_L_sn <IH //
  51 | <lift_path_A_sn <IH //
  52 | <lift_path_S_sn <IH //
  53 ]
  54 qed-.
  55
  56 (* Advanced constructions with structure ************************************)
  57
  58 lemma lift_d_empty_dx (n) (p) (f):
  59       (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
  60 #n #p #f <lift_append_proper_dx //
  61 qed.
  62
  63 lemma lift_m_dx (p) (f):
  64       ⊗p = ↑[f](p◖𝗺).
  65 #p #f <lift_append_proper_dx //
  66 qed.
  67
  68 lemma lift_L_dx (p) (f):
  69       (⊗p)◖𝗟 = ↑[f](p◖𝗟).
  70 #p #f <lift_append_proper_dx //
  71 qed.
  72
  73 lemma lift_A_dx (p) (f):
  74       (⊗p)◖𝗔 = ↑[f](p◖𝗔).
  75 #p #f <lift_append_proper_dx //
  76 qed.
  77
  78 lemma lift_S_dx (p) (f):
  79       (⊗p)◖𝗦 = ↑[f](p◖𝗦).
  80 #p #f <lift_append_proper_dx //
  81 qed.
  82
  83 lemma lift_root (f) (p):
  84       ∃∃r. 𝐞 = ⊗r & ⊗p●r = ↑[f]p.
  85 #f #p @(list_ind_rcons … p) -p
  86 [ /2 width=3 by ex2_intro/
  87 | #p * [ #n ] /2 width=3 by ex2_intro/
  88 ]
  89 qed-.
  90
  91 (* Advanced inversions with proj_path ***************************************)
  92
  93 lemma lift_path_inv_d_sn (k) (q) (p) (f):
  94       (𝗱k◗q) = ↑[f]p →
  95       ∃∃r,h. 𝐞 = ⊗r & (↑[r]f)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
  96 #k #q #p @(path_ind_lift … p) -p
  97 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
  98 [ <lift_path_empty #H destruct
  99 | <lift_path_d_empty_sn #H destruct -IH
 100   /2 width=5 by ex4_2_intro/
 101 | <lift_path_d_lcons_sn #H
 102   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
 103   /2 width=5 by ex4_2_intro/
 104 | <lift_path_m_sn #H
 105   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
 106   /2 width=5 by ex4_2_intro/
 107 | <lift_path_L_sn #H destruct
 108 | <lift_path_A_sn #H destruct
 109 | <lift_path_S_sn #H destruct
 110 ]
 111 qed-.
 112
 113 lemma lift_path_inv_m_sn (q) (p) (f):
 114       (𝗺◗q) = ↑[f]p → ⊥.
 115 #q #p @(path_ind_lift … p) -p
 116 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 117 [ <lift_path_empty #H destruct
 118 | <lift_path_d_empty_sn #H destruct
 119 | <lift_path_d_lcons_sn #H /2 width=2 by/
 120 | <lift_path_m_sn #H /2 width=2 by/
 121 | <lift_path_L_sn #H destruct
 122 | <lift_path_A_sn #H destruct
 123 | <lift_path_S_sn #H destruct
 124 ]
 125 qed-.
 126
 127 lemma lift_path_inv_L_sn (q) (p) (f):
 128       (𝗟◗q) = ↑[f]p →
 129       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[⫯↑[r1]f]r2 & r1●𝗟◗r2 = p.
 130 #q #p @(path_ind_lift … p) -p
 131 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 132 [ <lift_path_empty #H destruct
 133 | <lift_path_d_empty_sn #H destruct
 134 | <lift_path_d_lcons_sn #H
 135   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 136   /2 width=5 by ex3_2_intro/
 137 | <lift_path_m_sn #H
 138   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 139   /2 width=5 by ex3_2_intro/
 140 | <lift_path_L_sn #H destruct -IH
 141   /2 width=5 by ex3_2_intro/
 142 | <lift_path_A_sn #H destruct
 143 | <lift_path_S_sn #H destruct
 144 ]
 145 qed-.
 146
 147 lemma lift_path_inv_A_sn (q) (p) (f):
 148       (𝗔◗q) = ↑[f]p →
 149       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗔◗r2 = p.
 150 #q #p @(path_ind_lift … p) -p
 151 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 152 [ <lift_path_empty #H destruct
 153 | <lift_path_d_empty_sn #H destruct
 154 | <lift_path_d_lcons_sn #H
 155   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 156   /2 width=5 by ex3_2_intro/
 157 | <lift_path_m_sn #H
 158   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 159   /2 width=5 by ex3_2_intro/
 160 | <lift_path_L_sn #H destruct
 161 | <lift_path_A_sn #H destruct -IH
 162   /2 width=5 by ex3_2_intro/
 163 | <lift_path_S_sn #H destruct
 164 ]
 165 qed-.
 166
 167 lemma lift_path_inv_S_sn (q) (p) (f):
 168       (𝗦◗q) = ↑[f]p →
 169       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗦◗r2 = p.
 170 #q #p @(path_ind_lift … p) -p
 171 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 172 [ <lift_path_empty #H destruct
 173 | <lift_path_d_empty_sn #H destruct
 174 | <lift_path_d_lcons_sn #H
 175   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 176   /2 width=5 by ex3_2_intro/
 177 | <lift_path_m_sn #H
 178   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 179   /2 width=5 by ex3_2_intro/| <lift_path_L_sn #H destruct
 180 | <lift_path_A_sn #H destruct
 181 | <lift_path_S_sn #H destruct -IH
 182   /2 width=5 by ex3_2_intro/
 183 ]
 184 qed-.
 185
 186 (* Inversions with proper condition for path ********************************)
 187
 188 lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
 189       q2 ϵ 𝐏 → q1●q2 = ↑[f]p →
 190       ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
 191 #q2 #q1 elim q1 -q1
 192 [ #p #f #Hq2 <list_append_empty_sn #H destruct
 193   /2 width=5 by ex3_2_intro/
 194 | * [ #n1 ] #q1 #IH #p #f #Hq2 <list_append_lcons_sn #H
 195   [ elim (lift_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
 196     elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
 197     elim Hq2 -Hq2 //
 198   | elim (lift_path_inv_m_sn … H)
 199   | elim (lift_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
 200     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
 201     @(ex3_2_intro … (r1●𝗟◗p1)) //
 202     <structure_append <Hr1 -Hr1 //
 203   | elim (lift_path_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
 204     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
 205     @(ex3_2_intro … (r1●𝗔◗p1)) //
 206     <structure_append <Hr1 -Hr1 //
 207   | elim (lift_path_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
 208     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
 209     @(ex3_2_intro … (r1●𝗦◗p1)) //
 210     <structure_append <Hr1 -Hr1 //
 211   ]
 212 ]
 213 qed-.