-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 ≝
+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 = [].
+ #S; #w; #H; ninversion H; #; ndestruct;
+nqed.
+
+nlemma in_l_inv_s: ∀S.∀w:word S.∀x. w ∈ `x → w = [x].
+#S w x H; ninversion H; #; ndestruct; //.
+nqed.
+
+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 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 ?).
+
+notation > ".|term 19 e|" non associative with precedence 90 for @{forget ? $e}.
+nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