[newbie] wolf, goat and cabbage puzzle · Coq users

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...).

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.

Stream: Coq users

Topic: [newbie] wolf, goat and cabbage puzzle

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

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

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