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/unwind/unwind2_path.ma".
16 include "delayed_updating/syntax/path_inner.ma".
17 include "delayed_updating/syntax/path_proper.ma".
18 include "ground/xoa/ex_4_2.ma".
20 (* TAILED UNWIND FOR PATH ***************************************************)
22 (* Constructions with inner condition for path ******************************)
24 lemma unwind2_path_inner (f) (p):
26 #f * // * // #k #q #Hq
27 elim (pic_inv_d_dx … Hq)
30 (* Constructions with append and inner condition for path *******************)
32 lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 →
33 (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
34 #f #p * [ #Hp | * [ #k ] #q #_ ] //
35 [ <(unwind2_path_inner … Hp) -Hp //
36 | <unwind2_path_d_dx <unwind2_path_d_dx
37 /2 width=3 by trans_eq/
38 | <unwind2_path_L_dx <unwind2_path_L_dx //
39 | <unwind2_path_A_dx <unwind2_path_A_dx //
40 | <unwind2_path_S_dx <unwind2_path_S_dx //
44 (* Constructions with append and proper condition for path ******************)
46 lemma unwind2_path_append_proper_dx (f) (p) (q): q ϵ 𝐏 →
47 (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
48 #f #p * [ #Hq | * [ #k ] #q #_ ] //
49 [ elim (ppc_inv_empty … Hq)
50 | <unwind2_path_d_dx <unwind2_path_d_dx
51 /2 width=3 by trans_eq/
52 | <unwind2_path_L_dx <unwind2_path_L_dx //
53 | <unwind2_path_A_dx <unwind2_path_A_dx //
54 | <unwind2_path_S_dx <unwind2_path_S_dx //
58 (* Constructions with path_lcons ********************************************)
60 lemma unwind2_path_d_empty (f) (k):
61 (𝗱(f@⧣❨k❩)◗𝐞) = ▼[f](𝗱k◗𝐞).
64 lemma unwind2_path_d_lcons (f) (p) (l) (k:pnat):
65 ▼[f∘𝐮❨k❩](l◗p) = ▼[f](𝗱k◗l◗p).
66 #f #p #l #k <unwind2_path_append_proper_dx in ⊢ (???%); //
69 lemma unwind2_path_m_sn (f) (p):
71 #f #p <unwind2_path_append_inner_sn //
74 lemma unwind2_path_L_sn (f) (p):
75 (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
76 #f #p <unwind2_path_append_inner_sn //
79 lemma unwind2_path_A_sn (f) (p):
80 (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
81 #f #p <unwind2_path_append_inner_sn //
84 lemma unwind2_path_S_sn (f) (p):
85 (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
86 #f #p <unwind2_path_append_inner_sn //
89 (* Destructions with inner condition for path *******************************)
91 lemma unwind2_path_des_inner (f) (p):
93 #f * // * [ #k ] #p //
94 <unwind2_path_d_dx #H0
95 elim (pic_inv_d_dx … H0)
98 (* Destructions with append and inner condition for path ********************)
100 lemma unwind2_path_des_append_inner_sn (f) (p) (q1) (q2):
101 q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
102 ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
103 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
104 [ <list_append_empty_sn #H0 destruct
105 lapply (unwind2_path_des_inner … Hq1) -Hq1 #Hp
106 <(unwind2_path_inner … Hp) -Hp
107 /2 width=5 by ex3_2_intro/
108 | #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
109 elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
110 /2 width=5 by ex3_2_intro/
111 | #H0 elim (eq_inv_m_dx_unwind2_path … H0)
112 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
113 elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
114 @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
115 <unwind2_path_append_proper_dx //
116 <unwind2_path_L_sn <Hr2 -Hr2 //
117 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
118 elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
119 @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
120 <unwind2_path_append_proper_dx //
121 <unwind2_path_A_sn <Hr2 -Hr2 //
122 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
123 elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
124 @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
125 <unwind2_path_append_proper_dx //
126 <unwind2_path_S_sn <Hr2 -Hr2 //
130 (* Inversions with append and proper condition for path *********************)
132 lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
133 q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
134 ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
135 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
136 [ <list_append_empty_sn #H0 destruct
137 elim (ppc_inv_empty … Hq1)
138 | #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
139 elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
140 /2 width=5 by ex3_2_intro/
141 | #H0 elim (eq_inv_m_dx_unwind2_path … H0)
142 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
143 elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
144 @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
145 <unwind2_path_append_proper_dx //
146 <unwind2_path_L_sn <Hr2 -Hr2 //
147 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
148 elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
149 @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
150 <unwind2_path_append_proper_dx //
151 <unwind2_path_A_sn <Hr2 -Hr2 //
152 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
153 elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
154 @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
155 <unwind2_path_append_proper_dx //
156 <unwind2_path_S_sn <Hr2 -Hr2 //
160 (* Inversions with path_lcons ***********************************************)
162 lemma eq_inv_d_sn_unwind2_path (f) (q) (p) (k):
164 ∃∃r,h. 𝐞 = ⊗r & ▶[f]r@⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
165 #f * [| #l #q ] #p #k
166 [ <list_cons_comm #H0
167 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
168 /2 width=5 by ex4_2_intro/
169 | >list_cons_comm #H0
170 elim (unwind2_path_inv_append_proper_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
171 elim (eq_inv_d_dx_structure … Hr1)
175 lemma eq_inv_m_sn_unwind2_path (f) (q) (p):
179 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
180 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
181 elim (eq_inv_m_dx_structure … Hr1)
184 lemma eq_inv_L_sn_unwind2_path (f) (q) (p):
186 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▶[f]r1]r2 & r1●𝗟◗r2 = p.
189 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
190 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
191 elim (eq_inv_L_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
192 <list_append_assoc in H0; <list_append_assoc
193 <unwind2_path_append_proper_dx //
194 <unwind2_path_L_sn <H1 <list_append_empty_dx #H0
195 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
196 /2 width=5 by ex3_2_intro/
199 lemma eq_inv_A_sn_unwind2_path (f) (q) (p):
201 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗔◗r2 = p.
204 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
205 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
206 elim (eq_inv_A_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
207 <list_append_assoc in H0; <list_append_assoc
208 <unwind2_path_append_proper_dx //
209 <unwind2_path_A_sn <H1 <list_append_empty_dx #H0
210 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
211 /2 width=5 by ex3_2_intro/
214 lemma eq_inv_S_sn_unwind2_path (f) (q) (p):
216 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗦◗r2 = p.
219 elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
220 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
221 elim (eq_inv_S_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
222 <list_append_assoc in H0; <list_append_assoc
223 <unwind2_path_append_proper_dx //
224 <unwind2_path_S_sn <H1 <list_append_empty_dx #H0
225 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
226 /2 width=5 by ex3_2_intro/
229 (* Advanced eliminations with path ******************************************)
231 lemma path_ind_unwind (Q:predicate …):
233 (∀k. Q (𝐞) → Q (𝗱k◗𝐞)) →
234 (∀k,l,p. Q (l◗p) → Q (𝗱k◗l◗p)) →
235 (∀p. Q p → Q (𝗺◗p)) →
236 (∀p. Q p → Q (𝗟◗p)) →
237 (∀p. Q p → Q (𝗔◗p)) →
238 (∀p. Q p → Q (𝗦◗p)) →
240 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
241 @(list_ind_rcons … p) -p // #p * [ #k ]
242 [ @(list_ind_rcons … p) -p ]