From: matitaweb Date: Tue, 11 Oct 2011 14:18:38 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2215 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0747f3cb4a22db0024aacaa46e98eccb69ee72d;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index a32e29ba6..fba2b61ca 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -1,15 +1,99 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "arithmetics/nat.ma". +include "basics/logic.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. A more interesting case of type definition is +when some of the rules defining its elements are recursive, i.e. they +allow the formation of more elements of the type in terms of the already +defined ones. The most typical case is provided by the natural numbers, +that can be defined as the smallest set generated by a constant 0 and a +successor function from natural numbers to natural numbers *) + +inductive nat : Type[0] ≝ +| O :nat +| S: nat →nat. + +(* The two terms O and S are called constructors: they define the +signature of the type, whose objects are the elements freely generated +by means of them. So, examples of natural numbers are O, S O, S (S O), +S (S (S O)) and so on. + +The language of Matita allows the definition of well founded recursive functions +over inductive types; in order to guarantee termination of recursion you are +only allowed to make recursive calls on structurally smaller arguments than the +ones your received in input. +Most mathematical functions can be naturally defined in this way. For instance, +the sum of two natural numbers can be defined as follows *) + +let rec add n m ≝ +match n with +[ O ⇒ m +| 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 +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 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. + +The elim tactic, allow you to apply induction in a vcery 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). +Let us apply it to our case *) + +lemma add_0: ∀a. a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a. +#a elim a + +(* If you stop the computation here, you will see on the right the two subgoals + - add O O = O + - ∀x. add x 0 = x → add (S x) O = S x +After normalization, both goals are trivial. +*) + +normalize // qed. + + (* In a similar way, it is convenient to state a lemma about the behaviour of add when the +second argument is not zero. *) + +lemma add_S : ∀a,b. a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a b) 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/add.fix(0,0,1)"add/a a b). + +(* In the same way as before, we proceed by induction over a. *) + +#a #b elim a normalize // +qed. + +(* We are now in the position to prove the commutativity of the sum *) + +theorem add_comm : ∀a,b. a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a b a. +#a elim a normalize + +(* We have two sub goals: + G1: ∀b. b = add b O + G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x). +G1 is just our lemma add_O. For G2, we start introducing x and the induction +hypothesis IH; then, the goal is proved by rewriting using add_S and IH. +For Matita, the task is trivial and we can simply close the goal with // *) + +// qed. + +(* Let us now define the following function: *) + +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. *) + +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). + + + + include "basics.ma". include "basics/list.ma". interpretation "iff" 'iff a b = (iff a b).