Sections

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index 3d7eb7a56f60b61b6e5a137787c71e94f72316f9..51b810beec6309c9440679d76c6e7614c5bcfd26 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -1,3 +1,6 @@
+(*
+\ 5h1 class="section"\ 6Polymorphism and Higher Order\ 5/h1\ 6
+*)
 include "tutorial/chapter2.ma".
 include "basics/bool.ma".
 
@@ -24,7 +27,10 @@ and so on.
 
 Note that both constructos nil and cons are expecting in input the type parameter:
 in this case, bool.
+*)
 
+(*
+\ 5h2 class="section"\ 6Defining your own notation\ 5/h2\ 6
 We now add a bit of notation, in order to make the syntax more readable. In 
 particular, we would like to write [] instead of (nil A) and a::l instead of 
 (cons A a l), leaving the system the burden to infer A, whenever possible.
@@ -45,7 +51,9 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-(* Let us define a few basic functions over lists. Our first example is the 
+(* 
+\ 5h2 class="section"\ 6Basic operations on lists\ 5/h2\ 6
+Let us define a few basic functions over lists. Our first example is the 
 append function, concatenating two lists l1 and l2. The natural way is to proceed 
 by recursion on l1: if it is empty the result is simply l2, while if l1 = hd::tl 
 then we recursively append tl and l2 , and then add hd as first element. Note that 
@@ -91,7 +99,6 @@ definition tail ≝  λA.λl: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,
 example ex_head: ∀A.∀a,d,l. \ 5a href="cic:/matita/tutorial/chapter3/head.def(1)"\ 6head\ 5/a\ 6 A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) d \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6 a.
 #A #a #d #l normalize // qed.
 
-(* Problemi con la notazione *)
 example ex_tail: \ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"\ 6tail\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"\ 6cons\ 5/a\ 6 ? \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
 normalize // qed.
 
@@ -133,7 +140,9 @@ and l2 just requires a trivial induction on the first list. *)
   \ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l1) (\ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l2).
 #A #l1 elim l1 normalize // qed. 
 
-(* Let us come to a more interesting question. How can we prove that the empty 
+(* 
+\ 5h2 class="section"\ 6Comparing Costructors\ 5/h2\ 6
+Let us come to a more interesting question. How can we prove that the empty 
 list is different from any list with at least one element, that is from any list 
 of the kind (a::l)? We start defining a simple predicate stating if a list is 
 empty or not. The predicate is computed by inspection over the list *)
@@ -172,7 +181,9 @@ lemma nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind
   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
 #A #l1 cases l1 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ #a #tl #l2 #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
 
-(* Let us come to some important, higher order, polymorphic functionals 
+(* 
+\ 5h2 class="section"\ 6Higher Order Functionals\ 5/h2\ 6
+Let us come to some important, higher order, polymorphic functionals 
 acting over lists. A typical example is the map function, taking a function
 f:A → B, a list l = [a1; a2; ... ; an] and returning the list 
 [f a1; f a2; ... ; f an]. *)
@@ -218,7 +229,9 @@ of type A → list B → list B is the function mapping a and l to (f a)::l.
 
 definition map_again ≝ λA,B,f,l. \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 A (\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) (λa,l.f a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] l.
 
-(* Can we prove that map_again is "the same" as map? We should first of all
+(* 
+\ 5h2 class="section"\ 6Extensional equality\ 5/h2\ 6
+Can we prove that map_again is "the same" as map? We should first of all
 clarify in which sense we expect the two functions to be equal. Equality in
 Matita has an intentional meaning: it is the smallest predicate induced by 
 convertibility, i.e. syntactical equality up to normalization. From an 
@@ -251,9 +264,9 @@ inductive types; again the rest of the proof is trivial. *)
 
 #l (elim l) normalize // qed.
 
-(**************************** BIGOPS *******************************)
-
-(* Building a library of basic functions, it is important to achieve a 
+(*
+\ 5h2 class="section"\ 6Big Operators\ 5/h2\ 6
+Building a library of basic functions, it is important to achieve a 
 good degree of abstraction and generality, in order to be able to reuse
 suitable instances of the same function in different context. This has not
 only the obvious benefit of factorizing code, but especially to avoid