From 8075cc21208d7b0335d82eca82436f305390e7b9 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 12 Oct 2011 07:45:41 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) 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 ⇒ +| S a ⇒ +]. + + let p \def(div2 a) in + match (snd p) with + [ O ⇒ + | S b \Rightarrow + ] +]. \ No newline at end of file -- 2.39.2