X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;h=2942d61524b941cc00daa7c6e59adb49bf974416;hb=30172d86a0cd979e44ae3343655f6ce55043dd52;hp=11eb476e0f9cfa119e7b196f07f591497979aadf;hpb=7956b9a84e0556d2d24fffedbbbabcd9e248d702;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 11eb476e0..2942d6152 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -1,3 +1,6 @@
+(*
+h1 class="section"Induction and Recursion/h1
+*)
 include "basics/types.ma".
 
 (* Most of the types we have seen so far are enumerated types, composed by a 
@@ -29,7 +32,9 @@ match n with
 | S a ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (add a m)
 ].
 
-(* It is worth to observe that the previous algorithm works by recursion over the
+(*
+h2 class="section"Elimination/h2
+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 +101,9 @@ definition nat_of_bool ≝ λb. match b with
 
 definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a n n. 
 
-(* We are interested to prove that for any natural number n there exists a natural 
+(* 
+h2 class="section"Existential/h2
+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 +127,9 @@ also automatically close G1.
 *)
   [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) %1 //
 
-(* The case of G2 is more complex. We should start introducing x and the 
+(* 
+h2 class="section"Destructuration/h2
+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 +165,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, 
+(* 
+h2 class="section"Computing vs. Proving/h2
+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 +233,9 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
     ]
 qed.
 
-(* There is still another possibility, however, namely to mix the program and its 
+(* 
+h2 class="section"Mixing proofs and computations/h2
+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 
@@ -271,4 +284,4 @@ example quotient7: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"wi
 example quotient8: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"witness/a … (a href="cic:/matita/tutorial/chapter2/div2Pagain.def(4)"div2Pagain/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a)))))) 
        a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a))), a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
 // qed. 
-prepre /pre/pre
\ No newline at end of file
+prepre /pre/pre