Tutorial update.

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 7db002627402770106e1634d2ea9a3097f3f26e4..c2523f38c803f8472106b853b6d6e4e1d4d0d565 100644 (file)
--- 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.
-
-\ 5h2 class="section"\ 6The goat, the wolf and the cabbage\ 5/h2\ 6\ 5div class="paragraph"\ 6\ 5/div\ 6A 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.
+
+\ 5h2 class="section"\ 6The goat, the wolf and the cabbage\ 5/h2\ 6\ 5div class="paragraph"\ 6\ 5/div\ 6A 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 ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6
+  | west ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6
   ].
 
-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 : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.
+
+(* 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.