From: matitaweb Date: Fri, 2 Mar 2012 16:57:10 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1914 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2ba04cd90e76937720b16e37cb12a39b46181e3;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma index bc01f3c70..a3b88978b 100644 --- a/weblib/tutorial/chapter5.ma +++ b/weblib/tutorial/chapter5.ma @@ -11,10 +11,10 @@ include "tutorial/chapter4.ma". between an element x and a list l. Its definition is a straightforward recursion on l.*) -let rec memb (S:DeqSet) (x:S) (l: listspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span S) on l ≝ +let rec memb (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (x:S) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span S) on l ≝ match l with - [ nil ⇒ false - | cons a tl ⇒ (x =span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"/span= a) ∨ memb S x tl + [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a + | cons a tl ⇒ (x a title="eqb" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"/span= a) a title="boolean or" href="cic:/fakeuri.def(1)"∨/a memb S x tl ]. notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}. @@ -35,71 +35,71 @@ interpretation "boolean membership" 'memb a l = (memb ? a l). (op a b) is a member of (compose op l1 l2) *) -lemma memb_hd: ∀S,a,l. memb S a (a::l) = true. -#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) // +lemma memb_hd: ∀S,a,l. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#S #a #l normalize >(a href="cic:/matita/basics/logic/proj2.def(2)"proj2/a … (a href="cic:/matita/tutorial/chapter4/eqb_true.fix(0,0,4)"eqb_true/a S …) (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a S a)) // qed. lemma memb_cons: ∀S,a,b,l. - memb S a l = true → memba href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"/a S a (b::l) = true. -#S #a #b #l normalize cases (a==b) normalize // + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/aspan class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"/span S a (ba title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#S #a #b #l normalize cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize // qed. -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 /span class="autotactic"2span class="autotrace" trace absurd/span/span/] +lemma memb_single: ∀S,a,x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. +#S #a #x normalize cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x)) #H + [#_ >(\P H) // |>H normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] qed. lemma memb_append: ∀S,a,l1,l2. -memb S a (l1@a title="append" href="cic:/fakeuri.def(1)"/al2) = true → memb S a l1= true ∨ memb S a l2 = true. +a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (l1a title="append" href="cic:/fakeuri.def(1)"@/aspan class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"/spanl2) 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1a 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="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S #a #l1 elim l1 normalize [#l2 #H %2 //] -#b #tl #Hind #l2 cases (a==b) normalize /span class="autotactic"2span class="autotrace" trace orb_true_l/span/span/ +#b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a/span/span/ qed. lemma memb_append_l1: ∀S,a,l1,l2. - memb S a l1= true → memb S a (l1@a title="append" href="cic:/fakeuri.def(1)"/al2) = true. + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S #a #l1 elim l1 normalize - [normalize #le #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/ - |#b #tl #Hind #l2 cases (a==b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ + [normalize #le #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ ] qed. lemma memb_append_l2: ∀S,a,l1,l2. - memb S a l2= true → memb S a (l1@l2) = true. + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S #a #l1 elim l1 normalize // -#b #tl #Hind #l2 cases (a==b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ +#b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ qed. -lemma memb_exists: ∀S,a,l.memb S a l = truea href="cic:/matita/basics/bool/bool.con(0,1,0)"/a → ∃l1,l2.l=l1@(a::l2). -#S #a #l elim l [normalize #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/] -#b #tl #Hind #H cases (orb_true_l … H) - [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) // +lemma memb_exists: ∀S,a,l.a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/aspan class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"/span → a title="exists" href="cic:/fakeuri.def(1)"∃/al1,l2.la title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/al1a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l2). +#S #a #l elim l [normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] +#b #tl #Hind #H cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … H) + [#eqba @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S)) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … tl) >(\P eqba) // |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl - @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl // + @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (ba title="cons" href="cic:/fakeuri.def(1)":/a:l1)) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … l2) >eqtl // ] qed. lemma not_memb_to_not_eq: ∀S,a,b,l. - memb S a l = falsea href="cic:/matita/basics/bool/bool.con(0,2,0)"/a → 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 /span class="autotactic"2span class="autotrace" trace absurd/span/span/ + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S b l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +#S #a #b #l cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b)) // +#eqab >(\P eqab) #H >H #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. -lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → - memb S2 (f a) (map … f l) =a title="leibnitz's equality" href="cic:/fakeuri.def(1)"/a true. +lemma memb_map: ∀S1,S2,f,a,l. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S1 a la title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S2 (f a) (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a … f l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #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 /span class="autotactic"2span class="autotrace" trace /span/span/ +#x #tl #memba cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x)) + [#eqx >eqx >(\P eqx) >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … (f x))) normalize // + |#eqx >eqx cases (f aa title="eqb" href="cic:/fakeuri.def(1)"=/a=f x) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ ] qed. 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. + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S1 a1 l1 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S2 a2 l2 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S3 (op a1 a2) (a href="cic:/matita/basics/list/compose.def(2)"compose/a S1 S2 S3 op l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //] -#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_la href="cic:/matita/basics/bool/orb_true_l.def(2)"/a … memba1) - [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map // - |#membtl @memb_append_l2 @Hind // +#x #tl #Hind #l2 #memba1 #memba2 cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … memba1) + [#eqa1 >(\P eqa1) @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a @a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"memb_map/a // + |#membtl @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a @Hind // ] qed. @@ -108,84 +108,84 @@ to avoid duplications of elements. The following uniqueb check this property. *) (*************** unicity test *****************) -let rec uniqueb (S:DeqSet) l on l : bool ≝ +let rec uniqueb (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) l on l : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝ match l with - [ nil ⇒ true - | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl + [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a + | cons a tl ⇒ a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a tl) a title="boolean and" href="cic:/fakeuri.def(1)"∧/a uniqueb S tl ]. (* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *) -let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝ +let rec unique_append (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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 + if a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a r then r else aa title="cons" href="cic:/fakeuri.def(1)":/a:r ]. -axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. -(∀x. memb S x l1 =a title="leibnitz's equality" href="cic:/fakeuri.def(1)"/a true → P x) → (∀x. memb S x l2 = true → P x) → -∀x. memb S x (unique_append S l1 l2) = true → P x. +axiom unique_append_elim: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀P: S → Prop.∀l1,l2. +(∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"/span a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) → (∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) → +∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x. -lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true → - uniqueb S (unique_append S l1 l2) = true. +lemma unique_append_unique: ∀S,l1,l2. a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a S l2 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 href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a S (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2 -cases (true_or_falsea href="cic:/matita/basics/bool/true_or_false.def(1)"/a … (memb S a (unique_append S tl l2))) +cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a 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. + λS,l1,l2.∀a. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. lemma sublist_length: ∀S,l1,l2. - uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|. + a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a S l1 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 href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l1 l2 → a title="norm" href="cic:/fakeuri.def(1)"|/al1| a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a title="norm" href="cic:/fakeuri.def(1)"|/al2|. #S #l1 elim l1 // #a #tl #Hind #l2 #unique #sub -cut (∃a title="exists" href="cic:/fakeuri.def(1)"/al3,l4.l2=l3@(a::l4)) [@memb_exists @sub //] -* #l3 * #l4 #eql2 >eql2 >length_append normalize -applyS le_S_S eql2 >a href="cic:/matita/basics/list/length_append.def(2)"length_append/a normalize +applyS a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a <a href="cic:/matita/basics/list/length_append.def(2)"length_append/a @Hind [@(a href="cic:/matita/basics/bool/andb_true_r.def(4)"andb_true_r/a … unique)] >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 /span class="autotactic"2span class="autotrace" trace absurd/span/span/ |#membxl4 @memb_append_l2a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"/a // +cases (a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"memb_append/a … (sub x (a href="cic:/matita/basics/bool/orb_true_r2.def(3)"orb_true_r2/a … membx))) + [#membxl3 @a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"memb_append_l1/a // + |#membxal4 cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … membxal4) + [#eqxa @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a lapply (a href="cic:/matita/basics/bool/andb_true_l.def(4)"andb_true_l/a … unique) + <(\P eqxa) >membx normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ |#membxl4 @a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"memb_append_l2/a // ] ] qed. 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 /span class="autotactic"2span class="autotrace" trace absurd/span/span/] + ∀S,l1,l2. a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l1 (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2). +#S #l1 elim l1 normalize [#l2 #S #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] #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 +normalize cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x)) #eqax >eqax +[<(\P eqax) cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2))) + [#H >H normalize // | #H >H normalize >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … a)) //] +|cases (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2)) normalize [/span class="autotactic"2span class="autotrace" trace /span/span/ |>eqax normalize /span class="autotactic"2span class="autotrace" trace /span/span/] ] qed. lemma sublist_unique_append_l2: - ∀S,l1,l2. sublist S l2 (unique_append S l1 l2). + ∀S,l1,l2. a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l2 (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2). #S #l1 elim l1 [normalize //] #x #tl #Hind normalize -#l2 #a cases (memb S x (unique_appenda href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"/a S tl l2)) normalize -[@Hind | cases (a==x) normalize // @Hind] +#l2 #a cases (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2)) normalize +[@Hind | cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x) normalize // @Hind] qed. lemma decidable_sublist:∀S,l1,l2. - (sublist S l1 l2) ∨ ¬(sublist S l1 l2). + (a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l1 l2) a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a(a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S l1 l2). #S #l1 #l2 elim l1 - [%1 #a normalize in ⊢ (%→?); #abs @False_ind /span class="autotactic"2span class="autotrace" trace absurd/span/span/ + [%1 #a normalize in ⊢ (%→?); #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ |#a #tl * #subtl - [cases (true_or_false (memb S a l2)) #memba - [%1 whd #x #membx cases (orb_true_l … membx) + [cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2)) #memba + [%1 whd #x #membx cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … membx) [#eqax >(\P eqax) // |@subtl] - |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd + |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a … a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a memba)) #H1 @H1 @a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"memb_hd/a ] - |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_consa href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"/a // + |%2 @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … subtl) #H1 #x #H2 @H1 @a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"memb_cons/a // ] ] qed. @@ -193,38 +193,38 @@ qed. (********************* filtering *****************) 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 /span class="autotactic"2span class="autotrace" trace absurd/span/span/] -#b #tl #Hind cases (true_or_false (f b)) #H + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/basics/list/filter.def(2)"filter/a S f l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#S #f #a #l elim l [normalize #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] +#b #tl #Hind cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b)) #H normalize >H normalize [2:@Hind] -cases (true_or_false (a==b)) #eqab +cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b)) #eqab [#_ >(\P eqab) // | >eqab normalize @Hind] qed. lemma memb_filter_memb: ∀S,f,a,l. - memb S a (filter S f l) = true → memba href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"/a S a l = true. + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/basics/list/filter.def(2)"filter/a S f l) 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S #f #a #l elim l [normalize //] #b #tl #Hind normalize (cases (f b)) normalize -cases (a==b) normalize // @Hind +cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize // @Hind qed. -lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → -memb S x l = true ∧ (f x = true). -/span class="autotactic"3span class="autotrace" trace conj, filter_true, memb_filter_memba href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"/a/span/span/ qed. +lemma memb_filter: ∀S,f,l,x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? f l) 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l 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="logical and" href="cic:/fakeuri.def(1)"∧/a (f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a). +/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"memb_filter_memb/a, a href="cic:/matita/tutorial/chapter5/filter_true.def(5)"filter_true/a/span/span/ qed. -lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true → -memb S x (filter ? f l) = true. +lemma memb_filter_l: ∀S,f,x,l. (f x 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l 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 href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? f l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #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 // +#b #tl #Hind cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (xa title="eqb" href="cic:/fakeuri.def(1)"=/a=b)) #eqxb + [<(\P eqxb) >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … x)) >fx normalize >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … x)) normalize // |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind] ] qed. (********************* exists *****************) -let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : boola href="cic:/matita/basics/bool/bool.ind(1,0,0)"/a ≝ +let rec exists (A:Type[0]) (p:A → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝ match l with -[ nil ⇒ false -| cons h t ⇒ orb (p h) (exists A p t) +[ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a +| cons h t ⇒ a href="cic:/matita/basics/bool/orb.def(1)"orb/a (p h) (exists A p t) ]. \ No newline at end of file diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma index 21e6e75aa..1a8b65aa3 100644 --- a/weblib/tutorial/chapter6.ma +++ b/weblib/tutorial/chapter6.ma @@ -5,7 +5,7 @@ defined in Chapter 4 to formal languages. A formal language is an arbitrary set of words over a given alphabet, that we shall represent as a predicate over words. A word (or string) over an alphabet S is just a list of elements of S. *) -definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S. +definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"/span S. (* For any alphabet there is only one word of length 0, the iempty word/i, which is denoted by ϵ .*) @@ -27,7 +27,7 @@ A · B of two languages A and B, the so called Kleene's star A* of A and the derivative of a language A w.r.t. a given character a. *) definition cat : ∀S,l1,l2,w.Prop ≝ - λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aw1,w2.w1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 w2. + λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aspan class="error" title="Parse error: [sym_] or [ident] expected after [sym∃] (in [term])"/spanw1,w2.w1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/aspan class="error" title="Parse error: [term] expected after [sym∧] (in [term])"/span l2 w2. notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}. interpretation "cat lang" 'middot a b = (cat ? a b). @@ -40,7 +40,7 @@ match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons (* Given a list of words l and a language r, (conjunct l r) is true if and only if all words in l are in r, that is for every w in l, r w holds. *) -let rec conjunct (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop) on l: Prop ≝ +let rec conjunct (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/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 ]. (* Given a language l, the kleene's star of l, denoted by l*, is the set of @@ -58,7 +58,7 @@ sets. The operation of concatenation behaves well with respect to this equality. lemma cat_ext_l: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="cat lang" href="cic:/fakeuri.def(1)"·/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="cat lang" href="cic:/fakeuri.def(1)"·/a B. #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2 -cases (H w1) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ +cases (H w1) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. lemma cat_ext_r: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma index a4e3a8614..17316f031 100644 --- a/weblib/tutorial/chapter7.ma +++ b/weblib/tutorial/chapter7.ma @@ -31,11 +31,11 @@ interpretation "empty" 'empty = (z ?). (* The language sem{e} associated with the regular expression e is inductively defined by the following function: *) -let rec in_l (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (r : a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop ≝ +let rec in_l (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span) (r : a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/aspan class="error" title="Parse error: SYMBOL '≝' expected (in [let_defs])"/span S → Prop ≝ match r with [ z ⇒ a title="empty set" href="cic:/fakeuri.def(1)"∅/a | e ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a} -| s x ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/a (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) } +| s x ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/aspan class="error" title="Parse error: [ident] or [term level 19] expected after [sym{] (in [term])"/span (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) } | c r1 r2 ⇒ (in_l ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a (in_l ? r2) | o r1 r2 ⇒ (in_l ? r1) a title="union" href="cic:/fakeuri.def(1)"∪/a (in_l ? r2) | k r1 ⇒ (in_l ? r1) a title="star lang" href="cic:/fakeuri.def(1)"^/a*]. @@ -116,7 +116,7 @@ let rec forget (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"Deq | ps x ⇒ a title="atom" href="cic:/fakeuri.def(1)"`/ax | pp x ⇒ a title="atom" href="cic:/fakeuri.def(1)"`/ax | pc E1 E2 ⇒ (forget ? E1) a title="re cat" href="cic:/fakeuri.def(1)"·/a (forget ? E2) - | po E1 E2 ⇒ (forget ? E1) a title="re or" href="cic:/fakeuri.def(1)"+/a (forget ? E2) + | po E1 E2 ⇒ (forget ? E1) a title="re or" href="cic:/fakeuri.def(1)"+/aspan class="error" title="Parse error: [term] expected after [sym+] (in [term])"/span (forget ? E2) | pk E ⇒ (forget ? E)a title="re star" href="cic:/fakeuri.def(1)"^/a* ]. (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*) @@ -147,7 +147,7 @@ let rec beqitem S (i1,i2: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1 | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1a title="eqb" href="cic:/fakeuri.def(1)"=/a=y2 | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] | po i11 i12 ⇒ match i2 with [ po i21 i22 ⇒ beqitem S i11 i21 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a beqitem S i12 i22 - | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] + | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aspan class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"/span] | pc i11 i12 ⇒ match i2 with [ pc i21 i22 ⇒ beqitem S i11 i21 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a beqitem S i12 i22 | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] @@ -213,7 +213,7 @@ match r with | pe ⇒ a title="empty set" href="cic:/fakeuri.def(1)"∅/a | ps _ ⇒ a title="empty set" href="cic:/fakeuri.def(1)"∅/a | pp x ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/a (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) } -| pc r1 r2 ⇒ (in_pl ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"forget/a ? r2} a title="union" href="cic:/fakeuri.def(1)"∪/a (in_pl ? r2) +| pc r1 r2 ⇒ (in_pl ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"forget/a ? r2} a title="union" href="cic:/fakeuri.def(1)"∪/aspan class="error" title="Parse error: [term] expected after [sym∪] (in [term])"/span (in_pl ? r2) | po r1 r2 ⇒ (in_pl ? r1) a title="union" href="cic:/fakeuri.def(1)"∪/a (in_pl ? r2) | pk r1 ⇒ (in_pl ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"forget/a ? r1}a title="star lang" href="cic:/fakeuri.def(1)"^/a* ]. @@ -295,7 +295,7 @@ lemma minus_eps_item: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind ] qed. -lemma minus_eps_pre: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e}a title="substraction" href="cic:/fakeuri.def(1)"-/aa title="singleton" href="cic:/fakeuri.def(1)"{/aa title="nil" href="cic:/fakeuri.def(1)"[/a ]}. +lemma minus_eps_pre: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a title="in_pl" href="cic:/fakeuri.def(1)"\sem/aspan class="error" title="Parse error: [sym{] expected after [sym\sem ] (in [term])"/span{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e}a title="substraction" href="cic:/fakeuri.def(1)"-/aa title="singleton" href="cic:/fakeuri.def(1)"{/aa title="nil" href="cic:/fakeuri.def(1)"[/a ]}. #S * #i * [>a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a normalize in ⊢ (??%?); #w % [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ | * * // #H1 #H2 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a …H1 H2)] diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma index c0d4d91dc..7db597522 100644 --- a/weblib/tutorial/chapter8.ma +++ b/weblib/tutorial/chapter8.ma @@ -16,25 +16,50 @@ No point reached that end of b^*a + b hence no further propagation is possible. •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉 *) +include "tutorial/chapter7.ma". + +(* Broadcasting a point inside an item generates a pre, since the point could possibly reach +the end of the expression. +Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2. +If we define + 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉 +then, we just have •(i1+i2) = •(i1)⊕ •(i2). +*) include "tutorial/chapter7.ma". -definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉. +definition lo ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λa,b:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="pitem or" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a 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〉. +lemma lo_def: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b1,b2. a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1,b1〉a title="oplus" href="cic:/fakeuri.def(1)"⊕/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai2,b2〉a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai1a title="pitem or" href="cic:/fakeuri.def(1)"+/ai2,b1a title="boolean or" href="cic:/fakeuri.def(1)"∨/ab2〉. // qed. -definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. - match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉]. +(* +Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2 +we should start broadcasting it inside i1 and then proceed into i2 if and only if a +point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where +e ▹ i is a general operation of concatenation between a pre and an item, defined by +cases on the boolean in e: + + 〈i1,true〉 ▹ i2 = i1 ◃ •(i_2) + 〈i1,false〉 ▹ i2 = i1 · i2 +In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple: + i1 ◃ 〈i1,b〉 = 〈i_1 · i2, b〉 +Let us come to the formalized definitions: +*) + +definition pre_concat_r ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λi:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + match e with [ mk_Prod i1 b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pitem cat" href="cic:/fakeuri.def(1)"·/a 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 eq_to_ex_eq: ∀S.∀A,B:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop. + A a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a B → A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B. +#S #A #B #H >H #x % // qed. + +(* The behaviour of \triangleleft is summarized by the following, easy lemma: *) lemma sem_pre_concat_r : ∀S,i.∀e:pre S. \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}. @@ -42,6 +67,14 @@ lemma sem_pre_concat_r : ∀S,i.∀e:pre S. >sem_pre_true >sem_cat >sem_pre_true /2/ qed. +(* The definition of $\bullet(-)$ (\verb+eclose+) and +$\triangleright$ (\verb+pre_concat_l+) are mutually recursive. +In this situation, a viable alternative that is usually simpler +to reason about, is to abstract one of the two functions with respect +to the other. We make the notation declarations explicit in this +case, for the sake of clarity. +*) + 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 @@ -53,6 +86,8 @@ definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe 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). +(* We are ready to give the formal definition of the broadcasting operation. *) + notation "•" non associative with precedence 60 for @{eclose ?}. let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ @@ -68,6 +103,8 @@ let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ notation "• x" non associative with precedence 60 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). +(* Here are a few simple properties of •(-) *) + lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. •(i1 + i2) = •i1 ⊕ •i2. // qed. @@ -80,6 +117,9 @@ lemma eclose_star: ∀S:DeqSet.∀i:pitem S. •i^* = 〈(\fst(•i))^*,true〉. // qed. +(* The definition of •(-) (eclose) can then be lifted from items to pres +in the obvious way. *) + 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〉]. @@ -87,7 +127,32 @@ definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. definition preclose ≝ λS. lift S (eclose S). interpretation "preclose" 'eclose x = (preclose ? x). -(* theorem 16: 2 *) +(* Obviously, broadcasting does not change the carrier of the item, +as it is easily proved by structural induction. *) + +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) 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)