section in chapter 2

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 11eb476e0f9cfa119e7b196f07f591497979aadf..7260a33aff9d5ef96b975289df80d1dbe2c675f8 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -1,3 +1,4 @@
+\ 5h1 class="section"\ 6Induction and Recursion\ 5/h1\ 6
 include "basics/types.ma".
 
 (* Most of the types we have seen so far are enumerated types, composed by a 
@@ -29,7 +30,9 @@ match n with
 | S a ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (add a m)
 ].
 
-(* It is worth to observe that the previous algorithm works by recursion over the
+(*
+\ 5h2 class="section"\ 6Elimination\ 5/h2\ 6
+It is worth to observe that the previous algorithm works by recursion over the
 first argument. This means that, for instance, (add O x) will reduce to x, as 
 expected, but (add x O) is stuck. 
 How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do 
@@ -96,7 +99,9 @@ definition nat_of_bool ≝ λb. match b with
 
 definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 n n. 
 
-(* We are interested to prove that for any natural number n there exists a natural 
+(* 
+\ 5h2 class="section"\ 6Existential\ 5/h2\ 6
+We are interested to prove that for any natural number n there exists a natural 
 number m that is the integer half of n. This will give us the opportunity to 
 introduce new connectives and quantifiers and, later on, to make some interesting 
 consideration on proofs and computations. *)
@@ -120,7 +125,9 @@ also automatically close G1.
 *)
   [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) %1 //
 
-(* The case of G2 is more complex. We should start introducing x and the 
+(* 
+\ 5h2 class="section"\ 6Destructuration\ 5/h2\ 6
+The case of G2 is more complex. We should start introducing x and the 
 inductive hypothesis
      IH: ∃m. x = add m m ∨ x = S (add m m) 
 At this point we should assume the existence of m enjoying the inductive 
@@ -156,7 +163,9 @@ of (S x) is hence (S m), and have to follow the left branch of the disjunction.
   ]
 qed. 
 
-(* Instead of proving the existence of a number corresponding to the half of n, 
+(* 
+\ 5h2 class="section"\ 6Computing vs. Proving\ 5/h2\ 6
+Instead of proving the existence of a number corresponding to the half of n, 
 we could be interested in computing it. The best way to do it is to define this 
 division operation together with the remainder, that in our case is just a 
 boolean value: tt if the input term is even, and ff if the input term is odd. 
@@ -222,7 +231,8 @@ lemma div2_ok: ∀n,q,r. \ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
     ]
 qed.
 
-(* There is still another possibility, however, namely to mix the program and its 
+(* \ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
+There is still another possibility, however, namely to mix the program and its 
 specification into a single entity. The idea is to refine the output type of the 
 div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a 
 specific pair satisfying the specification of the function. In other words, we need