From: matitaweb Date: Thu, 13 Oct 2011 15:38:26 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2192 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e2f8faa727b72aeebc6eb5a49ca843dcb50dfe0;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index a4675f94e..b81ecb07c 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -96,7 +96,7 @@ definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)" (* We are interested to prove that for any natural number m there exists a natural number m that is the integer half of m. This will give us the opportunity to introduce new connectives and -quantifiers, and later on to make some interesting consideration on proofs and computations. *) +quantifiers and, later on, to make some interesting consideration on proofs and computations. *) theorem ex_half: ∀n.a title="exists" href="cic:/fakeuri.def(1)"∃/am. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m). #n elim n normalize @@ -183,7 +183,7 @@ n and a boolean indicating which one between the two conditions A(n) and B(n) is 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,tt〉 in div2. +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