From: matitaweb Date: Mon, 3 Oct 2011 10:16:02 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2248 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e8539409764826d67bae1df0b4b7f6aeda0c17c7;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 1d9359bb6..da0ed93fa 100644 --- 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: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a. normalize @a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a @@ -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. *) - -@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a ? (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a)) - -(* We now get three independent subgoals, all actives, and two of them are -trivial. Wespan style="font-family: Verdana,sans-serif;" /spancan 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 -*) - -@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"move_wolf/a … )) - -(* 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: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a] /2/ - -(* Alternatively, we can directly instantiate the bank into the move. Let -us complete the proof in this way. *) - -@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /2/ -@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a ?? a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a … )) /2/ -@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a ??? a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /2/ -@a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a /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. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a a b → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter1/opposite.def(1)"opposite/a 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. *)