1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "delayed_updating/substitution/prelift_label.ma".
16 include "delayed_updating/substitution/lift_rmap.ma".
18 (* LIFT FOR PATH ************************************************************)
20 rec definition lift_path (f) (p) on p: path ≝
23 | list_lcons l q ⇒ (lift_path f q)◖🠡[🠢[f]q]l
28 'UpTriangleArrow f l = (lift_path f l).
30 (* Basic constructions ******************************************************)
32 lemma lift_path_empty (f):
36 lemma lift_path_rcons (f) (p) (l):
37 (🠡[f]p)◖🠡[🠢[f]p]l = 🠡[f](p◖l).
40 lemma lift_path_d_dx (f) (p) (k):
41 (🠡[f]p)◖𝗱(🠢[f]p@⧣❨k❩) = 🠡[f](p◖𝗱k).
44 lemma lift_path_m_dx (f) (p):
45 (🠡[f]p)◖𝗺 = 🠡[f](p◖𝗺).
48 lemma lift_path_L_dx (f) (p):
49 (🠡[f]p)◖𝗟 = 🠡[f](p◖𝗟).
52 lemma lift_path_A_dx (f) (p):
53 (🠡[f]p)◖𝗔 = 🠡[f](p◖𝗔).
56 lemma lift_path_S_dx (f) (p):
57 (🠡[f]p)◖𝗦 = 🠡[f](p◖𝗦).
60 (* Constructions with path_append *******************************************)
62 lemma lift_path_append (f) (p) (q):
63 (🠡[f]p)●(🠡[🠢[f]p]q) = 🠡[f](p●q).
66 <lift_path_rcons <lift_path_rcons
67 <list_append_lcons_sn //
70 (* Constructions with path_lcons ********************************************)
72 lemma lift_path_lcons (f) (p) (l):
73 (🠡[f]l)◗🠡[🠢[f]l]p = 🠡[f](l◗p).
78 lemma lift_path_d_sn (f) (p) (k:pnat):
79 (𝗱(f@⧣❨k❩)◗🠡[⇂*[k]f]p) = 🠡[f](𝗱k◗p).
82 lemma lift_path_m_sn (f) (p):
83 (𝗺◗🠡[f]p) = 🠡[f](𝗺◗p).
86 lemma lift_path_L_sn (f) (p):
87 (𝗟◗🠡[⫯f]p) = 🠡[f](𝗟◗p).
90 lemma lift_path_A_sn (f) (p):
91 (𝗔◗🠡[f]p) = 🠡[f](𝗔◗p).
94 lemma lift_path_S_sn (f) (p):
95 (𝗦◗🠡[f]p) = 🠡[f](𝗦◗p).
98 (* Basic inversions *********************************************************)
100 lemma lift_path_inv_empty (f) (p):
103 <lift_path_rcons #H0 destruct
106 lemma lift_path_inv_rcons (f) (p2) (q1) (l1):
108 ∃∃q2,l2. q1 = 🠡[f]q2 & l1 = 🠡[🠢[f]q2]l2 & q2◖l2 = p2.
109 #f * [| #l2 #q2 ] #q1 #l1
114 /2 width=5 by ex3_2_intro/
117 (* Inversions with path_append **********************************************)
119 lemma lift_path_inv_append_sn (f) (q1) (r1) (p2):
121 ∃∃q2,r2. q1 = 🠡[f]q2 & r1 = 🠡[🠢[f]q2]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/
132 (* Main inversions **********************************************************)
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 //