# Crossing the River Safely¶

For the sake of brain scrambling, we're going to solve this ancient puzzle using Imandra (again!). As most polyvalent farmers will tell you, going to the market with your pet wolf, tastiest goat, and freshest cabbage is sometimes difficult as they tend to have appetite for one another. The good news is that there is a way to cross this river safely anyway.

First we should define the problem by tallying our goods and looking around.

In :
type location =
| Boat
| LeftCoast
| RightCoast
| Eaten

type boat =
| Left
| Right

type good = Cabbage | Goat | Wolf

Out:
type location = Boat | LeftCoast | RightCoast | Eaten
type boat = Left | Right
type good = Cabbage | Goat | Wolf


This problem is delicate and will require multiple steps to be solved. Each step should take us from a state to another state (where, hopefully, no cabbage nor goat was hurt).

In :
type state = {
cabbage : location;
goat : location;
wolf : location;
boat : boat;
}

Out:
type state = {
cabbage : location;
goat : location;
wolf : location;
boat : boat;
}


We can define a few helpers:

In :
let get_location (s:state) (g:good) = match g with
| Cabbage -> s.cabbage
| Goat -> s.goat
| Wolf -> s.wolf

let set_location (s:state) (g:good) (l:location) = match g with
| Cabbage -> { s with cabbage = l}
| Goat    -> { s with goat    = l}
| Wolf    -> { s with wolf    = l}

let boat_empty (s:state) =
(s.cabbage <> Boat) &&
(s.goat    <> Boat) &&
(s.wolf    <> Boat)

Out:
val get_location : state -> good -> location = <fun>
val set_location : state -> good -> location -> state = <fun>
val boat_empty : state -> bool = <fun>


Now, transition from a state to the next one is done via actions:

In :
type action =
| Pick of good
| Drop of good
| CrossRiver

let process_action (s:state) (m:action) : state =
match m with
| CrossRiver -> { s with boat = match s.boat with Left -> Right | Right -> Left }
| Pick x -> begin
if not @@ boat_empty s then s else
match get_location s x, s.boat with
|  LeftCoast ,  Left -> set_location s x Boat
| RightCoast , Right -> set_location s x Boat
| _ -> s
end
| Drop x -> begin
match get_location s x, s.boat with
| Boat ,  Left -> set_location s x LeftCoast
| Boat , Right -> set_location s x RightCoast
| _ -> s
end
;;

let process_eating s =
match s.boat, s.cabbage, s.goat, s.wolf with
| Right, LeftCoast, LeftCoast, _    -> Some { s with cabbage = Eaten }
| Right, _ , LeftCoast, LeftCoast   -> Some { s with goat = Eaten }
|  Left, RightCoast, RightCoast, _  -> Some { s with cabbage = Eaten }
|  Left, _ , RightCoast, RightCoast -> Some { s with goat = Eaten }
| _  -> None

(* is… it a bad state? *)
let anything_eaten s =
s.cabbage = Eaten || s.goat = Eaten

let one_step s a =
if anything_eaten s then s
else
match process_eating s with
| Some s -> s
| None ->
process_action s a

(* process many actions. Note that we have to specify that [acts] is
the argument that proves termination *)
let rec many_steps s acts =
match acts with
| [] -> s
| a :: acts ->
let s' = one_step s a in
many_steps s' acts

let solved s =
s.cabbage = RightCoast
&& s.goat = RightCoast
&& s.wolf = RightCoast
&& s.boat = Right
;;

Out:
type action = Pick of good | Drop of good | CrossRiver
val process_action : state -> action -> state = <fun>
val process_eating : state -> state option = <fun>
val anything_eaten : state -> bool = <fun>
val one_step : state -> action -> state = <fun>
val many_steps : state -> action list -> state = <fun>
val solved : state -> bool = <fun>

termination proof

### Termination proof

