matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.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/unwind/unwind2_rmap.ma".
  16 include "delayed_updating/syntax/path_structure.ma".
  17 include "delayed_updating/notation/functions/black_downtriangle_2.ma".
  18
  19 (* TAILED UNWIND FOR PATH ***************************************************)
  20
  21 definition unwind2_path (f) (p): path ≝
  22 match p with
  23 [ list_empty     ⇒ (𝐞)
  24 | list_lcons l q ⇒
  25   match l with
  26   [ label_d k ⇒ (⊗q)◖𝗱(▶[f]q＠⧣❨k❩)
  27   | label_m   ⇒ ⊗p
  28   | label_L   ⇒ ⊗p
  29   | label_A   ⇒ ⊗p
  30   | label_S   ⇒ ⊗p
  31   ]
  32 ].
  33
  34 interpretation
  35   "tailed unwind (path)"
  36   'BlackDownTriangle f p = (unwind2_path f p).
  37
  38 (* Basic constructions ******************************************************)
  39
  40 lemma unwind2_path_empty (f):
  41       (𝐞) = ▼[f]𝐞.
  42 // qed.
  43
  44 lemma unwind2_path_d_dx (f) (p) (k) :
  45       (⊗p)◖𝗱((▶[f]p)＠⧣❨k❩) = ▼[f](p◖𝗱k).
  46 // qed.
  47
  48 lemma unwind2_path_m_dx (f) (p):
  49       ⊗p = ▼[f](p◖𝗺).
  50 // qed.
  51
  52 lemma unwind2_path_L_dx (f) (p):
  53       (⊗p)◖𝗟 = ▼[f](p◖𝗟).
  54 // qed.
  55
  56 lemma unwind2_path_A_dx (f) (p):
  57       (⊗p)◖𝗔 = ▼[f](p◖𝗔).
  58 // qed.
  59
  60 lemma unwind2_path_S_dx (f) (p):
  61       (⊗p)◖𝗦 = ▼[f](p◖𝗦).
  62 // qed.
  63
  64 (* Constructions with structure *********************************************)
  65
  66 lemma structure_unwind2_path (f) (p):
  67       ⊗p = ⊗▼[f]p.
  68 #f * // * [ #k ] #p //
  69 qed.
  70
  71 lemma unwind2_path_structure (f) (p):
  72       ⊗p = ▼[f]⊗p.
  73 #f #p elim p -p // * [ #k ] #p #IH //
  74 [ <structure_L_dx <unwind2_path_L_dx //
  75 | <structure_A_dx <unwind2_path_A_dx //
  76 | <structure_S_dx <unwind2_path_S_dx //
  77 ]
  78 qed.
  79
  80 lemma unwind2_path_root (f) (p):
  81       ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
  82 #f * [| * [ #k ] #p ]
  83 /2 width=3 by ex2_intro/
  84 <unwind2_path_d_dx <structure_d_dx
  85 /2 width=3 by ex2_intro/
  86 qed-.
  87
  88 (* Destructions with structure **********************************************)
  89
  90 lemma unwind2_path_des_structure (f) (q) (p):
  91       ⊗q = ▼[f]p → ⊗q = ⊗p.
  92 // qed-.
  93
  94 (* Basic inversions *********************************************************)
  95
  96 lemma eq_inv_d_dx_unwind2_path (f) (q) (p) (h):
  97       q◖𝗱h = ▼[f]p →
  98       ∃∃r,k. q = ⊗r & h = ▶[f]r＠⧣❨k❩ & r◖𝗱k = p.
  99 #f #q * [| * [ #k ] #p ] #h
 100 [ <unwind2_path_empty #H0 destruct
 101 | <unwind2_path_d_dx #H0 destruct
 102   /2 width=5 by ex3_2_intro/
 103 | <unwind2_path_m_dx #H0
 104   elim (eq_inv_d_dx_structure … H0)
 105 | <unwind2_path_L_dx #H0 destruct
 106 | <unwind2_path_A_dx #H0 destruct
 107 | <unwind2_path_S_dx #H0 destruct
 108 ]
 109 qed-.
 110
 111 lemma eq_inv_m_dx_unwind2_path (f) (q) (p):
 112       q◖𝗺 = ▼[f]p → ⊥.
 113 #f #q * [| * [ #k ] #p ]
 114 [ <unwind2_path_empty #H0 destruct
 115 | <unwind2_path_d_dx #H0 destruct
 116 | <unwind2_path_m_dx #H0
 117   elim (eq_inv_m_dx_structure … H0)
 118 | <unwind2_path_L_dx #H0 destruct
 119 | <unwind2_path_A_dx #H0 destruct
 120 | <unwind2_path_S_dx #H0 destruct
 121 ]
 122 qed-.
 123
 124 lemma eq_inv_L_dx_unwind2_path (f) (q) (p):
 125       q◖𝗟 = ▼[f]p →
 126       ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗟◗r2 = p.
 127 #f #q * [| * [ #k ] #p ]
 128 [ <unwind2_path_empty #H0 destruct
 129 | <unwind2_path_d_dx #H0 destruct
 130 | <unwind2_path_m_dx #H0
 131   elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
 132   /2 width=5 by ex3_2_intro/
 133 | <unwind2_path_L_dx #H0 destruct
 134   /2 width=5 by ex3_2_intro/
 135 | <unwind2_path_A_dx #H0 destruct
 136 | <unwind2_path_S_dx #H0 destruct
 137 ]
 138 qed-.
 139
 140 lemma eq_inv_A_dx_unwind2_path (f) (q) (p):
 141       q◖𝗔 = ▼[f]p →
 142       ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗔◗r2 = p.
 143 #f #q * [| * [ #k ] #p ]
 144 [ <unwind2_path_empty #H0 destruct
 145 | <unwind2_path_d_dx #H0 destruct
 146 | <unwind2_path_m_dx #H0
 147   elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
 148   /2 width=5 by ex3_2_intro/
 149 | <unwind2_path_L_dx #H0 destruct
 150 | <unwind2_path_A_dx #H0 destruct
 151   /2 width=5 by ex3_2_intro/
 152 | <unwind2_path_S_dx #H0 destruct
 153 ]
 154 qed-.
 155
 156 lemma eq_inv_S_dx_unwind2_path (f) (q) (p):
 157       q◖𝗦 = ▼[f]p →
 158       ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗦◗r2 = p.
 159 #f #q * [| * [ #k ] #p ]
 160 [ <unwind2_path_empty #H0 destruct
 161 | <unwind2_path_d_dx #H0 destruct
 162 | <unwind2_path_m_dx #H0
 163   elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
 164   /2 width=5 by ex3_2_intro/
 165 | <unwind2_path_L_dx #H0 destruct
 166 | <unwind2_path_A_dx #H0 destruct
 167 | <unwind2_path_S_dx #H0 destruct
 168   /2 width=5 by ex3_2_intro/
 169 ]
 170 qed-.