commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 714dcb575db9e7f3f34a61a5d04a5000628b3d64..449838e3afe4ebb1b0bab1db44adef34736e445c 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -1,4 +1,4 @@
-include "basics/logic.ma".
+include "basics/types.ma".
 
 (* Most of the types we have seen so far are enumerated types, composed by a finite set of 
 alternatives, and records, composed by tuples of heteregoneous elements. 
@@ -29,8 +29,8 @@ match n with
 ].
 
 (* It is worth to observe that the previous algorithm works by recursion over the first 
-argument. This means that, for instance, (add 0 x) will reduce to x, as expected, but (add x 0)
-is stack. How can we prove that, for a generic x, (add x 0) = x? The mathematical tool do it is 
+argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O)
+is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool do it is 
 called induction. The induction principle states that, given a property P(n) over natural 
 numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude
 P(n) for any n. 
@@ -134,4 +134,24 @@ is hence (S m), and have to follow the left branch of the disjunction.
 *)
   [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … m) /2/ | @(\ 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,2,0)"\ 6S\ 5/a\ 6 m)) normalize /2/
   ]
-qed. 
\ No newline at end of file
+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 is 0 if the input term is even, and 1 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 N × N, defined in the basic library. The product type is just a sort of
+general purpose record, with standard fields fst and snd, called projections. *)
+
+let rec div2 n ≝ 
+match n with
+[ O ⇒ <O,O>
+| S a ⇒ <O,O>
+].
+
+ let p \def(div2 a) in
+   match (snd p) with
+   [ O ⇒ <fst p,1>
+   | S b \Rightarrow <S(fst p),O>  
+   ]
+]. 
\ No newline at end of file