X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter1.ma;h=4cf145d60f53f72c70b08846444700cd9b1afc7e;hb=f38fd769279794d0ca73c8945eac30e8b42e59be;hp=1d9359bb6332523cf89cc0da1ce1a4b01356f1a5;hpb=d96286a3200435e740518023ddecd5ce95435d8d;p=helm.git

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 1d9359bb6..4cf145d60 100644
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -1,4 +1,5 @@
-(*
+(* 
+h1Matita Interactive Tutorial/h1
 This is an interactive tutorial. To let you interact on line with the system, 
 you must first of all register yourself.
 
@@ -15,15 +16,20 @@ a file. The play button is meant to process the script up to a position
 previously selected by the user; the bottom button execute the whole script. 
 That's it: we arespan style="font-family: Verdana,sans-serif;" /spannow ready to start.
 
-The first thing to say is that in a system like Matita's very few things are 
-built-in: not even booleans or logical connectives. The main philosophy of 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. 
+h2 class="section"Data types, functions and theorems/h2
+Matita is both a programming language and a theorem proving environment:
+you define datatypes and programs, and then prove properties on them.
+Very few things are built-in: not even booleans or logical connectives
+(but you may of course use libraries, as in normal programming languages). 
+The main philosophy of 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 transfer a goat, a wolf and a cabbage across a river, but there
+bThe goat, the wolf and the cabbage/b
+A farmer need to transfer 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 items safely across the 
@@ -38,14 +44,14 @@ few preliminary notions not worth discussing for the moment.
 
 include "basics/logic.ma".
 
-inductive bank: Type[0] ≝
+img class="anchor" src="icons/tick.png" id="bank"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. *)
 
-definition opposite ≝ λs.
+img class="anchor" src="icons/tick.png" id="opposite"definition opposite ≝ λs.
 match s with
   [ 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
@@ -55,9 +61,11 @@ match s with
 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.
+img class="anchor" src="icons/tick.png" id="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
+(* 
+h2 class="section"The goal window/h2
+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
 
@@ -94,13 +102,14 @@ lemma performing some book-keeping operations.
 In this case, we avoid the unnecessary simplification step: // will take care of 
 it. *) 
 
-lemma west_to_east : a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
+img class="anchor" src="icons/tick.png" id="west_to_east"lemma west_to_east : a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
 // qed.
 
-(* A slightly more complex problem consists in proving that opposite is 
-idempotent *)
+(*
+h2 class="section"Introduction/h2
+A slightly more complex problem consists in proving that opposite is idempotent *)
 
-lemma idempotent_opposite : ∀x. a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a (a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
+img class="anchor" src="icons/tick.png" id="idempotent_opposite"lemma idempotent_opposite : ∀x. a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a (a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a x) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
 
 (* we start the proof moving x from the conclusion into the context, that is a 
 (backward) introduction step. Matita syntax for an introduction step is simply 
@@ -113,7 +122,10 @@ wish to rename x into b (since it is a bank), we just type #b. *)
 (* See the effect of the execution in the goal window on the right: b has been 
 added to the context (replacing x in the conclusion); moreover its implicit type 
 "bank" has been made explicit. 
+*)
 
+(*
+h2 class="section"Case analysis/h2
 But how are we supposed to proceed, now? Simplification cannot help us, since b
 is a variable: just try to call normalize and you will see that it has no effect.
 The point is that we must proceed by cases according to the possible values of b,
@@ -134,32 +146,72 @@ them in turn, in a way that will be described at the end of this section.
 
 // qed.
 
-(* Instead of working with functions, it is sometimes convenient to work with
+(* 
+h2 class="section"Predicates/h2
+Instead of working with functions, it is sometimes convenient to work with
 predicates. For instance, instead of defining a function computing the opposite 
 bank, we could declare a predicate stating when two banks are opposite to each 
-other. Only two cases are possible, leading naturally two the following 
+other. Only two cases are possible, leading naturally to the following 
 definition:
 *)
 
-inductive opp : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a → a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a → Prop ≝ 
+img class="anchor" src="icons/tick.png" id="opp"inductive opp : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a → a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a → Prop ≝ 
 | east_west : opp a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a
 | west_east : opp a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
 
 (* In precisely the same way as "bank" is the smallest type containing east and
 west, opp is the smallest predicate containing the two sub-cases east_west and
 weast_east. If you have some familiarity with Prolog, you may look at opp as the
-predicate definined by the two clauses - in this case, the two facts -
-(opp east west) and (opp west east). 
-At the end of this section we shall prove that forall a and b, 
-                  (opp a b) iff a = opposite b.
-For the moment, it is time to proceed with our formalization of the farmer's 
-problem. 
-A state of the system is defined by the position of four item: the goat, the 
+predicate defined by the two clauses - in this case, the two facts - ast_west and
+west_east.
+
+Between opp and opposite we have the following relation:
+    opp a b iff a = opposite b
+Let us prove it, starting from the left to right implication, first *)
+
+img class="anchor" src="icons/tick.png" id="opp_to_opposite"lemma opp_to_opposite: ∀a,b. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a a b → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a b.
+ 
+(* We start the proof introducing a, b and the hypothesis opp a b, that we
+call oppab. *)
+#a #b #oppab
+
+(* Now we proceed by cases on the possible proofs of (opp a b), that is on the 
+possible shapes of oppab. By definition, there are only two possibilities, 
+namely east_west or west_east. Both subcases are trivial, and can be closed by
+automation *)
+
+cases oppab // qed.
+
+(* 
+h2 class="section"Rewriting/h2
+Let us come to the opposite direction. *)
+
+img class="anchor" src="icons/tick.png" id="opposite_to_opp"lemma opposite_to_opp: ∀a,b. a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a b → a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a a b.
+
+(* As usual, we start introducing a, b and the hypothesis (a = opposite b), 
+that we call eqa. *)
+
+#a #b #eqa
+
+(* The right way to proceed, now, is by rewriting a into (opposite b). We do
+this by typing ">eqa". If we wished to rewrite in the opposite direction, namely
+opposite b into a, we would have typed "<eqa". *)
+
+>eqa
+
+(* We conclude the proof by cases on b. *)
+
+cases b // qed.
+
+(*
+h2 class="section"Records/h2
+It is time to proceed with our formalization of the farmer's problem. 
+A state of the system is defined by the position of four items: the goat, the 
 wolf, the cabbage, and the boat. The simplest way to declare such a data type
 is to use a record.
 *)
 
-record state : Type[0] ≝
+img class="anchor" src="icons/tick.png" id="state"record state : Type[0] ≝
   {goat_pos : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a;
    wolf_pos : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a;
    cabbage_pos: a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a;
@@ -169,14 +221,16 @@ record state : Type[0] ≝
 constructor named mk_foo. To construct a new record you pass as arguments to 
 mk_foo the values of the record fields *)
 
-definition start ≝ a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
-definition end ≝ a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a.
+img class="anchor" src="icons/tick.png" id="start"definition start ≝ a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a.
+img class="anchor" src="icons/tick.png" id="end"definition end ≝ a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a.
 
 (* We must now define the possible moves. A natural way to do it is in the form 
 of a relation (a binary predicate) over states. *)
 
-inductive move : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
-| move_goat: ∀g,g1,w,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a g g1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g1 w c g1) 
+img class="anchor" src="icons/tick.png" id="move"inductive move : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
+| move_goat: ∀g,g1,w,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a g g1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g1 w c g1)
+  (* We can move the goat from a bank g to the opposite bank g1 if and only if the
+     boat is on the same bank g of the goat and we move the boat along with it. *)
 | move_wolf: ∀g,w,w1,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a w w1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c w) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w1 c w1)
 | move_cabbage: ∀g,w,c,c1.a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a c c1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c c) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c1 c1)
 | move_boat: ∀g,w,c,b,b1. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a b b1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c b) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c b1).
