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".
17 include "ground/xoa/ex_3_2.ma".
19 (* LIFT FOR PATH ************************************************************)
21 rec definition lift_path (f) (p) on p: path ≝
24 | list_lcons l q ⇒ (lift_path f q)◖↑[↑[q]f]l
29 'UpArrow f l = (lift_path f l).
31 (* Basic constructions ******************************************************)
33 lemma lift_path_empty (f):
37 lemma lift_path_rcons (f) (p) (l):
38 (↑[f]p)◖↑[↑[p]f]l = ↑[f](p◖l).
41 lemma lift_path_d_dx (f) (p) (k):
42 (↑[f]p)◖𝗱((↑[p]f)@⧣❨k❩) = ↑[f](p◖𝗱k).
45 lemma lift_path_m_dx (f) (p):
46 (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
49 lemma lift_path_L_dx (f) (p):
50 (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
53 lemma lift_path_A_dx (f) (p):
54 (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
57 lemma lift_path_S_dx (f) (p):
58 (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
61 (* Constructions with path_append *******************************************)
63 lemma lift_path_append (f) (p) (q):
64 (↑[f]p)●(↑[↑[p]f]q) = ↑[f](p●q).
67 <lift_path_rcons <lift_path_rcons
68 <list_append_lcons_sn //
71 (* Constructions with path_lcons ********************************************)
73 lemma lift_path_lcons (f) (p) (l):
74 (↑[f]l)◗↑[↑[l]f]p = ↑[f](l◗p).
79 lemma lift_path_d_sn (f) (p) (k:pnat):
80 (𝗱(f@⧣❨k❩)◗↑[⇂*[k]f]p) = ↑[f](𝗱k◗p).
83 lemma lift_path_m_sn (f) (p):
84 (𝗺◗↑[f]p) = ↑[f](𝗺◗p).
87 lemma lift_path_L_sn (f) (p):
88 (𝗟◗↑[⫯f]p) = ↑[f](𝗟◗p).
91 lemma lift_path_A_sn (f) (p):
92 (𝗔◗↑[f]p) = ↑[f](𝗔◗p).
95 lemma lift_path_S_sn (f) (p):
96 (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
99 (* Basic inversions *********************************************************)
101 lemma lift_path_inv_empty (f) (p):
104 <lift_path_rcons #H0 destruct
107 lemma lift_path_inv_rcons (f) (p2) (q1) (l1):
109 ∃∃q2,l2. q1 = ↑[f]q2 & l1 = ↑[↑[q2]f]l2 & q2◖l2 = p2.
110 #f * [| #l2 #q2 ] #q1 #l1
115 /2 width=5 by ex3_2_intro/
118 (* Inversions with path_append **********************************************)
120 lemma lift_path_inv_append_sn (f) (q1) (r1) (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/
133 (* Main inversions **********************************************************)
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 //