matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_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/unwind1/unwind_eq.ma".
  16 include "delayed_updating/syntax/path_structure.ma".
  17 include "delayed_updating/syntax/path_inner.ma".
  18 include "delayed_updating/syntax/path_proper.ma".
  19 include "ground/xoa/ex_4_2.ma".
  20
  21 (* UNWIND FOR PATH *********************************************************)
  22
  23 (* Basic constructions with structure **************************************)
  24
  25 lemma structure_unwind (p) (f):
  26       ⊗p = ⊗▼[f]p.
  27 #p @(path_ind_unwind … p) -p // #p #IH #f
  28 <unwind_path_L_sn //
  29 qed.
  30
  31 lemma unwind_structure (p) (f):
  32       ⊗p = ▼[f]⊗p.
  33 #p @(path_ind_unwind … p) -p //
  34 qed.
  35
  36 (* Destructions with structure **********************************************)
  37
  38 lemma unwind_des_structure (q) (p) (f):
  39       ⊗q = ▼[f]p → ⊗q = ⊗p.
  40 // qed-.
  41
  42 (* Constructions with proper condition for path *****************************)
  43
  44 lemma unwind_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
  45       (⊗p1)●(▼[▼[p1]f]p2) = ▼[f](p1●p2).
  46 #p2 #p1 @(path_ind_unwind … p1) -p1 //
  47 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
  48 [ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
  49 | <unwind_path_d_lcons <IH //
  50 | <unwind_path_m_sn <IH //
  51 | <unwind_path_L_sn <IH //
  52 | <unwind_path_A_sn <IH //
  53 | <unwind_path_S_sn <IH //
  54 ]
  55 qed-.
  56
  57 (* Constructions with inner condition for path ******************************)
  58
  59 lemma unwind_append_inner_sn (p1) (p2) (f): p1 ϵ 𝐈 →
  60       (⊗p1)●(▼[▼[p1]f]p2) = ▼[f](p1●p2).
  61 #p1 @(list_ind_rcons … p1) -p1 // #p1 *
  62 [ #n ] #_ #p2 #f #Hp1
  63 [ elim (pic_inv_d_dx … Hp1)
  64 | <list_append_rcons_sn <unwind_append_proper_dx //
  65 | <list_append_rcons_sn <unwind_append_proper_dx //
  66   <structure_L_dx <list_append_rcons_sn //
  67 | <list_append_rcons_sn <unwind_append_proper_dx //
  68   <structure_A_dx <list_append_rcons_sn //
  69 | <list_append_rcons_sn <unwind_append_proper_dx //
  70   <structure_S_dx <list_append_rcons_sn //
  71 ]
  72 qed-.
  73
  74 (* Advanced constructions with proj_path ************************************)
  75
  76 lemma unwind_path_d_empty_dx (n) (p) (f):
  77       (⊗p)◖𝗱((▼[p]f)＠⧣❨n❩) = ▼[f](p◖𝗱n).
  78 #n #p #f <unwind_append_proper_dx //
  79 qed.
  80
  81 lemma unwind_path_m_dx (p) (f):
  82       ⊗p = ▼[f](p◖𝗺).
  83 #p #f <unwind_append_proper_dx //
  84 qed.
  85
  86 lemma unwind_path_L_dx (p) (f):
  87       (⊗p)◖𝗟 = ▼[f](p◖𝗟).
  88 #p #f <unwind_append_proper_dx //
  89 qed.
  90
  91 lemma unwind_path_A_dx (p) (f):
  92       (⊗p)◖𝗔 = ▼[f](p◖𝗔).
  93 #p #f <unwind_append_proper_dx //
  94 qed.
  95
  96 lemma unwind_path_S_dx (p) (f):
  97       (⊗p)◖𝗦 = ▼[f](p◖𝗦).
  98 #p #f <unwind_append_proper_dx //
  99 qed.
 100
 101 lemma unwind_path_root (f) (p):
 102       ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
 103 #f #p @(list_ind_rcons … p) -p
 104 [ /2 width=3 by ex2_intro/
 105 | #p * [ #n ] /2 width=3 by ex2_intro/
 106 ]
 107 qed-.
 108
 109 (* Advanced inversions with proj_path ***************************************)
 110
 111 lemma unwind_path_inv_d_sn (k) (q) (p) (f):
 112       (𝗱k◗q) = ▼[f]p →
 113       ∃∃r,h. 𝐞 = ⊗r & (▼[r]f)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
 114 #k #q #p @(path_ind_unwind … p) -p
 115 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 116 [ <unwind_path_empty #H destruct
 117 | <unwind_path_d_empty #H destruct -IH
 118   /2 width=5 by ex4_2_intro/
 119 | <unwind_path_d_lcons #H
 120   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
 121   /2 width=5 by ex4_2_intro/
 122 | <unwind_path_m_sn #H
 123   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
 124   /2 width=5 by ex4_2_intro/
 125 | <unwind_path_L_sn #H destruct
 126 | <unwind_path_A_sn #H destruct
 127 | <unwind_path_S_sn #H destruct
 128 ]
 129 qed-.
 130
 131 lemma unwind_path_inv_m_sn (q) (p) (f):
 132       (𝗺◗q) = ▼[f]p → ⊥.
 133 #q #p @(path_ind_unwind … p) -p
 134 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 135 [ <unwind_path_empty #H destruct
 136 | <unwind_path_d_empty #H destruct
 137 | <unwind_path_d_lcons #H /2 width=2 by/
 138 | <unwind_path_m_sn #H /2 width=2 by/
 139 | <unwind_path_L_sn #H destruct
 140 | <unwind_path_A_sn #H destruct
 141 | <unwind_path_S_sn #H destruct
 142 ]
 143 qed-.
 144
 145 lemma unwind_path_inv_L_sn (q) (p) (f):
 146       (𝗟◗q) = ▼[f]p →
 147       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▼[r1]f]r2 & r1●𝗟◗r2 = p.
 148 #q #p @(path_ind_unwind … p) -p
 149 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 150 [ <unwind_path_empty #H destruct
 151 | <unwind_path_d_empty #H destruct
 152 | <unwind_path_d_lcons #H
 153   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 154   /2 width=5 by ex3_2_intro/
 155 | <unwind_path_m_sn #H
 156   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 157   /2 width=5 by ex3_2_intro/
 158 | <unwind_path_L_sn #H destruct -IH
 159   /2 width=5 by ex3_2_intro/
 160 | <unwind_path_A_sn #H destruct
 161 | <unwind_path_S_sn #H destruct
 162 ]
 163 qed-.
 164
 165 lemma unwind_path_inv_A_sn (q) (p) (f):
 166       (𝗔◗q) = ▼[f]p →
 167       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▼[r1]f]r2 & r1●𝗔◗r2 = p.
 168 #q #p @(path_ind_unwind … p) -p
 169 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 170 [ <unwind_path_empty #H destruct
 171 | <unwind_path_d_empty #H destruct
 172 | <unwind_path_d_lcons #H
 173   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 174   /2 width=5 by ex3_2_intro/
 175 | <unwind_path_m_sn #H
 176   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 177   /2 width=5 by ex3_2_intro/
 178 | <unwind_path_L_sn #H destruct
 179 | <unwind_path_A_sn #H destruct -IH
 180   /2 width=5 by ex3_2_intro/
 181 | <unwind_path_S_sn #H destruct
 182 ]
 183 qed-.
 184
 185 lemma unwind_path_inv_S_sn (q) (p) (f):
 186       (𝗦◗q) = ▼[f]p →
 187       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▼[r1]f]r2 & r1●𝗦◗r2 = p.
 188 #q #p @(path_ind_unwind … p) -p
 189 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 190 [ <unwind_path_empty #H destruct
 191 | <unwind_path_d_empty #H destruct
 192 | <unwind_path_d_lcons #H
 193   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 194   /2 width=5 by ex3_2_intro/
 195 | <unwind_path_m_sn #H
 196   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
 197   /2 width=5 by ex3_2_intro/| <unwind_path_L_sn #H destruct
 198 | <unwind_path_A_sn #H destruct
 199 | <unwind_path_S_sn #H destruct -IH
 200   /2 width=5 by ex3_2_intro/
 201 ]
 202 qed-.
 203
 204 (* Inversions with proper condition for path ********************************)
 205
 206 lemma unwind_inv_append_proper_dx (q2) (q1) (p) (f):
 207       q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
 208       ∃∃p1,p2. ⊗p1 = q1 & ▼[▼[p1]f]p2 = q2 & p1●p2 = p.
 209 #q2 #q1 elim q1 -q1
 210 [ #p #f #Hq2 <list_append_empty_sn #H destruct
 211   /2 width=5 by ex3_2_intro/
 212 | * [ #n1 ] #q1 #IH #p #f #Hq2 <list_append_lcons_sn #H
 213   [ elim (unwind_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
 214     elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
 215     elim Hq2 -Hq2 //
 216   | elim (unwind_path_inv_m_sn … H)
 217   | elim (unwind_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
 218     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
 219     @(ex3_2_intro … (r1●𝗟◗p1)) //
 220     <structure_append <Hr1 -Hr1 //
 221   | elim (unwind_path_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
 222     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
 223     @(ex3_2_intro … (r1●𝗔◗p1)) //
 224     <structure_append <Hr1 -Hr1 //
 225   | elim (unwind_path_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
 226     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
 227     @(ex3_2_intro … (r1●𝗦◗p1)) //
 228     <structure_append <Hr1 -Hr1 //
 229   ]
 230 ]
 231 qed-.
 232
 233 (* Inversions with inner condition for path *********************************)
 234
 235 lemma unwind_inv_append_inner_sn (q1) (q2) (p) (f):
 236       q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
 237       ∃∃p1,p2. ⊗p1 = q1 & ▼[▼[p1]f]p2 = q2 & p1●p2 = p.
 238 #q1 @(list_ind_rcons … q1) -q1
 239 [ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
 240   /2 width=5 by ex3_2_intro/
 241 | #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
 242   [ elim (pic_inv_d_dx … Hq2)
 243   | <list_append_rcons_sn #H0
 244     elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
 245     elim (unwind_path_inv_m_sn … (sym_eq … H2))
 246   | <list_append_rcons_sn #H0
 247     elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
 248     elim (unwind_path_inv_L_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
 249     @(ex3_2_intro … (p1●r2◖𝗟)) [1,3: // ]
 250     [ <structure_append <structure_L_dx <Hr2 -Hr2 //
 251     | <list_append_assoc <list_append_rcons_sn //
 252     ]
 253   | <list_append_rcons_sn #H0
 254     elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
 255     elim (unwind_path_inv_A_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
 256     @(ex3_2_intro … (p1●r2◖𝗔)) [1,3: // ]
 257     [ <structure_append <structure_A_dx <Hr2 -Hr2 //
 258     | <list_append_assoc <list_append_rcons_sn //
 259     ]
 260   | <list_append_rcons_sn #H0
 261     elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
 262     elim (unwind_path_inv_S_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
 263     @(ex3_2_intro … (p1●r2◖𝗦)) [1,3: // ]
 264     [ <structure_append <structure_S_dx <Hr2 -Hr2 //
 265     | <list_append_assoc <list_append_rcons_sn //
 266     ]
 267   ]
 268 ]
 269 qed-.