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