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 [1]:
type location =
  | Boat
  | LeftCoast
  | RightCoast
  | Eaten

type boat =
  | Left
  | Right

type good = Cabbage | Goat | Wolf
Out[1]:
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 [2]:
type state = {
  cabbage : location;
  goat : location;
  wolf : location;
  boat : boat;
}
Out[2]:
type state = {
  cabbage : location;
  goat : location;
  wolf : location;
  boat : boat;
}

We can define a few helpers:

In [3]:
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[3]:
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 [4]:
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
[@@adm 1n]


let solved s =
  s.cabbage = RightCoast
  && s.goat = RightCoast
  && s.wolf = RightCoast
  && s.boat = Right
;;
Out[4]:
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 (Ordinal.count acts)
sub ordinalOrdinal.Int (Ordinal.count (List.tl acts))
path[not (acts = [])]
proof
detailed proof
ground_instances3
definitions2
inductions0
search_time
0.015s
details
Expand
smt_stats
num checks8
arith assert lower18
arith pivots7
rlimit count3014
mk clause29
datatype occurs check33
mk bool var129
arith assert upper21
datatype splits10
decisions29
arith add rows18
propagations19
conflicts11
arith fixed eqs11
datatype accessor ax11
minimized lits1
arith conflicts3
arith assert diseq9
datatype constructor ax28
num allocs1366286897
final checks9
added eqs113
del clause13
arith eq adapter16
memory16.180000
max memory18.750000
Expand
  • start[0.015s]
      not (acts = [])
      && Ordinal.count acts >= 0 && Ordinal.count (List.tl acts) >= 0
      ==> List.tl acts = []
          || Ordinal.Int (Ordinal.count (List.tl acts)) Ordinal.<<
             Ordinal.Int (Ordinal.count acts)
  • simplify
    into
    (not
     ((not (acts = []) && Ordinal.count acts >= 0)
      && Ordinal.count (List.tl acts) >= 0)
     || List.tl acts = [])
    || Ordinal.Int (Ordinal.count (List.tl acts)) Ordinal.<<
       Ordinal.Int (Ordinal.count acts)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_121| (|Ordinal.Int_112|
                            (|count_`action list`_2514| (|get.::.1_2502…
        expansions
        • unroll
          expr
          (|count_`action list`_2514| (|get.::.1_2502| acts_2504))
          expansions
          Ordinal.count
        • unroll
          expr
          (|count_`action list`_2514| acts_2504)
          expansions
          Ordinal.count
        • unsat
          (let ((a!1 (ite ((_ is (Pick_2464 (good_2434) action_2463))
                            (|get.::.0_2501| acts_…

        In [5]:
        (* 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[5]:
        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 [6]:
        #timeout 20_000;;
        
        instance (fun l -> solved @@ many_steps init_state l) ;;
        
        Out[6]:
        - : action list -> bool = <fun>
        module CX : sig val l : action list end
        
        Instance (after 18 steps, 18.546s):
         let l =
           [(Pick (Goat)); CrossRiver; (Drop (Goat)); CrossRiver; (Pick (Cabbage));
            CrossRiver; (Drop (Cabbage)); (Pick (Goat)); CrossRiver; (Drop (Goat));
            (Pick (Wolf)); CrossRiver; (Drop (Wolf)); CrossRiver; (Pick (Goat));
            CrossRiver; (Drop (Goat))]
        
        Instance
        proof attempt
        ground_instances18
        definitions126
        inductions0
        search_time
        18.546s
        details
        Expand
        smt_stats
        num checks37
        rlimit count11514469
        mk clause33435
        datatype occurs check2836
        restarts253
        mk bool var57796
        datatype splits145645
        decisions180140
        propagations2449249
        conflicts32012
        datatype accessor ax5056
        minimized lits329947
        datatype constructor ax82272
        num allocs4220737762
        final checks70
        added eqs4448687
        del clause2410
        dyn ack19
        memory173.810000
        max memory174.090000
        Expand
        • start[18.546s]
            (many_steps
             {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
             :var_0:).cabbage
            = RightCoast
            && (many_steps
                {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
                :var_0:).goat
               = RightCoast
               && (many_steps
                   {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast;
                    boat = Left}
                   :var_0:).wolf
                  = RightCoast
                  && (many_steps
                      {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast;
                       boat = Left}
                      :var_0:).boat
                     = Right
        • simplify

          into
          (((many_steps
             {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
             :var_0:).cabbage
            = RightCoast
            && (many_steps
                {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
                :var_0:).goat
               = RightCoast)
           && (many_steps
               {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
               :var_0:).wolf
              = RightCoast)
          && (many_steps
              {cabbage = LeftCoast; goat = LeftCoast; wolf = LeftCoast; boat = Left}
              :var_0:).boat
             = Right
          expansions
          []
          rewrite_steps
            forward_chaining
            • unroll
              expr
              (many_steps_2492 (|rec_mk.state_2533|
                                 LeftCoast_2428
                                 LeftCoast…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • unroll
              expr
              (let ((a!1 (or (= (cabbage_2439 (|rec_mk.state_2533|
                                                LeftCoast_242…
              expansions
              • get_location
              • get_locationset_location
              • get_locationset_locationboat_empty
              • get_locationset_locationboat_emptyprocess_action
              • get_locationset_locationboat_emptyprocess_actionprocess_eating
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eaten
              • get_locationset_locationboat_emptyprocess_actionprocess_eatinganything_eatenone_step
            • Sat (Some let l = [(Pick (Goat)); CrossRiver; (Drop (Goat)); CrossRiver; (Pick (Cabbage)); CrossRiver; (Drop (Cabbage)); (Pick (Goat)); CrossRiver; (Drop (Goat)); (Pick (Wolf)); CrossRiver; (Drop (Wolf)); CrossRiver; (Pick (Goat)); CrossRiver; (Drop (Goat))] )

            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 [7]:
            instance (fun l -> solved @@ many_steps init_state l)
            [@@blast] ;;
            
            Out[7]:
            - : action list -> bool = <fun>
            module CX : sig val l : action list end
            
            Instance (after 72 steps, 0.181s):
              let l =
                [Pick Goat; CrossRiver; Drop Goat; CrossRiver; Pick Cabbage; CrossRiver;
                 Drop Cabbage; Pick Goat; CrossRiver; Drop Goat; Pick Wolf; CrossRiver;
                 Drop Wolf; CrossRiver; Pick Goat; CrossRiver; Drop Goat]
            
            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.