commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 69466662ae9a1869ec177f508f6747c0c0540bf9..d2f3b31f29ae922e5e38f88c7c640d052fda48b2 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -213,8 +213,7 @@ 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
+normalize @\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6
 
 (* We have now four open subgoals:
 
@@ -271,40 +270,54 @@ 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 its 
-instantiation (more ? (mk_state east west west west)). The question mark is 
-an implicit argument to be guessed by the system. *)
+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. *)
 
-\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6@(\ 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)) 
+@(\ 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))
 
-(* All subgoals are focused (they are all red). Two of them are trivial; we
-just call automation at level 2, and it will close both of them, taking
-us to the third move.*)
+(* 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/ 
+/2/
 
-(* We must now move the wolf. Suppose that, instead of specifying the next state 
-we prefer to specify the move. In the style of the previous move, this amounts
-to apply the term (more … (move_wolf … )) The dots are a convenient syntax to 
-express an arbitrary number of implicit parameters. *) 
+(*  *)
 
-@(\ 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 … ))
+(* We start the proof introducing a, b and the hypothesis opp a b, that we
+call oppab. *)
+#a #b #oppab
 
-(* Unfortunately this is not enough to fully instantiate the intermediate state.
-All goals still depend from an unknown bank B. Calling automation in this situation
-does not help since it refuses to close subgoals instantiating other - still 
-open - goals. A way to proceed is to focus on the fourth "bank" subgoal,
-instantiating it with the appropriate value, in this case east; then we close 
-focusing, and call automation. To focus on subgoal i, instead of typing "|" several
-times we can just write "i:" as described by the following command. *)
+(* 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 *)
 
-  [4: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6]  /2/
+cases oppab // qed.
 
-(* An alternative, simpler way is to instantiate each move with the destination
-bank. Let us complete the proof adopting this style. *)
+(* Let us come to the opposite direction. *)
 
-@(\ 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.
\ No newline at end of file
+lemma opposite_to_opp: ∀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 → \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 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. 
+Let us state again the problem of the goat, the wolf and the cabbage, and let
+us retry to run automation. *)
+
+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