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/lift_eq.ma".
16 include "delayed_updating/syntax/path_structure.ma".
17 include "delayed_updating/syntax/path_proper.ma".
18 include "ground/xoa/ex_4_2.ma".
19 include "ground/xoa/ex_3_2.ma".
21 (* LIFT FOR PATH ***********************************************************)
23 (* Basic constructions with structure **************************************)
25 lemma structure_lift (p) (f):
27 #p @(path_ind_lift … p) -p // #p #IH #f
31 lemma lift_structure (p) (f):
33 #p @(path_ind_lift … p) -p //
36 (* Destructions with structure **********************************************)
38 lemma lift_des_structure (q) (p) (f):
42 (* Constructions with proper condition for path *****************************)
44 lemma lift_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
45 (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
46 #p2 #p1 @(path_ind_lift … p1) -p1 //
47 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
48 [ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
49 | <lift_path_d_lcons_sn <IH //
50 | <lift_path_m_sn <IH //
51 | <lift_path_L_sn <IH //
52 | <lift_path_A_sn <IH //
53 | <lift_path_S_sn <IH //
57 (* Advanced constructions with structure ************************************)
59 lemma lift_d_empty_dx (n) (p) (f):
60 (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
61 #n #p #f <lift_append_proper_dx //
64 lemma lift_m_dx (p) (f):
66 #p #f <lift_append_proper_dx //
69 lemma lift_L_dx (p) (f):
71 #p #f <lift_append_proper_dx //
74 lemma lift_A_dx (p) (f):
76 #p #f <lift_append_proper_dx //
79 lemma lift_S_dx (p) (f):
81 #p #f <lift_append_proper_dx //
84 lemma lift_root (f) (p):
85 ∃∃r. 𝐞 = ⊗r & ⊗p●r = ↑[f]p.
86 #f #p @(list_ind_rcons … p) -p
87 [ /2 width=3 by ex2_intro/
88 | #p * [ #n ] /2 width=3 by ex2_intro/
92 (* Advanced inversions with proj_path ***************************************)
94 lemma lift_path_inv_d_sn (k) (q) (p) (f):
96 ∃∃r,h. 𝐞 = ⊗r & (↑[r]f)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
97 #k #q #p @(path_ind_lift … p) -p
98 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
99 [ <lift_path_empty #H destruct
100 | <lift_path_d_empty_sn #H destruct -IH
101 /2 width=5 by ex4_2_intro/
102 | <lift_path_d_lcons_sn #H
103 elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
104 /2 width=5 by ex4_2_intro/
106 elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
107 /2 width=5 by ex4_2_intro/
108 | <lift_path_L_sn #H destruct
109 | <lift_path_A_sn #H destruct
110 | <lift_path_S_sn #H destruct
114 lemma lift_path_inv_m_sn (q) (p) (f):
116 #q #p @(path_ind_lift … p) -p
117 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
118 [ <lift_path_empty #H destruct
119 | <lift_path_d_empty_sn #H destruct
120 | <lift_path_d_lcons_sn #H /2 width=2 by/
121 | <lift_path_m_sn #H /2 width=2 by/
122 | <lift_path_L_sn #H destruct
123 | <lift_path_A_sn #H destruct
124 | <lift_path_S_sn #H destruct
128 lemma lift_path_inv_L_sn (q) (p) (f):
130 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[⫯↑[r1]f]r2 & r1●𝗟◗r2 = p.
131 #q #p @(path_ind_lift … p) -p
132 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
133 [ <lift_path_empty #H destruct
134 | <lift_path_d_empty_sn #H destruct
135 | <lift_path_d_lcons_sn #H
136 elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
137 /2 width=5 by ex3_2_intro/
139 elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
140 /2 width=5 by ex3_2_intro/
141 | <lift_path_L_sn #H destruct -IH
142 /2 width=5 by ex3_2_intro/
143 | <lift_path_A_sn #H destruct
144 | <lift_path_S_sn #H destruct
148 lemma lift_path_inv_A_sn (q) (p) (f):
150 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗔◗r2 = p.
151 #q #p @(path_ind_lift … p) -p
152 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
153 [ <lift_path_empty #H destruct
154 | <lift_path_d_empty_sn #H destruct
155 | <lift_path_d_lcons_sn #H
156 elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
157 /2 width=5 by ex3_2_intro/
159 elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
160 /2 width=5 by ex3_2_intro/
161 | <lift_path_L_sn #H destruct
162 | <lift_path_A_sn #H destruct -IH
163 /2 width=5 by ex3_2_intro/
164 | <lift_path_S_sn #H destruct
168 lemma lift_path_inv_S_sn (q) (p) (f):
170 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗦◗r2 = p.
171 #q #p @(path_ind_lift … p) -p
172 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
173 [ <lift_path_empty #H destruct
174 | <lift_path_d_empty_sn #H destruct
175 | <lift_path_d_lcons_sn #H
176 elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
177 /2 width=5 by ex3_2_intro/
179 elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
180 /2 width=5 by ex3_2_intro/| <lift_path_L_sn #H destruct
181 | <lift_path_A_sn #H destruct
182 | <lift_path_S_sn #H destruct -IH
183 /2 width=5 by ex3_2_intro/
187 (* Inversions with proper condition for path ********************************)
189 lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
190 q2 ϵ 𝐏 → q1●q2 = ↑[f]p →
191 ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
193 [ #p #f #Hq2 <list_append_empty_sn #H destruct
194 /2 width=5 by ex3_2_intro/
195 | * [ #n1 ] #q1 #IH #p #f #Hq2 <list_append_lcons_sn #H
196 [ elim (lift_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
197 elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
199 | elim (lift_path_inv_m_sn … H)
200 | elim (lift_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
201 elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
202 @(ex3_2_intro … (r1●𝗟◗p1)) //
203 <structure_append <Hr1 -Hr1 //
204 | elim (lift_path_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
205 elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
206 @(ex3_2_intro … (r1●𝗔◗p1)) //
207 <structure_append <Hr1 -Hr1 //
208 | elim (lift_path_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
209 elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
210 @(ex3_2_intro … (r1●𝗦◗p1)) //
211 <structure_append <Hr1 -Hr1 //