(*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 }.
| 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 ]
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 = [].
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 = [ ].
#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) →
projects / helm.git / blobdiff