new version

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index da0ed93fab4462bcd139fbee1b07fe1dac7a825c..1d9359bb6332523cf89cc0da1ce1a4b01356f1a5 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -212,7 +212,6 @@ expect to need several moves to transfer all items from a bank to the other, so
 we should start our proof by applying "more".
 *)
 
-(*
 lemma problem1: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.
 normalize @\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6
 
@@ -271,7 +270,51 @@ started with. *)
 
 (* 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 ca
+intermediate state, hence instead of applying more we can apply this term
+already instatated on the next intermediate state. As first argument, we
+type a question mark that stands for an implicit argument to be guessed by
+the system. *)
+
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 ? (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6))
+
+(* We now get three independent subgoals, all actives, and two of them are 
+trivial. We\ 5span style="font-family: Verdana,sans-serif;"\ 6 \ 5/span\ 6can just apply automation to all of them, and it will close the two
+trivial goals. *)
+
+/2/
+
+(* 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 
+move. In the spirit of the previous example, we can do it in the following way 
+*)
+
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"\ 6move_wolf\ 5/a\ 6 … ))
+
+(* The dots stand here for an arbitrary number of implicit arguments, to be 
+guessed by the system. 
+Unfortunately, the previous move is not enough to fully instantiate the new 
+intermediate state: a bank B remains unknown. Automation cannot help here,
+since all goals depend from this bank and automation refuses to close some
+subgoals instantiating other subgoals remaining open (the instantiation could
+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: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6] /2/
+
+(* Alternatively, we can directly instantiate the bank into the move. Let
+us complete the proof in this way. *)
+
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6 ?? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 … )) /2/
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6 ??? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
+@\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /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. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b.
  
 (* We start the proof introducing a, b and the hypothesis opp a b, that we
 call oppab. *)