]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
37a2b26186e814e70e9fb5e966bd7294dcfaf013
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_closed.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/syntax/path.ma".
16 include "delayed_updating/notation/functions/class_c_2.ma".
17 include "ground/arith/nat_plus.ma".
18 include "ground/arith/nat_pred_succ.ma".
19 include "ground/lib/subset.ma".
20 include "ground/lib/bool_and.ma".
21 include "ground/generated/insert_eq_1.ma".
22
23 (* CLOSED CONDITION FOR PATH ************************************************)
24
25 inductive pcc (o): relation2 nat path ≝
26 | pcc_empty:
27   pcc o (𝟎) (𝐞)
28 | pcc_d_dx (p) (n) (k):
29   (Ⓣ = o → n = ↑↓n) →
30   pcc o (n+ninj k) p → pcc o n (p◖𝗱k)
31 | pcc_m_dx (p) (n):
32   pcc o n p → pcc o n (p◖𝗺)
33 | pcc_L_dx (p) (n):
34   pcc o n p → pcc o (↑n) (p◖𝗟)
35 | pcc_A_dx (p) (n):
36   pcc o n p → pcc o n (p◖𝗔)
37 | pcc_S_dx (p) (n):
38   pcc o n p → pcc o n (p◖𝗦)
39 .
40
41 interpretation
42   "closed condition (path)"
43   'ClassC o n = (pcc o n).
44
45 (* Advanced constructions ***************************************************)
46
47 lemma pcc_false_d_dx (p) (n) (k:pnat):
48       p ϵ 𝐂❨Ⓕ,n+k❩ → p◖𝗱k ϵ 𝐂❨Ⓕ,n❩.
49 #p #n #k #H0
50 @pcc_d_dx [| // ]
51 #H0 destruct
52 qed.
53
54 lemma pcc_true_d_dx (p) (n:pnat) (k:pnat):
55       p ϵ 𝐂❨Ⓣ,n+k❩ → p◖𝗱k ϵ 𝐂❨Ⓣ,n❩.
56 /2 width=1 by pcc_d_dx/
57 qed.
58
59 (* Basic inversions ********************************************************)
60
61 lemma pcc_inv_empty (o) (n):
62       (𝐞) ϵ 𝐂❨o,n❩ → 𝟎 = n.
63 #o #n @(insert_eq_1 … (𝐞))
64 #x * -n //
65 #p #n [ #k #_ ] #_ #H0 destruct
66 qed-.
67
68 (**) (* alias *)
69 alias symbol "DownArrow" (instance 4) = "predecessor (non-negative integers)".
70 alias symbol "UpArrow" (instance 3) = "successor (non-negative integers)".
71 alias symbol "and" (instance 1) = "logical and".
72
73 lemma pcc_inv_d_dx (o) (p) (n) (k):
74       p◖𝗱k ϵ 𝐂❨o, n❩ →
75       ∧∧ (Ⓣ = o → n = ↑↓n)
76        & p ϵ 𝐂❨o, n+k❩.
77 #o #p #n #h @(insert_eq_1 … (p◖𝗱h))
78 #x * -x -n
79 [|*: #x #n [ #k #Ho ] #Hx ] #H0 destruct
80 /3 width=1 by conj/
81 qed-.
82
83 lemma pcc_inv_m_dx (o) (p) (n):
84       p◖𝗺 ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n❩.
85 #o #p #n @(insert_eq_1 … (p◖𝗺))
86 #x * -x -n
87 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
88 qed-.
89
90 lemma pcc_inv_L_dx (o) (p) (n):
91       p◖𝗟 ϵ 𝐂❨o,n❩ →
92       ∧∧ p ϵ 𝐂❨o,↓n❩ & n = ↑↓n.
93 #o #p #n @(insert_eq_1 … (p◖𝗟))
94 #x * -x -n
95 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct
96 <npred_succ /2 width=1 by conj/
97 qed-.
98
99 lemma pcc_inv_A_dx (o) (p) (n):
100       p◖𝗔 ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n❩.
101 #o #p #n @(insert_eq_1 … (p◖𝗔))
102 #x * -x -n
103 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
104 qed-.
105
106 lemma pcc_inv_S_dx (o) (p) (n):
107       p◖𝗦 ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n❩.
108 #o #p #n @(insert_eq_1 … (p◖𝗦))
109 #x * -x -n
110 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
111 qed-.
112
113 (* Advanced destructions ****************************************************)
114
115 lemma pcc_des_d_dx (o) (p) (n) (k):
116       p◖𝗱k ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n+k❩.
117 #o #p #n #k #H0
118 elim (pcc_inv_d_dx … H0) -H0 #H1 #H2 //
119 qed-.
120
121 lemma pcc_des_gen (o) (p) (n):
122       p ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨Ⓕ,n❩.
123 #o #p #n #H0 elim H0 -p -n //
124 #p #n [ #k #Ho ] #_ #IH
125 /2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx, pcc_false_d_dx/
126 qed-.
127
128 (* Advanced inversions ******************************************************)
129
130 lemma pcc_inv_empty_succ (o) (n):
131       (𝐞) ϵ 𝐂❨o,↑n❩ → ⊥.
132 #o #n #H0
133 lapply (pcc_inv_empty … H0) -H0 #H0
134 /2 width=7 by eq_inv_zero_nsucc/
135 qed-.
136
137 lemma pcc_true_inv_d_dx_zero (p) (k):
138       p◖𝗱k ϵ 𝐂❨Ⓣ,𝟎❩ → ⊥.
139 #p #k #H0
140 elim (pcc_inv_d_dx … H0) -H0 #H0 #_
141 elim (eq_inv_zero_nsucc … (H0 ?)) -H0 //
142 qed-.
143
144 lemma pcc_inv_L_dx_zero (o) (p):
145       p◖𝗟 ϵ 𝐂❨o,𝟎❩ → ⊥.
146 #o #p #H0
147 elim (pcc_inv_L_dx … H0) -H0 #_ #H0
148 /2 width=7 by eq_inv_zero_nsucc/
149 qed-.
150
151 lemma pcc_inv_L_dx_succ (o) (p) (n):
152       p◖𝗟 ϵ 𝐂❨o,↑n❩ → p ϵ 𝐂❨o,n❩.
153 #o #p #n #H0
154 elim (pcc_inv_L_dx … H0) -H0 //
155 qed-.
156
157 (* Constructions with land **************************************************)
158
159 lemma pcc_land_dx (o1) (o2) (p) (n):
160       p ϵ 𝐂❨o1,n❩ → p ϵ 𝐂❨o1∧o2,n❩.
161 #o1 * /2 width=2 by pcc_des_gen/
162 qed.
163
164 lemma pcc_land_sn (o1) (o2) (p) (n):
165       p ϵ 𝐂❨o2,n❩ → p ϵ 𝐂❨o1∧o2,n❩.
166 * /2 width=2 by pcc_des_gen/
167 qed.
168
169 (* Main constructions with path_append **************************************)
170
171 theorem pcc_append_bi (o1) (o2) (p) (q) (m) (n):
172         p ϵ 𝐂❨o1,m❩ → q ϵ 𝐂❨o2,n❩ → p●q ϵ 𝐂❨o1∧o2,m+n❩.
173 #o1 #o2 #p #q #m #n #Hm #Hn elim Hn -q -n
174 /2 width=1 by pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_land_dx/
175 #q #n [ #k #Ho2 ] #_ #IH
176 [ @pcc_d_dx // #H0
177   elim (andb_inv_true_sn … H0) -H0 #_ #H0 >Ho2 //
178   <nplus_succ_dx <npred_succ //
179 | <nplus_succ_dx /2 width=1 by pcc_L_dx/
180 ]
181 qed.
182
183 (* Constructions with path_lcons ********************************************)
184
185 lemma pcc_m_sn (o) (q) (n):
186       q ϵ 𝐂❨o,n❩ → (𝗺◗q) ϵ 𝐂❨o,n❩.
187 #o #q #n #Hq
188 lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗺) … Hq) -Hq
189 /2 width=3 by pcc_m_dx/
190 qed.
191
192 lemma pcc_L_sn (o) (q) (n):
193       q ϵ 𝐂❨o,n❩ → (𝗟◗q) ϵ 𝐂❨o,↑n❩.
194 #o #q #n #Hq
195 lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗟) … Hq) -Hq
196 /2 width=3 by pcc_L_dx/
197 qed.
198
199 lemma pcc_A_sn (o) (q) (n):
200       q ϵ 𝐂❨o,n❩ → (𝗔◗q) ϵ 𝐂❨o,n❩.
201 #o #q #n #Hq
202 lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗔) … Hq) -Hq
203 /2 width=3 by pcc_A_dx/
204 qed.
205
206 lemma pcc_S_sn (o) (q) (n):
207       q ϵ 𝐂❨o,n❩ → (𝗦◗q) ϵ 𝐂❨o,n❩.
208 #o #q #n #Hq
209 lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗦) … Hq) -Hq
210 /2 width=3 by pcc_S_dx/
211 qed.
212
213 (* Main inversions **********************************************************)
214
215 theorem pcc_mono (o1) (o2) (q) (n1):
216         q ϵ 𝐂❨o1,n1❩ → ∀n2. q ϵ 𝐂❨o2,n2❩ → n1 = n2.
217 #o1 #o2 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
218 [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] #n2 #Hn2
219 [ <(pcc_inv_empty … Hn2) -n2 //
220 | lapply (pcc_des_d_dx … Hn2) -Hn2 #Hn2
221   lapply (IH … Hn2) -q1 #H0
222   /2 width=2 by eq_inv_nplus_bi_dx/
223 | lapply (pcc_inv_m_dx … Hn2) -Hn2 #Hn2
224   <(IH … Hn2) -q1 -n2 //
225 | elim (pcc_inv_L_dx … Hn2) -Hn2 #Hn2 #H0
226   >(IH … Hn2) -q1 //
227 | lapply (pcc_inv_A_dx … Hn2) -Hn2 #Hn2
228   <(IH … Hn2) -q1 -n2 //
229 | lapply (pcc_inv_S_dx … Hn2) -Hn2 #Hn2
230   <(IH … Hn2) -q1 -n2 //
231 ]
232 qed-.
233
234 theorem pcc_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n):
235         q1 ϵ 𝐂❨o1,n❩ → ∀q2. q2 ϵ 𝐂❨o2,n❩ →
236         p1●𝗟◗q1 = p2●𝗟◗q2 → q1 = q2.
237 #o1 #o2 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
238 [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] * //
239 [1,3,5,7,9,11: #l2 #q2 ] #Hq2
240 <list_append_lcons_sn <list_append_lcons_sn #H0
241 elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
242 [ elim (pcc_inv_L_dx_zero … Hq2)
243 | lapply (pcc_des_d_dx … Hq2) -Hq2 #Hq2
244   <(IH … Hq2) //
245 | lapply (pcc_inv_m_dx … Hq2) -Hq2 #Hq2
246   <(IH … Hq2) //
247 | lapply (pcc_inv_L_dx_succ … Hq2) -Hq2 #Hq2
248   <(IH … Hq2) //
249 | lapply (pcc_inv_A_dx … Hq2) -Hq2 #Hq2
250   <(IH … Hq2) //
251 | lapply (pcc_inv_S_dx … Hq2) -Hq2 #Hq2
252   <(IH … Hq2) //
253 | elim (pcc_inv_empty_succ … Hq2)
254 ]
255 qed-.
256
257 theorem pcc_inv_L_sn (o) (q) (n) (m):
258         (𝗟◗q) ϵ 𝐂❨o,n❩ → q ϵ 𝐂❨o,m❩ →
259         ∧∧ ↓n = m & n = ↑↓n.
260 #o #q #n #m #H1q #H2q
261 lapply (pcc_L_sn … H2q) -H2q #H2q
262 <(pcc_mono … H2q … H1q) -q -n
263 /2 width=1 by conj/
264 qed-.