X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter1.ma;h=8e27cf450e7441849c2d3ada59b8692d5f27acc8;hb=9b077c63115106e3b61a4f06f5c03f7a059e7f45;hp=d2f3b31f29ae922e5e38f88c7c640d052fda48b2;hpb=718502fc6c07233d2c6940d95d39419c3a14cfa1;p=helm.git diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index d2f3b31f2..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. @@ -273,7 +307,7 @@ 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 syste. *) +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)) @@ -283,41 +317,29 @@ trivial goals. *) /2/ -(* *) - -(* 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 +@(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. -Let us state again the problem of the goat, the wolf and the cabbage, and let -us retry to run automation. *) +(* 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.