commit by user andrea

[helm.git] / weblib / tutorial / chapter5.ma

diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma
index f0c4977077a4bd9f789d2d9cf12a230d2f2edaa6..5e60831d07f8fc29581be0cbd54074eabf4733a0 100644 (file)
--- a/weblib/tutorial/chapter5.ma
+++ b/weblib/tutorial/chapter5.ma
@@ -1,5 +1,5 @@
 (* 
-\ 5h1 class="section"\ 5Effective searching/h1\ 6
+\ 5h1 class="section"\ 6Effective searching\ 5/h1\ 6
 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 *****************)
+(* 
+\ 5h2 class="section"\ 6Unicity\ 5/h2\ 6
+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:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) l on l : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
   match l with 
@@ -126,9 +127,11 @@ let rec unique_append (S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0
      if \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a r then r else a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:r
   ].
 
-axiom unique_append_elim: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀P: S → Prop.∀l1,l2. 
+lemma unique_append_elim: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀P: S → Prop.∀l1,l2. 
 (∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"\ 6\ 5/span\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x) → (∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x) →
 ∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x. 
+#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx) /2/ 
+qed.
 
 lemma unique_append_unique: ∀S,l1,l2. \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
   \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
@@ -137,7 +140,9 @@ cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6
 #H >H normalize [@Hind //] >H normalize @Hind //
 qed.
 
-(******************* sublist *******************)
+(*
+\ 5h2 class="section"\ 6Sublists\ 5/h2\ 6
+*)
 definition sublist ≝ 
   λS,l1,l2.∀a. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 
@@ -192,7 +197,7 @@ lemma decidable_sublist:∀S,l1,l2.
   ]
 qed.
 
-(********************* filtering *****************)
+(*\ 5h2 class="section"\ 6Filtering\ 5/h2\ 6*)
 
 lemma filter_true: ∀S,f,a,l. 
   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 S f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
@@ -223,7 +228,9 @@ lemma memb_filter_l: ∀S,f,x,l. (f x \ 5a title="leibnitz's equality" href="cic:/
   ]
 qed. 
 
-(********************* exists *****************)
+(*
+\ 5h2 class="section"\ 6Exists\ 5/h2\ 6
+*)
 
 let rec exists (A:Type[0]) (p:A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
 match l with