From c74a1a8237c8a05d26be0112f560d24de8cd9f0f Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 12 Dec 2011 13:58:30 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 44 +++++++++++++++++++------------------ 1 file changed, 23 insertions(+), 21 deletions(-) diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index fffe5e1cc..804ba58ba 100644 --- 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. *) -- 2.39.2