From: matitaweb Date: Tue, 11 Oct 2011 15:48:50 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2212 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06297588aea8f5a596ea559a231e030b31a6fcfe;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index b1292601a..2de8f8558 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -1,29 +1,26 @@ 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 *) +(* 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 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 *) +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 @@ -31,17 +28,18 @@ 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 -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. +(* 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 +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. @@ -55,7 +53,7 @@ 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 +(* 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). @@ -73,8 +71,8 @@ theorem add_comm : ∀a,b. a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1) (* 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. +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. @@ -110,8 +108,8 @@ It is worth to observe that invoking automation at depth /3/ would also automati IH: ∃m. x = add m m ∨ x = S (add m m) At this point we should assume the existence of m enjoying the inductive hypothesis. To eliminate the existential from the context we can just use the case tactic. This situation where -we introduce something into the context and immediately eliminate it by case analysis is -so frequent that Matita provides a convenient shorthand: you can just type a single "*". +we introduce something into the context and immediately eliminate it by case analysis is so +frequent that Matita provides a convenient shorthand: you can just type a single "*". The star symbol should be reminiscent of an explosion: the idea is that you have a structured hypothesis, and you ask to explode it into its constituents. In the case of the existential, it allows to pass from a goal of the shape