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. 
 
 (* 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 
 ].
 
 (* 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. 
 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/
   ]
 *)
   [@(\ 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