commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index fffe5e1cce96f933c9395dcaacfa42cb2953f89b..804ba58ba3c74d6771881c10e131f5bfa8478868 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -158,13 +158,14 @@ qed.
 
 (* 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. Since we 
-must return a pair, we could use a suitably defined record type, or simply a product 
-type nat × bool, defined in the basic library. The product type is just a sort of 
-general purpose record, with standard fields fst and snd, called projections. 
-A pair of values n and m is written (pair … m n) or \langle n,m \rangle - 
-visually rendered as 〈n,m〉 
+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. 
+Since we must return a pair, we could use a suitably defined record type, or 
+simply a product type nat × bool, defined in the basic library. The product type 
+is just a sort of general purpose record, with standard fields fst and snd, called 
+projections. 
+A pair of values n and m is written (pair … m n) or \langle n,m \rangle - visually 
+rendered as 〈n,m〉 
 
 We first write down the function, and then discuss it.*)
 
@@ -182,20 +183,21 @@ match n with
 (* The function is computed by recursion over the input n. If n is 0, then the 
 quotient is 0 and the remainder is tt. If n = S a, we start computing the half 
 of a, say 〈q,b〉. Then we have two cases according to the possible values of b: 
-if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return 〈S q,tt〉.
-
-It is important to point out the deep, substantial analogy between the algorithm for 
-computing div2 and the the proof of ex_half. In particular ex_half returns a 
-proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the witness
-n and a boolean indicating which one between the two conditions A(n) and B(n) is met.
-This is precisely the quotient-remainder pair returned by div2.
-In both cases we proceed by recurrence (respectively, induction or recursion) over the 
-input argument n. In case n = 0, we conclude the proof in ex_half by providing the
-witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in div2.
-Similarly, in the inductive case n = S a, we must exploit the inductive hypothesis 
-for a (i.e. the result of the recursive call), distinguishing two subcases according 
-to the the two possibilites A(a) or B(a) (i.e. the two possibile values of the remainder 
-for a). The reader is strongly invited to check all remaining details.
+if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return 
+〈S q,tt〉.
+
+It is important to point out the deep, substantial analogy between the algorithm 
+for computing div2 and the the proof of ex_half. In particular ex_half returns a 
+proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the 
+witness n and a boolean indicating which one between the two conditions A(n) and 
+B(n) is met. This is precisely the quotient-remainder pair returned by div2.
+In both cases we proceed by recurrence (respectively, induction or recursion) over 
+the input argument n. In case n = 0, we conclude the proof in ex_half by providing 
+the witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in 
+div2. Similarly, in the inductive case n = S a, we must exploit the inductive 
+hypothesis for a (i.e. the result of the recursive call), distinguishing two subcases 
+according to the the two possibilites A(a) or B(a) (i.e. the two possibile values of 
+the remainder for a). The reader is strongly invited to check all remaining details.
 
 Let us now prove that our div2 function has the expected behaviour.
 *)