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/syntax/path.ma".
16 include "delayed_updating/notation/functions/circled_times_1.ma".
17 include "ground/xoa/ex_3_2.ma".
19 (* STRUCTURE FOR PATH *******************************************************)
21 rec definition structure (p) on p ≝
26 [ label_d k ⇒ structure q
27 | label_m ⇒ structure q
28 | label_L ⇒ (structure q)◖𝗟
29 | label_A ⇒ (structure q)◖𝗔
30 | label_S ⇒ (structure q)◖𝗦
36 'CircledTimes p = (structure p).
38 (* Basic constructions ******************************************************)
40 lemma structure_empty:
44 lemma structure_d_dx (p) (k):
48 lemma structure_m_dx (p):
52 lemma structure_L_dx (p):
56 lemma structure_A_dx (p):
60 lemma structure_S_dx (p):
64 (* Main constructions *******************************************************)
66 theorem structure_idem (p):
68 #p elim p -p [| * [ #k ] #p #IH ] //
71 theorem structure_append (p) (q):
73 #p #q elim q -q [| * [ #k ] #q #IH ]
74 [||*: <list_append_lcons_sn ] //
77 (* Constructions with path_lcons ********************************************)
79 lemma structure_d_sn (p) (k):
81 #p #n <structure_append //
84 lemma structure_m_sn (p):
86 #p <structure_append //
89 lemma structure_L_sn (p):
91 #p <structure_append //
94 lemma structure_A_sn (p):
96 #p <structure_append //
99 lemma structure_S_sn (p):
101 #p <structure_append //
104 (* Basic inversions *********************************************************)
106 lemma eq_inv_d_dx_structure (h) (q) (p):
108 #h #q #p elim p -p [| * [ #k ] #p #IH ]
109 [ <structure_empty #H0 destruct
110 | <structure_d_dx #H0 /2 width=1 by/
111 | <structure_m_dx #H0 /2 width=1 by/
112 | <structure_L_dx #H0 destruct
113 | <structure_A_dx #H0 destruct
114 | <structure_S_dx #H0 destruct
118 lemma eq_inv_m_dx_structure (q) (p):
120 #q #p elim p -p [| * [ #k ] #p #IH ]
121 [ <structure_empty #H0 destruct
122 | <structure_d_dx #H0 /2 width=1 by/
123 | <structure_m_dx #H0 /2 width=1 by/
124 | <structure_L_dx #H0 destruct
125 | <structure_A_dx #H0 destruct
126 | <structure_S_dx #H0 destruct
130 lemma eq_inv_L_dx_structure (q) (p):
132 ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
133 #q #p elim p -p [| * [ #k ] #p #IH ]
134 [ <structure_empty #H0 destruct
135 | <structure_d_dx #H0
136 elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
137 /2 width=5 by ex3_2_intro/
138 | <structure_m_dx #H0
139 elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
140 /2 width=5 by ex3_2_intro/
141 | <structure_L_dx #H0 destruct -IH
142 /2 width=5 by ex3_2_intro/
143 | <structure_A_dx #H0 destruct
144 | <structure_S_dx #H0 destruct
148 lemma eq_inv_A_dx_structure (q) (p):
150 ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.
151 #q #p elim p -p [| * [ #k ] #p #IH ]
152 [ <structure_empty #H0 destruct
153 | <structure_d_dx #H0
154 elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
155 /2 width=5 by ex3_2_intro/
156 | <structure_m_dx #H0
157 elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
158 /2 width=5 by ex3_2_intro/
159 | <structure_L_dx #H0 destruct
160 | <structure_A_dx #H0 destruct -IH
161 /2 width=5 by ex3_2_intro/
162 | <structure_S_dx #H0 destruct
166 lemma eq_inv_S_dx_structure (q) (p):
168 ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.
169 #q #p elim p -p [| * [ #k ] #p #IH ]
170 [ <structure_empty #H0 destruct
171 | <structure_d_dx #H0
172 elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
173 /2 width=5 by ex3_2_intro/
174 | <structure_m_dx #H0
175 elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
176 /2 width=5 by ex3_2_intro/
177 | <structure_L_dx #H0 destruct
178 | <structure_A_dx #H0 destruct
179 | <structure_S_dx #H0 destruct -IH
180 /2 width=5 by ex3_2_intro/
184 (* Main inversions **********************************************************)
186 theorem eq_inv_append_structure (p) (q) (r):
188 ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.
189 #p #q elim q -q [| * [ #k ] #q #IH ] #r
190 [ <list_append_empty_sn #H0 destruct
191 /2 width=5 by ex3_2_intro/
192 | #H0 elim (eq_inv_d_dx_structure … H0)
193 | #H0 elim (eq_inv_m_dx_structure … H0)
194 | #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
195 elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
196 @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
197 <structure_append <structure_L_sn <Hr2 -Hr2 //
198 | #H0 elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
199 elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
200 @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
201 <structure_append <structure_A_sn <Hr2 -Hr2 //
202 | #H0 elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
203 elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
204 @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
205 <structure_append <structure_S_sn <Hr2 -Hr2 //
209 (* Inversions with path_lcons ***********************************************)
211 lemma eq_inv_d_sn_structure (h) (q) (p):
213 #h #q #p >list_cons_comm #H0
214 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
215 <list_cons_comm #H0 #H1 #H2 destruct
216 elim (eq_inv_d_dx_structure … H0)
219 lemma eq_inv_m_sn_structure (q) (p):
221 #q #p >list_cons_comm #H0
222 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
223 <list_cons_comm #H0 #H1 #H2 destruct
224 elim (eq_inv_m_dx_structure … H0)
227 lemma eq_inv_L_sn_structure (q) (p):
229 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗟◗r2 = p.
230 #q #p >list_cons_comm #H0
231 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
232 <list_cons_comm #H0 #H1 #H2 destruct
233 elim (eq_inv_L_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
234 @(ex3_2_intro … s1 (s2●r2)) // -s1
235 <structure_append <H2 -s2 //
238 lemma eq_inv_A_sn_structure (q) (p):
240 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗔◗r2 = p.
241 #q #p >list_cons_comm #H0
242 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
243 <list_cons_comm #H0 #H1 #H2 destruct
244 elim (eq_inv_A_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
245 @(ex3_2_intro … s1 (s2●r2)) // -s1
246 <structure_append <H2 -s2 //
249 lemma eq_inv_S_sn_structure (q) (p):
251 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗦◗r2 = p.
252 #q #p >list_cons_comm #H0
253 elim (eq_inv_append_structure … H0) -H0 #r1 #r2
254 <list_cons_comm #H0 #H1 #H2 destruct
255 elim (eq_inv_S_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
256 @(ex3_2_intro … s1 (s2●r2)) // -s1
257 <structure_append <H2 -s2 //