-(*
-definition legal_state ≝ λs.
- goat_pos s = boat_pos s ∨
- (goat_pos s = change_side (cabbage_pos s) ∧
- goat_pos s = change_side (wolf_pos s)). *)
-
-inductive legal_state : state → Prop ≝
-| with_boat : ∀g,w,c.legal_state (mk_state g w c g)
-| opposite_side : ∀g,b.
- legal_state (mk_state g (change_side g) (change_side g) b).
-
-inductive reachable : state → state → Prop ≝
-| one : ∀s1,s2.move s1 s2 → reachable s1 s2
-| more : ∀s1,s2,s3. reachable s1 s2 → legal_state s2 → move s2 s3 →
- reachable s1 s3.
-
-definition end ≝ mk_state west west west west.
-definition second ≝ mk_state west east east west.
-definition third ≝ mk_state west east east east.
-definition fourth ≝ mk_state west west east west.
-definition fifth ≝ mk_state east west east east.
-definition sixth ≝ mk_state east west west west.
-definition seventh ≝ mk_state east west west east.
-
-lemma problem: reachable start end.
-normalize /8/ qed.
-
-lemma problem: reachable start end.
-normalize
-@more [4: @move_goat || 3: //]
-@more [4: @move_boat || 3: //]
-@more [4: @move_wolf || 3: //]
-@more [4: @move_goat || 3: //]
-@more [4: @move_cabbage || 3: //]
-@more [4: @move_boat || 3: //]
-@one //
-qed.
+\ 5img class="anchor" src="icons/tick.png" id="state"\ 6record state : Type[0] ≝
+ {goat_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
+ wolf_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
+ cabbage_pos: \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
+ boat_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6}.
+
+(* When you define a record named foo, the system automatically defines a record
+constructor named mk_foo. To construct a new record you pass as arguments to
+mk_foo the values of the record fields *)
+
+\ 5img class="anchor" src="icons/tick.png" id="start"\ 6definition start ≝ \ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="end"\ 6definition end ≝ \ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.
+
+(* We must now define the possible moves. A natural way to do it is in the form
+of a relation (a binary predicate) over states. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="move"\ 6inductive 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)
+ (* 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).
+
+(* A state is safe if either the goat is on the same bank of the boat, or both
+the wolf and the cabbage are on the opposite bank of the goat. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="safe_state"\ 6inductive safe_state : \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5/a\ 6 → Prop ≝
+| with_boat : ∀g,w,c.safe_state (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c g)
+| opposite_side : ∀g,g1,b.\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 g g1 → safe_state (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g g1 g1 b).
+
+(* Finally, a state y is reachable from x if either there is a single move
+leading from x to y, or there is a safe state z such that z is reachable from x
+and there is a move leading from z to y *)
+
+\ 5img class="anchor" src="icons/tick.png" id="reachable"\ 6inductive reachable : \ 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 ≝
+| one : ∀x,y.\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"\ 6move\ 5/a\ 6 x y → reachable x y
+| more : ∀x,z,y. \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6reachable x z → \ 5a href="cic:/matita/tutorial/chapter1/safe_state.ind(1,0,0)"\ 6safe_state\ 5/a\ 6 z → \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"\ 6move\ 5/a\ 6 z y → reachable x y.
+
+(*
+\ 5h2 class="section"\ 6Automation\ 5/h2\ 6
+Remarkably, Matita is now able to solve the problem by itslef, provided
+you allow automation to exploit more resources. The command /n/ is similar to
+//, where n is a measure of this complexity: in particular it is a bound to
+the depth of the expected proof tree (more precisely, to the number of nested
+applicative nodes). In this case, there is a solution in six moves, and we
+need a few more applications to handle reachability, and side conditions.
+The magic number to let automation work is, in this case, 9. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="problem"\ 6lemma problem: \ 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 /\ 5span class="autotactic"\ 69\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"\ 6opposite_side\ 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/move.con(0,2,0)"\ 6move_wolf\ 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/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+(*
+\ 5h2 class="section"\ 6Application\ 5/h2\ 6
+Let us now try to derive the proof in a more interactive way. Of course, we
+expect to need several moves to transfer all items from a bank to the other, so
+we should start our proof by applying "more". Matita syntax for invoking the
+application of a property named foo is to write "@foo". In general, the philosophy
+of Matita is to describe each proof of a property P as a structured collection of
+objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining
+the way it is actually used (e.g. for introduction, rewriting, in an applicative
+step, and so on).
+*)
+
+\ 5img class="anchor" src="icons/tick.png" id="problem1"\ 6lemma problem1: \ 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 @\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6