]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/re/re.ma
new intro:
[helm.git] / helm / software / matita / nlibrary / re / re.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 "logic/connectives.ma".*)
16 (*include "logic/equality.ma".*)
17 include "datatypes/list.ma".
18 include "datatypes/pairs.ma".
19
20 (*include "Plogic/equality.ma".*)
21
22 ndefinition word ≝ λS:Type[0].list S.
23
24 ninductive re (S: Type[0]) : Type[0] ≝
25    z: re S
26  | e: re S
27  | s: S → re S
28  | c: re S → re S → re S
29  | o: re S → re S → re S
30  | k: re S → re S.
31
32 (*
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.
43 *)
44
45 ninductive in_l (S: Type[0]): word S → re S → Prop ≝
46    in_e: in_l S [] (e ?)
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).
53
54 naxiom in_l_inv_z:
55  ∀S,w. ¬ (in_l S w (z ?)).
56 (* #S; #w; #H; ninversion H
57   [ #_; #b; ndestruct
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 ]
64 nqed. *)
65
66 nlemma in_l_inv_e:
67  ∀S,w. in_l S w (e ?) → w = [].
68  #S; #w; #H; ninversion H; #; ndestruct; //.
69 nqed.
70
71 naxiom in_l_inv_s: 
72  ∀S,w,x. in_l S w (s ? x) → w = [x].
73
74 naxiom in_l_inv_c:
75  ∀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.
76
77 ninductive pre (S: Type[0]) : Type[0] ≝
78    pz: pre S
79  | pe: pre S
80  | ps: S → pre S
81  | pp: S → pre S
82  | pc: pre S → pre S → pre S
83  | po: pre S → pre S → pre S
84  | pk: pre S → pre S.
85
86 nlet rec forget (S: Type[0]) (l : pre S) on l: re S ≝
87  match l with
88   [ pz ⇒ z S
89   | pe ⇒ e S
90   | ps x ⇒ s S x
91   | pp x ⇒ s S x
92   | pc E1 E2 ⇒ c S (forget ? E1) (forget ? E2)
93   | po E1 E2 ⇒ o S (forget ? E1) (forget ? E2)
94   | pk E ⇒ k S (forget ? E) ].
95
96 ninductive in_pl (S: Type[0]): word S → pre S → Prop ≝
97    in_pp: ∀x. in_pl S [x] (pp S x) 
98  | in_pc1: ∀w1,w2,e1,e2. in_pl ? w1 e1 → in_l ? w2 (forget ? e2) →
99             in_pl S (w1@w2) (pc ? e1 e2)
100  | in_pc2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (pc ? e1 e2)
101  | in_po1: ∀w,e1,e2. in_pl ? w e1 → in_pl S w (po ? e1 e2)
102  | in_po2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (po ? e1 e2)
103  | in_pki: ∀w1,w2,e. in_pl ? w1 e → in_l ? w2 (k ? (forget ? e)) →
104            in_pl S (w1@w2) (pk ? e).
105
106 nlet rec eclose (S: Type[0]) (E: pre S) on E ≝
107  match E with
108   [ pz ⇒ 〈 false, pz ? 〉
109   | pe ⇒ 〈 true, pe ? 〉
110   | ps x ⇒ 〈 false, pp ? x 〉
111   | pp x ⇒ 〈 false, pp ? x 〉
112   | pc E1 E2 ⇒
113      let E1' ≝ eclose ? E1 in
114      let E1'' ≝ snd … E1' in
115       match fst … E1' with
116        [ true ⇒ 
117           let E2' ≝ eclose ? E2 in
118            〈 fst … E2', pc ? E1'' (snd … E2') 〉
119        | false ⇒ 〈 false, pc ? E1'' E2 〉 ]
120   | po E1 E2 ⇒
121      let E1' ≝ eclose ? E1 in
122      let E2' ≝ eclose ? E2 in
123       〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
124   | pk E ⇒ 〈 true, pk ? (snd … (eclose S E)) 〉 ].
125
126 ntheorem forget_eclose:
127  ∀S,E. forget S (snd … (eclose … E)) = forget ? E.
128  #S; #E; nelim E; nnormalize; //;
129  #p; ncases (fst … (eclose S p)); nnormalize; //.
130 nqed.
131
132 ntheorem eclose_true:
133  ∀S,E. (* bug refiner se si scambia true con il termine *)
134   true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E).
135  #S; #E; nelim E; nnormalize; //
136   [ #H; ncases (?: False); /2/
137   | #x H; #H; ncases (?: False); /2/
138   | #x; #H; ncases (?: False); /2/
139   | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
140     #_; #_; #H; ncases (?:False); /2/
141   | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/]
142 nqed.
143
144 (* to be moved *)
145 nlemma eq_append_nil_to_eq_nil1:
146  ∀A.∀l1,l2:list A. l1 @ l2 = [] → l1 = [].
147  #A; #l1; nelim l1; nnormalize; /2/;
148  #x; #tl; #_; #l3; #K; ndestruct.
149 nqed.
150
151 (* to be moved *)
152 nlemma eq_append_nil_to_eq_nil2:
153  ∀A.∀l1,l2:list A. l1 @ l2 = [] → l2 = [].
154  #A; #l1; nelim l1; nnormalize; /2/;
155  #x; #tl; #_; #l3; #K; ndestruct.
156 nqed.
157
158 ntheorem in_l_empty_c:
159  ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2.
160  #S; #E1; #E2; #H; ninversion H
161   [##1,2,4,5,6,7: #; ndestruct
162   | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
163     nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
164     ndestruct; // ]
165 nqed.
166
167 ntheorem eclose_true':
168  ∀S,E. (* bug refiner se si scambia true con il termine *)
169   in_l S [] (forget S E) → true = fst bool (pre S) (eclose S E).
170  #S; #E; nelim E; nnormalize; //
171   [ #H; ncases (?:False); /2/
172   |##2,3: #x; #H; ncases (?:False); nlapply (in_l_inv_s ??? H); #K; ndestruct
173   | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
174      [ #H1; #H2; #H3; ninversion H3; /3/;
175    ##| #H1; #H2; #H3; ninversion H3
176         [ ##1,2,4,5,6,7: #; ndestruct
177         | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
178           napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //]##]
179 ##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
180     #E2; #H1; #H2; #H3; ninversion H3
181      [ ##1,2,3,5,6,7: #; ndestruct; /2/
182      | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
183        ncases (?: False); napply (absurd ?? (not_eq_true_false …));
184        /2/ ]##]
185 nqed.     
186
187 (*
188 ntheorem eclose_superset:
189  ∀S,E.
190   ∀w. in_l S w (forget … E) ∨ in_pl ? w E → 
191        let E' ≝ eclose … E in
192        in_pl ? w (snd … E') ∨ fst … E' = true ∧ w = [].
193  #S; #E; #w; *
194   [ ngeneralize in match w; nelim E; nnormalize
195      [ #w'; #H; ncases (? : False); /2/
196    ##| #w'; #H; @2; @; //; napply in_l_inv_e; //; (* auto non va *)
197    ##|##3,4: #x; #w'; #H; @1; nrewrite > (in_l_inv_s … H); //;
198    ##| #E1; #E2; #H1; #H2; #w'; #H3;
199        ncases (in_l_inv_c … H3); #w1; *; #w2; *; *; #H4; #H5; #H6;
200        ncases (fst … (eclose S E1)) in H1 H2 ⊢ %; nnormalize
201         [ #H1; #H2; ncases (H1 … H5); ncases (H2 … H6)
202           [ #K1; #K2; nrewrite > H4; /3/;
203         ##| *; #_; #K1; #K2; nrewrite > H4; /3/;
204         ##| #K1; *; #_; #K2; nrewrite > H4; @1; nrewrite > K2;
205             /3/ ]
206    
207     @2; @; //; ninversion H; //;
208 ##| #H; nwhd; @1; (* manca intro per letin*)
209     (* LEMMA A PARTE? *) (* manca clear E' *)
210     nelim H; nnormalize; /2/
211      [ #w1; #w2; #p; ncases (fst … (eclose S p));
212        nnormalize; /2/
213      | #w; #p; ncases (fst … (eclose S p));
214        nnormalize; /2/ ]
215 nqed.
216 *)
217
218 nrecord decidable : Type[1] ≝
219  { carr :> Type[0];
220    eqb: carr → carr → bool;
221    eqb_true: ∀x,y. eqb x y = true → x=y;
222    eqb_false: ∀x,y. eqb x y = false → x≠y
223  }.
224
225 nlet rec move (S: decidable) (x:S) (E: pre S) on E ≝
226  match E with
227   [ pz ⇒ 〈 false, pz ? 〉
228   | pe ⇒ 〈 false, pe ? 〉
229   | ps y ⇒ 〈false, ps ? y 〉
230   | pp y ⇒ 〈 eqb … x y, ps ? y 〉
231   | pc E1 E2 ⇒
232      let E1' ≝ move ? x E1 in
233      let E2' ≝ move ? x E2 in
234      let E1'' ≝ snd … E1' in
235      let E2'' ≝ snd ?? E2' in
236       match fst … E1' with
237        [ true =>
238           let E2''' ≝ eclose S E2'' in
239            〈 fst … E2' ∨ fst … E2''', pc ? E1'' (snd … E2''') 〉
240        | false ⇒ 〈 fst … E2', pc ? E1'' E2'' 〉 ]
241   | po E1 E2 ⇒
242      let E1' ≝ move ? x E1 in
243      let E2' ≝ move ? x E2 in
244       〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
245   | pk E ⇒
246      let E' ≝ move S x E in
247      let E'' ≝ snd bool (pre S) E' in
248       match fst … E' with
249        [ true ⇒ 〈 true, pk ? (snd … (eclose … E'')) 〉
250        | false ⇒ 〈 false, pk ? E'' 〉 ]].
251
252 (*
253 ntheorem move_ok:
254  ∀S:decidable.∀E,a,w.
255   in_pl S w (snd … (move S a E)) → in_pl S (a::w) E.
256  #S; #E; #a; #w;
257 nqed.
258 *)
259
260 nlet rec move_star S w E on w ≝
261  match w with
262   [ nil ⇒ E
263   | cons x w' ⇒ move_star S w' (move S x (snd … E))].
264
265 ndefinition in_moves ≝ λS,w,E. fst … (move_star S w E).
266
267 ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
268  mk_equiv:
269   ∀E1,E2: bool × (pre S).
270    fst ?? E1  = fst ?? E2 →
271     (∀x. equiv S (move S x (snd … E1)) (move S x (snd … E2))) →
272      equiv S E1 E2.
273
274 ndefinition NAT: decidable.
275  @ nat eqb; /2/.
276 nqed.
277
278 ninductive unit: Type[0] ≝ I: unit.
279
280 nlet corec foo_nop (b: bool):
281  equiv NAT
282   〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
283   〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
284  @; //; #x; ncases x
285   [ nnormalize in ⊢ (??%%); napply (foo_nop false)
286   | #y; ncases y
287      [ nnormalize in ⊢ (??%%); napply (foo_nop false)
288      | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
289 nqed.
290
291 (*
292 nlet corec foo (a: unit):
293  equiv NAT
294   (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
295   (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
296 ≝ ?.
297  @;
298   ##[ nnormalize; //
299   ##| #x; ncases x
300        [ nnormalize in ⊢ (??%%);
301          nnormalize in foo: (? → ??%%);
302          @; //; #y; ncases y
303            [ nnormalize in ⊢ (??%%); napply foo_nop
304            | #y; ncases y
305               [ nnormalize in ⊢ (??%%);
306                 
307             ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
308      ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
309   ##]
310 nqed.
311 *)
312
313 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
314 notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
315 interpretation "star" 'pk a = (pk ? a).
316                       
317 notation "❨a|b❩" non associative with precedence 90 for @{ 'po $a $b}.
318 interpretation "or" 'po a b = (po ? a b).
319            
320 notation < "a b" non associative with precedence 60 for @{ 'pc $a $b}.
321 notation > "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
322 interpretation "cat" 'pc a b = (pc ? a b).
323
324 notation < "a" non associative with precedence 90 for @{ 'pp $a}.
325 notation > "` term 90 a" non associative with precedence 90 for @{ 'pp $a}.
326 interpretation "atom" 'pp a = (pp ? a).
327
328 (* to get rid of \middot *)
329 ncoercion rex_concat : ∀S:Type[0].∀p:pre S. pre S → pre S  ≝ pc
330 on _p : pre ? to ∀_:?.?.
331 (* we could also get rid of ` with a coercion from nat → pre nat *) 
332
333 ndefinition test1 ≝ ❨ `0 | `1 ❩^* `0.
334 ndefinition test2 ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
335 ndefinition test3 ≝ (`0 (`0`1)^* `1)^*.
336
337 nlemma foo: in_moves NAT
338   [0;0;1;0;1;1] (eclose ? test3) = true.
339  nnormalize in match test3;
340  nnormalize;
341 //;
342 nqed.
343
344 (**********************************************************)
345
346 ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
347    der_z: der S a (z S) (z S)
348  | der_e: der S a (e S) (z S)
349  | der_s1: der S a (s S a) (e ?)
350  | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
351  | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
352             der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
353  | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
354             der S a (c ? e1 e2) (c ? e1' e2)
355  | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
356     der S a (o ? e1 e2) (o ? e1' e2').
357
358 nlemma eq_rect_CProp0_r:
359  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
360  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
361 nqed.
362
363 nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
364
365 naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
366 (* #S; #r1; #r2; #w; nelim r1
367   [ #K; ninversion K
368   | #H1; #H2; napply (in_c ? []); //
369   | (* tutti casi assurdi *) *)
370
371 ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
372    in_l_empty1: ∀E.in_l S [] E → in_l' S [] E 
373  | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
374
375 ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
376    mk_eq_re: ∀E1,E2.
377     (in_l S [] E1 → in_l S [] E2) →
378     (in_l S [] E2 → in_l S [] E1) →
379     (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
380       eq_re S E1 E2.
381
382 (* serve il lemma dopo? *)
383 ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
384  #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
385   [ #r; #K (* ok *)
386   | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
387
388 (* IL VICEVERSA NON VALE *)
389 naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
390 (* #S; #w; #E; #H; nelim H
391   [ //
392   | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
393   ]
394 nqed. *)
395
396 ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
397  #S; #a; #E; #E'; #w; #H; nelim H
398   [##1,2: #H1; ninversion H1
399      [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
400      |##2,9: #X; #Y; #K; ncases (?:False); /2/
401      |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
402      |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
403      |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
404      |##6,13: #x; #y; #K; ncases (?:False); /2/
405      |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
406 ##| #H1; ninversion H1
407      [ //
408      | #X; #Y; #K; ncases (?:False); /2/
409      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
410      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
411      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
412      | #x; #y; #K; ncases (?:False); /2/
413      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
414 ##| #H1; #H2; #H3; ninversion H3
415      [ #_; #K; ncases (?:False); /2/
416      | #X; #Y; #K; ncases (?:False); /2/
417      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
418      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
419      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
420      | #x; #y; #K; ncases (?:False); /2/
421      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
422 ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
423