X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter1.ma;h=8e27cf450e7441849c2d3ada59b8692d5f27acc8;hb=9b077c63115106e3b61a4f06f5c03f7a059e7f45;hp=da0ed93fab4462bcd139fbee1b07fe1dac7a825c;hpb=e8539409764826d67bae1df0b4b7f6aeda0c17c7;p=helm.git diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index da0ed93fa..8e27cf450 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -149,11 +149,45 @@ inductive opp : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a west, opp is the smallest predicate containing the two sub-cases east_west and weast_east. If you have some familiarity with Prolog, you may look at opp as the predicate definined by the two clauses - in this case, the two facts - -(opp east west) and (opp west east). -At the end of this section we shall prove that forall a and b, - (opp a b) iff a = opposite b. -For the moment, it is time to proceed with our formalization of the farmer's -problem. + +Between opp and opposite we have the following relation: + opp a b iff a = opposite b +Let us prove it, starting from the left to right implication, first *) + +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. *) +#a #b #oppab + +(* 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 *) + +cases oppab // qed. + +(* Let us come to the opposite direction. *) + +lemma opposite_to_opp: ∀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 → a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a 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 + +(* We conclude the proof by cases on b. *) + +cases b // qed. + +(* +It is time to proceed with our formalization of the farmer's problem. A state of the system is defined by the position of four item: the goat, the wolf, the cabbage, and the boat. The simplest way to declare such a data type is to use a record. @@ -204,15 +238,14 @@ 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: 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 /9/ qed. *) +lemma problem: 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 /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: 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,41 +304,42 @@ 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 - -(* We start the proof introducing a, b and the hypothesis opp a b, that we -call oppab. *) -#a #b #oppab +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. *) -(* 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 *) +@(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)) -cases oppab // qed. +(* 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. *) -(* Let us come to the opposite direction. *) +/2/ -lemma opposite_to_opp: ∀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 → a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a 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 +@(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 … )) -(* We conclude the proof by cases on b. *) +(* 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. *) -cases b // qed. +[4: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a] /2/ -(* 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/. *) +(* Alternatively, we can directly instantiate the bank into the move. Let +us complete the proof in this, very readable way. *) -lemma problem_bis: 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 /9/ \ No newline at end of file +@(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.