From: matitaweb Date: Wed, 7 Mar 2012 10:26:46 +0000 (+0000) Subject: section in chapter 2 X-Git-Tag: make_still_working~1884 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4a04a5af0748535ad7522c2a95dd3ae4344eac7;p=helm.git section in chapter 2 --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 11eb476e0..7260a33af 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -1,3 +1,4 @@ +h1 class="section"Induction and Recursion/h1 include "basics/types.ma". (* Most of the types we have seen so far are enumerated types, composed by a @@ -29,7 +30,9 @@ match n with | S a ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (add a m) ]. -(* It is worth to observe that the previous algorithm works by recursion over the +(* +h2 class="section"Elimination/h2 +It is worth to observe that the previous algorithm works by recursion over the first argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O) is stuck. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do @@ -96,7 +99,9 @@ definition nat_of_bool ≝ λb. match b with definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a n n. -(* We are interested to prove that for any natural number n there exists a natural +(* +h2 class="section"Existential/h2 +We are interested to prove that for any natural number n there exists a natural number m that is the integer half of n. This will give us the opportunity to introduce new connectives and quantifiers and, later on, to make some interesting consideration on proofs and computations. *) @@ -120,7 +125,9 @@ also automatically close G1. *) [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a) %1 // -(* The case of G2 is more complex. We should start introducing x and the +(* +h2 class="section"Destructuration/h2 +The case of G2 is more complex. We should start introducing x and the inductive hypothesis IH: ∃m. x = add m m ∨ x = S (add m m) At this point we should assume the existence of m enjoying the inductive @@ -156,7 +163,9 @@ of (S x) is hence (S m), and have to follow the left branch of the disjunction. ] qed. -(* Instead of proving the existence of a number corresponding to the half of n, +(* +h2 class="section"Computing vs. Proving/h2 +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. @@ -222,7 +231,8 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)" ] qed. -(* There is still another possibility, however, namely to mix the program and its +(* h2 class="section"Mixing proofs and computations/h2 +There is still another possibility, however, namely to mix the program and its specification into a single entity. The idea is to refine the output type of the div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a specific pair satisfying the specification of the function. In other words, we need