]> matita.cs.unibo.it Git - helm.git/blob - unwind_gen_structure.ma
5c92a9af5a364189d99d17b24a6cc7554b6c6710
[helm.git] / unwind_gen_structure.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/unwind/unwind_gen.ma".
16 include "delayed_updating/syntax/path_structure.ma".
17 include "delayed_updating/syntax/path_inner.ma".
18 include "delayed_updating/syntax/path_proper.ma".
19 include "ground/xoa/ex_4_2.ma".
20 include "ground/xoa/ex_3_2.ma".
21
22 (* GENERIC UNWIND FOR PATH **************************************************)
23
24 (* Basic constructions with structure ***************************************)
25
26 lemma structure_unwind_gen (p) (f):
27       ⊗p = ⊗◆[f]p.
28 #p @(path_ind_unwind … p) -p //
29 qed.
30
31 lemma unwind_gen_structure (p) (f):
32       ⊗p = ◆[f]⊗p.
33 #p @(path_ind_unwind … p) -p //
34 qed.
35
36 (* Destructions with structure **********************************************)
37
38 lemma unwind_gen_des_structure (q) (p) (f):
39       ⊗q = ◆[f]p → ⊗q = ⊗p.
40 // qed-.
41
42 (* Constructions with proper condition for path *****************************)
43
44 lemma unwind_gen_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
45       (⊗p1)●(◆[f]p2) = ◆[f](p1●p2).
46 #p2 #p1 @(path_ind_unwind … p1) -p1 //
47 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
48 [ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H0 destruct //
49 | <unwind_gen_d_lcons <IH //
50 | <unwind_gen_m_sn <IH //
51 | <unwind_gen_L_sn <IH //
52 | <unwind_gen_A_sn <IH //
53 | <unwind_gen_S_sn <IH //
54 ]
55 qed-.
56
57 (* Constructions with inner condition for path ******************************)
58
59 lemma unwind_gen_append_inner_sn (p1) (p2) (f): p1 ϵ 𝐈 →
60       (⊗p1)●(◆[f]p2) = ◆[f](p1●p2).
61 #p1 @(list_ind_rcons … p1) -p1 //
62 #p1 * [ #n ] #_ #p2 #f #Hp1
63 [ elim (pic_inv_d_dx … Hp1)
64 | <list_append_rcons_sn <unwind_gen_append_proper_dx //
65 | <list_append_rcons_sn <unwind_gen_append_proper_dx //
66   <structure_L_dx <list_append_rcons_sn //
67 | <list_append_rcons_sn <unwind_gen_append_proper_dx //
68   <structure_A_dx <list_append_rcons_sn //
69 | <list_append_rcons_sn <unwind_gen_append_proper_dx //
70   <structure_S_dx <list_append_rcons_sn //
71 ]
72 qed-.
73
74 (* Advanced constructions with list_rcons ***********************************)
75
76 lemma unwind_gen_d_dx (f) (p) (n):
77       (⊗p)◖𝗱(f@⧣❨n❩) = ◆[f](p◖𝗱n).
78 #f #p #n <unwind_gen_append_proper_dx //
79 qed.
80
81 lemma unwind_gen_m_dx (f) (p):
82       ⊗p = ◆[f](p◖𝗺).
83 #f #p <unwind_gen_append_proper_dx //
84 qed.
85
86 lemma unwind_gen_L_dx (f) (p):
87       (⊗p)◖𝗟 = ◆[f](p◖𝗟).
88 #f #p <unwind_gen_append_proper_dx //
89 qed.
90
91 lemma unwind_gen_A_dx (f) (p):
92       (⊗p)◖𝗔 = ◆[f](p◖𝗔).
93 #f #p <unwind_gen_append_proper_dx //
94 qed.
95
96 lemma unwind_gen_S_dx (f) (p):
97       (⊗p)◖𝗦 = ◆[f](p◖𝗦).
98 #f #p <unwind_gen_append_proper_dx //
99 qed.
100
101 lemma unwind_gen_root (f) (p):
102       ∃∃r. 𝐞 = ⊗r & ⊗p●r = ◆[f]p.
103 #f #p @(list_ind_rcons … p) -p
104 [ /2 width=3 by ex2_intro/
105 | #p * [ #n ] /2 width=3 by ex2_intro/
106 ]
107 qed-.
108
109 (* Advanced inversions ******************************************************)
110
111 lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
112       (𝗱k◗q) = ◆[f]p →
113       ∃∃r,h. 𝐞 = ⊗r & f@⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
114 #k #q #p @(path_ind_unwind … p) -p
115 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
116 [ <unwind_gen_empty #H destruct
117 | <unwind_gen_d_empty #H destruct -IH
118   /2 width=5 by ex4_2_intro/
119 | <unwind_gen_d_lcons #H
120   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
121   /2 width=5 by ex4_2_intro/
122 | <unwind_gen_m_sn #H
123   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
124   /2 width=5 by ex4_2_intro/
125 | <unwind_gen_L_sn #H destruct
126 | <unwind_gen_A_sn #H destruct
127 | <unwind_gen_S_sn #H destruct
128 ]
129 qed-.
130
131 lemma unwind_gen_inv_m_sn (q) (p) (f):
132       (𝗺◗q) = ◆[f]p → ⊥.
133 #q #p @(path_ind_unwind … p) -p
134 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
135 [ <unwind_gen_empty #H destruct
136 | <unwind_gen_d_empty #H destruct
137 | <unwind_gen_d_lcons #H /2 width=2 by/
138 | <unwind_gen_m_sn #H /2 width=2 by/
139 | <unwind_gen_L_sn #H destruct
140 | <unwind_gen_A_sn #H destruct
141 | <unwind_gen_S_sn #H destruct
142 ]
143 qed-.
144
145 lemma unwind_gen_inv_L_sn (q) (p) (f):
146       (𝗟◗q) = ◆[f]p →
147       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ◆[f]r2 & r1●𝗟◗r2 = p.
148 #q #p @(path_ind_unwind … p) -p
149 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
150 [ <unwind_gen_empty #H destruct
151 | <unwind_gen_d_empty #H destruct
152 | <unwind_gen_d_lcons #H
153   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
154   /2 width=5 by ex3_2_intro/
155 | <unwind_gen_m_sn #H
156   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
157   /2 width=5 by ex3_2_intro/
158 | <unwind_gen_L_sn #H destruct -IH
159   /2 width=5 by ex3_2_intro/
160 | <unwind_gen_A_sn #H destruct
161 | <unwind_gen_S_sn #H destruct
162 ]
163 qed-.
164
165 lemma unwind_gen_inv_A_sn (q) (p) (f):
166       (𝗔◗q) = ◆[f]p →
167       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ◆[f]r2 & r1●𝗔◗r2 = p.
168 #q #p @(path_ind_unwind … p) -p
169 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
170 [ <unwind_gen_empty #H destruct
171 | <unwind_gen_d_empty #H destruct
172 | <unwind_gen_d_lcons #H
173   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
174   /2 width=5 by ex3_2_intro/
175 | <unwind_gen_m_sn #H
176   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
177   /2 width=5 by ex3_2_intro/
178 | <unwind_gen_L_sn #H destruct
179 | <unwind_gen_A_sn #H destruct -IH
180   /2 width=5 by ex3_2_intro/
181 | <unwind_gen_S_sn #H destruct
182 ]
183 qed-.
184
185 lemma unwind_gen_inv_S_sn (q) (p) (f):
186       (𝗦◗q) = ◆[f]p →
187       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ◆[f]r2 & r1●𝗦◗r2 = p.
188 #q #p @(path_ind_unwind … p) -p
189 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
190 [ <unwind_gen_empty #H destruct
191 | <unwind_gen_d_empty #H destruct
192 | <unwind_gen_d_lcons #H
193   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
194   /2 width=5 by ex3_2_intro/
195 | <unwind_gen_m_sn #H
196   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
197   /2 width=5 by ex3_2_intro/| <unwind_gen_L_sn #H destruct
198 | <unwind_gen_A_sn #H destruct
199 | <unwind_gen_S_sn #H destruct -IH
200   /2 width=5 by ex3_2_intro/
201 ]
202 qed-.
203
204 (* Inversions with proper condition for path ********************************)
205
206 lemma unwind_gen_inv_append_proper_dx (q2) (q1) (p) (f):
207       q2 ϵ 𝐏 → q1●q2 = ◆[f]p →
208       ∃∃p1,p2. ⊗p1 = q1 & ◆[f]p2 = q2 & p1●p2 = p.
209 #q2 #q1 elim q1 -q1
210 [ #p #f #Hq2 <list_append_empty_sn #H destruct
211   /2 width=5 by ex3_2_intro/
212 | * [ #n1 ] #q1 #IH #p #f #Hq2 <list_append_lcons_sn #H
213   [ elim (unwind_gen_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
214     elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
215     elim Hq2 -Hq2 //
216   | elim (unwind_gen_inv_m_sn … H)
217   | elim (unwind_gen_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
218     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
219     @(ex3_2_intro … (r1●𝗟◗p1)) //
220     <structure_append <Hr1 -Hr1 //
221   | elim (unwind_gen_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
222     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
223     @(ex3_2_intro … (r1●𝗔◗p1)) //
224     <structure_append <Hr1 -Hr1 //
225   | elim (unwind_gen_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
226     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
227     @(ex3_2_intro … (r1●𝗦◗p1)) //
228     <structure_append <Hr1 -Hr1 //
229   ]
230 ]
231 qed-.
232
233 (* Inversions with inner condition for path *********************************)
234
235 lemma unwind_gen_inv_append_inner_sn (q1) (q2) (p) (f):
236       q1 ϵ 𝐈 → q1●q2 = ◆[f]p →
237       ∃∃p1,p2. ⊗p1 = q1 & ◆[f]p2 = q2 & p1●p2 = p.
238 #q1 @(list_ind_rcons … q1) -q1
239 [ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
240   /2 width=5 by ex3_2_intro/
241 | #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
242   [ elim (pic_inv_d_dx … Hq2)
243   | <list_append_rcons_sn #H0
244     elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
245     elim (unwind_gen_inv_m_sn … (sym_eq … H2))
246   | <list_append_rcons_sn #H0
247     elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
248     elim (unwind_gen_inv_L_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
249     @(ex3_2_intro … (p1●r2◖𝗟)) [1,3: // ]
250     [ <structure_append <structure_L_dx <Hr2 -Hr2 //
251     | <list_append_assoc <list_append_rcons_sn //
252     ]
253   | <list_append_rcons_sn #H0
254     elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
255     elim (unwind_gen_inv_A_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
256     @(ex3_2_intro … (p1●r2◖𝗔)) [1,3: // ]
257     [ <structure_append <structure_A_dx <Hr2 -Hr2 //
258     | <list_append_assoc <list_append_rcons_sn //
259     ]
260   | <list_append_rcons_sn #H0
261     elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
262     elim (unwind_gen_inv_S_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
263     @(ex3_2_intro … (p1●r2◖𝗦)) [1,3: // ]
264     [ <structure_append <structure_S_dx <Hr2 -Hr2 //
265     | <list_append_assoc <list_append_rcons_sn //
266     ]
267   ]
268 ]
269 qed-.