matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.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_path.ma".
  16 include "delayed_updating/syntax/path_inner.ma".
  17 include "delayed_updating/syntax/path_proper.ma".
  18 include "ground/xoa/ex_4_2.ma".
  19
  20 (* TAILED UNWIND FOR PATH ***************************************************)
  21
  22 (* Constructions with inner condition for path ******************************)
  23
  24 lemma unwind2_path_inner (f) (p):
  25       p ϵ 𝐈 → ⊗p = ▼[f]p.
  26 #f * // * // #k #q #Hq
  27 elim (pic_inv_d_dx … Hq)
  28 qed-.
  29
  30 (* Constructions with append and inner condition for path *******************)
  31
  32 lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 →
  33       (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
  34 #f #p * [ #Hp | * [ #k ] #q #_ ] //
  35 [ <(unwind2_path_inner … Hp) -Hp //
  36 | <unwind2_path_d_dx <unwind2_path_d_dx
  37   /2 width=3 by trans_eq/
  38 | <unwind2_path_L_dx <unwind2_path_L_dx //
  39 | <unwind2_path_A_dx <unwind2_path_A_dx //
  40 | <unwind2_path_S_dx <unwind2_path_S_dx //
  41 ]
  42 qed.
  43
  44 (* Constructions with append and proper condition for path ******************)
  45
  46 lemma unwind2_path_append_proper_dx (f) (p) (q): q ϵ 𝐏 →
  47       (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
  48 #f #p * [ #Hq | * [ #k ] #q #_ ] //
  49 [ elim (ppc_inv_empty … Hq)
  50 | <unwind2_path_d_dx <unwind2_path_d_dx
  51   /2 width=3 by trans_eq/
  52 | <unwind2_path_L_dx <unwind2_path_L_dx //
  53 | <unwind2_path_A_dx <unwind2_path_A_dx //
  54 | <unwind2_path_S_dx <unwind2_path_S_dx //
  55 ]
  56 qed.
  57
  58 (* Constructions with path_lcons ********************************************)
  59
  60 lemma unwind2_path_d_empty (f) (k):
  61       (𝗱(f＠⧣❨k❩)◗𝐞) = ▼[f](𝗱k◗𝐞).
  62 // qed.
  63
  64 lemma unwind2_path_d_lcons (f) (p) (l) (k:pnat):
  65       ▼[f∘𝐮❨k❩](l◗p) = ▼[f](𝗱k◗l◗p).
  66 #f #p #l #k <unwind2_path_append_proper_dx in ⊢ (???%); //
  67 qed.
  68
  69 lemma unwind2_path_m_sn (f) (p):
  70       ▼[f]p = ▼[f](𝗺◗p).
  71 #f #p <unwind2_path_append_inner_sn //
  72 qed.
  73
  74 lemma unwind2_path_L_sn (f) (p):
  75       (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
  76 #f #p <unwind2_path_append_inner_sn //
  77 qed.
  78
  79 lemma unwind2_path_A_sn (f) (p):
  80       (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
  81 #f #p <unwind2_path_append_inner_sn //
  82 qed.
  83
  84 lemma unwind2_path_S_sn (f) (p):
  85       (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
  86 #f #p <unwind2_path_append_inner_sn //
  87 qed.
  88
  89 (* Destructions with inner condition for path *******************************)
  90
  91 lemma unwind2_path_des_inner (f) (p):
  92       ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
  93 #f * // * [ #k ] #p //
  94 <unwind2_path_d_dx #H0
  95 elim (pic_inv_d_dx … H0)
  96 qed-.
  97
  98 (* Destructions with append and inner condition for path ********************)
  99
 100 lemma unwind2_path_des_append_inner_sn (f) (p) (q1) (q2):
 101       q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
 102       ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
 103 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
 104 [ <list_append_empty_sn #H0 destruct
 105   lapply (unwind2_path_des_inner … Hq1) -Hq1 #Hp
 106   <(unwind2_path_inner … Hp) -Hp
 107   /2 width=5 by ex3_2_intro/
 108 | #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
 109   elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
 110   /2 width=5 by ex3_2_intro/
 111 | #H0 elim (eq_inv_m_dx_unwind2_path … H0)
 112 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 113   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 114   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
 115   <unwind2_path_append_proper_dx //
 116   <unwind2_path_L_sn <Hr2 -Hr2 //
 117 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 118   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 119   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
 120   <unwind2_path_append_proper_dx //
 121   <unwind2_path_A_sn <Hr2 -Hr2 //
 122 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 123   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 124   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
 125   <unwind2_path_append_proper_dx //
 126   <unwind2_path_S_sn <Hr2 -Hr2 //
 127 ]
 128 qed-.
 129
 130 (* Inversions with append and proper condition for path *********************)
 131
 132 lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
 133       q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
 134       ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
 135 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
 136 [ <list_append_empty_sn #H0 destruct
 137   elim (ppc_inv_empty … Hq1)
 138 | #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
 139   elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
 140   /2 width=5 by ex3_2_intro/
 141 | #H0 elim (eq_inv_m_dx_unwind2_path … H0)
 142 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 143   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 144   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
 145   <unwind2_path_append_proper_dx //
 146   <unwind2_path_L_sn <Hr2 -Hr2 //
 147 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 148   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 149   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
 150   <unwind2_path_append_proper_dx //
 151   <unwind2_path_A_sn <Hr2 -Hr2 //
 152 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
 153   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 154   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
 155   <unwind2_path_append_proper_dx //
 156   <unwind2_path_S_sn <Hr2 -Hr2 //
 157 ]
 158 qed-.
 159
 160 (* Inversions with path_lcons ***********************************************)
 161
 162 lemma eq_inv_d_sn_unwind2_path (f) (q) (p) (k):
 163       (𝗱k◗q) = ▼[f]p →
 164       ∃∃r,h. 𝐞 = ⊗r & ▶[f]r＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
 165 #f * [| #l #q ] #p #k
 166 [ <list_cons_comm #H0
 167   elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 168   /2 width=5 by ex4_2_intro/
 169 | >list_cons_comm #H0
 170   elim (unwind2_path_inv_append_proper_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
 171   elim (eq_inv_d_dx_structure … Hr1)
 172 ]
 173 qed-.
 174
 175 lemma eq_inv_m_sn_unwind2_path (f) (q) (p):
 176       (𝗺◗q) = ▼[f]p → ⊥.
 177 #f #q #p
 178 >list_cons_comm #H0
 179 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
 180 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 181 elim (eq_inv_m_dx_structure … Hr1)
 182 qed-.
 183
 184 lemma eq_inv_L_sn_unwind2_path (f) (q) (p):
 185       (𝗟◗q) = ▼[f]p →
 186       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▶[f]r1]r2 & r1●𝗟◗r2 = p.
 187 #f #q #p
 188 >list_cons_comm #H0
 189 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
 190 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 191 elim (eq_inv_L_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 192 <list_append_assoc in H0; <list_append_assoc
 193 <unwind2_path_append_proper_dx //
 194 <unwind2_path_L_sn <H1 <list_append_empty_dx #H0
 195 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 196 /2 width=5 by ex3_2_intro/
 197 qed-.
 198
 199 lemma eq_inv_A_sn_unwind2_path (f) (q) (p):
 200       (𝗔◗q) = ▼[f]p →
 201       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗔◗r2 = p.
 202 #f #q #p
 203 >list_cons_comm #H0
 204 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
 205 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 206 elim (eq_inv_A_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 207 <list_append_assoc in H0; <list_append_assoc
 208 <unwind2_path_append_proper_dx //
 209 <unwind2_path_A_sn <H1 <list_append_empty_dx #H0
 210 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 211 /2 width=5 by ex3_2_intro/
 212 qed-.
 213
 214 lemma eq_inv_S_sn_unwind2_path (f) (q) (p):
 215       (𝗦◗q) = ▼[f]p →
 216       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗦◗r2 = p.
 217 #f #q #p
 218 >list_cons_comm #H0
 219 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
 220 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 221 elim (eq_inv_S_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 222 <list_append_assoc in H0; <list_append_assoc
 223 <unwind2_path_append_proper_dx //
 224 <unwind2_path_S_sn <H1 <list_append_empty_dx #H0
 225 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 226 /2 width=5 by ex3_2_intro/
 227 qed-.
 228
 229 (* Advanced eliminations with path ******************************************)
 230
 231 lemma path_ind_unwind (Q:predicate …):
 232       Q (𝐞) →
 233       (∀k. Q (𝐞) → Q (𝗱k◗𝐞)) →
 234       (∀k,l,p. Q (l◗p) → Q (𝗱k◗l◗p)) →
 235       (∀p. Q p → Q (𝗺◗p)) →
 236       (∀p. Q p → Q (𝗟◗p)) →
 237       (∀p. Q p → Q (𝗔◗p)) →
 238       (∀p. Q p → Q (𝗦◗p)) →
 239       ∀p. Q p.
 240 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
 241 @(list_ind_rcons … p) -p // #p * [ #k ]
 242 [ @(list_ind_rcons … p) -p ]
 243 /2 width=1 by/
 244 qed-.