call many_steps (one_step s (List.hd acts)) (List.tl acts) from many_steps s acts
originalmany_steps s acts
submany_steps (one_step s (List.hd acts)) (List.tl acts)
original ordinalOrdinal.Int (_cnt acts)
sub ordinalOrdinal.Int (_cnt (List.tl acts))
path[not Is_a([], acts)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.028s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 22 arith-max-columns 14 arith-conflicts 1 rlimit count 2933 mk clause 39 datatype occurs check 23 mk bool var 140 arith-lower 16 datatype splits 27 decisions 49 propagations 50 arith-max-rows 3 conflicts 14 datatype accessor ax 23 datatype constructor ax 50 num allocs 1.26078e+06 final checks 6 added eqs 207 del clause 20 arith eq adapter 16 arith-upper 19 memory 7.2 max memory 7.2
Expand
• start[0.028s]
let (_x_0 : int) = count.list count.action acts in
let (_x_1 : action list) = List.tl acts in
let (_x_2 : int) = count.list count.action _x_1 in
not Is_a([], acts) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : action list) = List.tl acts in let (_x_1 : int) = count.list count.action _x_0 in let (_x_2 : int) = count.list count.action acts in (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], acts) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list count.action_1733| acts_1721) expansions
• unroll
 expr (|count.list count.action_1733| (|get.::.1_1717| acts_1721)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list count.action_1733| … expansions
• Unsat

In :
(* initial state, on the west bank of Anduin with empty pockets and fuzzy side-kicks *)
let init_state = {
cabbage = LeftCoast;
goat = LeftCoast;
wolf = LeftCoast;
boat = Left;
}

Out:
val init_state : state =
{cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}


We are now ready to ask for a solution! Because we're looking for a given solution rather than a universal proof, instance is the most natural.

In :
#timeout 10_000;;

instance (fun l -> solved @@ many_steps init_state l) ;;

Out:
- : action list -> bool = <fun>

Unknown (Verification aborted by the solver (after 16 steps))
Expand
 expanded let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in let (_x_4 : action list) = List.tl _x_3 in let (_x_5 : action list) = List.tl _x_4 in let (_x_6 : action list) = List.tl _x_5 in let (_x_7 : action list) = List.tl _x_6 in many_steps (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.hd _x_4)) (List.hd _x_5)) (List.hd _x_6)) (List.hd _x_7)) (List.tl _x_7)let (_x_0 : action list) = List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl l))))))))))) in let (_x_1 : action list) = List.tl _x_0 in many_steps (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.tl _x_1)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in let (_x_4 : action list) = List.tl _x_3 in let (_x_5 : action list) = List.tl _x_4 in many_steps (one_step (one_step (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.hd _x_4)) (List.hd _x_5)) (List.tl _x_5)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in let (_x_4 : action list) = List.tl _x_3 in let (_x_5 : action list) = List.tl _x_4 in let (_x_6 : action list) = List.tl _x_5 in many_steps (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.hd _x_4)) (List.hd _x_5)) (List.hd _x_6)) (List.tl _x_6)let (_x_0 : action list) = List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl l))))))))))) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in many_steps (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.tl _x_2)let (_x_0 : action list) = List.tl l in let (_x_1 : action list) = List.tl _x_0 in many_steps (one_step (one_step (one_step {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left} (List.hd l)) (List.hd _x_0)) (List.hd _x_1)) (List.tl _x_1)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in let (_x_4 : action list) = List.tl _x_3 in let (_x_5 : action list) = List.tl _x_4 in let (_x_6 : action list) = List.tl _x_5 in let (_x_7 : action list) = List.tl _x_6 in let (_x_8 : action list) = List.tl _x_7 in many_steps (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.hd _x_4)) (List.hd _x_5)) (List.hd _x_6)) (List.hd _x_7)) (List.hd _x_8)) (List.tl _x_8)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in let (_x_4 : action list) = List.tl _x_3 in let (_x_5 : action list) = List.tl _x_4 in let (_x_6 : action list) = List.tl _x_5 in let (_x_7 : action list) = List.tl _x_6 in let (_x_8 : action list) = List.tl _x_7 in let (_x_9 : action list) = List.tl _x_8 in many_steps (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.hd _x_4)) (List.hd _x_5)) (List.hd _x_6)) (List.hd _x_7)) (List.hd _x_8)) (List.hd _x_9)) (List.tl _x_9)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in many_steps (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.tl _x_2)many_steps (one_step {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left} (List.hd l)) (List.tl l)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in let (_x_4 : action list) = List.tl _x_3 in many_steps (one_step (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.hd _x_4)) (List.tl _x_4)let (_x_0 : action list) = List.tl l in many_steps (one_step (one_step {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left} (List.hd l)) (List.hd _x_0)) (List.tl _x_0)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in many_steps (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.tl _x_3)let (_x_0 : action list) = List.tl l in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in many_steps (one_step (one_step (one_step (one_step {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left} (List.hd l)) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.tl _x_2)let (_x_0 : action list) = List.tl (List.tl (List.tl l)) in let (_x_1 : action list) = List.tl _x_0 in many_steps (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.tl _x_1)many_steps {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left} l blocked let (_x_0 : action list) = List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl (List.tl l))))))))))) in let (_x_1 : action list) = List.tl _x_0 in let (_x_2 : action list) = List.tl _x_1 in let (_x_3 : action list) = List.tl _x_2 in many_steps (one_step (one_step (one_step (one_step (one_step … …) (List.hd _x_0)) (List.hd _x_1)) (List.hd _x_2)) (List.hd _x_3)) (List.tl _x_3)
proof attempt
 ground_instances 16 definitions 0 inductions 0 search_time 45.490s
Expand
• start[45.490s]
let (_x_0 : state)
= many_steps
{cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
( :var_0: )
in
_x_0.cabbage = RightCoast
&& _x_0.goat = RightCoast && _x_0.wolf = RightCoast && _x_0.boat = Right
• #### simplify

 into let (_x_0 : state) = many_steps {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left} ( :var_0: ) in ((_x_0.cabbage = RightCoast && _x_0.goat = RightCoast) && _x_0.wolf = RightCoast) && _x_0.boat = Right expansions [] rewrite_steps forward_chaining
• unroll
 expr (many_steps_96 (|rec_mk.state_1729| LeftCoast_16 LeftCoast_16 … expansions
• unroll
 expr (many_steps_96 (one_step_91 (|rec_mk.state_1729| LeftCoast_16 … expansions
• unroll
 expr (many_steps_96 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions
• unroll
 expr (let ((a!1 (one_step_91 (one_step_91 (one_step_91 (|rec_mk.state_1729| … expansions

That seems to take a bit of time, because this problem is not that easy for Imandra's unrolling algorithm. Let's try [@@blast] to see if we can get a result faster:

In :
instance (fun l -> solved @@ many_steps init_state l)
[@@blast] ;;

Out:
- : action list -> bool = <fun>
module CX : sig val l : action list end

Instance (after 72 steps, 0.136s):
let l =
let (_x_0 : action) = Pick Goat in
let (_x_1 : action) = Drop Goat in
[_x_0; CrossRiver; _x_1; CrossRiver; Pick Wolf; CrossRiver; Drop Wolf;
_x_0; CrossRiver; _x_1; Pick Cabbage; CrossRiver; Drop Cabbage;
CrossRiver; _x_0; CrossRiver; _x_1]

Instance

It only took a fraction of second! 🎉

Now we have a clear plan for crossing the river. How to sell the goat and cabbage is left as an exercise to the reader.