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