commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 161cd325ce5eec0a13095a7bab4fe3ed0a3617e4..8e27cf450e7441849c2d3ada59b8692d5f27acc8 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -149,11 +149,45 @@ inductive opp : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6
 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. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b → \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 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". *)
+
+>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: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6] /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. *)
 
 @(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
 @(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6 ?? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 … )) /2/
 @(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6 ??? \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
 @\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /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. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b → \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 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". *)
-
->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: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.
-normalize /9/ qed.  *)
\ No newline at end of file