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