@@ -184,7 +238,7 @@ inductive move : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state
 (* A state is safe if either the goat is on the same bank of the boat, or both 
 the wolf and the cabbage are on the opposite bank of the goat. *)
 
-inductive safe_state : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
+img class="anchor" src="icons/tick.png" id="safe_state"inductive safe_state : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
 | with_boat : ∀g,w,c.safe_state (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g)
 | opposite_side : ∀g,g1,b.a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a g g1 → safe_state (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g g1 g1 b).
 
@@ -192,11 +246,13 @@ inductive safe_state : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"
 leading from x to y, or there is a safe state z such that z is reachable from x 
 and there is a move leading from z to y *)
 
-inductive reachable : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
+img class="anchor" src="icons/tick.png" id="reachable"inductive reachable : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝
 | one : ∀x,y.a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"move/a x y → reachable x y
 | more : ∀x,z,y. span style="text-decoration: underline;"/spanreachable x z → a href="cic:/matita/tutorial/chapter1/safe_state.ind(1,0,0)"safe_state/a z → span style="text-decoration: underline;"/spana href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"move/a z y → reachable x y.
 
-(* Remarkably, Matita is now able to solve the problem by itslef, provided
+(* 
+h2 class="section"Automation/h2
+Remarkably, Matita is now able to solve the problem by itslef, provided
 you allow automation to exploit more resources. The command /n/ is similar to
 //, where n is a measure of this complexity: in particular it is a bound to
 the depth of the expected proof tree (more precisely, to the number of nested
@@ -204,18 +260,27 @@ applicative nodes). In this case, there is a solution in six moves, and we
 need a few more applications to handle reachability, and side conditions. 
 The magic number to let automation work is, in this case, 9.  *)
 
-(* lemma problem: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
-normalize /9/ qed. *)
+img class="anchor" src="icons/tick.png" id="problem"lemma problem: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
+normalize /span class="autotactic"9span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a, a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a, a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"move_wolf/a, a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a, a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/ qed. 
 
-(* Let us now try to derive the proof in a more interactive way. Of course, we
+(* 
+h2 class="section"Application/h2
+Let us now try to derive the proof in a more interactive way. Of course, we
 expect to need several moves to transfer all items from a bank to the other, so 
-we should start our proof by applying "more".
+we should start our proof by applying "more". Matita syntax for invoking the 
+application of a property named foo is to write "@foo". In general, the philosophy 
+of Matita is to describe each proof of a property P as a structured collection of 
+objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining 
+the way it is actually used (e.g. for introduction, rewriting, in an applicative 
+step, and so on).
 *)
 
-lemma problem1: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
+img class="anchor" src="icons/tick.png" id="problem1"lemma problem1: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
 normalize @a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a
 
-(* We have now four open subgoals:
+(* 
+h2 class="section"Focusing/h2
+After performing the previous application, we have four open subgoals:
 
   X : STATE
   Y : reachable [east,east,east,east] X
@@ -266,9 +331,11 @@ requires /2/ since move_goat opens an additional subgoal. By applying "]" we
 refocus on the skipped goal, going back to a situation similar to the one we
 started with. *)
 
-  | /2/ ] 
+  | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/ ] 
 
-(* Let us perform the next step, namely moving back the boat, in a sligtly 
+(* 
+h2 class="section"Implicit arguments/h2
+Let us perform the next step, namely moving back the boat, in a sligtly 
 different way. The more operation expects as second argument the new 
 intermediate state, hence instead of applying more we can apply this term
 already instatated on the next intermediate state. As first argument, we
@@ -281,7 +348,7 @@ the system. *)
 trivial. Wespan style="font-family: Verdana,sans-serif;" /spancan just apply automation to all of them, and it will close the two
 trivial goals. *)
 
-/2/
+/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
 
 (* Let us come to the next step, that consists in moving the wolf. Suppose that 
 instead of specifying the next intermediate state, we prefer to specify the next 
@@ -300,55 +367,12 @@ be arbitrary). The simplest way to proceed is to focus on the bank, that is
 the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|",
 we can perform focusing by typing "4:" as described by the following command. *)
 
