From: matitaweb Date: Thu, 29 Sep 2011 13:37:58 +0000 (+0000) Subject: Tutorial update. X-Git-Tag: make_still_working~2266 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3476afc7e71ac34beec061b94cf712e5ff85802f;p=helm.git Tutorial update. --- diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 7db002627..c2523f38c 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -1,37 +1,77 @@ (* -In a system like Matita's very few things are built-in: not even booleans or logical connectives. -The main philosophy od the system is to let you define your own data-types and functions using a powerful computational -mechanism based on the declaration of inductive types. - -Let us start this tutorial with a simple example based on the following well known problem. - -h2 class="section"The goat, the wolf and the cabbage/h2div class="paragraph"/divA farmer need to tranfer a goat, a wolf and a cabbage across a river, but there is only one place available -on his boat. Furthermore, the goat will eat the cabbage if they are left alone on the same bank, and similarly -the wolf will eat the goat. The problem consists in bringing all three item safely across the river. - -Our first data type defines the two banks of the river, which we will call east and west. It is a simple -example of enumerated type, defined by explicitly declaring all its elements. The type itself is called -"bank". - +In a system like Matita's very few things are built-in: not even booleans or +logical connectives. The main philosophy od the system is to let you define your +own data-types and functions using a powerful computational mechanism based on +the declaration of inductive types. + +Let us start this tutorial with a simple example based on the following well known +problem. + +h2 class="section"The goat, the wolf and the cabbage/h2div class="paragraph"/divA farmer need to tranfer a goat, a wolf and a cabbage across a river, but there is +only one place available on his boat. Furthermore, the goat will eat the cabbage if +they are left alone on the same bank, and similarly the wolf will eat the goat. +The problem consists in bringing all three item safely across the river. + +Our first data type defines the two banks of the river, which we will call east and +west. It is a simple example of enumerated type, defined by explicitly declaring all +its elements. The type itself is called "bank". +Before giving its definition we "include" the file "logic.ma" that contains a a few +preliminary notions not worth discussing here. *) -include "basics/pts.ma". +include "basics/logic.ma". inductive bank: Type[0] ≝ | east : bank | west : bank. (* We can now define a simple function computing, for each bank of the river, -the opposite one *) +the opposite one. *) definition opposite ≝ λs. match s with - [ east ⇒ west - | west ⇒ east + [ east ⇒ a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a + | west ⇒ a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a ]. -lemma east_to_west : change_side east = west. +(* Functions are live entities, and can be actually computed. To check this, let +us state the property that the opposite bank of east is west; every lemma needs a +name for further reference, and we call it "east_to_west". *) + +lemma east_to_west : a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a. + +(* If you stop the execution here you will see a new window on the right side +of the screen: it is the goal window, providing a sequent like representation of +the form + +B1 +B2 +.... +Bk +----------------------- +A + +for each open goal remaining to be solved. A is the conclusion of the goal and +B1, ..., Bk is its context, that is the set of current hypothesis and type +declarations. In this case, we have only one goal, and its context is empty. +The proof proceeds by typing commands to the system. In this case, we +want to evaluate the function, that can be done by invoking the "normalize" +command: +*) + +normalize + +(* By executing it - just type the advance command - you will see that the goal +has changed to west = west, by reducing the subexpression (opposite east). +You may use the retract bottom to undo the step, if you wish. + +The new goal west = west is trivial: it is just a consequence of reflexivity. +Such trivial steps can be just closed in Matita by typing a double slash. +We complete the proof by the qed command, that instructs the system to store the +lemma performing some bookkeeping operations. +*) + // qed. lemma west_to_east : change_side west = east.