From 223a5b91a4e403094084d27e9c0909228925b4b8 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 8 Mar 2012 07:43:21 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 7 +++++-- weblib/tutorial/chapter5.ma | 25 ++++++++++++++++--------- 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 32a3f23ea..ff6071764 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -44,7 +44,8 @@ sets *) 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). -(* h2 class="section"Set Quality/h2 +(* +h2 class="section"Set Equality/h2 Two sets are equals if and only if they have the same elements, that is, if the two characteristic functions are extensionally equivalent: *) @@ -92,7 +93,9 @@ lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="substraction" href="cic:/fakeuri.def(1)"-/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="substraction" href="cic:/fakeuri.def(1)"-/a C. #U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/iff_not.def(4)"iff_not/a/span/span/ qed. -(* We can now prove several properties of the previous set-theoretic operations. +(* +h2 class="section"Simple properties of sets/h2 +We can now prove several properties of the previous set-theoretic operations. In particular, union is commutative and associative, and the empty set is an identity element: *) diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma index f0c497707..5e60831d0 100644 --- a/weblib/tutorial/chapter5.ma +++ b/weblib/tutorial/chapter5.ma @@ -1,5 +1,5 @@ (* -h1 class="section"Effective searching/h1 +h1 class="section"Effective searching/h1 The fact of being able to decide, via a computable boolean function, the equality between elements of a given set is an essential prerequisite for effectively searching an element of that set inside a data structure. In this @@ -105,10 +105,11 @@ lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2. ] qed. -(* If we are interested in representing finite sets as lists, is is convenient -to avoid duplications of elements. The following uniqueb check this property. *) - -(*************** unicity test *****************) +(* +h2 class="section"Unicity/h2 +If we are interested in representing finite sets as lists, is is convenient +to avoid duplications of elements. The following uniqueb check this property. +*) 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 @@ -126,9 +127,11 @@ let rec unique_append (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0 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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀P: S → Prop.∀l1,l2. +lemma 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. +#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx) /2/ +qed. 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. @@ -137,7 +140,9 @@ cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a #H >H normalize [@Hind //] >H normalize @Hind // qed. -(******************* sublist *******************) +(* +h2 class="section"Sublists/h2 +*) definition sublist ≝ λ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. @@ -192,7 +197,7 @@ lemma decidable_sublist:∀S,l1,l2. ] qed. -(********************* filtering *****************) +(*h2 class="section"Filtering/h2*) lemma filter_true: ∀S,f,a,l. 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. @@ -223,7 +228,9 @@ lemma memb_filter_l: ∀S,f,x,l. (f x a title="leibnitz's equality" href="cic:/ ] qed. -(********************* exists *****************) +(* +h2 class="section"Exists/h2 +*) 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 -- 2.39.2