matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_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/unwind/unwind2_path.ma".
  16 include "delayed_updating/unwind/unwind_gen_structure.ma".
  17 include "delayed_updating/syntax/path_inner.ma".
  18 include "delayed_updating/syntax/path_proper.ma".
  19 include "ground/xoa/ex_4_2.ma".
  20
  21 (* UNWIND FOR PATH **********************************************************)
  22
  23 (* Constructions with list_rcons ********************************************)
  24
  25 lemma unwind2_path_d_dx (f) (p) (n) :
  26       (⊗p)◖𝗱((▶[f](pᴿ))＠⧣❨n❩) = ▼[f](p◖𝗱n).
  27 #f #p #n <unwind2_path_unfold
  28 <unwind_gen_d_dx //
  29 qed.
  30
  31 lemma unwind2_path_m_dx (f) (p):
  32       ⊗p = ▼[f](p◖𝗺).
  33 #f #p <unwind2_path_unfold //
  34 qed.
  35
  36 lemma unwind2_path_L_dx (f) (p):
  37       (⊗p)◖𝗟 = ▼[f](p◖𝗟).
  38 #f #p <unwind2_path_unfold //
  39 qed.
  40
  41 lemma unwind2_path_A_dx (f) (p):
  42       (⊗p)◖𝗔 = ▼[f](p◖𝗔).
  43 #f #p <unwind2_path_unfold //
  44 qed.
  45
  46 lemma unwind2_path_S_dx (f) (p):
  47       (⊗p)◖𝗦 = ▼[f](p◖𝗦).
  48 #f #p <unwind2_path_unfold //
  49 qed.
  50
  51 lemma unwind2_path_root (f) (p):
  52       ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
  53 #f #p
  54 elim (unwind_gen_root)
  55 /2 width=3 by ex2_intro/
  56 qed-.
  57
  58 (* Constructions with proper condition for path *****************************)
  59
  60 lemma unwind2_path_append_proper_dx (f) (p1) (p2): p2 ϵ 𝐏 →
  61       (⊗p1)●(▼[▶[f]p1ᴿ]p2) = ▼[f](p1●p2).
  62 #f #p1 #p2 #Hp2 <unwind2_path_unfold <unwind2_path_unfold
  63 <unwind_gen_append_proper_dx // -Hp2 <reverse_append
  64 @(list_ind_rcons … p2) -p2 // #q2 #l2 #_
  65 <reverse_rcons <list_tl_lcons <list_tl_lcons //
  66 qed-.
  67
  68 (* Constructions with inner condition for path ******************************)
  69
  70 lemma unwind2_path_append_inner_sn (f) (p1) (p2): p1 ϵ 𝐈 →
  71       (⊗p1)●(▼[▶[f]p1ᴿ]p2) = ▼[f](p1●p2).
  72 #f #p1 #p2 #Hp1 <unwind2_path_unfold <unwind2_path_unfold
  73 <unwind_gen_append_inner_sn // -Hp1 <reverse_append
  74 @(list_ind_rcons … p2) -p2 // #q2 #l2 #_
  75 <reverse_rcons <list_tl_lcons <list_tl_lcons //
  76 qed-.
  77
  78 (* Inversions with list_lcons ***********************************************)
  79
  80 lemma unwind2_path_inv_S_sn (f) (p) (q):
  81       (𝗦◗q) = ▼[f]p →
  82       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1ᴿ]r2 & r1●𝗦◗r2 = p.
  83 #f #p #q #H0
  84 elim (unwind_gen_inv_S_sn … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
  85 <reverse_append <reverse_lcons
  86 @(list_ind_rcons … r2) -r2 [ /2 width=5 by ex3_2_intro/ ] #r2 #l2 #_
  87 <reverse_rcons <list_append_lcons_sn <list_append_rcons_sn
  88 <list_tl_lcons <unwind2_rmap_append <unwind2_rmap_S_sn
  89 /2 width=5 by ex3_2_intro/
  90 qed-.
  91
  92 (* Inversions with proper condition for path ********************************)
  93
  94 lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
  95       q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
  96       ∃∃p1,p2. ⊗p1 = q1 & ▼[▶[f]p1ᴿ]p2 = q2 & p1●p2 = p.
  97 #f #p #q1 #q2 #Hq2 #H0
  98 elim (unwind_gen_inv_append_proper_dx … Hq2 H0) -Hq2 -H0
  99 #p1 #p2 #H1 #H2 #H3 destruct <reverse_append
 100 @(list_ind_rcons … p2) -p2 [ /2 width=5 by ex3_2_intro/ ] #q2 #l2 #_
 101 <reverse_rcons <list_tl_lcons <unwind2_rmap_append
 102 @ex3_2_intro [4: |*: // ] <unwind2_path_unfold // (**) (* auto fails *)
 103 qed-.
 104
 105 (* Inversions with inner condition for path *********************************)
 106
 107 lemma unwind2_path_inv_append_inner_sn (f) (p) (q1) (q2):
 108       q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
 109       ∃∃p1,p2. ⊗p1 = q1 & ▼[▶[f]p1ᴿ]p2 = q2 & p1●p2 = p.
 110 #f #p #q1 #q2 #Hq1 #H0
 111 elim (unwind_gen_inv_append_inner_sn … Hq1 H0) -Hq1 -H0
 112 #p1 #p2 #H1 #H2 #H3 destruct <reverse_append
 113 @(list_ind_rcons … p2) -p2 [ /2 width=5 by ex3_2_intro/ ] #q2 #l2 #_
 114 <reverse_rcons <list_tl_lcons <unwind2_rmap_append
 115 @ex3_2_intro [4: |*: // ] <unwind2_path_unfold // (**) (* auto fails *)
 116 qed-.