From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 May 2010 16:40:26 +0000 (+0000)
Subject: Regular expressions.
X-Git-Tag: make_still_working~2916
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=85521efd364ec494e4cc024bbf87182a312e1b7b;p=helm.git

Regular expressions.
---

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
new file mode 100644
index 000000000..10f446bc5
--- /dev/null
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -0,0 +1,178 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/connectives.ma".
+(*include "logic/equality.ma".*)
+include "datatypes/list.ma".
+include "datatypes/bool.ma".
+include "datatypes/pairs.ma".
+
+include "Plogic/equality.ma".
+
+ndefinition word ≝ λS:Type[0].list S.
+
+ninductive re (S: Type[0]) : Type[0] ≝
+   z: re S
+ | e: re S
+ | s: S → re S
+ | c: re S → re S → re S
+ | o: re S → re S → re S
+ | k: re S → re S.
+
+nlemma foo1: ∀S. ¬ (z S = e S). #S; @; #H; ndestruct. nqed.
+nlemma foo2: ∀S,x. ¬ (z S = s S x). #S; #x; @; #H; ndestruct. nqed.
+nlemma foo3: ∀S,x1,x2. ¬ (z S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
+nlemma foo4: ∀S,x1,x2. ¬ (z S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
+nlemma foo5: ∀S,x. ¬ (z S = k S x). #S; #x; @; #H; ndestruct. nqed.
+nlemma foo6: ∀S,x. ¬ (e S = s S x). #S; #x; @; #H; ndestruct. nqed.
+nlemma foo7: ∀S,x1,x2. ¬ (e S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
+nlemma foo8: ∀S,x1,x2. ¬ (e S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
+nlemma foo9: ∀S,x. ¬ (e S = k S x). #S; #x; @; #H; ndestruct. nqed.
+
+ninductive in_l (S: Type[0]): word S → re S → CProp[0] ≝
+   in_e: in_l S [] (e ?)
+ | in_s: ∀x. in_l S [x] (s ? x)
+ | in_c: ∀w1,w2,e1,e2. in_l ? w1 e1 → in_l ? w2 e2 → in_l S (w1@w2) (c ? e1 e2)
+ | in_o1: ∀w,e1,e2. in_l ? w e1 → in_l S w (o ? e1 e2)
+ | in_o2: ∀w,e1,e2. in_l ? w e2 → in_l S w (o ? e1 e2)
+ | in_ke: ∀e. in_l S [] (k ? e)
+ | in_ki: ∀w1,w2,e. in_l ? w1 e → in_l ? w2 (k ? e) → in_l S (w1@w2) (k ? e).
+
+ninductive pre (S: Type[0]) : Type[0] ≝
+   pp: pre S → pre S
+ | pz: pre S
+ | pe: pre S
+ | ps: S → pre S
+ | pc: pre S → pre S → pre S
+ | po: pre S → pre S → pre S
+ | pk: pre S → pre S.
+
+nlet rec forget (S: Type[0]) (l : pre S) on l: re S ≝
+ match l with
+  [ pp E ⇒ forget S E
+  | pz ⇒ z S
+  | pe ⇒ e S
+  | ps x ⇒ s S x
+  | pc E1 E2 ⇒ c S (forget ? E1) (forget ? E2)
+  | po E1 E2 ⇒ o S (forget ? E1) (forget ? E2)
+  | pk E ⇒ k S (forget ? E) ].
+
+ninductive in_pl (S: Type[0]): word S → pre S → CProp[0] ≝
+   in_pp: ∀w,E. in_l S w (forget ? E) → in_pl S w (pp S E) 
+ | in_pc1: ∀w1,w2,e1,e2. in_pl ? w1 e1 → in_l ? w2 (forget ? e2) →
+            in_pl S (w1@w2) (pc ? e1 e2)
+ | in_pc2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (pc ? e1 e2)
+ | in_po1: ∀w,e1,e2. in_pl ? w e1 → in_pl S w (po ? e1 e2)
+ | in_po2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (po ? e1 e2)
+ | in_pki: ∀w1,w2,e. in_pl ? w1 e → in_l ? w2 (k ? (forget ? e)) →
+           in_pl S (w1@w2) (pk ? e).
+
+nlet rec eclose (S: Type[0]) (b: bool) (E: pre S) on E ≝
+ match E with
+  [ pp E' ⇒ eclose ? true E'
+  | pz ⇒ 〈 false, pz ? 〉
+  | pe ⇒ 〈 b, pe ? 〉
+  | ps x ⇒ 〈 false, ps ? x 〉
+  | pc E1 E2 ⇒
+     let E1' ≝ eclose ? b E1 in
+     let E1'' ≝ snd … E1' in
+     let E2' ≝ eclose ? (fst … E1') E2 in
+      〈 fst … E2', pc ? E1'' (snd … E2') 〉
+  | po E1 E2 ⇒
+     let E1' ≝ eclose ? b E1 in
+     let E2' ≝ eclose ? b E2 in
+      〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
+  | pk E ⇒
+     〈 true, pk ? (snd … (eclose S b E)) 〉 ].
+      
+(**********************************************************)
+
+ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
+   der_z: der S a (z S) (z S)
+ | der_e: der S a (e S) (z S)
+ | der_s1: der S a (s S a) (e ?)
+ | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
+ | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
+            der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
+ | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
+            der S a (c ? e1 e2) (c ? e1' e2)
+ | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
+    der S a (o ? e1 e2) (o ? e1' e2').
+
+nlemma eq_rect_CProp0_r:
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
+
+naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
+(* #S; #r1; #r2; #w; nelim r1
+  [ #K; ninversion K
+  | #H1; #H2; napply (in_c ? []); //
+  | (* tutti casi assurdi *) *)
+
+ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
+   in_l_empty1: ∀E.in_l S [] E → in_l' S [] E 
+ | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
+
+ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
+   mk_eq_re: ∀E1,E2.
+    (in_l S [] E1 → in_l S [] E2) →
+    (in_l S [] E2 → in_l S [] E1) →
+    (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
+      eq_re S E1 E2.
+
+(* serve il lemma dopo? *)
+ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
+ #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
+  [ #r; #K (* ok *)
+  | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
+
+(* IL VICEVERSA NON VALE *)
+naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
+(* #S; #w; #E; #H; nelim H
+  [ //
+  | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
+  ]
+nqed. *)
+
+ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
+ #S; #a; #E; #E'; #w; #H; nelim H
+  [##1,2: #H1; ninversion H1
+     [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
+     |##2,9: #X; #Y; #K; ncases (?:False); /2/
+     |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
+     |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+     |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+     |##6,13: #x; #y; #K; ncases (?:False); /2/
+     |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
+##| #H1; ninversion H1
+     [ //
+     | #X; #Y; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+     | #x; #y; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
+##| #H1; #H2; #H3; ninversion H3
+     [ #_; #K; ncases (?:False); /2/
+     | #X; #Y; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+     | #x; #y; #K; ncases (?:False); /2/
+     | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
+##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
+