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_m   ⇒ structure q
  28    | label_L   ⇒ (structure q)◖𝗟
  29    | label_A   ⇒ (structure q)◖𝗔
  30    | label_S   ⇒ (structure q)◖𝗦
  31    ]
  32 ].
  33
  34 interpretation
  35   "structure (path)"
  36   'CircledTimes p = (structure p).
  37
  38 (* Basic constructions ******************************************************)
  39
  40 lemma structure_empty:
  41       𝐞 = ⊗𝐞.
  42 // qed.
  43
  44 lemma structure_d_dx (p) (k):
  45       ⊗p = ⊗(p◖𝗱k).
  46 // qed.
  47
  48 lemma structure_m_dx (p):
  49       ⊗p = ⊗(p◖𝗺).
  50 // qed.
  51
  52 lemma structure_L_dx (p):
  53       (⊗p)◖𝗟 = ⊗(p◖𝗟).
  54 // qed.
  55
  56 lemma structure_A_dx (p):
  57       (⊗p)◖𝗔 = ⊗(p◖𝗔).
  58 // qed.
  59
  60 lemma structure_S_dx (p):
  61       (⊗p)◖𝗦 = ⊗(p◖𝗦).
  62 // qed.
  63
  64 (* Main constructions *******************************************************)
  65
  66 theorem structure_idem (p):
  67         ⊗p = ⊗⊗p.
  68 #p elim p -p [| * [ #k ] #p #IH ] //
  69 qed.
  70
  71 theorem structure_append (p) (q):
  72         ⊗p●⊗q = ⊗(p●q).
  73 #p #q elim q -q [| * [ #k ] #q #IH ]
  74 [||*: <list_append_lcons_sn ] //
  75 qed.
  76
  77 (* Constructions with path_lcons ********************************************)
  78
  79 lemma structure_d_sn (p) (k):
  80       ⊗p = ⊗(𝗱k◗p).
  81 #p #n <structure_append //
  82 qed.
  83
  84 lemma structure_m_sn (p):
  85       ⊗p = ⊗(𝗺◗p).
  86 #p <structure_append //
  87 qed.
  88
  89 lemma structure_L_sn (p):
  90       (𝗟◗⊗p) = ⊗(𝗟◗p).
  91 #p <structure_append //
  92 qed.
  93
  94 lemma structure_A_sn (p):
  95       (𝗔◗⊗p) = ⊗(𝗔◗p).
  96 #p <structure_append //
  97 qed.
  98
  99 lemma structure_S_sn (p):
 100       (𝗦◗⊗p) = ⊗(𝗦◗p).
 101 #p <structure_append //
 102 qed.
 103
 104 (* Basic inversions *********************************************************)
 105
 106 lemma eq_inv_d_dx_structure (h) (q) (p):
 107       q◖𝗱h = ⊗p → ⊥.
 108 #h #q #p elim p -p [| * [ #k ] #p #IH ]
 109 [ <structure_empty #H0 destruct
 110 | <structure_d_dx #H0 /2 width=1 by/
 111 | <structure_m_dx #H0 /2 width=1 by/
 112 | <structure_L_dx #H0 destruct
 113 | <structure_A_dx #H0 destruct
 114 | <structure_S_dx #H0 destruct
 115 ]
 116 qed-.
 117
 118 lemma eq_inv_m_dx_structure (q) (p):
 119       q◖𝗺 = ⊗p → ⊥.
 120 #q #p elim p -p [| * [ #k ] #p #IH ]
 121 [ <structure_empty #H0 destruct
 122 | <structure_d_dx #H0 /2 width=1 by/
 123 | <structure_m_dx #H0 /2 width=1 by/
 124 | <structure_L_dx #H0 destruct
 125 | <structure_A_dx #H0 destruct
 126 | <structure_S_dx #H0 destruct
 127 ]
 128 qed-.
 129
 130 lemma eq_inv_L_dx_structure (q) (p):
 131       q◖𝗟 = ⊗p →
 132       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
 133 #q #p elim p -p [| * [ #k ] #p #IH ]
 134 [ <structure_empty #H0 destruct
 135 | <structure_d_dx #H0
 136   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 137   /2 width=5 by ex3_2_intro/
 138 | <structure_m_dx #H0
 139   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 140   /2 width=5 by ex3_2_intro/
 141 | <structure_L_dx #H0 destruct -IH
 142   /2 width=5 by ex3_2_intro/
 143 | <structure_A_dx #H0 destruct
 144 | <structure_S_dx #H0 destruct
 145 ]
 146 qed-.
 147
 148 lemma eq_inv_A_dx_structure (q) (p):
 149       q◖𝗔 = ⊗p →
 150       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.
 151 #q #p elim p -p [| * [ #k ] #p #IH ]
 152 [ <structure_empty #H0 destruct
 153 | <structure_d_dx #H0
 154   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 155   /2 width=5 by ex3_2_intro/
 156 | <structure_m_dx #H0
 157   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 158   /2 width=5 by ex3_2_intro/
 159 | <structure_L_dx #H0 destruct
 160 | <structure_A_dx #H0 destruct -IH
 161   /2 width=5 by ex3_2_intro/
 162 | <structure_S_dx #H0 destruct
 163 ]
 164 qed-.
 165
 166 lemma eq_inv_S_dx_structure (q) (p):
 167       q◖𝗦 = ⊗p →
 168       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.
 169 #q #p elim p -p [| * [ #k ] #p #IH ]
 170 [ <structure_empty #H0 destruct
 171 | <structure_d_dx #H0
 172   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 173   /2 width=5 by ex3_2_intro/
 174 | <structure_m_dx #H0
 175   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
 176   /2 width=5 by ex3_2_intro/
 177 | <structure_L_dx #H0 destruct
 178 | <structure_A_dx #H0 destruct
 179 | <structure_S_dx #H0 destruct -IH
 180   /2 width=5 by ex3_2_intro/
 181 ]
 182 qed-.
 183
 184 (* Main inversions **********************************************************)
 185
 186 theorem eq_inv_append_structure (p) (q) (r):
 187         p●q = ⊗r →
 188         ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.
 189 #p #q elim q -q [| * [ #k ] #q #IH ] #r
 190 [ <list_append_empty_sn #H0 destruct
 191   /2 width=5 by ex3_2_intro/
 192 | #H0 elim (eq_inv_d_dx_structure … H0)
 193 | #H0 elim (eq_inv_m_dx_structure … H0)
 194 | #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 195   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 196   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
 197   <structure_append <structure_L_sn <Hr2 -Hr2 //
 198 | #H0 elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 199   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 200   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
 201   <structure_append <structure_A_sn <Hr2 -Hr2 //
 202 | #H0 elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 203   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 204   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
 205   <structure_append <structure_S_sn <Hr2 -Hr2 //
 206 ]
 207 qed-.
 208
 209 (* Inversions with path_lcons ***********************************************)
 210
 211 lemma eq_inv_d_sn_structure (h) (q) (p):
 212       (𝗱h◗q) = ⊗p → ⊥.
 213 #h #q #p >list_cons_comm #H0
 214 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 215 <list_cons_comm #H0 #H1 #H2 destruct
 216 elim (eq_inv_d_dx_structure … H0)
 217 qed-.
 218
 219 lemma eq_inv_m_sn_structure (q) (p):
 220       (𝗺 ◗q) = ⊗p → ⊥.
 221 #q #p >list_cons_comm #H0
 222 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 223 <list_cons_comm #H0 #H1 #H2 destruct
 224 elim (eq_inv_m_dx_structure … H0)
 225 qed-.
 226
 227 lemma eq_inv_L_sn_structure (q) (p):
 228       (𝗟◗q) = ⊗p →
 229       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗟◗r2 = p.
 230 #q #p >list_cons_comm #H0
 231 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 232 <list_cons_comm #H0 #H1 #H2 destruct
 233 elim (eq_inv_L_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
 234 @(ex3_2_intro … s1 (s2●r2)) // -s1
 235 <structure_append <H2 -s2 //
 236 qed-.
 237
 238 lemma eq_inv_A_sn_structure (q) (p):
 239       (𝗔◗q) = ⊗p →
 240       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗔◗r2 = p.
 241 #q #p >list_cons_comm #H0
 242 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 243 <list_cons_comm #H0 #H1 #H2 destruct
 244 elim (eq_inv_A_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
 245 @(ex3_2_intro … s1 (s2●r2)) // -s1
 246 <structure_append <H2 -s2 //
 247 qed-.
 248
 249 lemma eq_inv_S_sn_structure (q) (p):
 250       (𝗦◗q) = ⊗p →
 251       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗦◗r2 = p.
 252 #q #p >list_cons_comm #H0
 253 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 254 <list_cons_comm #H0 #H1 #H2 destruct
 255 elim (eq_inv_S_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
 256 @(ex3_2_intro … s1 (s2●r2)) // -s1
 257 <structure_append <H2 -s2 //
 258 qed-.