commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index d2f3b31f29ae922e5e38f88c7c640d052fda48b2..1d9359bb6332523cf89cc0da1ce1a4b01356f1a5 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -204,8 +204,8 @@ 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: \ 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 /9/ qed. 
+(* lemma problem: \ 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 /9/ qed. *)
 
 (* 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 
@@ -273,7 +273,7 @@ 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
 type a question mark that stands for an implicit argument to be guessed by
-the syste. *)
+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))
 
@@ -283,8 +283,39 @@ 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. *)
 #a #b #oppab
@@ -315,9 +346,9 @@ opposite b into a, we would have typed "<eqa". *)
 
 cases b // qed.
 
-(* Let's do now an important remark. 
-Let us state again the problem of the goat, the wolf and the cabbage, and let
-us retry to run automation. *)
+(* 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/. *)
 
 lemma problem_bis: \ 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 /9/  
\ No newline at end of file