(* *)
(**************************************************************************)
-include "logic/connectives.ma".
+(*include "logic/connectives.ma".*)
(*include "logic/equality.ma".*)
include "datatypes/list.ma".
-include "datatypes/bool.ma".
include "datatypes/pairs.ma".
+include "arithmetics/nat.ma".
-include "Plogic/equality.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).
+
+(* 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 ∀_:?. ?.
-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 ≝
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 ≝
+ [ 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.
+
+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.
+
+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.
+
+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.
+
+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
- [ 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)) 〉 ].
-
+ [ 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.
+
+
+nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
+#S w abs; ninversion abs; #; ndestruct;
+nqed.
+
+nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False.
+#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
+nqed.
+
+
+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: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.
+
+
+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' ⇒ w' ↦* (x ↦ \snd 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 (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 ?
+ 〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
+ 〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
+ @; //; #x; ncases x
+ [ nnormalize in ⊢ (??%%); napply (foo_nop false)
+ | #y; ncases y
+ [ nnormalize in ⊢ (??%%); napply (foo_nop false)
+ | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
+nqed.
+
+(*
+nlet corec foo (a: unit):
+ equiv NAT
+ (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
+ (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
+≝ ?.
+ @;
+ ##[ nnormalize; //
+ ##| #x; ncases x
+ [ nnormalize in ⊢ (??%%);
+ nnormalize in foo: (? → ??%%);
+ @; //; #y; ncases y
+ [ nnormalize in ⊢ (??%%); napply foo_nop
+ | #y; ncases y
+ [ nnormalize in ⊢ (??%%);
+
+ ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
+ ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
+ ##]
+nqed.
+*)
+
+ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0.
+ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
+ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*.
+
+
+nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
+ nnormalize in match test3;
+ nnormalize;
+//;
+nqed.
+
(**********************************************************)
ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
projects / helm.git / blobdiff