X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fre%2Fre.ma;h=6b6a985245fc1bad66dfe2f15720f52442cb5aff;hb=5fee26d2afb3a67370c92481bfbfdbd9ebed741e;hp=e939cc04f52cc08e2894bbe78bddfe59222586bc;hpb=5dcae34c6e44a40e236db641f59ddb096d1a16ec;p=helm.git

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index e939cc04f..6b6a98524 100644
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -20,11 +20,12 @@ include "arithmetics/nat.ma".
 
 (*include "Plogic/equality.ma".*)
 
+interpretation "iff" 'iff a b = (iff a b).  
+
 nrecord Alpha : Type[1] ≝
  { carr :> Type[0];
    eqb: carr → carr → bool;
-   eqb_true: ∀x,y. (eqb x y = true) = (x=y);
-   eqb_false: ∀x,y. (eqb x y = false) = (x≠y)
+   eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
  }.
  
 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
@@ -72,13 +73,15 @@ ninductive in_l (S : Alpha) : word S → re S → Prop ≝
  | in_ki: ∀w1,w2,e. w1 ∈ e → w2 ∈ e^* → w1@w2 ∈ e^*.
 interpretation "in_l" 'mem w l = (in_l ? w l).
 
-(*
 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
 interpretation "orb" 'orb a b = (orb a b).
 
 notation "a && b" left associative with precedence 40 for @{'andb $a $b}.
 interpretation "andb" 'andb a b = (andb a b).
 
+notation "~~ a" non associative with precedence 40 for @{'notb $a}.
+interpretation "notb" 'notb a = (notb a).
+
 nlet rec weq (S : Alpha) (l1, l2 : word S) on l1 : bool ≝ 
 match l1 with 
 [ nil ⇒ match l2 with [ nil ⇒ true | cons _ _ ⇒ false ]
@@ -87,9 +90,143 @@ match l1 with
 ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 notation > "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
+interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
+
+interpretation "qew" 'eqb a b = (weq ? a b).
+
+ndefinition is_epsilon ≝ λA.λw:word A. w == [ ].
+ndefinition is_empty ≝ λA.λw:word A.false.
+ndefinition is_char ≝ λA,x.λw:word A. w == [ x ].
+
+nlemma andP : ∀a,b.(a && b) = true ↔ (a = true ∧ b = true).
+#a b; ncases a; ncases b; nnormalize; @; ##[##2,4,6,8: *] /2/;
+nqed.
+
+nlemma orP : ∀a,b.(a || b) = true ↔ (a = true ∨ b = true).
+#a b; ncases a; ncases b; nnormalize; @; ##[##2,4,6,8: *] /2/;
+nqed.
+
+nlemma iff_l2r : ∀a,p.a = true ↔ p → a = true → p.
+#a p; *; /2/;
+nqed.
+
+nlemma iff_r2l : ∀a,p.a = true ↔ p → p → a = true.
+#a p; *; /2/;
+nqed.
+
+ncoercion xx : ∀a,p.∀H:a = true ↔ p. a = true → p ≝ iff_l2r
+on _H : (? = true) ↔ ? to ∀_:?. ?.
+
+ncoercion yy : ∀a,p.∀H:a = true ↔ p. p → a = true ≝ iff_r2l
+on _H : (? = true) ↔ ? to ∀_:?. ?.
+
+ndefinition wAlpha : Alpha → Alpha. #A; @ (word A) (weq A).
+#x; nelim x; ##[ #y; ncases y; /2/; #x xs; @; nnormalize; #; ndestruct; ##]
+#x xs; #IH y; nelim y; ##[ @; nnormalize; #; ndestruct; ##]
+#y ys; *; #H1 H2; @; #H3;
+##[ ##2: ncases (IH ys); #_; #H; ndestruct; nrewrite > (iff_r2l ?? (eqb_true ???) ?); //; napply H; //]
+nrewrite > (iff_l2r ?? (eqb_true ? x y) ?); nnormalize in H3; ncases (x == y) in H3; nnormalize; /2/;
+##[ #H; ncases (IH ys); #E; #_; nrewrite > (E H); //] #; ndestruct;
+nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ T; Y ≟ T, X ≟  (wAlpha T) ⊢ carr X ≡ word Y.
+unification hint 0 ≔ T; Y ≟ T, X ≟  (wAlpha T) ⊢ carr X ≡ list Y.
+unification hint 0 ≔ T,x,y; Y ≟ T, X ≟ (wAlpha T) ⊢ eqb X x y ≡ weq Y x y.
+
+nlet rec ex_split (A : Alpha) (p1,p2 : word A → bool) (w : word A) on w : bool ≝
+  match w with
+  [ nil ⇒ p1 [ ] && p2 [ ]
+  | cons x xs ⇒ p1 [ ] && p2 (x::xs) || ex_split … (λw.p1 (x :: w)) p2 xs].
+
+nlemma ex_splitP : 
+  ∀A,w,p1,p2. ex_split A p1 p2 w = true ↔ 
+              ∃w1,w2. w = w1 @ w2 ∧ p1 w1 = true ∧ p2 w2 = true.
+#A w; nelim w;
+##[ #p1 p2; @;
+   ##[ #H; @[ ]; @[ ]; ncases (iff_l2r ?? (andP ??) H); (* bug coercions *) 
+       #E1 E2; nrewrite > E1; nrewrite > E2; /3/;
+   ##| *; #w1; *;#w2; *; *; ncases w1; ncases w2; nnormalize; #abs H1 H2; #;
+       ndestruct; nrewrite > H1 ; nrewrite > H2; //]
+##| #x xs IH p1 p2; @;
+   ##[ #H; ncases (iff_l2r ?? (orP ??) H);
+      ##[ #H1; ncases (iff_l2r ?? (andP ??) H1); #p1T p2T;
+          @[ ]; @(x::xs); nnormalize; /3/;
+      ##| #E; ncases (iff_l2r ?? (IH ??) E); #l1; *; #l2; *; *; #defxs p1T p2T;
+          @(x :: l1); @l2; ndestruct; /3/; ##]
+    ##| *; #w1; *; #w2; *; *; ncases w1;
+       ##[ nnormalize in ⊢ (% → ?); ncases w2; ##[ #; ndestruct] #y ys defw2 p1T p2T;
+           nchange with ((p1 [ ] && p2 (x::xs) || ex_split ? (λw0.p1 (x::w0)) p2 xs) = true);
+           napply (iff_r2l ?? (orP ??)); @1; napply (iff_r2l ?? (andP ??));
+           ndestruct; /2/;
+       ##| #y ys; nnormalize in ⊢ (% → ?); #E p1T p2T;
+           nchange with ((p1 [ ] && p2 (x::xs) || ex_split ? (λw0.p1 (x::w0)) p2 xs) = true);
+           napply (iff_r2l ?? (orP ??)); @2; napply (iff_r2l ?? (IH ??));
+           @ys; @w2; ndestruct; /3/; ##]##]##]
+nqed.
+
+nlet rec allb (A : Alpha) (p,fresh_p : word A → bool) (w : word A) on w : bool ≝
+  match w with
+  [ nil ⇒ p [ ]
+  | cons x xs ⇒ p [x] && (xs == [ ] || allb … fresh_p fresh_p xs) 
+                || allb … (λw.p (x :: w)) fresh_p xs].
+
+nlemma allbP :
+  ∀A,w,p.allb A p p w = true ↔ 
+    ∃w1,w2.w = w1 @ w2 ∧ p w1 = true ∧ (w2 = [ ] ∨ allb ? p p w2 = true).
+#A w; nelim w;
+##[ #p; @; 
+   ##[ #H; @[ ]; @[ ]; nnormalize in H; /4/ by conj, or_introl;
+   ##| *; #w1; *; #w2; ncases w1;
+       ##[ *; *; nnormalize in ⊢ (% → ?); #defw2 pnil; *; ##[ #; ndestruct] //;
+       ##| #y ys; *; *; nnormalize in ⊢ (% → ?); #; ndestruct; ##]##]
+##| #y ys IH p; @;
+   ##[ #E; ncases (iff_l2r ?? (orP ??) E);
+       ##[ #H; ncases (iff_l2r ?? (andP ??) H); #px allys;
+           nlapply (iff_l2r ?? (orP ??) allys); *; 
+           ##[ #defys; @[y]; @[ ]; nrewrite > (iff_l2r ?? (eqb_true ? ys ?) defys);
+               /4/ by conj, or_introl;
+           ##| #IHa; ncases (iff_l2r ?? (IH ?) IHa); #z; *; #zs; *; *;
+               #defys pz; *; 
+               ##[ #; ndestruct; @[y]; @z;
+                   nrewrite > (append_nil ? z) in IHa; /4/ by or_intror, conj;
+               ##| #allzs; @[y]; @(z@zs); nrewrite > defys; /3/ by or_intror, conj;##]##]
+       ##| #allbp;
+               ; 
+                   
+           
+
+nlet rec in_lb (A : Alpha) (e : re A) on e : word A → bool ≝ 
+  match e with
+  [ e ⇒ is_epsilon …
+  | z ⇒ is_empty …
+  | s x ⇒ is_char … x
+  | o e1 e2 ⇒ λw.in_lb … e1 w || in_lb … e2 w
+  | c e1 e2 ⇒ ex_split … (in_lb A e1) (in_lb A e2)
+  | k e ⇒ allb … (in_lb A e) (in_lb A e)].
+  
+  
+nlemma equiv_l_lb : ∀A,e,w. w ∈ e ↔ in_lb A e w = true.
+#A e; nelim e; nnormalize;
+##[ #w; @; ##[##2: #; ndestruct] #H; ninversion H; #; ndestruct;
+##| #w; @; ##[##2: #H; nrewrite > (l2r ??? H); //; ##]
+    #H; ninversion H; #; ndestruct; //;
+##| #x w; @; ##[ #H; ninversion H; #; ndestruct; nrewrite > (r2l ????); //; ##]
+    #H; nrewrite > (l2r ??? H); @2;
+##| #e1 e2 IH1 IH2 w; @; #E; 
+    ##[ ninversion E; ##[##1,2,4,5,6,7: #; ndestruct]
+        #w1 w2 e1 e2 w1r1 w2r2 H1 H2 defw defr1r2; ndestruct;
+        nlapply (IH1 w1); *; #IH1; #_; nlapply (IH1 w1r1);
+        nlapply (IH2 w2); *; #IH2; #_; nlapply (IH2 w2r2);
+        nelim w1;nnormalize; ncases w2; //; nnormalize;
+
+    ##[ nelim w; ##[ nnormalize; //] #x xs IH E; nnormalize;
+    nlapply (IH1 [x]); nlapply (IH2 xs);
+    ncases (in_lb A e1 [x]); ncases (in_lb A e2 xs); nnormalize; *; #E1 E2; *; #E3 E4; /2/;
+    ##[ ncases xs in IH E3 E4; nnormalize; //; #xx xs H; #_;
+    
+     *; nnormalize;
 
-*)
 
 nlemma in_l_inv_e:
  ∀S.∀w:word S. w ∈ ∅ → w = [].
@@ -166,7 +303,7 @@ notation > "w .∈ E" non associative with precedence 40 for @{'in_pl $w $E}.
 notation < "w\shy .∈\shy E" non associative with precedence 40 for @{'in_pl $w $E}.   
 interpretation "in_prl" 'in_pl w l = (in_prl ? w l).
 
-interpretation "iff" 'iff a b = (iff a b).
+
 
 nlemma append_eq_nil : 
   ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w1 = [ ].
@@ -278,9 +415,6 @@ nlemma XXze :  ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ)  → False.
 #S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
 nqed.
 
-nlemma eqb_t : ∀S:Alpha.∀a,b:S.∀p:a == b = true. a = b.
-#S a b H; nrewrite < (eqb_true ? a b); //.
-nqed.
 
 naxiom in_move_cat:
  ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) →