## Stream: Coq users

### Topic: [newbie] wolf, goat and cabbage puzzle

#### Thales MG (Sep 08 2021 at 14:36):

Hello!

I'm trying to learn Coq, and I decided to try and model the
wolf + goat + cabbage problem as an exercise. I ran into a few problems and
would like some feedback, if possible, on how to improve.

In my first version, I managed to make a (long) proof of the puzzle
that was compatible with a known solution. But the modelling had a
problem, in that it allowed a "single step" solution, as `eauto` later
showed me, in which basically all objects would "jump" to the other
river bank in one step. Later I managed to change the inductive
definition to account for that (or so I think...).

The definitions of the first version are:

``````From Coq Require Import Lists.List. Import ListNotations.

Inductive Object :=
| Wolf
| Goat
| Cabbage.

Inductive Direction :=
| Right
| Left.

Definition eats (o1 o2 : Object) :  bool :=
match (o1, o2) with
| (Wolf, Goat) => true
| (Goat, Wolf) => true
| (Goat, Cabbage) => true
| (Cabbage, Goat) => true
| _ => false
end.

(* forbidden combinations to be left alone *)
Inductive NoEats : list Object -> Prop :=
| NoEatsNil : NoEats []
| NoEatsOne : forall o, NoEats [o]
| NoEatsMore : forall o os,
NoEats os -> forallb (eats o) os = false -> NoEats (o :: os).

(* First attempt; this has problems! *)
Inductive RiverCrossing :
Direction -> list Object -> list Object -> Prop :=
| initial : forall l,
In Wolf l ->
In Goat l ->
In Cabbage l ->
RiverCrossing Right l []
| goRightAlone :
forall l r,
NoEats l -> RiverCrossing Right l r ->
RiverCrossing Left l r
| goLeftAlone :
forall l r,
NoEats r -> RiverCrossing Left l r ->
RiverCrossing Right l r
| goRight :
forall o l r l' r',
In o l -> ~ (In o l') -> In o r' -> NoEats l' ->
RiverCrossing Right l r ->
RiverCrossing Left l' r'
| goLeft :
forall o l r l' r',
In o r -> ~ (In o r') -> In o l' -> NoEats r' ->
RiverCrossing Left l r ->
RiverCrossing Right  l' r'.
``````

After I realized something was wrong in the `RiverCrossing`
definition, I changed it into the following:

``````Inductive RiverCrossing :
Direction -> list Object -> list Object -> Prop :=
| initial : forall l,
In Wolf l ->
In Goat l ->
In Cabbage l ->
RiverCrossing Right l []
| goRightAlone :
forall l r,
NoEats l -> RiverCrossing Right l r ->
RiverCrossing Left l r
| goLeftAlone :
forall l r,
NoEats r -> RiverCrossing Left l r ->
RiverCrossing Right l r
| goRight :
forall l r l' r',
(exists o,
In o l /\ ~ (In o r)
/\ (forall ol,
In ol l ->
(ol = o /\ In ol r') \/ (ol <> o /\ In ol l' /\ ~(In ol r')))
/\ (forall or,
(In or r -> (or <> o /\ In or r')))) ->
NoEats l' ->
RiverCrossing Right l r ->
RiverCrossing Left l' r'
| goLeft :
forall l r l' r',
(exists o,
In o r /\ ~ (In o l)
/\ (forall or,
In or r ->
(or = o /\ In or l') \/ (or <> o /\ In or r' /\ ~(In or l')))
/\ (forall ol,
(In ol l -> (ol <> o /\ In ol l')))) ->
NoEats r' ->
RiverCrossing Left l r ->
RiverCrossing Right l' r'.
``````

I still managed to find a seemingly reasonable solution (also very
long), but I lost the ability to use `eauto`, so I'm not sure if there
is another problem with it.

But I think there are still a few problems with this:

• it seems overly complicated, and possibly wrong again;
• the proof is "backwards": we must provide the steps in reverse order;
• we need to specify `l` and `r` river banks on every step;
• the proof gets nested deeper and deeper, if bullet points are
used.

Any tips on how could I address those issues?

Thanks! :beers:

#### Thales MG (Sep 08 2021 at 14:42):

By the way, I placed the code with more details in this gist.

#### Thales MG (Sep 08 2021 at 16:56):

And this is the second version using some automation: https://gist.github.com/thalesmg/30429efb34620da3039ab1145351cbb3

Last updated: Oct 03 2023 at 02:34 UTC