From bf776a7d58bdee34f479e3236f7c220bdfca669a Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 17 Oct 2011 07:13:18 +0000 Subject: [PATCH] commit by user lroversi --- weblib/tutorial/chapter1.ma | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 8e27cf450..6598df5c1 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -23,7 +23,7 @@ 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. -h2 class="section"The goat, the wolf and the cabbage/h2div class="paragraph"/divA farmer need to transfer a goat, a wolf and a cabbage across a river, but there +h2 class="section"The goat, the wolf and the cabbage/h2A 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 +137,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: *) @@ -210,7 +210,12 @@ definition end ≝ a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_s of a relation (a binary predicate) over states. *) inductive move : a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"state/a → Prop ≝ -| move_goat: ∀g,g1,w,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a g g1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g1 w c g1) +| move_goat: ∀g,g1,w,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a g g1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g1 w c g1) + (* Every time g and g1 are two opposite banks, it is legal to put + the state "a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c g", which says that goat and boat are on the same bank g, + and the state "a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g1 w c g1", which says that goat and boat are on the same bank g1 + in the relation "move" because, for example, moving the goat from bank g to bank g1 requires + moving the boat as well. *) | move_wolf: ∀g,w,w1,c. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a w w1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c w) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w1 c w1) | move_cabbage: ∀g,w,c,c1.a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a c c1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c c) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c1 c1) | move_boat: ∀g,w,c,b,b1. a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"opp/a b b1 → move (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c b) (a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"mk_state/a g w c b1). @@ -342,4 +347,4 @@ 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. +@a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a /2/ qed. \ No newline at end of file -- 2.39.2