From ea12b736382320bcedad780ec0eb522ff5cc35a5 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 11 Oct 2011 11:08:50 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter1.ma | 89 +++++++++++++++++-------------------- 1 file changed, 40 insertions(+), 49 deletions(-) diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 161cd325c..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. @@ -303,52 +337,9 @@ 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. *) +us complete the proof in this, very readable 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. *) -#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. - -(* 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/. - -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/ qed. *) \ No newline at end of file -- 2.39.2