From: matitaweb Date: Wed, 22 Feb 2012 09:28:17 +0000 (+0000) Subject: Complete outline. Raw scripts. X-Git-Tag: make_still_working~1944 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df8e8b840c36a1a789ec7bebc47c3cc8aca4f663;p=helm.git Complete outline. Raw scripts. --- diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index a0a5a938d..b358f8232 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -1,126 +1,200 @@ +include "basics/logic.ma". +(**** a subset of A is just an object of type A→Prop ****) -(**************************************************************************) -(* ___ *) -(* ||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/ +definition empty_set ≝ λA:Type[0].λa:A.False. +notation "\emptyv" non associative with precedence 90 for @{'empty_set}. +interpretation "empty set" 'empty_set = (empty_set ?). + +definition singleton ≝ λA.λx,a:A.x=a. +(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *) +interpretation "singleton" 'singl x = (singleton ? x). + +definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a. +interpretation "union" 'union a b = (union ? a b). + +definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a. +interpretation "intersection" 'intersects a b = (intersection ? a b). + +definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w. +interpretation "complement" 'not a = (complement ? a). + +definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w. +interpretation "substraction" 'minus a b = (substraction ? a b). + +definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a). +interpretation "subset" 'subseteq a b = (subset ? a b). + +(* extensional equality *) +definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a. +notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}. +interpretation "extensional equality" 'eqP a b = (eqP ? a b). + +lemma eqP_sym: ∀U.∀A,B:U →Prop. + A =1 B → B =1 A. +#U #A #B #eqAB #a @iff_sym @eqAB qed. + +lemma eqP_trans: ∀U.∀A,B,C:U →Prop. + A =1 B → B =1 C → A =1 C. +#U #A #B #C #eqAB #eqBC #a @iff_trans // qed. + +lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. + A =1 C → A ∪ B =1 C ∪ B. +#U #A #B #C #eqAB #a @iff_or_r @eqAB qed. + +lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. + B =1 C → A ∪ B =1 A ∪ C. +#U #A #B #C #eqBC #a @iff_or_l @eqBC qed. + +lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. + A =1 C → A ∩ B =1 C ∩ B. +#U #A #B #C #eqAB #a @iff_and_r @eqAB qed. + +lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. + B =1 C → A ∩ B =1 A ∩ C. +#U #A #B #C #eqBC #a @iff_and_l @eqBC qed. + +lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. + A =1 C → A - B =1 C - B. +#U #A #B #C #eqAB #a @iff_and_r @eqAB qed. + +lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. + B =1 C → A - B =1 A - C. +#U #A #B #C #eqBC #a @iff_and_l /2/ qed. + +(* set equalities *) +lemma union_empty_r: ∀U.∀A:U→Prop. + A ∪ ∅ =1 A. +#U #A #w % [* // normalize #abs @False_ind /2/ | /2/] 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/ +lemma union_comm : ∀U.∀A,B:U →Prop. + A ∪ B =1 B ∪ A. +#U #A #B #a % * /2/ qed. + +lemma union_assoc: ∀U.∀A,B,C:U → Prop. + A ∪ B ∪ C =1 A ∪ (B ∪ C). +#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/] +qed. + +lemma cap_comm : ∀U.∀A,B:U →Prop. + A ∩ B =1 B ∩ A. +#U #A #B #a % * /2/ qed. + +lemma union_idemp: ∀U.∀A:U →Prop. + A ∪ A =1 A. +#U #A #a % [* // | /2/] qed. + +lemma cap_idemp: ∀U.∀A:U →Prop. + A ∩ A =1 A. +#U #A #a % [* // | /2/] qed. + +(*distributivities *) + +lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. + (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C). +#U #A #B #C #w % [* * /3/ | * * /3/] 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/] +lemma distribute_substract : ∀U.∀A,B,C:U→Prop. + (A ∪ B) - C =1 (A - C) ∪ (B - C). +#U #A #B #C #w % [* * /3/ | * * /3/] qed. -lemma espilon_in_star: ∀S.∀A:word S → Prop. - A^* ϵ. -#S #A @(ex_intro … [ ]) normalize /2/ +(* substraction *) +lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B. +#U #A #B #w 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. +include "basics/types.ma". +include "basics/bool.ma". -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 Type[0]; + eqb: carr → carr → bool; + eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y) +}. -lemma star_fix_eps : ∀S.∀A:word S → Prop. - A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}. -#S #A #w % - [* #l elim l - [* whd in ⊢ ((??%?)→?); #eqw #_ %2 (\P eqa) >(\P eqb) // + |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) // + ] qed. +definition DeqProd ≝ λA,B:DeqSet. + mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B). + +unification hint 0 ≔ C1,C2; + T1 ≟ carr C1, + T2 ≟ carr C2, + X ≟ DeqProd C1 C2 +(* ---------------------------------------- *) ⊢ + T1×T2 ≡ carr X. + +unification hint 0 ≔ T1,T2,p1,p2; + X ≟ DeqProd T1 T2 +(* ---------------------------------------- *) ⊢ + eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2. + +example hint2: ∀b1,b2. + 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉. +#b1 #b2 #H @(\P H). \ No newline at end of file diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma index 3f58c2c48..12df4cc6d 100644 --- a/weblib/tutorial/chapter5.ma +++ b/weblib/tutorial/chapter5.ma @@ -1,437 +1,215 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) +(* boolean functions over lists *) -include "re/lang.ma". +include "basics/list.ma". +include "basics/sets.ma". +include "basics/deqsets.ma". -inductive re (S: DeqSet) : 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. +(********* search *********) -interpretation "re epsilon" 'epsilon = (e ?). -interpretation "re or" 'plus a b = (o ? a b). -interpretation "re cat" 'middot a b = (c ? a b). -interpretation "re star" 'star a = (k ? a). - -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 @{ 'empty }. -interpretation "empty" 'empty = (z ?). - -let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝ -match r with -[ z ⇒ ∅ -| 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) ^*]. - -notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}. -interpretation "in_l" 'in_l E = (in_l ? E). -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 - | 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. - -definition pre ≝ λS.pitem S × bool. - -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 "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 - [ pz ⇒ `∅ - | pe ⇒ ϵ - | ps x ⇒ `x - | pp x ⇒ `x - | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2) - | po E1 E2 ⇒ (forget ? E1) + (forget ? E2) - | pk E ⇒ (forget ? E)^* ]. - -(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*) -interpretation "forget" 'norm a = (forget ? a). - -let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝ -match r with -[ pz ⇒ ∅ -| pe ⇒ ∅ -| ps _ ⇒ ∅ -| pp x ⇒ { [x] } -| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2) -| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2) -| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ]. - -interpretation "in_pl" 'in_l E = (in_pl ? E). -interpretation "in_pl mem" 'mem w l = (in_pl ? l w). - -definition in_prl ≝ λS : DeqSet.λp:pre S. - 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} ∪ {ϵ}. -// qed. - -lemma sem_pre_false : ∀S.∀i:pitem S. - \sem{〈i,false〉} = \sem{i}. -// qed. - -lemma sem_cat: ∀S.∀i1,i2:pitem S. - \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}. -// qed. - -lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w. - \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w). -// qed. - -lemma sem_plus: ∀S.∀i1,i2:pitem S. - \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}. -// qed. - -lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w. - \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w). -// qed. - -lemma sem_star : ∀S.∀i:pitem S. - \sem{i^*} = \sem{i} · \sem{|i|}^*. -// qed. - -lemma sem_star_w : ∀S.∀i:pitem S.∀w. - \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2). -// qed. +let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝ + match l with + [ nil ⇒ false + | cons a tl ⇒ (x == a) ∨ memb S x tl + ]. -lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ. -#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed. +notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}. +interpretation "boolean membership" 'memb a l = (memb ? a l). -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/ - |#r1 #r2 #n1 #n2 % * /2/ - |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/ - ] +lemma memb_hd: ∀S,a,l. memb S a (a::l) = true. +#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) // qed. -(* lemma 12 *) -lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true. -#S * #i #b cases b // normalize #H @False_ind /2/ +lemma memb_cons: ∀S,a,b,l. + memb S a l = true → memb S a (b::l) = true. +#S #a #b #l normalize cases (a==b) normalize // qed. -lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e. -#S * #i #b #btrue normalize in btrue; >btrue %2 // +lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x. +#S #a #x normalize cases (true_or_false … (a==x)) #H + [#_ >(\P H) // |>H normalize #abs @False_ind /2/] qed. -definition lo ≝ λS:DeqSet.λ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). +lemma memb_append: ∀S,a,l1,l2. +memb S a (l1@l2) = true → + memb S a l1= true ∨ memb S a l2 = true. +#S #a #l1 elim l1 normalize [#l2 #H %2 //] +#b #tl #Hind #l2 cases (a==b) normalize /2/ +qed. -lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉. -// qed. +lemma memb_append_l1: ∀S,a,l1,l2. + memb S a l1= true → memb S a (l1@l2) = true. +#S #a #l1 elim l1 normalize + [normalize #le #abs @False_ind /2/ + |#b #tl #Hind #l2 cases (a==b) normalize /2/ + ] +qed. + +lemma memb_append_l2: ∀S,a,l1,l2. + memb S a l2= true → memb S a (l1@l2) = true. +#S #a #l1 elim l1 normalize // +#b #tl #Hind #l2 cases (a==b) normalize /2/ +qed. + +lemma memb_exists: ∀S,a,l.memb S a l = true → + ∃l1,l2.l=l1@(a::l2). +#S #a #l elim l [normalize #abs @False_ind /2/] +#b #tl #Hind #H cases (orb_true_l … H) + [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) // + |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl + @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl // + ] +qed. -definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. - match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉]. +lemma not_memb_to_not_eq: ∀S,a,b,l. + memb S a l = false → memb S b l = true → a==b = false. +#S #a #b #l cases (true_or_false (a==b)) // +#eqab >(\P eqab) #H >H #abs @False_ind /2/ +qed. -notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}. -interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e). - -lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. - A = B → A =1 B. -#S #A #B #H >H /2/ qed. - -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: @eq_to_ex_eq //] ->sem_pre_true >sem_cat >sem_pre_true /2/ +lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → + memb S2 (f a) (map … f l) = true. +#S1 #S2 #f #a #l elim l normalize [//] +#x #tl #memba cases (true_or_false (a==x)) + [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize // + |#eqx >eqx cases (f a==f x) normalize /2/ + ] qed. - -definition lc ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S. - match e1 with - [ mk_Prod i1 b1 ⇒ match b1 with - [ true ⇒ (i1 ◂ (bcast ? i2)) - | false ⇒ 〈i1 · i2,false〉 - ] - ]. - -definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. - match e with - [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉]. - -notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}. -interpretation "lc" 'lc op a b = (lc ? op a b). - -definition lk ≝ λS:DeqSet.λbcast:∀S:DeqSet.∀E:pitem S.pre S.λe:pre S. - match e with - [ mk_Prod i1 b1 ⇒ - match b1 with - [true ⇒ 〈(\fst (bcast ? i1))^*, true〉 - |false ⇒ 〈i1^*,false〉 - ] - ]. - -(* 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}. - -notation "•" non associative with precedence 60 for @{eclose ?}. -let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ - match i with - [ pz ⇒ 〈 `∅, false 〉 - | pe ⇒ 〈 ϵ, true 〉 - | ps x ⇒ 〈 `.x, false〉 - | pp x ⇒ 〈 `.x, false 〉 - | po i1 i2 ⇒ •i1 ⊕ •i2 - | pc i1 i2 ⇒ •i1 ▸ i2 - | pk i ⇒ 〈(\fst (•i))^*,true〉]. - -notation "• x" non associative with precedence 60 for @{'eclose $x}. -interpretation "eclose" 'eclose x = (eclose ? x). - -lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. - •(i1 + i2) = •i1 ⊕ •i2. -// qed. - -lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S. - •(i1 · i2) = •i1 ▸ i2. -// qed. - -lemma eclose_star: ∀S:DeqSet.∀i:pitem S. - •i^* = 〈(\fst(•i))^*,true〉. -// qed. - -definition reclose ≝ λS. lift S (eclose S). -interpretation "reclose" 'eclose x = (reclose ? x). - -(* theorem 16: 2 *) -lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S. - \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. -#S * #i1 #b1 * #i2 #b2 #w % - [cases b1 cases b2 normalize /2/ * /3/ * /3/ - |cases b1 cases b2 normalize /2/ * /3/ * /3/ +lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2. + memb S1 a1 l1 = true → memb S2 a2 l2 = true → + memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true. +#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //] +#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1) + [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map // + |#membtl @memb_append_l2 @Hind // ] qed. -lemma odot_true : - ∀S.∀i1,i2:pitem S. - 〈i1,true〉 ▸ i2 = i1 ◂ (•i2). -// qed. - -lemma odot_true_bis : - ∀S.∀i1,i2:pitem S. - 〈i1,true〉 ▸ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉. -#S #i1 #i2 normalize cases (•i2) // qed. - -lemma odot_false: - ∀S.∀i1,i2:pitem S. - 〈i1,false〉 ▸ i2 = 〈i1 · i2, false〉. -// qed. - -lemma LcatE : ∀S.∀e1,e2:pitem S. - \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. -// qed. - -lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|). -// qed. +(**************** unicity test *****************) -lemma erase_plus : ∀S.∀i1,i2:pitem S. - |i1 + i2| = |i1| + |i2|. -// qed. - -lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. -// qed. - -lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|. -#S #i elim i // - [ #i1 #i2 #IH1 #IH2 >erase_dot eclose_dot - cases (•i1) #i11 #b1 cases b1 // odot_true_bis // - | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) eclose_star >(erase_star … i) odot_false >sem_pre_false >sem_pre_false >sem_cat /2/ - |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …)) - >erase_bull @eqP_trans [|@(eqP_union_l … H)] - @eqP_trans [|@eqP_union_l[|@union_comm ]] - @eqP_trans [|@eqP_sym @union_assoc ] /3/ - ] -qed. +(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *) -lemma sem_fst: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}. -#S * #i * - [>sem_pre_true normalize in ⊢ (??%?); #w % - [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)] - |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ] - ] -qed. +let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝ + match l1 with + [ nil ⇒ l2 + | cons a tl ⇒ + let r ≝ unique_append S tl l2 in + if memb S a r then r else a::r + ]. -lemma item_eps: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}. -#S #i #w % - [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) // - |* // +axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. +(∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) → +∀x. memb S x (unique_append S l1 l2) = true → P x. + +lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true → + uniqueb S (unique_append S l1 l2) = true. +#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2 +cases (true_or_false … (memb S a (unique_append S tl l2))) +#H >H normalize [@Hind //] >H normalize @Hind // +qed. + +(******************* sublist *******************) +definition sublist ≝ + λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true. + +lemma sublist_length: ∀S,l1,l2. + uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|. +#S #l1 elim l1 // +#a #tl #Hind #l2 #unique #sub +cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub //] +* #l3 * #l4 #eql2 >eql2 >length_append normalize +applyS le_S_S eql2 in sub; #sub #x #membx +cases (memb_append … (sub x (orb_true_r2 … membx))) + [#membxl3 @memb_append_l1 // + |#membxal4 cases (orb_true_l … membxal4) + [#eqxa @False_ind lapply (andb_true_l … unique) + <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 // + ] ] qed. - -lemma sem_fst_aux: ∀S.∀e:pre S.∀i:pitem S.∀A. - \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}). -#S #e #i #A #seme -@eqP_trans [|@sem_fst] -@eqP_trans [||@eqP_union_r [|@eqP_sym @item_eps]] -@eqP_trans [||@distribute_substract] -@eqP_substract_r // -qed. -(* theorem 16: 1 *) -theorem sem_bull: ∀S:DeqSet. ∀e:pitem S. \sem{•e} =1 \sem{e} ∪ \sem{|e|}. -#S #e elim e - [#w normalize % [/2/ | * //] - |/2/ - |#x normalize #w % [ /2/ | * [@False_ind | //]] - |#x normalize #w % [ /2/ | * // ] - |#i1 #i2 #IH1 #IH2 >eclose_dot - @eqP_trans [|@odot_dot_aux //] >sem_cat - @eqP_trans - [|@eqP_union_r - [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]] - @eqP_trans [|@union_assoc] - @eqP_trans [||@eqP_sym @union_assoc] - @eqP_union_l // - |#i1 #i2 #IH1 #IH2 >eclose_plus - @eqP_trans [|@sem_oplus] >sem_plus >erase_plus - @eqP_trans [|@(eqP_union_l … IH2)] - @eqP_trans [|@eqP_sym @union_assoc] - @eqP_trans [||@union_assoc] @eqP_union_r - @eqP_trans [||@eqP_sym @union_assoc] - @eqP_trans [||@eqP_union_l [|@union_comm]] - @eqP_trans [||@union_assoc] /2/ - |#i #H >sem_pre_true >sem_star >erase_bull >sem_star - @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@sem_fst_aux //]]] - @eqP_trans [|@eqP_union_r [|@distr_cat_r]] - @eqP_trans [|@union_assoc] @eqP_union_l >erase_star - @eqP_sym @star_fix_eps +lemma sublist_unique_append_l1: + ∀S,l1,l2. sublist S l1 (unique_append S l1 l2). +#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/] +#x #tl #Hind #l2 #a +normalize cases (true_or_false … (a==x)) #eqax >eqax +[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2))) + [#H >H normalize // | #H >H normalize >(\b (refl … a)) //] +|cases (memb S x (unique_append S tl l2)) normalize + [/2/ |>eqax normalize /2/] +] +qed. + +lemma sublist_unique_append_l2: + ∀S,l1,l2. sublist S l2 (unique_append S l1 l2). +#S #l1 elim l1 [normalize //] #x #tl #Hind normalize +#l2 #a cases (memb S x (unique_append S tl l2)) normalize +[@Hind | cases (a==x) normalize // @Hind] +qed. + +lemma decidable_sublist:∀S,l1,l2. + (sublist S l1 l2) ∨ ¬(sublist S l1 l2). +#S #l1 #l2 elim l1 + [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/ + |#a #tl * #subtl + [cases (true_or_false (memb S a l2)) #memba + [%1 whd #x #membx cases (orb_true_l … membx) + [#eqax >(\P eqax) // |@subtl] + |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd + ] + |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons // + ] ] qed. -definition lifted_cat ≝ λS:DeqSet.λe:pre S. - lift S (lc S eclose e). +(********************* filtering *****************) -notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}. - -interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2). - -lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b. - 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉. -#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) // -qed. - -lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b. - 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉. -// -qed. +lemma filter_true: ∀S,f,a,l. + memb S a (filter S f l) = true → f a = true. +#S #f #a #l elim l [normalize #H @False_ind /2/] +#b #tl #Hind cases (true_or_false (f b)) #H +normalize >H normalize [2:@Hind] +cases (true_or_false (a==b)) #eqab + [#_ >(\P eqab) // | >eqab normalize @Hind] +qed. -lemma erase_odot:∀S.∀e1,e2:pre S. - |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|). -#S * #i1 * * #i2 #b2 // >odot_true_b // +lemma memb_filter_memb: ∀S,f,a,l. + memb S a (filter S f l) = true → memb S a l = true. +#S #f #a #l elim l [normalize //] +#b #tl #Hind normalize (cases (f b)) normalize +cases (a==b) normalize // @Hind qed. - -lemma ostar_true: ∀S.∀i:pitem S. - 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉. -// qed. - -lemma ostar_false: ∀S.∀i:pitem S. - 〈i,false〉^⊛ = 〈i^*, false〉. -// qed. -lemma erase_ostar: ∀S.∀e:pre S. - |\fst (e^⊛)| = |\fst e|^*. -#S * #i * // qed. - -lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i. - \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▸ i} ∪ { [ ] }. -#S #e1 #i -cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▸ i), \snd(e1 ▸ i) ∨ true〉) [//] -#H >H cases (e1 ▸ i) #i1 #b1 cases b1 - [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc] - @eqP_union_l /2/ - |/2/ +lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → +memb S x l = true ∧ (f x = true). +/3/ qed. + +lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true → +memb S x (filter ? f l) = true. +#S #f #x #l #fx elim l normalize // +#b #tl #Hind cases (true_or_false (x==b)) #eqxb + [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize // + |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind] ] -qed. +qed. -lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i. - e1 ⊙ 〈i,false〉 = e1 ▸ i. -#S #e1 #i -cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▸ i), \snd(e1 ▸ i) ∨ false〉) [//] -cases (e1 ▸ i) #i1 #b1 cases b1 #H @H -qed. +(********************* exists *****************) -lemma sem_odot: - ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}. -#S #e1 * #i2 * - [>sem_pre_true - @eqP_trans [|@sem_odot_true] - @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux // - |>sem_pre_false >eq_odot_false @odot_dot_aux // - ] -qed. +let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ +match l with +[ nil ⇒ false +| cons h t ⇒ orb (p h) (exists A p t) +]. -(* theorem 16: 4 *) -theorem sem_ostar: ∀S.∀e:pre S. - \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*. -#S * #i #b cases b - [>sem_pre_true >sem_pre_true >sem_star >erase_bull - @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@sem_fst_aux //]]] - @eqP_trans [|@eqP_union_r [|@distr_cat_r]] - @eqP_trans [||@eqP_sym @distr_cat_r] - @eqP_trans [|@union_assoc] @eqP_union_l - @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps - |>sem_pre_false >sem_pre_false >sem_star /2/ - ] +lemma Exists_exists : ∀A,P,l. + Exists A P l → + ∃x. P x. +#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ] qed. - diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma index 58e349509..430fc3f21 100644 --- a/weblib/tutorial/chapter6.ma +++ b/weblib/tutorial/chapter6.ma @@ -1,97 +1,132 @@ -include "basics/logic.ma". - -(* Given a universe A, we can consider sets of elements of type A by means of their -characteristic predicates A → Prop. *) - -definition set ≝ λA:Type[0].A → Prop. - -(* For instance, the empty set is the set defined by an always False predicate *) - -definition empty : ∀A.a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA.λa:A.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. - -(* the singleton set {a} can be defined by the characteristic predicate stating -equality with a *) - -definition singleton: ∀A.A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA.λa,x.aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax. - -(* Complement, union and intersection are easily defined, by means of logical -connectives *) - -definition complement: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,x.a title="logical not" href="cic:/fakeuri.def(1)"¬/a(P x). - -definition intersection: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,Q,x.(P x) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (Q x). - -definition union: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,Q,x.(P x) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (Q x). - - - - - - - - (* The reader could probably wonder what is the difference between Prop and bool. -In fact, they are quite distinct entities. In type theory, all objects are structured -in a three levels hierarchy - t : A : s -where, t is a term, A is a type, and s is called a sort. Sorts are special, primitive -constants used to give a type to types. Now, Prop is a primitive sort, while bool is -just a user defined data type (whose sort his Type[0]). In particular, Prop is the -sort of Propositions: its elements are logical statements in the usual sense. The important -point is that statements are inhabited by their proofs: a triple of the kind - p : Q : Prop -should be read as p is a proof of the proposition Q.*) - - - -include "arithmetics/nat.ma". include "basics/list.ma". +include "basics/sets.ma". +include "basics/deqsets.ma". -interpretation "iff" 'iff a b = (iff a b). - -record Alpha : Type[1] ≝ { carr :> Type[0]; - eqb: carr → carr → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a; - eqb_true: ∀x,y. (eqb x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) a title="iff" href="cic:/fakeuri.def(1)"↔/a (x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y) -}. - -notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }. -interpretation "eqb" 'eqb a b = (eqb ? a b). - -definition word ≝ λS:a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S. - -inductive re (S: a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) : 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 -coercion 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). +definition word ≝ λS:DeqSet.list S. 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 : a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/re/word.def(3)"word/a S)) on l : a href="cic:/matita/tutorial/re/word.def(3)"word/a S ≝ -match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons w tl ⇒ w a title="append" href="cic:/fakeuri.def(1)"@/a flatten ? tl ]. - -let rec conjunct (S : a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/re/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/re/word.def(3)"word/a S → Prop) on l: Prop ≝ -match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons w tl ⇒ r w a title="logical and" href="cic:/fakeuri.def(1)"∧/a conjunct ? tl r ]. +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 cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅. +#S #A #w % [|*] * #w1 * #w2 * * #_ * +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. + +(* derivative *) + +definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w). + +lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → + deriv S (A·B) a =1 (deriv S A a) · B. +#S #A #B #a #noteps #w normalize % + [* #w1 cases w1 + [* #w2 * * #_ #Aeps @False_ind /2/ + |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct + #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % // + ] + |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1)) + @(ex_intro … w2) % // % normalize // + ] +qed. + +(* star properties *) +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 @{ 'empty }. +interpretation "empty" 'empty = (z ?). + +let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝ +match r with +[ z ⇒ ∅ +| 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) ^*]. + +notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}. +interpretation "in_l" 'in_l E = (in_l ? E). +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 + | 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. + +definition pre ≝ λS.pitem S × bool. + +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 "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 + [ pz ⇒ `∅ + | pe ⇒ ϵ + | ps x ⇒ `x + | pp x ⇒ `x + | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2) + | po E1 E2 ⇒ (forget ? E1) + (forget ? E2) + | pk E ⇒ (forget ? E)^* ]. + +(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*) +interpretation "forget" 'norm a = (forget ? a). + +lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|). +// qed. + +lemma erase_plus : ∀S.∀i1,i2:pitem S. + |i1 + i2| = |i1| + |i2|. +// qed. + +lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. +// qed. + +(* boolean equality *) +let rec beqitem S (i1,i2: pitem S) on i1 ≝ + match i1 with + [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false] + | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false] + | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false] + | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false] + | po i11 i12 ⇒ match i2 with + [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22 + | _ ⇒ false] + | pc i11 i12 ⇒ match i2 with + [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22 + | _ ⇒ false] + | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false] + ]. + +lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2). +#S #i1 elim i1 + [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct + |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct + |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct + [>(\P H) // | @(\b (refl …))] + |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct + [>(\P H) // | @(\b (refl …))] + |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % + normalize #H destruct + [cases (true_or_false (beqitem S i11 i21)) #H1 + [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H + |>H1 in H; normalize #abs @False_ind /2/ + ] + |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) // + ] + |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % + normalize #H destruct + [cases (true_or_false (beqitem S i11 i21)) #H1 + [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H + |>H1 in H; normalize #abs @False_ind /2/ + ] + |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) // + ] + |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] % + normalize #H destruct + [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //] + ] +qed. + +definition DeqItem ≝ λS. + mk_DeqSet (pitem S) (beqitem S) (beqitem_true S). + +unification hint 0 ≔ S; + X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S) +(* ---------------------------------------- *) ⊢ + pitem S ≡ carr X. + +unification hint 0 ≔ S,i1,i2; + X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S) +(* ---------------------------------------- *) ⊢ + beqitem S i1 i2 ≡ eqb X i1 i2. + +(* semantics *) + +let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝ +match r with +[ pz ⇒ ∅ +| pe ⇒ ∅ +| ps _ ⇒ ∅ +| pp x ⇒ { [x] } +| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2) +| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2) +| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ]. + +interpretation "in_pl" 'in_l E = (in_pl ? E). +interpretation "in_pl mem" 'mem w l = (in_pl ? l w). + +definition in_prl ≝ λS : DeqSet.λp:pre S. + 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} ∪ {ϵ}. +// qed. + +lemma sem_pre_false : ∀S.∀i:pitem S. + \sem{〈i,false〉} = \sem{i}. +// qed. + +lemma sem_cat: ∀S.∀i1,i2:pitem S. + \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}. +// qed. + +lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w. + \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w). +// qed. + +lemma sem_plus: ∀S.∀i1,i2:pitem S. + \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}. +// qed. + +lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w. + \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w). +// qed. + +lemma sem_star : ∀S.∀i:pitem S. + \sem{i^*} = \sem{i} · \sem{|i|}^*. +// qed. + +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 = ϵ. +#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed. + +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/ + |#r1 #r2 #n1 #n2 % * /2/ + |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/ + ] +qed. + +(* lemma 12 *) +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. +#S * #i #b #btrue normalize in btrue; >btrue %2 // +qed. + +lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}. +#S #i #w % + [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) // + |* // + ] +qed. + +lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}. +#S * #i * + [>sem_pre_true normalize in ⊢ (??%?); #w % + [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)] + |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ] + ] +qed. + +definition lo ≝ λS:DeqSet.λ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). + +lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉. +// qed. + +definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. + match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉]. + +notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}. +interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e). + +lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. + A = B → A =1 B. +#S #A #B #H >H /2/ qed. + +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: @eq_to_ex_eq //] +>sem_pre_true >sem_cat >sem_pre_true /2/ +qed. + +definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S. + match e1 with + [ mk_Prod i1 b1 ⇒ match b1 with + [ true ⇒ (i1 ◃ (bcast ? i2)) + | false ⇒ 〈i1 · i2,false〉 + ] + ]. + +notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}. +interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b). + +notation "•" non associative with precedence 60 for @{eclose ?}. + +let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ + match i with + [ pz ⇒ 〈 `∅, false 〉 + | pe ⇒ 〈 ϵ, true 〉 + | ps x ⇒ 〈 `.x, false〉 + | pp x ⇒ 〈 `.x, false 〉 + | po i1 i2 ⇒ •i1 ⊕ •i2 + | pc i1 i2 ⇒ •i1 ▹ i2 + | pk i ⇒ 〈(\fst (•i))^*,true〉]. + +notation "• x" non associative with precedence 60 for @{'eclose $x}. +interpretation "eclose" 'eclose x = (eclose ? x). + +lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. + •(i1 + i2) = •i1 ⊕ •i2. +// qed. + +lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S. + •(i1 · i2) = •i1 ▹ i2. +// qed. + +lemma eclose_star: ∀S:DeqSet.∀i:pitem S. + •i^* = 〈(\fst(•i))^*,true〉. +// qed. + +definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. + match e with + [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉]. + +definition preclose ≝ λS. lift S (eclose S). +interpretation "preclose" 'eclose x = (preclose ? x). + +(* theorem 16: 2 *) +lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S. + \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. +#S * #i1 #b1 * #i2 #b2 #w % + [cases b1 cases b2 normalize /2/ * /3/ * /3/ + |cases b1 cases b2 normalize /2/ * /3/ * /3/ + ] +qed. + +lemma odot_true : + ∀S.∀i1,i2:pitem S. + 〈i1,true〉 ▹ i2 = i1 ◃ (•i2). +// qed. + +lemma odot_true_bis : + ∀S.∀i1,i2:pitem S. + 〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉. +#S #i1 #i2 normalize cases (•i2) // qed. + +lemma odot_false: + ∀S.∀i1,i2:pitem S. + 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉. +// qed. + +lemma LcatE : ∀S.∀e1,e2:pitem S. + \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. +// qed. + +lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|. +#S #i elim i // + [ #i1 #i2 #IH1 #IH2 >erase_dot eclose_dot + cases (•i1) #i11 #b1 cases b1 // odot_true_bis // + | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) eclose_star >(erase_star … i) odot_false >sem_pre_false >sem_pre_false >sem_cat /2/ + |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …)) + >erase_bull @eqP_trans [|@(eqP_union_l … H)] + @eqP_trans [|@eqP_union_l[|@union_comm ]] + @eqP_trans [|@eqP_sym @union_assoc ] /3/ + ] +qed. + +lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A. + \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}). +#S #e #i #A #seme +@eqP_trans [|@minus_eps_pre] +@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]] +@eqP_trans [||@distribute_substract] +@eqP_substract_r // +qed. + +(* theorem 16: 1 *) +theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}. +#S #e elim e + [#w normalize % [/2/ | * //] + |/2/ + |#x normalize #w % [ /2/ | * [@False_ind | //]] + |#x normalize #w % [ /2/ | * // ] + |#i1 #i2 #IH1 #IH2 >eclose_dot + @eqP_trans [|@odot_dot_aux //] >sem_cat + @eqP_trans + [|@eqP_union_r + [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]] + @eqP_trans [|@union_assoc] + @eqP_trans [||@eqP_sym @union_assoc] + @eqP_union_l // + |#i1 #i2 #IH1 #IH2 >eclose_plus + @eqP_trans [|@sem_oplus] >sem_plus >erase_plus + @eqP_trans [|@(eqP_union_l … IH2)] + @eqP_trans [|@eqP_sym @union_assoc] + @eqP_trans [||@union_assoc] @eqP_union_r + @eqP_trans [||@eqP_sym @union_assoc] + @eqP_trans [||@eqP_union_l [|@union_comm]] + @eqP_trans [||@union_assoc] /2/ + |#i #H >sem_pre_true >sem_star >erase_bull >sem_star + @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]] + @eqP_trans [|@eqP_union_r [|@distr_cat_r]] + @eqP_trans [|@union_assoc] @eqP_union_l >erase_star + @eqP_sym @star_fix_eps + ] +qed. + +(* blank item *) +let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝ + match i with + [ z ⇒ `∅ + | e ⇒ ϵ + | s y ⇒ `y + | o e1 e2 ⇒ (blank S e1) + (blank S e2) + | c e1 e2 ⇒ (blank S e1) · (blank S e2) + | k e ⇒ (blank S e)^* ]. + +lemma forget_blank: ∀S.∀e:re S.|blank S e| = e. +#S #e elim e normalize // +qed. + +lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅. +#S #e elim e + [1,2:@eq_to_ex_eq // + |#s @eq_to_ex_eq // + |#e1 #e2 #Hind1 #Hind2 >sem_cat + @eqP_trans [||@(union_empty_r … ∅)] + @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r + @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1 + |#e1 #e2 #Hind1 #Hind2 >sem_plus + @eqP_trans [||@(union_empty_r … ∅)] + @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1 + |#e #Hind >sem_star + @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind + ] +qed. + +theorem re_embedding: ∀S.∀e:re S. + \sem{•(blank S e)} =1 \sem{e}. +#S #e @eqP_trans [|@sem_bull] >forget_blank +@eqP_trans [|@eqP_union_r [|@sem_blank]] +@eqP_trans [|@union_comm] @union_empty_r. +qed. + +(* lefted operations *) +definition lifted_cat ≝ λS:DeqSet.λe:pre S. + lift S (pre_concat_l S eclose e). + +notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}. + +interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2). + +lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b. + 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉. +#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) // +qed. + +lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b. + 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉. +// +qed. + +lemma erase_odot:∀S.∀e1,e2:pre S. + |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|). +#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot // +qed. + +definition lk ≝ λS:DeqSet.λe:pre S. + match e with + [ mk_Prod i1 b1 ⇒ + match b1 with + [true ⇒ 〈(\fst (eclose ? i1))^*, true〉 + |false ⇒ 〈i1^*,false〉 + ] + ]. + +(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*) +interpretation "lk" 'lk a = (lk ? a). +notation "a^⊛" non associative with precedence 90 for @{'lk $a}. + + +lemma ostar_true: ∀S.∀i:pitem S. + 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉. +// qed. + +lemma ostar_false: ∀S.∀i:pitem S. + 〈i,false〉^⊛ = 〈i^*, false〉. +// qed. + +lemma erase_ostar: ∀S.∀e:pre S. + |\fst (e^⊛)| = |\fst e|^*. +#S * #i * // qed. + +lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i. + \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }. +#S #e1 #i +cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//] +#H >H cases (e1 ▹ i) #i1 #b1 cases b1 + [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc] + @eqP_union_l /2/ + |/2/ + ] +qed. + +lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i. + e1 ⊙ 〈i,false〉 = e1 ▹ i. +#S #e1 #i +cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//] +cases (e1 ▹ i) #i1 #b1 cases b1 #H @H +qed. + +lemma sem_odot: + ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}. +#S #e1 * #i2 * + [>sem_pre_true + @eqP_trans [|@sem_odot_true] + @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux // + |>sem_pre_false >eq_odot_false @odot_dot_aux // + ] +qed. + +(* theorem 16: 4 *) +theorem sem_ostar: ∀S.∀e:pre S. + \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*. +#S * #i #b cases b + [>sem_pre_true >sem_pre_true >sem_star >erase_bull + @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]] + @eqP_trans [|@eqP_union_r [|@distr_cat_r]] + @eqP_trans [||@eqP_sym @distr_cat_r] + @eqP_trans [|@union_assoc] @eqP_union_l + @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps + |>sem_pre_false >sem_pre_false >sem_star /2/ + ] +qed. + diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma new file mode 100644 index 000000000..dc7474e21 --- /dev/null +++ b/weblib/tutorial/chapter8.ma @@ -0,0 +1,485 @@ +include "re.ma". +include "basics/listb.ma". + +let rec move (S: DeqSet) (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)^⊛ ]. + +lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S. + move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2). +// qed. + +lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S. + move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2). +// qed. + +lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S. + move S x i^* = (move ? x i)^⊛. +// qed. + +definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e). + +lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b. + pmove ? x 〈i,b〉 = move ? x i. +// qed. + +lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b. + a::l1 = b::l2 → a = b. +#A #l1 #l2 #a #b #H destruct // +qed. + +lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S. + |\fst (move ? a i)| = |i|. +#S #a #i elim i // + [#i1 #i2 #H1 #H2 >move_cat >erase_odot // + |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); // + ] +qed. + +theorem move_ok: + ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S. + \sem{move ? a i} w ↔ \sem{i} (a::w). +#S #a #i elim i + [normalize /2/ + |normalize /2/ + |normalize /2/ + |normalize #x #w cases (true_or_false (a==x)) #H >H normalize + [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/] + |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //] + ] + |#i1 #i2 #HI1 #HI2 #w >move_cat + @iff_trans[|@sem_odot] >same_kernel >sem_cat_w + @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r + @iff_trans[||@iff_sym @deriv_middot //] + @cat_ext_l @HI1 + |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w + @iff_trans[|@sem_oplus] + @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //] + |#i1 #HI1 #w >move_star + @iff_trans[|@sem_ostar] >same_kernel >sem_star_w + @iff_trans[||@iff_sym @deriv_middot //] + @cat_ext_l @HI1 + ] +qed. + +notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}. +let rec moves (S : DeqSet) w e on w : pre S ≝ + match w with + [ nil ⇒ e + | cons x w' ⇒ w' ↦* (move S x (\fst e))]. + +lemma moves_empty: ∀S:DeqSet.∀e:pre S. + moves ? [ ] e = e. +// qed. + +lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. + moves ? (a::w) e = moves ? w (move S a (\fst e)). +// qed. + +lemma moves_left : ∀S,a,w,e. + moves S (w@[a]) e = move S a (\fst (moves S w e)). +#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons // +qed. + +lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S. + iff ((a::w) ∈ e) ((a::w) ∈ \fst e). +#S #a #w * #i #b cases b normalize + [% /2/ * // #H destruct |% normalize /2/] +qed. + +lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S. + |\fst (moves ? w e)| = |\fst e|. +#S #w elim w // +qed. + +theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. + (\snd (moves ? w e) = true) ↔ \sem{e} w. +#S #w elim w + [* #i #b >moves_empty cases b % /2/ + |#a #w1 #Hind #e >moves_cons + @iff_trans [||@iff_sym @not_epsilon_sem] + @iff_trans [||@move_ok] @Hind + ] +qed. + +(************************ pit state ***************************) +definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. + +let rec occur (S: DeqSet) (i: re S) on i ≝ + match i with + [ z ⇒ [ ] + | e ⇒ [ ] + | s y ⇒ [y] + | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) + | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) + | k e ⇒ occur S e]. + +lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true → + move S a i = pit_pre S i. +#S #a #i elim i // + [#x normalize cases (a==x) normalize // #H @False_ind /2/ + |#i1 #i2 #Hind1 #Hind2 #H >move_cat + >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //] + >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] // + |#i1 #i2 #Hind1 #Hind2 #H >move_plus + >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //] + >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] // + |#i #Hind #H >move_star >Hind // + ] +qed. + +lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i. +#S #a #i elim i // + [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // + |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 // + |#i #Hind >move_star >Hind // + ] +qed. + +lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i. +#S #w #i elim w // +qed. + +lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) → + moves S w e = pit_pre S (\fst e). +#S #w elim w + [#e * #H @False_ind @H normalize #a #abs @False_ind /2/ + |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|)))) + [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a) + @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb) + [#H2 >(\P H2) // |#H2 @H1 //] + |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ + ] + ] +qed. + +(* bisimulation *) +definition cofinal ≝ λS.λp:(pre S)×(pre S). + \snd (\fst p) = \snd (\snd p). + +theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. + \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉. +#S #e1 #e2 % +[#same_sem #w + cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2)) + [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]] + #Hcut @Hcut @iff_trans [|@decidable_sem] + @iff_trans [|@same_sem] @iff_sym @decidable_sem +|#H #w1 @iff_trans [||@decidable_sem] to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //] + >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //] + // +qed. + +lemma equiv_sem_occ: ∀S.∀e1,e2:pre S. +(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉) +→ \sem{e1}=1\sem{e2}. +#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H +qed. + +definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S). + map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l. + +lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true → + ∃a.(move ? a (\fst (\fst q)) = \fst p ∧ + move ? a (\fst (\snd q)) = \snd p). +#S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/] +#a #tl #Hind #p #q #H cases (orb_true_l … H) -H + [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H] +qed. + +definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S. + ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l). + +lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S. + is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}. +#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ +#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?)) +lapply Hsub @(list_elim_left … w) [//] +#a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?))) + [#x #Hx @Hsub @memb_append_l1 // + |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa + @(memb_map … occa) + ] +qed. + +(* the algorithm *) +let rec bisim S l n (frontier,visited: list ?) on n ≝ + match n with + [ O ⇒ 〈false,visited〉 (* assert false *) + | S m ⇒ + match frontier with + [ nil ⇒ 〈true,visited〉 + | cons hd tl ⇒ + if beqb (\snd (\fst hd)) (\snd (\snd hd)) then + bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited))) + (sons S l hd)) tl) (hd::visited) + else 〈false,visited〉 + ] + ]. + +lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?. + bisim S l n frontier visited = + match n with + [ O ⇒ 〈false,visited〉 (* assert false *) + | S m ⇒ + match frontier with + [ nil ⇒ 〈true,visited〉 + | cons hd tl ⇒ + if beqb (\snd (\fst hd)) (\snd (\snd hd)) then + bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited))) + (sons S l hd)) tl) (hd::visited) + else 〈false,visited〉 + ] + ]. +#S #l #n cases n // qed. + +lemma bisim_never: ∀S,l.∀frontier,visited: list ?. + bisim S l O frontier visited = 〈false,visited〉. +#frontier #visited >unfold_bisim // +qed. + +lemma bisim_end: ∀Sig,l,m.∀visited: list ?. + bisim Sig l (S m) [] visited = 〈true,visited〉. +#n #visisted >unfold_bisim // +qed. + +lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?. +beqb (\snd (\fst p)) (\snd (\snd p)) = true → + bisim Sig l (S m) (p::frontier) visited = + bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited))) + (sons Sig l p)) frontier) (p::visited). +#Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // +qed. + +lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?. +beqb (\snd (\fst p)) (\snd (\snd p)) = false → + bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉. +#Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // +qed. + +lemma notb_eq_true_l: ∀b. notb b = true → b = false. +#b cases b normalize // +qed. + +let rec pitem_enum S (i:re S) on i ≝ + match i with + [ z ⇒ [pz S] + | e ⇒ [pe S] + | s y ⇒ [ps S y; pp S y] + | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2) + | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2) + | k i ⇒ map ?? (pk S) (pitem_enum S i) + ]. + +lemma pitem_enum_complete : ∀S.∀i:pitem S. + memb (DeqItem S) i (pitem_enum S (|i|)) = true. +#S #i elim i + [1,2:// + |3,4:#c normalize >(\b (refl … c)) // + |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) // + |#i #Hind @(memb_map (DeqItem S)) // + ] +qed. + +definition pre_enum ≝ λS.λi:re S. + compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false]. + +lemma pre_enum_complete : ∀S.∀e:pre S. + memb ? e (pre_enum S (|\fst e|)) = true. +#S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉)) +// cases b normalize // +qed. + +definition space_enum ≝ λS.λi1,i2:re S. + compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2). + +lemma space_enum_complete : ∀S.∀e1,e2: pre S. + memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true. +#S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉)) +// qed. + +definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?. +uniqueb ? l = true ∧ + ∀p. memb ? p l = true → + ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p). + +definition disjoint ≝ λS:DeqSet.λl1,l2. + ∀p:S. memb S p l1 = true → memb S p l2 = false. + +lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} → + ∀l,n.∀frontier,visited:list ((pre S)×(pre S)). + |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→ + all_reachable S e1 e2 visited → + all_reachable S e1 e2 frontier → + disjoint ? frontier visited → + \fst (bisim S l n frontier visited) = true. +#Sig #e1 #e2 #same #l #n elim n + [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs) + @le_to_not_lt @sublist_length // * #e11 #e21 #membp + cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|)) + [|* #H1 #H2

same_kernel_moves // + |#m #HI * [#visited #vinv #finv >bisim_end //] + #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier + #disjoint + cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p)) + [@(r_frontier … (memb_hd … ))] #rp + cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true) + [cases rp #w * #fstp #sndp (bisim_step_true … ptest) @HI -HI + [(disjoint … (memb_hd …)) whd in ⊢ (??%?); // + |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited] + ] + |whd % [@unique_append_unique @(andb_true_r … u_frontier)] + @unique_append_elim #q #H + [cases (memb_sons … (memb_filter_memb … H)) -H + #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a])) + >moves_left >moves_left >mw1 >mw2 >m1 >m2 % // + |@r_frontier @memb_cons // + ] + |@unique_append_elim #q #H + [@injective_notb @(filter_true … H) + |cut ((q==p) = false) + [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //] + cases (andb_true … u_frontier) #notp #_ @(\bf ?) + @(not_to_not … not_eq_true_false) #eqqp H // + ] + ] + ] +qed. + +definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true → + (beqb (\snd (\fst p)) (\snd (\snd p)) = true). + +definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S). +memb ? x l1 = true → sublist ? (sons ? l x) l2. + +lemma bisim_complete: + ∀S,l,n.∀frontier,visited,visited_res:list ?. + all_true S visited → + sub_sons S l visited (frontier@visited) → + bisim S l n frontier visited = 〈true,visited_res〉 → + is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res. +#S #l #n elim n + [#fron #vis #vis_res #_ #_ >bisim_never #H destruct + |#m #Hind * + [(* case empty frontier *) + -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?); + #H1 destruct % #p + [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1] + |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd)))) + [|(* case head of the frontier is non ok (absurd) *) + #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct] + (* frontier = hd:: tl and hd is ok *) + #H #tl #visited #visited_res #allv >(bisim_step_true … H) + (* new_visited = hd::visited are all ok *) + cut (all_true S (hd::visited)) + [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]] + (* we now exploit the induction hypothesis *) + #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind + [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp + [cases (orb_true_l … membp) -membp #membp + [@memb_append_l2 >(\P membp) @memb_hd + |@memb_append_l1 @sublist_unique_append_l2 // + ] + |@memb_append_l2 @memb_cons // + ] + |(* the only thing left to prove is the sub_sons invariant *) + #x #membx cases (orb_true_l … membx) + [(* case x = hd *) + #eqhdx <(\P eqhdx) #xa #membxa + (* xa is a son of x; we must distinguish the case xa + was already visited form the case xa is new *) + cases (true_or_false … (memb ? xa (x::visited))) + [(* xa visited - trivial *) #membxa @memb_append_l2 // + |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l + [>membxa //|//] + ] + |(* case x in visited *) + #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa)) + [#H2 (cases (orb_true_l … H2)) + [#H3 @memb_append_l2 <(\P H3) @memb_hd + |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3 + ] + |#H2 @memb_append_l2 @memb_cons @H2 + ] + ] + ] + ] +qed. + +definition equiv ≝ λSig.λre1,re2:re Sig. + let e1 ≝ •(blank ? re1) in + let e2 ≝ •(blank ? re2) in + let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in + let sig ≝ (occ Sig e1 e2) in + (bisim ? sig n [〈e1,e2〉] []). + +theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig. + \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}. +#Sig #re1 #re2 % + [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding] + cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉) + [(memb_single … H) @(ex_intro … ϵ) /2/ + |#p #_ normalize // + ] + ] +qed. + +lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m. +#n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true] +qed. + +definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true. + +definition a ≝ s DeqNat O. +definition b ≝ s DeqNat (S O). +definition c ≝ s DeqNat (S (S O)). + +definition exp1 ≝ ((a·b)^*·a). +definition exp2 ≝ a·(b·a)^*. +definition exp4 ≝ (b·a)^*. + +definition exp6 ≝ a·(a ·a ·b^* + b^* ). +definition exp7 ≝ a · a^* · b^*. + +definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ). +definition exp9 ≝ (a·a·a + a·a·a·a·a)^*. + +example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true. +normalize // qed. + + + + + + + diff --git a/weblib/tutorial/sets.ma b/weblib/tutorial/sets.ma deleted file mode 100644 index 58e349509..000000000 --- a/weblib/tutorial/sets.ma +++ /dev/null @@ -1,97 +0,0 @@ -include "basics/logic.ma". - -(* Given a universe A, we can consider sets of elements of type A by means of their -characteristic predicates A → Prop. *) - -definition set ≝ λA:Type[0].A → Prop. - -(* For instance, the empty set is the set defined by an always False predicate *) - -definition empty : ∀A.a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA.λa:A.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. - -(* the singleton set {a} can be defined by the characteristic predicate stating -equality with a *) - -definition singleton: ∀A.A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA.λa,x.aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax. - -(* Complement, union and intersection are easily defined, by means of logical -connectives *) - -definition complement: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,x.a title="logical not" href="cic:/fakeuri.def(1)"¬/a(P x). - -definition intersection: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,Q,x.(P x) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (Q x). - -definition union: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,Q,x.(P x) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (Q x). - - - - - - - - (* The reader could probably wonder what is the difference between Prop and bool. -In fact, they are quite distinct entities. In type theory, all objects are structured -in a three levels hierarchy - t : A : s -where, t is a term, A is a type, and s is called a sort. Sorts are special, primitive -constants used to give a type to types. Now, Prop is a primitive sort, while bool is -just a user defined data type (whose sort his Type[0]). In particular, Prop is the -sort of Propositions: its elements are logical statements in the usual sense. The important -point is that statements are inhabited by their proofs: a triple of the kind - p : Q : Prop -should be read as p is a proof of the proposition Q.*) - - - -include "arithmetics/nat.ma". -include "basics/list.ma". - -interpretation "iff" 'iff a b = (iff a b). - -record Alpha : Type[1] ≝ { carr :> Type[0]; - eqb: carr → carr → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a; - eqb_true: ∀x,y. (eqb x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) a title="iff" href="cic:/fakeuri.def(1)"↔/a (x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y) -}. - -notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }. -interpretation "eqb" 'eqb a b = (eqb ? a b). - -definition word ≝ λS:a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S. - -inductive re (S: a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) : 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 -coercion 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 ?). - -let rec flatten (S : a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/re/word.def(3)"word/a S)) on l : a href="cic:/matita/tutorial/re/word.def(3)"word/a S ≝ -match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons w tl ⇒ w a title="append" href="cic:/fakeuri.def(1)"@/a flatten ? tl ]. - -let rec conjunct (S : a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/re/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/re/word.def(3)"word/a S → Prop) on l: Prop ≝ -match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons w tl ⇒ r w a title="logical and" href="cic:/fakeuri.def(1)"∧/a conjunct ? tl r ]. - -definition empty_lang ≝ λS.λw:a href="cic:/matita/tutorial/re/word.def(3)"word/a S.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. -notation "{}" non associative with precedence 90 f \ No newline at end of file