From: Andrea Asperti Date: Tue, 13 Dec 2011 11:38:15 +0000 (+0000) Subject: Splitted re into lang.ma nd re.ma X-Git-Tag: make_still_working~2015 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c71d6a1d1461007f941f73d2cc7975c7116fd0d;p=helm.git Splitted re into lang.ma nd re.ma --- diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma new file mode 100644 index 000000000..a0a5a938d --- /dev/null +++ b/matita/matita/lib/re/lang.ma @@ -0,0 +1,126 @@ + + +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "arithmetics/nat.ma". +include "basics/lists/list.ma". +include "basics/sets.ma". + +definition word ≝ λS:DeqSet.list S. + +notation "ϵ" non associative with precedence 90 for @{ 'epsilon }. +interpretation "epsilon" 'epsilon = (nil ?). + +(* concatenation *) +definition cat : ∀S,l1,l2,w.Prop ≝ + λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2. +notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}. +interpretation "cat lang" 'middot a b = (cat ? a b). + +let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ +match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. + +let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝ +match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. + +(* kleene's star *) +definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. +notation "a ^ *" non associative with precedence 90 for @{ 'star $a}. +interpretation "star lang" 'star l = (star ? l). + +lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop. + A =1 C → A · B =1 C · B. +#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2 +cases (H w1) /6/ +qed. + +lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop. + B =1 C → A · B =1 A · C. +#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2 +cases (H w2) /6/ +qed. + +lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop. + (A ∪ B) · C =1 A · C ∪ B · C. +#S #A #B #C #w % + [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/] +qed. + +lemma espilon_in_star: ∀S.∀A:word S → Prop. + A^* ϵ. +#S #A @(ex_intro … [ ]) normalize /2/ +qed. + +lemma cat_to_star:∀S.∀A:word S → Prop. + ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2). +#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) +% normalize /2/ +qed. + +lemma fix_star: ∀S.∀A:word S → Prop. + A^* =1 A · A^* ∪ {ϵ}. +#S #A #w % + [* #l generalize in match w; -w cases l [normalize #w * /2/] + #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); * + #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl)) + % /2/ whd @(ex_intro … tl) /2/ + |* [2: whd in ⊢ (%→?); #eqw "` 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 ?). -let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ -match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. - -let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝ -match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. - -(* -definition empty_lang ≝ λS.λw:word S.False. -notation "{}" non associative with precedence 90 for @{'empty_lang}. -interpretation "empty lang" 'empty_lang = (empty_lang ?). - -definition sing_lang ≝ λS.λx,w:word S.x=w. -(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}.*) -interpretation "sing lang" 'singl x = (sing_lang ? x). - -definition union : ∀S,l1,l2,w.Prop ≝ λS.λl1,l2.λw:word S.l1 w ∨ l2 w. -interpretation "union lang" 'union a b = (union ? a b). *) - -definition cat : ∀S,l1,l2,w.Prop ≝ - λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2. -interpretation "cat lang" 'pc a b = (cat ? a b). - -definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. -interpretation "star lang" 'pk l = (star ? l). - let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝ match r with [ z ⇒ ∅ -| e ⇒ { [ ] } -| s x ⇒ { [x] } +| e ⇒ {ϵ} +| s x ⇒ {[x]} | c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2) | o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2) | k r1 ⇒ (in_l ? r1) ^*]. @@ -91,6 +50,8 @@ interpretation "in_l mem" 'mem w l = (in_l ? l w). lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*. // qed. + +(* pointed items *) inductive pitem (S: DeqSet) : Type[0] ≝ pz: pitem S | pe: pitem S @@ -102,20 +63,15 @@ inductive pitem (S: DeqSet) : Type[0] ≝ definition 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). +interpretation "pitem star" 'star a = (pk ? a). +interpretation "pitem or" 'plus a b = (po ? a b). +interpretation "pitem cat" 'middot 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 ?). +interpretation "pitem pp" 'pp a = (pp ? a). +interpretation "pitem ps" 'ps a = (ps ? a). +interpretation "pitem epsilon" 'epsilon = (pe ?). +interpretation "pitem empty" 'empty = (pz ?). let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝ match l with @@ -143,22 +99,14 @@ match r with interpretation "in_pl" 'in_l E = (in_pl ? E). interpretation "in_pl mem" 'mem w l = (in_pl ? l w). -(* -definition epsilon : ∀S:DeqSet.bool → word S → Prop -≝ λS,b.if b then { ([ ] : word S) } else ∅. - -interpretation "epsilon" 'epsilon = (epsilon ?). -notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}. -interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b). *) - definition in_prl ≝ λS : DeqSet.λp:pre S. - if (\snd p) then \sem{\fst p} ∪ { ([ ] : word S) } else \sem{\fst p}. + if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}. interpretation "in_prl mem" 'mem w l = (in_prl ? l w). interpretation "in_prl" 'in_l E = (in_prl ? E). lemma sem_pre_true : ∀S.∀i:pitem S. - \sem{〈i,true〉} = \sem{i} ∪ { ([ ] : word S) }. + \sem{〈i,true〉} = \sem{i} ∪ {ϵ}. // qed. lemma sem_pre_false : ∀S.∀i:pitem S. @@ -189,10 +137,10 @@ lemma sem_star_w : ∀S.∀i:pitem S.∀w. \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2). // qed. -lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ]. +lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ. #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed. -lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ ([ ] ∈ e). +lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e). #S #e elim e normalize /2/ [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/ @@ -202,11 +150,11 @@ lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ ([ ] ∈ e). qed. (* lemma 12 *) -lemma epsilon_to_true : ∀S.∀e:pre S. [ ] ∈ e → \snd e = true. +lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true. #S * #i #b cases b // normalize #H @False_ind /2/ qed. -lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → [ ] ∈ e. +lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e. #S * #i #b #btrue normalize in btrue; >btrue %2 // qed. @@ -222,10 +170,6 @@ definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}. interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e). - -definition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w. -notation "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}. -interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b). lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. A = B → A =1 B. @@ -233,7 +177,7 @@ lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. lemma sem_pre_concat_r : ∀S,i.∀e:pre S. \sem{i ◂ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}. -#S #i * #i1 #b1 cases b1 /2/ +#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] >sem_pre_true >sem_cat >sem_pre_true /2/ qed. @@ -261,23 +205,6 @@ definition lk ≝ λS:DeqSet.λbcast:∀S:DeqSet.∀E:pitem S.pre S.λe:pre S. ] ]. -(* -lemma oplus_tt : ∀S: DeqSet.∀i1,i2:pitem S. - 〈i1,true〉 ⊕ 〈i2,true〉 = 〈i1 + i2,true〉. -// qed. - -lemma oplus_tf : ∀S: DeqSet.∀i1,i2:pitem S. - 〈i1,true〉 ⊕ 〈i2,false〉 = 〈i1 + i2,true〉. -// qed. - -lemma oplus_ft : ∀S: DeqSet.∀i1,i2:pitem S. - 〈i1,false〉 ⊕ 〈i2,true〉 = 〈i1 + i2,true〉. -// qed. - -lemma oplus_ff : ∀S: DeqSet.∀i1,i2:pitem S. - 〈i1,false〉 ⊕ 〈i2,false〉 = 〈i1 + i2,false〉. -// qed. *) - (* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.*) interpretation "lk" 'lk op a = (lk ? op a). notation "a^⊛" non associative with precedence 90 for @{'lk eclose $a}. @@ -359,113 +286,11 @@ lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|. | #i #IH >eclose_star >(erase_star … i) H1; nrewrite > H2; nrewrite > (dot0…); nrewrite > (cupID…);// -##| #e1 e2 H1 H2; nchange in match (𝐋\p (pre_of_re S (e1+e2))) with (?∪?); - nrewrite > H1; nrewrite > H2; nrewrite > (cupID…); // -##| #e1 H1; nchange in match (𝐋\p (pre_of_re S (e1^* ))) with (𝐋\p (pre_of_re ??) · ?); - nrewrite > H1; napply dot0; ##] -nqed. - -nlemma erase_pre_of_reK : ∀S.∀e. 𝐋 |pre_of_re S e| = 𝐋 e. -#S A; nelim A; //; -##[ #e1 e2 H1 H2; nchange in match (𝐋 (e1 · e2)) with (𝐋 e1·?); - nrewrite < H1; nrewrite < H2; // -##| #e1 e2 H1 H2; nchange in match (𝐋 (e1 + e2)) with (𝐋 e1 ∪ ?); - nrewrite < H1; nrewrite < H2; // -##| #e1 H1; nchange in match (𝐋 (e1^* )) with ((𝐋 e1)^* ); - nrewrite < H1; //] -nqed. - -(* corollary 17 *) -nlemma L_Lp_bull : ∀S.∀e:re S.𝐋 e = 𝐋\p (•pre_of_re ? e). -#S e; nrewrite > (bull_cup…); nrewrite > (Lp_pre_of_re…); -nrewrite > (cupC…); nrewrite > (cup0…); nrewrite > (erase_pre_of_reK…); //; -nqed. - -nlemma Pext : ∀S.∀f,g:word S → Prop. f = g → ∀w.f w → g w. -#S f g H; nrewrite > H; //; nqed. - -(* corollary 18 *) -ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ |e|. -#S e; @; -##[ #defsnde; nlapply (bull_cup ? e); nchange in match (𝐋\p (•e)) with (?∪?); - nrewrite > defsnde; #H; - nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //; - -*) - -