matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_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/substitution/prelift_label.ma".
  16 include "delayed_updating/substitution/lift_rmap.ma".
  17
  18 (* LIFT FOR PATH ************************************************************)
  19
  20 rec definition lift_path (f) (p) on p: path ≝
  21 match p with
  22 [ list_empty     ⇒ (𝐞)
  23 | list_lcons l q ⇒ (lift_path f q)◖↑[↑[q]f]l
  24 ].
  25
  26 interpretation
  27   "lift (path)"
  28   'UpArrow f l = (lift_path f l).
  29
  30 (* Basic constructions ******************************************************)
  31
  32 lemma lift_path_empty (f):
  33       (𝐞) = ↑[f]𝐞.
  34 // qed.
  35
  36 lemma lift_path_rcons (f) (p) (l):
  37       (↑[f]p)◖↑[↑[p]f]l = ↑[f](p◖l).
  38 // qed.
  39
  40 lemma lift_path_d_dx (f) (p) (k):
  41       (↑[f]p)◖𝗱((↑[p]f)＠⧣❨k❩) = ↑[f](p◖𝗱k).
  42 // qed.
  43
  44 lemma lift_path_m_dx (f) (p):
  45       (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
  46 // qed.
  47
  48 lemma lift_path_L_dx (f) (p):
  49       (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
  50 // qed.
  51
  52 lemma lift_path_A_dx (f) (p):
  53       (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
  54 // qed.
  55
  56 lemma lift_path_S_dx (f) (p):
  57       (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
  58 // qed.
  59
  60 (* Constructions with path_append *******************************************)
  61
  62 lemma lift_path_append (f) (p) (q):
  63       (↑[f]p)●(↑[↑[p]f]q) = ↑[f](p●q).
  64 #f #p #q elim q -q //
  65 #l #q #IH
  66 <lift_path_rcons <lift_path_rcons
  67 <list_append_lcons_sn //
  68 qed.
  69
  70 (* Constructions with path_lcons ********************************************)
  71
  72 lemma lift_path_lcons (f) (p) (l):
  73       (↑[f]l)◗↑[↑[l]f]p = ↑[f](l◗p).
  74 #f #p #l
  75 <lift_path_append //
  76 qed.
  77
  78 lemma lift_path_d_sn (f) (p) (k:pnat):
  79       (𝗱(f＠⧣❨k❩)◗↑[⇂*[k]f]p) = ↑[f](𝗱k◗p).
  80 // qed.
  81
  82 lemma lift_path_m_sn (f) (p):
  83       (𝗺◗↑[f]p) = ↑[f](𝗺◗p).
  84 // qed.
  85
  86 lemma lift_path_L_sn (f) (p):
  87       (𝗟◗↑[⫯f]p) = ↑[f](𝗟◗p).
  88 // qed.
  89
  90 lemma lift_path_A_sn (f) (p):
  91       (𝗔◗↑[f]p) = ↑[f](𝗔◗p).
  92 // qed.
  93
  94 lemma lift_path_S_sn (f) (p):
  95       (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
  96 // qed.
  97
  98 (* Basic inversions *********************************************************)
  99
 100 lemma lift_path_inv_empty (f) (p):
 101       (𝐞) = ↑[f]p → 𝐞 = p.
 102 #f * // #p #l
 103 <lift_path_rcons #H0 destruct
 104 qed-.
 105
 106 lemma lift_path_inv_rcons (f) (p2) (q1) (l1):
 107       q1◖l1 = ↑[f]p2 →
 108       ∃∃q2,l2. q1 = ↑[f]q2 & l1 = ↑[↑[q2]f]l2 & q2◖l2 = p2.
 109 #f * [| #l2 #q2 ] #q1 #l1
 110 [ <lift_path_empty
 111 | <lift_path_rcons
 112 ]
 113 #H0 destruct
 114 /2 width=5 by ex3_2_intro/
 115 qed-.
 116
 117 (* Inversions with path_append **********************************************)
 118
 119 lemma lift_path_inv_append_sn (f) (q1) (r1) (p2):
 120       q1●r1 = ↑[f]p2 →
 121       ∃∃q2,r2. q1 = ↑[f]q2 & r1 = ↑[↑[q2]f]r2 & q2●r2 = p2.
 122 #f #q1 #r1 elim r1 -r1 [| #l1 #r1 #IH ] #p2
 123 [ <list_append_empty_sn #H0 destruct
 124   /2 width=5 by ex3_2_intro/
 125 | <list_append_lcons_sn #H0
 126   elim (lift_path_inv_rcons … H0) -H0 #x2 #l2 #H0 #H1 #H2 destruct
 127   elim (IH … H0) -IH -H0 #q2 #r2 #H1 #H2 #H3 destruct
 128   /2 width=5 by ex3_2_intro/
 129 ]
 130 qed-.
 131
 132 (* Main inversions **********************************************************)
 133
 134 theorem lift_path_inj (f) (p1) (p2):
 135         ↑[f]p1 = ↑[f]p2 → p1 = p2.
 136 #f #p1 elim p1 -p1 [| #l1 #q1 #IH ] #p2
 137 [ <lift_path_empty #H0
 138   <(lift_path_inv_empty … H0) -H0 //
 139 | <lift_path_rcons #H0
 140   elim (lift_path_inv_rcons … H0) -H0 #q2 #l2 #Hq
 141   <(IH … Hq) -IH -q2 #Hl #H0 destruct
 142   <(prelift_label_inj … Hl) -l2 //
 143 ]
 144 qed-.