matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_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.ma".
  16 include "delayed_updating/notation/functions/circled_times_1.ma".
  17 include "ground/xoa/ex_3_2.ma".
  18
  19 (* STRUCTURE FOR PATH *******************************************************)
  20
  21 rec definition structure (p) on p ≝
  22 match p with
  23 [ list_empty     ⇒ 𝐞
  24 | list_lcons l q ⇒
  25    match l with
  26    [ label_d k    ⇒ structure q
  27    | label_d2 k d ⇒ structure q
  28    | label_m      ⇒ structure q
  29    | label_L      ⇒ (structure q)◖𝗟
  30    | label_A      ⇒ (structure q)◖𝗔
  31    | label_S      ⇒ (structure q)◖𝗦
  32    ]
  33 ].
  34
  35 interpretation
  36   "structure (path)"
  37   'CircledTimes p = (structure p).
  38
  39 (* Basic constructions ******************************************************)
  40
  41 lemma structure_empty:
  42       𝐞 = ⊗𝐞.
  43 // qed.
  44
  45 lemma structure_d_dx (p) (k):
  46       ⊗p = ⊗(p◖𝗱k).
  47 // qed.
  48
  49 lemma structure_d2_dx (p) (k) (d):
  50       ⊗p = ⊗(p◖𝗱❨k,d❩).
  51 // qed.
  52
  53 lemma structure_m_dx (p):
  54       ⊗p = ⊗(p◖𝗺).
  55 // qed.
  56
  57 lemma structure_L_dx (p):
  58       (⊗p)◖𝗟 = ⊗(p◖𝗟).
  59 // qed.
  60
  61 lemma structure_A_dx (p):
  62       (⊗p)◖𝗔 = ⊗(p◖𝗔).
  63 // qed.
  64
  65 lemma structure_S_dx (p):
  66       (⊗p)◖𝗦 = ⊗(p◖𝗦).
  67 // qed.
  68
  69 (* Main constructions *******************************************************)
  70
  71 theorem structure_idem (p):
  72         ⊗p = ⊗⊗p.
  73 #p elim p -p //
  74 * [ #k | #k #d ] #p #IH //
  75 qed.
  76
  77 theorem structure_append (p) (q):
  78         ⊗p●⊗q = ⊗(p●q).
  79 #p #q elim q -q //
  80 * [ #k | #k #d ] #q #IH //
  81 <list_append_lcons_sn //
  82 qed.
  83
  84 (* Constructions with path_lcons ********************************************)
  85
  86 lemma structure_d_sn (p) (k):
  87       ⊗p = ⊗(𝗱k◗p).
  88 #p #k <structure_append //
  89 qed.
  90
  91 lemma structure_d2_sn (p) (k) (d):
  92       ⊗p = ⊗(𝗱❨k,d❩◗p).
  93 #p #k #d <structure_append //
  94 qed.
  95
  96 lemma structure_m_sn (p):
  97       ⊗p = ⊗(𝗺◗p).
  98 #p <structure_append //
  99 qed.
 100
 101 lemma structure_L_sn (p):
 102       (𝗟◗⊗p) = ⊗(𝗟◗p).
 103 #p <structure_append //
 104 qed.
 105
 106 lemma structure_A_sn (p):
 107       (𝗔◗⊗p) = ⊗(𝗔◗p).
 108 #p <structure_append //
 109 qed.
 110
 111 lemma structure_S_sn (p):
 112       (𝗦◗⊗p) = ⊗(𝗦◗p).
 113 #p <structure_append //
 114 qed.
 115
 116 (* Basic inversions *********************************************************)
 117
 118 lemma eq_inv_d_dx_structure (h) (q) (p):
 119       q◖𝗱h = ⊗p → ⊥.
 120 #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 121 [ <structure_empty #H0 destruct
 122 | <structure_d_dx #H0 /2 width=1 by/
 123 | <structure_d2_dx #H0 /2 width=1 by/
 124 | <structure_m_dx #H0 /2 width=1 by/
 125 | <structure_L_dx #H0 destruct
 126 | <structure_A_dx #H0 destruct
 127 | <structure_S_dx #H0 destruct
 128 ]
 129 qed-.
 130
 131 lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
 132       q◖𝗱❨h,d❩ = ⊗p → ⊥.
 133 #d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 134 [ <structure_empty #H0 destruct
 135 | <structure_d_dx #H0 /2 width=1 by/
 136 | <structure_d2_dx #H0 /2 width=1 by/
 137 | <structure_m_dx #H0 /2 width=1 by/
 138 | <structure_L_dx #H0 destruct
 139 | <structure_A_dx #H0 destruct
 140 | <structure_S_dx #H0 destruct
 141 ]
 142 qed-.
 143
 144 lemma eq_inv_m_dx_structure (q) (p):
 145       q◖𝗺 = ⊗p → ⊥.
 146 #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 147 [ <structure_empty #H0 destruct
 148 | <structure_d_dx #H0 /2 width=1 by/
 149 | <structure_d2_dx #H0 /2 width=1 by/
 150 | <structure_m_dx #H0 /2 width=1 by/
 151 | <structure_L_dx #H0 destruct
 152 | <structure_A_dx #H0 destruct
 153 | <structure_S_dx #H0 destruct
 154 ]
 155 qed-.
 156
 157 lemma eq_inv_L_dx_structure (q) (p):
 158       q◖𝗟 = ⊗p →
 159       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
 160 #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 161 [ <structure_empty #H0 destruct
 162 | <structure_d_dx #H0
 163   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 164   /2 width=5 by ex3_2_intro/
 165 | <structure_d2_dx #H0
 166   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 167   /2 width=5 by ex3_2_intro/
 168 | <structure_m_dx #H0
 169   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 170   /2 width=5 by ex3_2_intro/
 171 | <structure_L_dx #H0 destruct -IH
 172   /2 width=5 by ex3_2_intro/
 173 | <structure_A_dx #H0 destruct
 174 | <structure_S_dx #H0 destruct
 175 ]
 176 qed-.
 177
 178 lemma eq_inv_A_dx_structure (q) (p):
 179       q◖𝗔 = ⊗p →
 180       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.
 181 #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 182 [ <structure_empty #H0 destruct
 183 | <structure_d_dx #H0
 184   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 185   /2 width=5 by ex3_2_intro/
 186 | <structure_d2_dx #H0
 187   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 188   /2 width=5 by ex3_2_intro/
 189 | <structure_m_dx #H0
 190   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 191   /2 width=5 by ex3_2_intro/
 192 | <structure_L_dx #H0 destruct
 193 | <structure_A_dx #H0 destruct -IH
 194   /2 width=5 by ex3_2_intro/
 195 | <structure_S_dx #H0 destruct
 196 ]
 197 qed-.
 198
 199 lemma eq_inv_S_dx_structure (q) (p):
 200       q◖𝗦 = ⊗p →
 201       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.
 202 #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 203 [ <structure_empty #H0 destruct
 204 | <structure_d_dx #H0
 205   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 206   /2 width=5 by ex3_2_intro/
 207 | <structure_d2_dx #H0
 208   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 209   /2 width=5 by ex3_2_intro/
 210 | <structure_m_dx #H0
 211   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 212   /2 width=5 by ex3_2_intro/
 213 | <structure_L_dx #H0 destruct
 214 | <structure_A_dx #H0 destruct
 215 | <structure_S_dx #H0 destruct -IH
 216   /2 width=5 by ex3_2_intro/
 217 ]
 218 qed-.
 219
 220 (* Main inversions **********************************************************)
 221
 222 theorem eq_inv_append_structure (p) (q) (r):
 223         p●q = ⊗r →
 224         ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.
 225 #p #q elim q -q [| * [ #k | #k #d ] #q #IH ] #r
 226 [ <list_append_empty_sn #H0 destruct
 227   /2 width=5 by ex3_2_intro/
 228 | #H0 elim (eq_inv_d_dx_structure … H0)
 229 | #H0 elim (eq_inv_d2_dx_structure … H0)
 230 | #H0 elim (eq_inv_m_dx_structure … H0)
 231 | #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 232   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 233   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
 234   <structure_append <structure_L_sn <Hr2 -Hr2 //
 235 | #H0 elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 236   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 237   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
 238   <structure_append <structure_A_sn <Hr2 -Hr2 //
 239 | #H0 elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 240   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 241   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
 242   <structure_append <structure_S_sn <Hr2 -Hr2 //
 243 ]
 244 qed-.
 245
 246 (* Inversions with path_lcons ***********************************************)
 247
 248 lemma eq_inv_d_sn_structure (h) (q) (p):
 249       (𝗱h◗q) = ⊗p → ⊥.
 250 #h #q #p >list_cons_comm #H0
 251 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 252 <list_cons_comm #H0 #H1 #H2 destruct
 253 elim (eq_inv_d_dx_structure … H0)
 254 qed-.
 255
 256 lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
 257       (𝗱❨h,d❩◗q) = ⊗p → ⊥.
 258 #d #h #q #p >list_cons_comm #H0
 259 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 260 <list_cons_comm #H0 #H1 #H2 destruct
 261 elim (eq_inv_d2_dx_structure … H0)
 262 qed-.
 263
 264 lemma eq_inv_m_sn_structure (q) (p):
 265       (𝗺 ◗q) = ⊗p → ⊥.
 266 #q #p >list_cons_comm #H0
 267 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 268 <list_cons_comm #H0 #H1 #H2 destruct
 269 elim (eq_inv_m_dx_structure … H0)
 270 qed-.
 271
 272 lemma eq_inv_L_sn_structure (q) (p):
 273       (𝗟◗q) = ⊗p →
 274       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗟◗r2 = p.
 275 #q #p >list_cons_comm #H0
 276 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 277 <list_cons_comm #H0 #H1 #H2 destruct
 278 elim (eq_inv_L_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
 279 @(ex3_2_intro … s1 (s2●r2)) // -s1
 280 <structure_append <H2 -s2 //
 281 qed-.
 282
 283 lemma eq_inv_A_sn_structure (q) (p):
 284       (𝗔◗q) = ⊗p →
 285       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗔◗r2 = p.
 286 #q #p >list_cons_comm #H0
 287 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 288 <list_cons_comm #H0 #H1 #H2 destruct
 289 elim (eq_inv_A_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
 290 @(ex3_2_intro … s1 (s2●r2)) // -s1
 291 <structure_append <H2 -s2 //
 292 qed-.
 293
 294 lemma eq_inv_S_sn_structure (q) (p):
 295       (𝗦◗q) = ⊗p →
 296       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗦◗r2 = p.
 297 #q #p >list_cons_comm #H0
 298 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 299 <list_cons_comm #H0 #H1 #H2 destruct
 300 elim (eq_inv_S_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
 301 @(ex3_2_intro … s1 (s2●r2)) // -s1
 302 <structure_append <H2 -s2 //
 303 qed-.