-[4: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a] /2/
+[4: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/
 
 (* Alternatively, we can directly instantiate the bank into the move. Let
-us complete the proof in this way. *)
-
-@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /2/
-@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a ?? a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a … )) /2/
-@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a ??? a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /2/
-@a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a /2/ qed.
-
-(* Let us now go back to the problem of proving that, for all a and b,
-   (opp a b) iff a = opposite b.
-Let us start from the first implication. *)
-
-lemma opp_to_opposite: ∀a,b. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a a b → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a b.
- 
-(* We start the proof introducing a, b and the hypothesis opp a b, that we
-call oppab. *)
-#a #b #oppab
-
-(* Now we proceed by cases on the possible proofs of (opp a b), that is on the 
-possible shapes of oppab. By definition, there are only two possibilities, 
-namely east_west or west_east. Both subcases are trivial, and can be closed by
-automation *)
-
-cases oppab // qed.
-
-(* Let us come to the opposite direction. *)
-
-lemma opposite_to_opp: ∀a,b. a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a b → a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a a b.
-
-(* As usual, we start introducing a, b and the hypothesis (a = opposite b), 
-that we call eqa. *)
-
-#a #b #eqa
-
-(* The right way to proceed, now, is by rewriting a into (opposite b). We do
-this by typing ">eqa". If we wished to rewrite in the opposite direction, namely
-opposite b into a, we would have typed "<eqa". *)
-
->eqa
-
-(* We conclude the proof by cases on b. *)
-
-cases b // qed.
-
-(* Let's do now an important remark.
-Comment both problem and problem1, state another time the problem of the goat, the
-wolf and the cabbage, and try again to run automation at level /9/. *)
+us complete the proof in this, very readable way. *)
 
-lemma problem_bis: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
-normalize /9/  
\ No newline at end of file
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a ?? a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a ??? a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/ qed.
\ No newline at end of file