commit by user andrea

[helm.git] / weblib / tutorial / chapter1.ma

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 8e27cf450e7441849c2d3ada59b8692d5f27acc8..b21fd3e1787add792e06acdb24dbf62c14dba2b0 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -23,7 +23,8 @@ computational mechanism based on the declaration of inductive types.
 Let us start this tutorial with a simple example based on the following well 
 known problem.
 
-\ 5h2 class="section"\ 6The goat, the wolf and the cabbage\ 5/h2\ 6\ 5div class="paragraph"\ 6\ 5/div\ 6A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
+\ 5h2 class="section"\ 6The goat, the wolf and the cabbage\ 5/h2\ 6
+A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
 is only one place available on his boat. Furthermore, the goat will eat the 
 cabbage if they are left alone on the same bank, and similarly the wolf will eat
 the goat. The problem consists in bringing all three items safely across the 
@@ -137,7 +138,7 @@ them in turn, in a way that will be described at the end of this section.
 (* Instead of working with functions, it is sometimes convenient to work with
 predicates. For instance, instead of defining a function computing the opposite 
 bank, we could declare a predicate stating when two banks are opposite to each 
-other. Only two cases are possible, leading naturally two the following 
+other. Only two cases are possible, leading naturally to the following 
 definition:
 *)
 
@@ -148,7 +149,8 @@ inductive opp : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6
 (* In precisely the same way as "bank" is the smallest type containing east and
 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 -
+predicate defined by the two clauses - in this case, the two facts - ast_west and
+west_east.
 
 Between opp and opposite we have the following relation:
     opp a b iff a = opposite b
@@ -210,7 +212,9 @@ definition end ≝ \ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_s
 of a relation (a binary predicate) over states. *)
 
 inductive move : \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5/a\ 6 → Prop ≝
-| move_goat: ∀g,g1,w,c. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 g g1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c g) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g1 w c g1) 
+| move_goat: ∀g,g1,w,c. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 g g1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c g) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g1 w c g1)
+  (* We can move the goat from a bank g to the opposite bank g1 if and only if the
+     boat is on the same bank g of the goat and we move the boat along with it. *)
 | move_wolf: ∀g,w,w1,c. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 w w1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c w) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w1 c w1)
 | move_cabbage: ∀g,w,c,c1.\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 c c1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c c) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c1 c1)
 | move_boat: ∀g,w,c,b,b1. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 b b1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c b) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c b1).
@@ -342,4 +346,4 @@ 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.
+@\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /2/ qed.
\ No newline at end of file