From 718502fc6c07233d2c6940d95d39419c3a14cfa1 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 3 Oct 2011 09:29:37 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter1.ma | 73 ++++++++++++++++++++++--------------- 1 file changed, 43 insertions(+), 30 deletions(-) diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 69466662a..d2f3b31f2 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -213,8 +213,7 @@ 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 +normalize @a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a (* We have now four open subgoals: @@ -271,40 +270,54 @@ 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 its -instantiation (more ? (mk_state east west west west)). The question mark is -an implicit argument to be guessed by the system. *) +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. *) -span style="text-decoration: underline;"/span@(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)) +@(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)) -(* All subgoals are focused (they are all red). Two of them are trivial; we -just call automation at level 2, and it will close both of them, taking -us to the third move.*) +(* 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/ +/2/ -(* We must now move the wolf. Suppose that, instead of specifying the next state -we prefer to specify the move. In the style of the previous move, this amounts -to apply the term (more … (move_wolf … )) The dots are a convenient syntax to -express an arbitrary number of implicit parameters. *) +(* *) -@(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 start the proof introducing a, b and the hypothesis opp a b, that we +call oppab. *) +#a #b #oppab -(* Unfortunately this is not enough to fully instantiate the intermediate state. -All goals still depend from an unknown bank B. Calling automation in this situation -does not help since it refuses to close subgoals instantiating other - still -open - goals. A way to proceed is to focus on the fourth "bank" subgoal, -instantiating it with the appropriate value, in this case east; then we close -focusing, and call automation. To focus on subgoal i, instead of typing "|" several -times we can just write "i:" as described by the following command. *) +(* 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 *) - [4: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/aspan style="text-decoration: underline;"/span] /2/ +cases oppab // qed. -(* An alternative, simpler way is to instantiate each move with the destination -bank. Let us complete the proof adopting this style. *) +(* Let us come to the opposite direction. *) -@(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. \ No newline at end of file +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. + +(* 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. *) + +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 -- 2.39.2