From 536fb8fcbdc36f5d860e4c7380890a355490a213 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 3 Oct 2011 10:42:28 +0000 Subject: [PATCH] new version --- weblib/tutorial/chapter1.ma | 47 +++++++++++++++++++++++++++++++++++-- 1 file changed, 45 insertions(+), 2 deletions(-) diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index da0ed93fa..1d9359bb6 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -212,7 +212,6 @@ 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 @@ -271,7 +270,51 @@ 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 ca +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. (* We start the proof introducing a, b and the hypothesis opp a b, that we call oppab. *) -- 2.39.2