commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 1d9359bb6332523cf89cc0da1ce1a4b01356f1a5..da0ed93fab4462bcd139fbee1b07fe1dac7a825c 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -212,6 +212,7 @@ 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,51 +271,7 @@ 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 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.
+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. *)