From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Thu, 8 Mar 2012 07:43:21 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1873
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=223a5b91a4e403094084d27e9c0909228925b4b8;p=helm.git

commit by user andrea
---

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