commit by user andrea

[helm.git] / weblib / tutorial / chapter1.ma

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index d2f3b31f29ae922e5e38f88c7c640d052fda48b2..da0ed93fab4462bcd139fbee1b07fe1dac7a825c 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -204,14 +204,15 @@ 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 
 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
 
@@ -270,21 +271,8 @@ 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 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. *)
-
-@(\ 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/
-
-(*  *)
-
+intermediate state, hence instead of applying more we ca
+ 
 (* We start the proof introducing a, b and the hypothesis opp a b, that we
 call oppab. *)
 #a #b #oppab
@@ -315,9 +303,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