From: matitaweb Date: Tue, 11 Oct 2011 16:26:12 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2210 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c1011db3fc76ca4ed011fd35e8593245403e254;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index d309eeed2..714dcb575 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -35,7 +35,7 @@ called induction. The induction principle states that, given a property P(n) ove 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. -The elim tactic, allow you to apply induction in a vcery simple way. If your goal is P(n), the +The elim tactic, allow you to apply induction in a very simple way. If your goal is P(n), the invocation of elim n will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m). @@ -81,11 +81,9 @@ For Matita, the task is trivial and we can simply close the goal 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 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. *) +(* 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. *) 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