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:

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

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

Last updated: Jun 16 2024 at 01:42 UTC