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