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=300812ce89ccff39d7be66f2b507ad6097496684;hpb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;p=helm.git

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 300812ce8..6b6a98524 100644
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -16,269 +16,484 @@
 (*include "logic/equality.ma".*)
 include "datatypes/list.ma".
 include "datatypes/pairs.ma".
+include "arithmetics/nat.ma".
 
 (*include "Plogic/equality.ma".*)
 
-ndefinition word ≝ λS:Type[0].list S.
+interpretation "iff" 'iff a b = (iff a b).  
 
-ninductive re (S: Type[0]) : Type[0] ≝
+nrecord Alpha : Type[1] ≝
+ { carr :> Type[0];
+   eqb: carr → carr → bool;
+   eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
+ }.
+ 
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+ndefinition word ≝ λS:Alpha.list S.
+
+ninductive re (S: Alpha) : 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.
+ 
+notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
+notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
+interpretation "star" 'pk a = (k ? a).
+interpretation "or" 'plus a b = (o ? a b).
+           
+notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+interpretation "cat" 'pc a b = (c ? a b).
 
-(*
-alias symbol "not" (instance 1) = "Clogical not".
-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.
-*)
+(* to get rid of \middot *)
+ncoercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?.
+
+notation < "a" non associative with precedence 90 for @{ 'ps $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
+interpretation "atom" 'ps a = (s ? a).
+
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (e ?).
+
+notation "∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (z ?).
+
+notation > "w ∈ E" non associative with precedence 45 for @{in_l ? $w $E}.
+ninductive in_l (S : Alpha) : word S → re S → Prop ≝
+ | in_e: [ ] ∈ ϵ
+ | in_s: ∀x:S. [x] ∈ `x
+ | in_c: ∀w1,w2,e1,e2. w1 ∈ e1 → w2 ∈ e2 → w1@w2 ∈ e1 · e2
+ | in_o1: ∀w,e1,e2. w ∈ e1 → w ∈ e1 + e2
+ | in_o2: ∀w,e1,e2. w ∈ e2 → w ∈ e1 + e2
+ | in_ke: ∀e. [ ] ∈ e^*
+ | 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 ]
+| cons x xs ⇒ match l2 with [ nil ⇒ false | cons y ys ⇒ (x == y) && weq S xs ys]].
+
+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 "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;
 
-ninductive in_l (S: Type[0]): word S → re S → Prop ≝
-   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).
-
-naxiom in_l_inv_z:
- ∀S,w. ¬ (in_l S w (z ?)).
-(* #S; #w; #H; ninversion H
-  [ #_; #b; ndestruct
-  | #a; #b; #c; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; ndestruct
-  | #a; #b; #c; ndestruct
-  | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
-nqed. *)
 
 nlemma in_l_inv_e:
- ∀S,w. in_l S w (e ?) → w = [].
- #S; #w; #H; ninversion H; #; ndestruct; //.
+ ∀S.∀w:word S. w ∈ ∅ → w = [].
+ #S; #w; #H; ninversion H; #; ndestruct;
 nqed.
 
-naxiom in_l_inv_s: 
- ∀S,w,x. in_l S w (s ? x) → w = [x].
+nlemma in_l_inv_s: ∀S.∀w:word S.∀x. w ∈ `x → w = [x].
+#S w x H; ninversion H; #; ndestruct; //.
+nqed.
 
-naxiom in_l_inv_c:
- ∀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.
+nlemma in_l_inv_c:
+ ∀S.∀w:word S.∀E1,E2. w ∈ E1 · E2 → ∃w1.∃w2. w = w1@w2 ∧ w1 ∈ E1 ∧ w2 ∈ E2.
+#S w e1 e2 H; ninversion  H; ##[##1,2,4,5,6,7: #; ndestruct; ##]
+#w1 w2 r1 r2 w1r1 w2r2; #_; #_; #defw defe; @w1; @w2; ndestruct; /3/.
+nqed.
 
-ninductive pre (S: Type[0]) : Type[0] ≝
-   pz: pre S
- | pe: pre S
- | ps: S → pre S
- | pp: S → pre S
- | pc: pre S → pre S → pre S
- | po: pre S → pre S → pre S
- | pk: pre S → pre S.
+ninductive pitem (S: Alpha) : Type[0] ≝
+   pz: pitem S
+ | pe: pitem S
+ | ps: S → pitem S
+ | pp: S → pitem S
+ | pc: pitem S → pitem S → pitem S
+ | po: pitem S → pitem S → pitem S
+ | pk: pitem S → pitem S.
+ 
+ndefinition pre ≝ λS.pitem S × bool.
+
+interpretation "pstar" 'pk a = (pk ? a).
+interpretation "por" 'plus a b = (po ? a b).
+interpretation "pcat" 'pc a b = (pc ? a b).
+notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
+notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
+interpretation "ppatom" 'pp a = (pp ? a).
+(* to get rid of \middot *)
+ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S  ≝ pc on _p : pitem ? to ∀_:?.?.
+interpretation "patom" 'ps a = (ps ? a).
+interpretation "pepsilon" 'epsilon = (pe ?).
+interpretation "pempty" 'empty = (pz ?).
 
-nlet rec forget (S: Type[0]) (l : pre S) on l: re S ≝
+notation > ".|term 19 e|" non associative with precedence 90 for @{forget ? $e}.
+nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
  match l with
-  [ pz ⇒ z S
-  | pe ⇒ e S
-  | ps x ⇒ s S x
-  | pp 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 → Prop ≝
-   in_pp: ∀x. in_pl S [x] (pp S x) 
- | 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]) (E: pre S) on E ≝
- match E with
-  [ pz ⇒ 〈 false, pz ? 〉
-  | pe ⇒ 〈 true, pe ? 〉
-  | ps x ⇒ 〈 false, pp ? x 〉
-  | pp x ⇒ 〈 false, pp ? x 〉
-  | pc E1 E2 ⇒
-     let E1' ≝ eclose ? E1 in
-     let E1'' ≝ snd … E1' in
-      match fst … E1' with
-       [ true ⇒ 
-          let E2' ≝ eclose ? E2 in
-           〈 fst … E2', pc ? E1'' (snd … E2') 〉
-       | false ⇒ 〈 false, pc ? E1'' E2 〉 ]
-  | po E1 E2 ⇒
-     let E1' ≝ eclose ? E1 in
-     let E2' ≝ eclose ? E2 in
-      〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
-  | pk E ⇒ 〈 true, pk ? (snd … (eclose S E)) 〉 ].
-
-ntheorem forget_eclose:
- ∀S,E. forget S (snd … (eclose … E)) = forget ? E.
- #S; #E; nelim E; nnormalize; //;
- #p; ncases (fst … (eclose S p)); nnormalize; //.
+  [ pz ⇒ ∅
+  | pe ⇒ ϵ
+  | ps x ⇒ `x
+  | pp x ⇒ `x
+  | pc E1 E2 ⇒ .|E1| .|E2|
+  | po E1 E2 ⇒ .|E1| + .|E2|
+  | pk E ⇒ .|E|^* ].
+notation < ".|term 19 e|" non associative with precedence 90 for @{'forget $e}.
+interpretation "forget" 'forget a = (forget ? a).
+
+notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
+interpretation "fst" 'fst x = (fst ? ? x).
+notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
+interpretation "snd" 'snd x = (snd ? ? x).
+
+notation > "w .∈ E" non associative with precedence 40 for @{in_pl ? $w $E}.
+ninductive in_pl (S: Alpha): word S → pitem S → Prop ≝
+ | in_pp:  ∀x:S.[x] .∈ `.x
+ | in_pc1: ∀w1,w2:word S.∀e1,e2:pitem S. 
+             w1 .∈ e1 → w2 ∈ .|e2| → (w1@w2) .∈ e1 · e2
+ | in_pc2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 · e2
+ | in_po1: ∀w,e1,e2. w .∈ e1 → w .∈ e1 + e2
+ | in_po2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 + e2
+ | in_pki: ∀w1,w2,e. w1 .∈ e → w2 ∈ .|e|^* → (w1@w2) .∈ e^*.
+ 
+interpretation "in_pl" 'in_pl w l = (in_pl ? w l).
+ 
+ndefinition in_prl ≝ λS : Alpha.λw:word S.λp:pre S.
+  (w = [ ] ∧ \snd p = true) ∨ w .∈ (\fst p).
+  
+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).
+
+
+
+nlemma append_eq_nil : 
+  ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w1 = [ ].
+#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct;
 nqed.
 
-ntheorem eclose_true:
- ∀S,E. (* bug refiner se si scambia true con il termine *)
-  true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E).
- #S; #E; nelim E; nnormalize; //
-  [ #H; ncases (?: False); /2/
-  | #x H; #H; ncases (?: False); /2/
-  | #x; #H; ncases (?: False); /2/
-  | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
-    #_; #_; #H; ncases (?:False); /2/
-  | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/]
+nlemma append_eq_nil_r : 
+  ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w2 = [ ].
+#S w1; nelim w1; ##[ #w2 H; nrewrite > H; // ]
+#x tl IH w2; nnormalize; #abs; ndestruct;
 nqed.
 
-(* to be moved *)
-nlemma eq_append_nil_to_eq_nil1:
- ∀A.∀l1,l2:list A. l1 @ l2 = [] → l1 = [].
- #A; #l1; nelim l1; nnormalize; /2/;
- #x; #tl; #_; #l3; #K; ndestruct.
+nlemma lemma16 : 
+  ∀S.∀e:pre S. [ ] .∈ e ↔ \snd e = true.
+#S p; ncases p; #e b; @; ##[##2: #H; nrewrite > H; @; @; //. ##]
+ncases b; //; *; ##[*; //] nelim e; 
+##[##1,2: #abs; ninversion abs; #; ndestruct;
+##|##3,4: #x abs; ninversion abs; #; ndestruct;
+##|#p1 p2 H1 H2 H; ninversion H; ##[##1,3,4,5,6: #; ndestruct; /2/. ##]
+   #w1 w2 r1 r2 w1r1 w2fr2 H3 H4 Ep1p2; ndestruct;
+   nrewrite > (append_eq_nil … H4) in w1r1; /2/ by {};
+##|#r1 r2 H1 H2 H; ninversion H; #; ndestruct; /2/ by {};
+##|#r H1 H2; ninversion H2; ##[##1,2,3,4,5: #; ndestruct; ##]
+   #w1 w2 r1 w1r1 w1er1 H11 H21 H31;
+   nrewrite > (append_eq_nil … H21) in w1r1 H1;
+   nrewrite > (?: r = r1); /2/ by {};
+   ndestruct; //. ##]
 nqed.
 
-(* to be moved *)
-nlemma eq_append_nil_to_eq_nil2:
- ∀A.∀l1,l2:list A. l1 @ l2 = [] → l2 = [].
- #A; #l1; nelim l1; nnormalize; /2/;
- #x; #tl; #_; #l3; #K; ndestruct.
+ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
+notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+interpretation "oplus" 'oplus a b = (lo ? a b).
+
+ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
+   match a with [ mk_pair e1 b1 ⇒
+   match b with [ mk_pair e2 b2 ⇒
+   match b1 with 
+   [ false ⇒ 〈e1 · e2, b2〉 
+   | true ⇒ match bcast ? e2 with [ mk_pair e2' b2' ⇒ 〈e1 · e2', b2 || b2'〉 ]]]].
+   
+notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
+interpretation "lc" 'lc op a b = (lc ? op a b).
+notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
+
+ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
+   match a with [ mk_pair e1 b1 ⇒
+   match b1 with 
+   [ false ⇒ 〈e1^*, false〉 
+   | true ⇒ match bcast ? e1 with [ mk_pair e1' b1' ⇒ 〈e1'^*, true〉 ]]].
+
+notation < "a \sup ⊛" non associative with precedence 90 for @{'lk ? $a}.
+interpretation "lk" 'lk op a = (lk ? op a).
+notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
+
+notation > "•" non associative with precedence 60 for @{eclose ?}.
+nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
+ match E with
+  [ pz ⇒ 〈 ∅, false 〉
+  | pe ⇒ 〈 ϵ,  true 〉
+  | ps x ⇒ 〈 `.x, false 〉
+  | pp x ⇒ 〈 `.x, false 〉
+  | po E1 E2 ⇒ •E1 ⊕ •E2
+  | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉 
+  | pk E ⇒ 〈E,true〉^⊛].
+notation < "• x" non associative with precedence 60 for @{'eclose $x}.
+interpretation "eclose" 'eclose x = (eclose ? x).
+notation > "• x" non associative with precedence 60 for @{'eclose $x}.
+
+ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
+interpretation "reclose" 'eclose x = (reclose ? x).
+
+nlemma lemma19_2 :
+ ∀S:Alpha.∀e1,e2:pre S.∀w. w .∈ e1 ⊕ e2 → w .∈ e1 ∨ w .∈ e2.
+#S e1 e2 w H; nnormalize in H; ncases H;
+##[ *; #defw; ncases e1; #p b; ncases b; nnormalize;
+    ##[ #_; @1; @1; /2/ by conj;
+    ##| #H1; @2; @1; /2/ by conj; ##]
+##| #H1; ninversion H1; #; ndestruct; /4/ by or_introl, or_intror; ##]
 nqed.
 
-ntheorem in_l_empty_c:
- ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2.
- #S; #E1; #E2; #H; ninversion H
-  [##1,2,4,5,6,7: #; ndestruct
-  | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
-    nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
-    ndestruct; // ]
+notation > "\move term 90 x term 90 E" 
+non associative with precedence 60 for @{move ? $x $E}.
+nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
+ match E with
+  [ pz ⇒ 〈 ∅, false 〉
+  | pe ⇒ 〈 ϵ, false 〉
+  | ps y ⇒ 〈 `y, false 〉
+  | pp y ⇒ 〈 `y, x == y 〉
+  | po e1 e2 ⇒ \move x e1 ⊕ \move x e2 
+  | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
+  | pk e ⇒ (\move x e)^⊛ ].
+notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+interpretation "move" 'move x E = (move ? x E).
+
+ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
+interpretation "rmove" 'move x E = (rmove ? x E).
+
+nlemma XXz :  ∀S:Alpha.∀w:word S. w .∈ ∅ → False.
+#S w abs; ninversion abs; #; ndestruct;
 nqed.
 
-ntheorem eclose_true':
- ∀S,E. (* bug refiner se si scambia true con il termine *)
-  in_l S [] (forget S E) → true = fst bool (pre S) (eclose S E).
- #S; #E; nelim E; nnormalize; //
-  [ #H; ncases (?:False); /2/
-  |##2,3: #x; #H; ncases (?:False); nlapply (in_l_inv_s ??? H); #K; ndestruct
-  | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
-     [ #H1; #H2; #H3; ninversion H3; /3/;
-   ##| #H1; #H2; #H3; ninversion H3
-        [ ##1,2,4,5,6,7: #; ndestruct
-        | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
-          napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //]##]
-##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
-    #E2; #H1; #H2; #H3; ninversion H3
-     [ ##1,2,3,5,6,7: #; ndestruct; /2/
-     | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
-       ncases (?: False); napply (absurd ?? (not_eq_true_false …));
-       /2/ ]##]
-nqed.     
 
-(*
-ntheorem eclose_superset:
- ∀S,E.
-  ∀w. in_l S w (forget … E) ∨ in_pl ? w E → 
-       let E' ≝ eclose … E in
-       in_pl ? w (snd … E') ∨ fst … E' = true ∧ w = [].
- #S; #E; #w; *
-  [ ngeneralize in match w; nelim E; nnormalize
-     [ #w'; #H; ncases (? : False); /2/
-   ##| #w'; #H; @2; @; //; napply in_l_inv_e; //; (* auto non va *)
-   ##|##3,4: #x; #w'; #H; @1; nrewrite > (in_l_inv_s … H); //;
-   ##| #E1; #E2; #H1; #H2; #w'; #H3;
-       ncases (in_l_inv_c … H3); #w1; *; #w2; *; *; #H4; #H5; #H6;
-       ncases (fst … (eclose S E1)) in H1 H2 ⊢ %; nnormalize
-        [ #H1; #H2; ncases (H1 … H5); ncases (H2 … H6)
-          [ #K1; #K2; nrewrite > H4; /3/;
-        ##| *; #_; #K1; #K2; nrewrite > H4; /3/;
-        ##| #K1; *; #_; #K2; nrewrite > H4; @1; nrewrite > K2;
-            /3/ ]
-   
-    @2; @; //; ninversion H; //;
-##| #H; nwhd; @1; (* manca intro per letin*)
-    (* LEMMA A PARTE? *) (* manca clear E' *)
-    nelim H; nnormalize; /2/
-     [ #w1; #w2; #p; ncases (fst … (eclose S p));
-       nnormalize; /2/
-     | #w; #p; ncases (fst … (eclose S p));
-       nnormalize; /2/ ]
+nlemma XXe :  ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
+#S w abs; ninversion abs; #; ndestruct;
 nqed.
-*)
 
-nrecord decidable : 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
- }.
+nlemma XXze :  ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ)  → False.
+#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
+nqed.
 
-nlet rec move (S: decidable) (x:S) (E: pre S) on E ≝
- match E with
-  [ pz ⇒ 〈 false, pz ? 〉
-  | pe ⇒ 〈 false, pe ? 〉
-  | ps y ⇒ 〈false, ps ? y 〉
-  | pp y ⇒ 〈 eqb … x y, ps ? y 〉
-  | pc E1 E2 ⇒
-     let E1' ≝ move ? x E1 in
-     let E2' ≝ move ? x E2 in
-     let E1'' ≝ snd … E1' in
-     let E2'' ≝ snd ?? E2' in
-      match fst … E1' with
-       [ true =>
-          let E2''' ≝ eclose S E2'' in
-           〈 fst … E2' ∨ fst … E2''', pc ? E1'' (snd … E2''') 〉
-       | false ⇒ 〈 fst … E2', pc ? E1'' E2'' 〉 ]
-  | po E1 E2 ⇒
-     let E1' ≝ move ? x E1 in
-     let E2' ≝ move ? x E2 in
-      〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
-  | pk E ⇒
-     let E' ≝ move S x E in
-     let E'' ≝ snd bool (pre S) E' in
-      match fst … E' with
-       [ true ⇒ 〈 true, pk ? (snd … (eclose … E'')) 〉
-       | false ⇒ 〈 false, pk ? E'' 〉 ]].
 
-(*
+naxiom in_move_cat:
+ ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) → 
+   (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2.
+#S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2);
+ncases e1 in H; ncases e2;
+##[##1: *; ##[*; nnormalize; #; ndestruct] 
+   #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+   nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
+##|##2: *; ##[*; nnormalize; #; ndestruct] 
+   #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+   nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
+##| #r; *; ##[ *; nnormalize; #; ndestruct] 
+   #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+   ##[##2: nnormalize; #; ndestruct; @2; @2; //.##]
+   nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz;
+##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##]
+   #H; ninversion H; nnormalize; #; ndestruct; 
+   ##[ncases (?:False); /2/ by XXz] /3/ by or_intror;
+##| #r1 r2; *; ##[ *; #defw]
+    ...
+nqed.
+
 ntheorem move_ok:
- ∀S:decidable.∀E,a,w.
-  in_pl S w (snd … (move S a E)) → in_pl S (a::w) E.
- #S; #E; #a; #w;
+ ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E. 
+#S E; ncases E; #r b; nelim r;
+##[##1,2: #a w; @; 
+   ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##]
+      #H; ninversion H; #; ndestruct;
+   ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##]
+       #H; ninversion H; #; ndestruct;##]
+##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##]
+   *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct;
+##|#a c w; @; nnormalize; 
+   ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2;  nrewrite > (eqb_t … ca); @; ##]
+       #H; ninversion H; #; ndestruct;
+   ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct]
+              #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##]
+##|#r1 r2 H1 H2 a w; @;
+   ##[ #H; ncases (in_move_cat … H);
+      ##[ *; #w1; *; #w2; *; *; #defw w1m w2m;
+          ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good; 
+          nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //.
+      ##|
+      ...
+##|
+##|
+##]
 nqed.
-*)
 
-nlet rec move_star S w E on w ≝
+
+notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
  match w with
   [ nil ⇒ E
-  | cons x w' ⇒ move_star S w' (move S x (snd … E))].
+  | cons x w' ⇒ w' ↦* (x ↦ \snd E)].
 
-ndefinition in_moves ≝ λS,w,E. fst … (move_star S w E).
+ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E).
 
 ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
  mk_equiv:
   ∀E1,E2: bool × (pre S).
-   fst ?? E1  = fst ?? E2 →
-    (∀x. equiv S (move S x (snd … E1)) (move S x (snd … E2))) →
+   \fst E1  = \fst E2 →
+    (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) →
      equiv S E1 E2.
 
 ndefinition NAT: decidable.
  @ nat eqb; /2/.
 nqed.
 
+include "hints_declaration.ma".
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat.
+
 ninductive unit: Type[0] ≝ I: unit.
 
 nlet corec foo_nop (b: bool):
- equiv NAT
+ equiv ?
   〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
   〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
  @; //; #x; ncases x
@@ -310,32 +525,12 @@ nlet corec foo (a: unit):
 nqed.
 *)
 
-notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
-notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
-interpretation "star" 'pk a = (pk ? a).
-                      
-notation "❨a|b❩" non associative with precedence 90 for @{ 'po $a $b}.
-interpretation "or" 'po a b = (po ? a b).
-           
-notation < "a b" non associative with precedence 60 for @{ 'pc $a $b}.
-notation > "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
-interpretation "cat" 'pc a b = (pc ? a b).
-
-notation < "a" non associative with precedence 90 for @{ 'pp $a}.
-notation > "` term 90 a" non associative with precedence 90 for @{ 'pp $a}.
-interpretation "atom" 'pp a = (pp ? a).
-
-(* to get rid of \middot *)
-ncoercion rex_concat : ∀S:Type[0].∀p:pre S. pre S → pre S  ≝ pc
-on _p : pre ? to ∀_:?.?.
-(* we could also get rid of ` with a coercion from nat → pre nat *) 
+ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0.
+ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
+ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*.
 
-ndefinition test1 ≝ ❨ `0 | `1 ❩^* `0.
-ndefinition test2 ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
-ndefinition test3 ≝ (`0 (`0`1)^* `1)^*.
 
-nlemma foo: in_moves NAT
-  [0;0;1;0;1;1] (eclose ? test3) = true.
+nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
  nnormalize in match test3;
  nnormalize;
 //;