From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Oct 2011 07:45:41 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~2206
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8075cc21208d7b0335d82eca82436f305390e7b9;p=helm.git

commit by user andrea
---

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 714dcb575..449838e3a 100644
--- 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.
 *)
   [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … m) /2/ | @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a 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