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 "logic/connectives.ma".*)
16 (*include "logic/equality.ma".*)
17 include "datatypes/list.ma".
18 include "datatypes/pairs.ma".
20 (*include "Plogic/equality.ma".*)
22 ndefinition word ≝ λS:Type[0].list S.
24 ninductive re (S: Type[0]) : Type[0] ≝
28 | c: re S → re S → re S
29 | o: re S → re S → re S
33 alias symbol "not" (instance 1) = "Clogical not".
34 nlemma foo1: ∀S. ¬ (z S = e S). #S; @; #H; ndestruct. nqed.
35 nlemma foo2: ∀S,x. ¬ (z S = s S x). #S; #x; @; #H; ndestruct. nqed.
36 nlemma foo3: ∀S,x1,x2. ¬ (z S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
37 nlemma foo4: ∀S,x1,x2. ¬ (z S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
38 nlemma foo5: ∀S,x. ¬ (z S = k S x). #S; #x; @; #H; ndestruct. nqed.
39 nlemma foo6: ∀S,x. ¬ (e S = s S x). #S; #x; @; #H; ndestruct. nqed.
40 nlemma foo7: ∀S,x1,x2. ¬ (e S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
41 nlemma foo8: ∀S,x1,x2. ¬ (e S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
42 nlemma foo9: ∀S,x. ¬ (e S = k S x). #S; #x; @; #H; ndestruct. nqed.
45 ninductive in_l (S: Type[0]): word S → re S → Prop ≝
47 | in_s: ∀x. in_l S [x] (s ? x)
48 | in_c: ∀w1,w2,e1,e2. in_l ? w1 e1 → in_l ? w2 e2 → in_l S (w1@w2) (c ? e1 e2)
49 | in_o1: ∀w,e1,e2. in_l ? w e1 → in_l S w (o ? e1 e2)
50 | in_o2: ∀w,e1,e2. in_l ? w e2 → in_l S w (o ? e1 e2)
51 | in_ke: ∀e. in_l S [] (k ? e)
52 | in_ki: ∀w1,w2,e. in_l ? w1 e → in_l ? w2 (k ? e) → in_l S (w1@w2) (k ? e).
55 ∀S,w. ¬ (in_l S w (z ?)).
56 (* #S; #w; #H; ninversion H
58 | #a; #b; #c; ndestruct
59 | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
60 | #a; #b; #c; #d; #e; #f; #g; ndestruct
61 | #a; #b; #c; #d; #e; #f; #g; ndestruct
62 | #a; #b; #c; ndestruct
63 | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
67 ∀S,w. in_l S w (e ?) → w = [].
68 #S; #w; #H; ninversion H
69 [ #a; #b; ndestruct; //
70 | #a; #b; #c; ndestruct
71 | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
72 | #a; #b; #c; #d; #e; #f; #g; ndestruct
73 | #a; #b; #c; #d; #e; #f; #g; ndestruct
74 | #a; #b; #c; ndestruct
75 | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
79 ∀S,w,x. in_l S w (s ? x) → w = [x].
82 ∀S,w,E1,E2. in_l S w (c S E1 E2) → ∃w1.∃w2. w = w1@w2 ∧ in_l S w1 E1 ∧ in_l S w2 E2.
84 ninductive pre (S: Type[0]) : Type[0] ≝
89 | pc: pre S → pre S → pre S
90 | po: pre S → pre S → pre S
93 nlet rec forget (S: Type[0]) (l : pre S) on l: re S ≝
99 | pc E1 E2 ⇒ c S (forget ? E1) (forget ? E2)
100 | po E1 E2 ⇒ o S (forget ? E1) (forget ? E2)
101 | pk E ⇒ k S (forget ? E) ].
103 ninductive in_pl (S: Type[0]): word S → pre S → Prop ≝
104 in_pp: ∀x. in_pl S [x] (pp S x)
105 | in_pc1: ∀w1,w2,e1,e2. in_pl ? w1 e1 → in_l ? w2 (forget ? e2) →
106 in_pl S (w1@w2) (pc ? e1 e2)
107 | in_pc2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (pc ? e1 e2)
108 | in_po1: ∀w,e1,e2. in_pl ? w e1 → in_pl S w (po ? e1 e2)
109 | in_po2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (po ? e1 e2)
110 | in_pki: ∀w1,w2,e. in_pl ? w1 e → in_l ? w2 (k ? (forget ? e)) →
111 in_pl S (w1@w2) (pk ? e).
113 nlet rec eclose (S: Type[0]) (E: pre S) on E ≝
115 [ pz ⇒ 〈 false, pz ? 〉
116 | pe ⇒ 〈 true, pe ? 〉
117 | ps x ⇒ 〈 false, pp ? x 〉
118 | pp x ⇒ 〈 false, pp ? x 〉
120 let E1' ≝ eclose ? E1 in
121 let E1'' ≝ snd … E1' in
124 let E2' ≝ eclose ? E2 in
125 〈 fst … E2', pc ? E1'' (snd … E2') 〉
126 | false ⇒ 〈 false, pc ? E1'' E2 〉 ]
128 let E1' ≝ eclose ? E1 in
129 let E2' ≝ eclose ? E2 in
130 〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
131 | pk E ⇒ 〈 true, pk ? (snd … (eclose S E)) 〉 ].
133 ntheorem forget_eclose:
134 ∀S,E. forget S (snd … (eclose … E)) = forget ? E.
135 #S; #E; nelim E; nnormalize; //;
136 #p; ncases (fst … (eclose S p)); nnormalize; //.
139 ntheorem eclose_true:
140 ∀S,E. (* bug refiner se si scambia true con il termine *)
141 true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E).
142 #S; #E; nelim E; nnormalize; //
143 [ #H; ncases (?: False); /2/
144 | #x; #H; ncases (?: False); /2/
145 | #x; #H; ncases (?: False); /2/
146 | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
147 #_; #_; #H; ncases (?:False); /2/
148 | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/]
152 nlemma eq_append_nil_to_eq_nil1:
153 ∀A.∀l1,l2:list A. l1 @ l2 = [] → l1 = [].
154 #A; #l1; nelim l1; nnormalize; /2/;
155 #x; #tl; #_; #l3; #K; ndestruct.
159 nlemma eq_append_nil_to_eq_nil2:
160 ∀A.∀l1,l2:list A. l1 @ l2 = [] → l2 = [].
161 #A; #l1; nelim l1; nnormalize; /2/;
162 #x; #tl; #_; #l3; #K; ndestruct.
165 ntheorem in_l_empty_c:
166 ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2.
167 #S; #E1; #E2; #H; ninversion H
170 | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
171 nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
173 | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
174 | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
175 | #E; #_; #K; ndestruct
176 | #w1; #w2; #w3; #H1; #H2; #H3; #H4; #H5; #H6; ndestruct ]
179 ntheorem eclose_true':
180 ∀S,E. (* bug refiner se si scambia true con il termine *)
181 in_l S [] (forget S E) → true = fst bool (pre S) (eclose S E).
182 #S; #E; nelim E; nnormalize; //
183 [ #H; ncases (?:False); /2/
184 |##2,3: #x; #H; ncases (?:False); nlapply (in_l_inv_s ??? H); #K; ndestruct
185 | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
186 [ #H1; #H2; #H3; ninversion H3; /3/;
187 ##| #H1; #H2; #H3; ninversion H3
190 | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
191 napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //
192 | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
193 | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
194 | #E'; #_; #K; ndestruct
195 | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]##]
196 ##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
197 #E2; #H1; #H2; #H3; ninversion H3
199 | #w; #_; #K; ndestruct
200 | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
201 | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
202 ncases (?: False); napply (absurd ?? (not_eq_true_false …));
204 | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; /2/
205 | #a; #b; #c; ndestruct
206 | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct]##]
210 ntheorem eclose_superset:
212 ∀w. in_l S w (forget … E) ∨ in_pl ? w E →
213 let E' ≝ eclose … E in
214 in_pl ? w (snd … E') ∨ fst … E' = true ∧ w = [].
216 [ ngeneralize in match w; nelim E; nnormalize
217 [ #w'; #H; ncases (? : False); /2/
218 ##| #w'; #H; @2; @; //; napply in_l_inv_e; //; (* auto non va *)
219 ##|##3,4: #x; #w'; #H; @1; nrewrite > (in_l_inv_s … H); //;
220 ##| #E1; #E2; #H1; #H2; #w'; #H3;
221 ncases (in_l_inv_c … H3); #w1; *; #w2; *; *; #H4; #H5; #H6;
222 ncases (fst … (eclose S E1)) in H1 H2 ⊢ %; nnormalize
223 [ #H1; #H2; ncases (H1 … H5); ncases (H2 … H6)
224 [ #K1; #K2; nrewrite > H4; /3/;
225 ##| *; #_; #K1; #K2; nrewrite > H4; /3/;
226 ##| #K1; *; #_; #K2; nrewrite > H4; @1; nrewrite > K2;
229 @2; @; //; ninversion H; //;
230 ##| #H; nwhd; @1; (* manca intro per letin*)
231 (* LEMMA A PARTE? *) (* manca clear E' *)
232 nelim H; nnormalize; /2/
233 [ #w1; #w2; #p; ncases (fst … (eclose S p));
235 | #w; #p; ncases (fst … (eclose S p));
240 nrecord decidable : Type[1] ≝
242 eqb: carr → carr → bool;
243 eqb_true: ∀x,y. eqb x y = true → x=y;
244 eqb_false: ∀x,y. eqb x y = false → x≠y
247 nlet rec move (S: decidable) (x:S) (E: pre S) on E ≝
249 [ pz ⇒ 〈 false, pz ? 〉
250 | pe ⇒ 〈 false, pe ? 〉
251 | ps y ⇒ 〈false, ps ? y 〉
252 | pp y ⇒ 〈 eqb … x y, ps ? y 〉
254 let E1' ≝ move ? x E1 in
255 let E2' ≝ move ? x E2 in
256 let E1'' ≝ snd … E1' in
257 let E2'' ≝ snd ?? E2' in
260 let E2''' ≝ eclose S E2'' in
261 〈 fst … E2' ∨ fst … E2''', pc ? E1'' (snd … E2''') 〉
262 | false ⇒ 〈 fst … E2', pc ? E1'' E2'' 〉 ]
264 let E1' ≝ move ? x E1 in
265 let E2' ≝ move ? x E2 in
266 〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
268 let E' ≝ move S x E in
269 let E'' ≝ snd bool (pre S) E' in
271 [ true ⇒ 〈 true, pk ? (snd … (eclose … E'')) 〉
272 | false ⇒ 〈 false, pk ? E'' 〉 ]].
277 in_pl S w (snd … (move S a E)) → in_pl S (a::w) E.
282 nlet rec move_star S w E on w ≝
285 | cons x w' ⇒ move_star S w' (move S x (snd … E))].
287 ndefinition in_moves ≝ λS,w,E. fst … (move_star S w E).
289 ndefinition NAT: decidable.
294 pc ? (pk ? (po ? (ps ? 0) (ps ? 1))) (ps ? 0).
298 (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0))
299 (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 1)).
302 pk ? (pc ? (pc ? (ps ? 0) (pk ? (pc ? (ps ? 0) (ps ? 1)))) (ps ? 1)).
304 nlemma foo: in_moves NAT
305 [0;0;1;0;1;1] (eclose ? test3) = true.
308 (**********************************************************)
310 ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
311 der_z: der S a (z S) (z S)
312 | der_e: der S a (e S) (z S)
313 | der_s1: der S a (s S a) (e ?)
314 | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
315 | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
316 der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
317 | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
318 der S a (c ? e1 e2) (c ? e1' e2)
319 | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
320 der S a (o ? e1 e2) (o ? e1' e2').
322 nlemma eq_rect_CProp0_r:
323 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
324 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
327 nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
329 naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
330 (* #S; #r1; #r2; #w; nelim r1
332 | #H1; #H2; napply (in_c ? []); //
333 | (* tutti casi assurdi *) *)
335 ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
336 in_l_empty1: ∀E.in_l S [] E → in_l' S [] E
337 | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
339 ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
341 (in_l S [] E1 → in_l S [] E2) →
342 (in_l S [] E2 → in_l S [] E1) →
343 (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
346 (* serve il lemma dopo? *)
347 ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
348 #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
350 | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
352 (* IL VICEVERSA NON VALE *)
353 naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
354 (* #S; #w; #E; #H; nelim H
356 | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
360 ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
361 #S; #a; #E; #E'; #w; #H; nelim H
362 [##1,2: #H1; ninversion H1
363 [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
364 |##2,9: #X; #Y; #K; ncases (?:False); /2/
365 |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
366 |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
367 |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
368 |##6,13: #x; #y; #K; ncases (?:False); /2/
369 |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
370 ##| #H1; ninversion H1
372 | #X; #Y; #K; ncases (?:False); /2/
373 | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
374 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
375 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
376 | #x; #y; #K; ncases (?:False); /2/
377 | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
378 ##| #H1; #H2; #H3; ninversion H3
379 [ #_; #K; ncases (?:False); /2/
380 | #X; #Y; #K; ncases (?:False); /2/
381 | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
382 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
383 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
384 | #x; #y; #K; ncases (?:False); /2/
385 | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
386 ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;