tags: coq ; puzzles ; formal methods

Introduction

Earlier this year, I attended the Formal Methods for the Informal Engineer workshop, and found that quite fascinating. It is a huge field, and the topic is quite deep and dense, as one would expect. It was my first introduction to the interactive theorem prover Coq, during the nice tutorial by Cody Roux.

Some time later, after working thought the Logical Foundations book from the Software Foundations series, I wanted to try and practice it on my own on some toy problem. The “wolf, goat and cabbage problem” came to mind, and I have previously seems examples that show that the Alloy Analyzer and Z3 could be used to solve it automatically. But I could not find an equivalent solution in Coq. So I tried to see if I could do it with my current knowledge.

In my first attempt, I managed to model and reproduce a known solution as a proof! Or so I thought… The modeling had a problem which allowed for a “single step” nonsense solution. That was uncovered after I tried to use Coq’s proof automation to see if it worked. Then it showed me the bogus “solution”, and I had to rethink how to represent the problem.

The problem was that I was not constraining the contents of both river banks correctly during the crossing, so it was possible that a bank would suddenly change composition after a step. After constraining those values more, I could reproduce the known solution, but lost the ability to use the standard automation machinery… I guess I’d need to create my own version of the auto or eauto tactics, like Adam Chlipala’s crush, but I don’t know how to do that quite yet.

Even with this second solution, there some issues with it and I’m still not sure if it is correct, since the first time and it was not obvious to me that I had messed up. I’ll share both solutions below, and maybe one day someone can give me some hints on how to fix and correct those issues.

I should also say that I used Alectryon by Clément Pit-Claudel to produce the Coq snippets with proof states below, and it is quite magical. That, in turn, was taken from Philip Zucker’s post about translating his Z3 tutorial from the FMIE workshop to Coq. If you hover your cursor over the proof lines, it should show the hypothesis and the goals at that point.

Basic definitions

The definition below did not change between attempts, and were shared by both solutions.

First, we need to import some modules so we can use a notation for list literals. This is an amazing feature of Coq: the ability to define custom notation.

From Coq Require Import Lists.List. Import ListNotations.

Then, we define the “objects” that the farmer wants to take from one river bank to the other. Maybe it’s strange to call a wolf and a goat objects, but I couldn’t think of another name for the type, and I went with the nomenclature from the Alloy tutorial.

Inductive Object :=
| Wolf
| Goat
| Cabbage.

In each step, the farmer must cross from one side of the river to the other alone or carrying one of the objects. I modeled the state of the problem by defining which is the river bank the farmer will go to next: either the left or the right side of the river.

Inductive Direction :=
| Right
| Left.

But some pairs of objects cannot be left unattended, else they eat each other. Those pairs are “forbidden” when crossing the river. The eats function tells us if either of two objects eats the other, and the NoEats predicate uses that to assert that list of objects, representing one side of the river, contains no forbidden pairs of objects.

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

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 (problematic!)

Module FirstAttempt.

The RiverCrossing predicate represents the state of the problem. It is parameterized by the direction the farmer is going next, the contents of the left and the right river banks. Then comes the constructors of this predicate.

We have the initial state, where all objects are on the left bank, the right bank is empty, and the farmer is going right. I used the In predicate to avoid having to deal with specific list orderings.

Then the farmer can go right or left, alone. In that case, the contents of both banks do not change, but we must enforce that the objects that were just left alone do not eat each other.

Else, the farmer takes one object along the trip. I just checked that the object being carried exists on the source bank in the initial state and disappears from there in the final state, and that the remaining objects don’t eat each other. This has the problem I alluded before: the constraints on the initial and final compositions of each river bank are too loose, allowing for “quantum jumps”.

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

For reference, I’ll just reproduce the proof using this model below, but beware that it is wrong, as said before. Also, another thing of notice is that the steps are “backwards”: we start from the final state (everything in the right bank) and work our way towards the initial state, which should be the only way to produce a RiverCrossing out of thin air.

Theorem solution : forall r,
    In Wolf r ->
    In Goat r ->
    In Cabbage r ->
    RiverCrossing Left [] r.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
Proof.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
  intros r Hw Hg Hc.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [] r
  (* step 7 : [G] -G> [W; C] => [] || [G; W; C] *)
  apply goRight with (o := Goat) (l := [Goat]) (r := [Cabbage; Wolf]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Goat []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Cabbage; Wolf]
  (* Goat in initial left bank *)
  apply in_eq.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Goat []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Cabbage; Wolf]
  (* Goat not in final left bank *)
  apply in_nil.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Cabbage; Wolf]
  (* Goat in final right bank *)
  assumption.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Cabbage; Wolf]
  (* final left bank is empty, so it's safe *)
  apply NoEatsNil.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Cabbage; Wolf]

  (* step 6 : [G] <- [W; C] => [G] || [W; C] *)
  apply goLeftAlone.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage; Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Goat] [Cabbage; Wolf]
  (* proof that Wolf doesn't eat Cabbage *)
  apply NoEatsMore.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forallb (eats Cabbage) [Wolf] = false
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Goat] [Cabbage; Wolf] apply NoEatsOne.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forallb (eats Cabbage) [Wolf] = false
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Goat] [Cabbage; Wolf] trivial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Goat] [Cabbage; Wolf]

  (* step 5 : [C; G] -C> [W] => [G] || [W; C] *)
  apply goRight with (o := Cabbage) (l := [Cabbage; Goat]) (r := [Wolf]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Cabbage; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Cabbage; Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Cabbage; Goat] [Wolf]
  (* Cabbage in initial left bank *)
  apply in_eq.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Cabbage; Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Cabbage; Goat] [Wolf]
  (* Cabbage not in final left bank *)
  intros contra; inversion contra; inversion H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Cabbage; Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Cabbage; Goat] [Wolf]
  (* Cabbage in final right bank *)
  apply in_eq.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Cabbage; Goat] [Wolf]
  (* final left bank just has the Goat, so it's safe *)
  apply NoEatsOne.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Cabbage; Goat] [Wolf]

  (* step 4 : [C] <G- [W; G] => [C; G] || [W] *)
  apply goLeft with (o := Goat) (l := [Cabbage]) (r := [Wolf; Goat]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Goat [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Cabbage; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  (* Goat in initial right bank *)
  simpl; right; left; reflexivity.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Goat [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Cabbage; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  (* Goat not in final right bank *)
  intros contra; inversion contra; inversion H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Cabbage; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  (* Goat in final Left bank *)
  simpl; right; left; reflexivity.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  (* final right bank just has the Wolf, so it's safe *)
  apply NoEatsOne.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]

  (* step 3 : [W; C] -W> [G] => [C] || [W; G] *)
  apply goRight with (o := Wolf) (l := [Wolf; Cabbage]) (r := [Goat]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Wolf [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Wolf [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Wolf [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  (* Wolf in initial left bank *)
  apply in_eq.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Wolf [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Wolf [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  (* Wolf not in final left bank *)
  intros contra; inversion contra; inversion H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Wolf [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  (* Wolf in final right bank *)
  apply in_eq.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  (* final left bank just has the Cabbage, so it's safe *)
  apply NoEatsOne.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]

  (* step 2 : [W; C] <- [G] => [W; C] || [G] *)
  apply goLeftAlone.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Wolf; Cabbage] [Goat]
  (* proof that Goat doesn't eat itself *)
  apply NoEatsOne.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Wolf; Cabbage] [Goat]

  (* step 1 : [W; G; C] -G> [] => [W; C] || [G] *)
  apply goRight with (o := Goat) (l := [Wolf; Goat; Cabbage]) (r := []).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Wolf; Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  (* Goat in initial left bank *)
  simpl; right; left; reflexivity.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  (* Goat not in final left bank *)
  intros contra; inversion contra; inversion H; inversion H0.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  (* Goat in final right bank *)
  apply in_eq.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  (* proof that Wolf doesn't eat Cabbage *)
  apply NoEatsMore.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forallb (eats Wolf) [Cabbage] = false
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] apply NoEatsOne.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forallb (eats Wolf) [Cabbage] = false
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] trivial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []

  (* initial state: everyone on the left bank *)
  apply initial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Wolf [Wolf; Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Wolf; Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Wolf; Goat; Cabbage]
  (* Wolf on the initial left bank *)
  simpl; left; reflexivity.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Wolf; Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Wolf; Goat; Cabbage]
  (* Goat on the initial left bank *)
  simpl; right; left; reflexivity.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Wolf; Goat; Cabbage]
  (* Cabbage on the initial left bank *)
  simpl; right; right; left; reflexivity.
Qed.

I was quite satisfied that this worked out, but luckily that model was amenable to simple proof automation. Using the info_eauto tactic, it proved that the objects could go all to the right side… But by a strange path…

I also needed to add the constructors and functions relevant to the problem in a hint database called local so that eauto could use them.

Hint Constructors Object : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Constructors Direction : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Constructors NoEats : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve eats : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Unfold eats : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Constructors RiverCrossing : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Unfold In : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve in_nil : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve in_eq : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve ex_intro : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]

Theorem solution_auto : forall r,
    In Wolf r ->
    In Goat r ->
    In Cabbage r ->
    RiverCrossing Left [] r.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
Proof.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
  info_eauto with local.(* info eauto: *)
intro.
intro.
intro.
intro.
simple eapply goRight.
exact H1.
simple apply in_nil.
exact H1.
exact NoEatsNil.
simple apply initial.
exact H.
exact H0.
exact H1.
Qed.

Theorem bogus_solution : forall r,
    In Wolf r ->
    In Goat r ->
    In Cabbage r ->
    RiverCrossing Left [] r.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
Proof.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
  (* found by eauto *)
  intro.r: list Object
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
  intro.r: list Object
H: In Wolf r
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
  intro.r: list Object
H: In Wolf r
H0: In Goat r
In Cabbage r -> RiverCrossing Left [] r
  intro.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
RiverCrossing Left [] r
  simple eapply goRight.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In ?o ?l
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
~ In ?o []
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In ?o r
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
NoEats []
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
RiverCrossing Right ?l ?r
  exact H1.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
~ In Cabbage []
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Cabbage r
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
NoEats []
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
RiverCrossing Right r ?r
  simple apply in_nil.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Cabbage r
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
NoEats []
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
RiverCrossing Right r ?r
  exact H1.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
NoEats []
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
RiverCrossing Right r ?r
  exact NoEatsNil.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
RiverCrossing Right r ?r
  (* oh no *)
  simple apply initial.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Wolf r
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Goat r
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Cabbage r
  exact H.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Goat r
r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Cabbage r
  exact H0.r: list Object
H: In Wolf r
H0: In Goat r
H1: In Cabbage r
In Cabbage r
  exact H1.
Qed.

End FirstAttempt.

Second attempt

Module SecondAttempt.

In my second attempt, I only changed the goRight and goLeft constructors to tighten up the restrictions on the contents of both river banks. Anything on the opposing side in the initial state should still be present in the final state plus the object that just crossed. The initial side should contain a special object, the one being carried, and all objects in that side should be present there in the final state, except the carried object. This was the essential change.

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

Hint Constructors Object : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Constructors Direction : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Constructors NoEats : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve eats : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Unfold eats : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Constructors RiverCrossing : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Unfold In : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve in_nil : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve in_eq : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve ex_intro : local.The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]

Unfortunately, with those changes, neither auto nor eauto work anymore. There are some goals that are repeated during the proof, especially regarding goals and hypothesis of the forms In X Xs and ~ (In X Xs). Using some excerpts from the CPDT and PLF books, I managed to make some rudimentary automated tactics for those cases.

Ltac auto_not_in :=
  repeat match goal with
  | |- ~ (In ?X ?Xs) =>
    intros contra;
    repeat (destruct contra as [contra | contra];
            try discriminate;
            try apply contra);
    try destruct contra
  end.

Ltac not_in_absurd H :=
  match type of H with
  | In _ [] => exfalso; apply in_nil in H; apply H
  | In _ _ =>
    let H0 := fresh "H0" in
    try (inversion H as [H0 | H0]; try discriminate; not_in_absurd H0)
  end.

(* taken from:
 https://softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html#lab524
 *)
Ltac jauto_set_hyps :=
  repeat match goal with H: ?T |- _ =>
    match T with
    | _ /\ _ => destruct H
    | exists a, _ => destruct H
    | _ => generalize H; clear H
    end
  end.

Ltac jauto_set_goal :=
  repeat match goal with
  | |- exists a, _ => esplit
  | |- _ /\ _ => split
  end.

Ltac jauto_set :=
  intros; jauto_set_hyps;
  intros; jauto_set_goal;
  unfold not in *.

Tactic Notation "jauto" :=
  try solve [ jauto_set; eauto with local ]; try auto_not_in.
Tactic Notation "jauto_fast" :=
  try solve [ auto with local | eauto with local | jauto ].

Armed with that, I redid my solution from before. Alas, I’m not able at the moment to check if there are bogus solutions as I did before… Again, I’ll just reproduce the solution below.

Theorem solution : forall r,
    In Wolf r ->
    In Goat r ->
    In Cabbage r ->
    RiverCrossing Left [] r.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
Proof.forall r : list Object,
In Wolf r ->
In Goat r -> In Cabbage r -> RiverCrossing Left [] r
  intros r Hw Hg Hc.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [] r

  (* step 7 : [G] -G> [W; C] => [] || [G; W; C] *)
  apply goRight with (l := [Goat]) (r := [Wolf; Cabbage]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
exists o : Object,
  In o [Goat] /\
  ~ In o [Wolf; Cabbage] /\
  (forall ol : Object,
   In ol [Goat] ->
   ol = o /\ In ol r \/
   ol <> o /\ In ol [] /\ ~ In ol r) /\
  (forall or : Object,
   In or [Wolf; Cabbage] -> or <> o /\ In or r)
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]
  exists Goat.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Goat] /\
~ In Goat [Wolf; Cabbage] /\
(forall ol : Object,
 In ol [Goat] ->
 ol = Goat /\ In ol r \/
 ol <> Goat /\ In ol [] /\ ~ In ol r) /\
(forall or : Object,
 In or [Wolf; Cabbage] -> or <> Goat /\ In or r)
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]
  try repeat (split; jauto).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forall ol : Object,
In ol [Goat] ->
ol = Goat /\ In ol r \/
ol <> Goat /\ In ol [] /\ ~ In ol r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
or <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
In or r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]
  destruct ol; intros H; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat]
Goat = Goat /\ In Goat r \/
Goat <> Goat /\ In Goat [] /\ ~ In Goat r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
or <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
In or r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]
  left.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat]
Goat = Goat /\ In Goat r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
or <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
In or r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat]
Goat = Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat]
In Goat r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
or <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
In or r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage] trivial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat]
In Goat r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
or <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
In or r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage] assumption.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
or <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
In or r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]
  destruct or; try discriminate; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf; Cabbage]
In or r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]
  destruct or; try discriminate; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Cabbage]
In Wolf r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
In Cabbage r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]
  assumption.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
In Cabbage r
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage] assumption.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats []
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage] constructor.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat] [Wolf; Cabbage]

  (* step 6 : [G] <- [W; C] => [G] || [W; C] *)
  apply goLeftAlone.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Goat] [Wolf; Cabbage]
  auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Goat] [Wolf; Cabbage]

  (* step 5 : [C; G] -C> [W] => [G] || [W; C] *)
  apply goRight with (l := [Goat; Cabbage]) (r := [Wolf]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
exists o : Object,
  In o [Goat; Cabbage] /\
  ~ In o [Wolf] /\
  (forall ol : Object,
   In ol [Goat; Cabbage] ->
   ol = o /\ In ol [Wolf; Cabbage] \/
   ol <> o /\ In ol [Goat] /\ ~ In ol [Wolf; Cabbage]) /\
  (forall or : Object,
   In or [Wolf] -> or <> o /\ In or [Wolf; Cabbage])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  exists Cabbage.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Cabbage [Goat; Cabbage] /\
~ In Cabbage [Wolf] /\
(forall ol : Object,
 In ol [Goat; Cabbage] ->
 ol = Cabbage /\ In ol [Wolf; Cabbage] \/
 ol <> Cabbage /\
 In ol [Goat] /\ ~ In ol [Wolf; Cabbage]) /\
(forall or : Object,
 In or [Wolf] ->
 or <> Cabbage /\ In or [Wolf; Cabbage])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  try repeat (split; jauto).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forall ol : Object,
In ol [Goat; Cabbage] ->
ol = Cabbage /\ In ol [Wolf; Cabbage] \/
ol <> Cabbage /\
In ol [Goat] /\ ~ In ol [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  destruct ol; intros H; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
Goat = Cabbage /\ In Goat [Wolf; Cabbage] \/
Goat <> Cabbage /\
In Goat [Goat] /\ ~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage] \/
Cabbage <> Cabbage /\
In Cabbage [Goat] /\ ~ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  right.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
Goat <> Cabbage /\
In Goat [Goat] /\ ~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage] \/
Cabbage <> Cabbage /\
In Cabbage [Goat] /\ ~ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
Goat <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
In Goat [Goat] /\ ~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage] \/
Cabbage <> Cabbage /\
In Cabbage [Goat] /\ ~ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] discriminate.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
In Goat [Goat] /\ ~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage] \/
Cabbage <> Cabbage /\
In Cabbage [Goat] /\ ~ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage] \/
Cabbage <> Cabbage /\
In Cabbage [Goat] /\ ~ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Goat; Cabbage]
~ In Goat [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage] \/
Cabbage <> Cabbage /\
In Cabbage [Goat] /\ ~ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] auto_not_in.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage] \/
Cabbage <> Cabbage /\
In Cabbage [Goat] /\ ~ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  left.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage /\ In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] trivial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Goat; Cabbage]
H0: In Cabbage [Cabbage]
In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
or <> Cabbage
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  destruct or; try discriminate; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Wolf]
In or [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  destruct or; try discriminate; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf]
In Wolf [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]
  auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf] constructor.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Goat; Cabbage] [Wolf]

  (* step 4 : [C] <G- [W; G] => [C; G] || [W] *)
  apply goLeft with (l := [Cabbage]) (r := [Wolf; Goat]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
exists o : Object,
  In o [Wolf; Goat] /\
  ~ In o [Cabbage] /\
  (forall or0 : Object,
   In or0 [Wolf; Goat] ->
   or0 = o /\ In or0 [Goat; Cabbage] \/
   or0 <> o /\
   In or0 [Wolf] /\ ~ In or0 [Goat; Cabbage]) /\
  (forall ol : Object,
   In ol [Cabbage] -> ol <> o /\ In ol [Goat; Cabbage])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  exists Goat.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Wolf; Goat] /\
~ In Goat [Cabbage] /\
(forall or0 : Object,
 In or0 [Wolf; Goat] ->
 or0 = Goat /\ In or0 [Goat; Cabbage] \/
 or0 <> Goat /\
 In or0 [Wolf] /\ ~ In or0 [Goat; Cabbage]) /\
(forall ol : Object,
 In ol [Cabbage] ->
 ol <> Goat /\ In ol [Goat; Cabbage])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  try repeat (split; jauto).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forall or0 : Object,
In or0 [Wolf; Goat] ->
or0 = Goat /\ In or0 [Goat; Cabbage] \/
or0 <> Goat /\
In or0 [Wolf] /\ ~ In or0 [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  destruct or; intros H; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
Wolf = Goat /\ In Wolf [Goat; Cabbage] \/
Wolf <> Goat /\
In Wolf [Wolf] /\ ~ In Wolf [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage] \/
Goat <> Goat /\
In Goat [Wolf] /\ ~ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  right.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
Wolf <> Goat /\
In Wolf [Wolf] /\ ~ In Wolf [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage] \/
Goat <> Goat /\
In Goat [Wolf] /\ ~ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
Wolf <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
In Wolf [Wolf] /\ ~ In Wolf [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage] \/
Goat <> Goat /\
In Goat [Wolf] /\ ~ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] discriminate.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
In Wolf [Wolf] /\ ~ In Wolf [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage] \/
Goat <> Goat /\
In Goat [Wolf] /\ ~ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
In Wolf [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
~ In Wolf [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage] \/
Goat <> Goat /\
In Goat [Wolf] /\ ~ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat]
~ In Wolf [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage] \/
Goat <> Goat /\
In Goat [Wolf] /\ ~ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] auto_not_in.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage] \/
Goat <> Goat /\
In Goat [Wolf] /\ ~ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  left.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat /\ In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
Goat = Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] trivial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat]
H0: In Goat [Goat]
In Goat [Goat; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
ol: Object
H: In ol [Cabbage]
ol <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  destruct ol; try discriminate; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]
  auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Cabbage] [Wolf; Goat]

  (* step 3 : [W; C] -W> [G] => [C] || [W; G] *)
  apply goRight with (l := [Wolf; Cabbage]) (r := [Goat]).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
exists o : Object,
  In o [Wolf; Cabbage] /\
  ~ In o [Goat] /\
  (forall ol : Object,
   In ol [Wolf; Cabbage] ->
   ol = o /\ In ol [Wolf; Goat] \/
   ol <> o /\ In ol [Cabbage] /\ ~ In ol [Wolf; Goat]) /\
  (forall or : Object,
   In or [Goat] -> or <> o /\ In or [Wolf; Goat])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  exists Wolf.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Wolf [Wolf; Cabbage] /\
~ In Wolf [Goat] /\
(forall ol : Object,
 In ol [Wolf; Cabbage] ->
 ol = Wolf /\ In ol [Wolf; Goat] \/
 ol <> Wolf /\ In ol [Cabbage] /\ ~ In ol [Wolf; Goat]) /\
(forall or : Object,
 In or [Goat] -> or <> Wolf /\ In or [Wolf; Goat])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  try repeat (split; jauto).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forall ol : Object,
In ol [Wolf; Cabbage] ->
ol = Wolf /\ In ol [Wolf; Goat] \/
ol <> Wolf /\ In ol [Cabbage] /\ ~ In ol [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  destruct ol; intros H; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Cabbage]
Wolf = Wolf /\ In Wolf [Wolf; Goat] \/
Wolf <> Wolf /\
In Wolf [Cabbage] /\ ~ In Wolf [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Wolf /\ In Cabbage [Wolf; Goat] \/
Cabbage <> Wolf /\
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  left.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Cabbage]
Wolf = Wolf /\ In Wolf [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Wolf /\ In Cabbage [Wolf; Goat] \/
Cabbage <> Wolf /\
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Cabbage]
Wolf = Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Cabbage]
In Wolf [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Wolf /\ In Cabbage [Wolf; Goat] \/
Cabbage <> Wolf /\
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] trivial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Cabbage]
In Wolf [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Wolf /\ In Cabbage [Wolf; Goat] \/
Cabbage <> Wolf /\
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage = Wolf /\ In Cabbage [Wolf; Goat] \/
Cabbage <> Wolf /\
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  right.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage <> Wolf /\
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
Cabbage <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] discriminate.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
In Cabbage [Cabbage] /\ ~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
In Cabbage [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Cabbage]
H0: In Cabbage [Cabbage]
~ In Cabbage [Wolf; Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat] auto_not_in.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
or: Object
H: In or [Goat]
or <> Wolf
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  destruct or; try discriminate; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]
  auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Cabbage] [Goat]

  (* step 2 : [W; C] <- [G] => [W; C] || [G] *)
  apply goLeftAlone.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Wolf; Cabbage] [Goat]
  auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Left [Wolf; Cabbage] [Goat]

  (* step 1 : [W; G; C] -G> [] => [W; C] || [G] *)
  apply goRight with (l := [Wolf; Goat; Cabbage]) (r := []).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
exists o : Object,
  In o [Wolf; Goat; Cabbage] /\
  ~ In o [] /\
  (forall ol : Object,
   In ol [Wolf; Goat; Cabbage] ->
   ol = o /\ In ol [Goat] \/
   ol <> o /\ In ol [Wolf; Cabbage] /\ ~ In ol [Goat]) /\
  (forall or : Object,
   In or [] -> or <> o /\ In or [Goat])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  exists Goat.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
In Goat [Wolf; Goat; Cabbage] /\
~ In Goat [] /\
(forall ol : Object,
 In ol [Wolf; Goat; Cabbage] ->
 ol = Goat /\ In ol [Goat] \/
 ol <> Goat /\ In ol [Wolf; Cabbage] /\ ~ In ol [Goat]) /\
(forall or : Object,
 In or [] -> or <> Goat /\ In or [Goat])
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  try repeat (split; jauto).r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
forall ol : Object,
In ol [Wolf; Goat; Cabbage] ->
ol = Goat /\ In ol [Goat] \/
ol <> Goat /\ In ol [Wolf; Cabbage] /\ ~ In ol [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  destruct ol; intros H; not_in_absurd H.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
Wolf = Goat /\ In Wolf [Goat] \/
Wolf <> Goat /\
In Wolf [Wolf; Cabbage] /\ ~ In Wolf [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat] \/
Goat <> Goat /\
In Goat [Wolf; Cabbage] /\ ~ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  right.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
Wolf <> Goat /\
In Wolf [Wolf; Cabbage] /\ ~ In Wolf [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat] \/
Goat <> Goat /\
In Goat [Wolf; Cabbage] /\ ~ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
Wolf <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
In Wolf [Wolf; Cabbage] /\ ~ In Wolf [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat] \/
Goat <> Goat /\
In Goat [Wolf; Cabbage] /\ ~ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] discriminate.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
In Wolf [Wolf; Cabbage] /\ ~ In Wolf [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat] \/
Goat <> Goat /\
In Goat [Wolf; Cabbage] /\ ~ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
In Wolf [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
~ In Wolf [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat] \/
Goat <> Goat /\
In Goat [Wolf; Cabbage] /\ ~ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Wolf [Wolf; Goat; Cabbage]
~ In Wolf [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat] \/
Goat <> Goat /\
In Goat [Wolf; Cabbage] /\ ~ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] auto_not_in.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat] \/
Goat <> Goat /\
In Goat [Wolf; Cabbage] /\ ~ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  left.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat /\ In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
Goat = Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] trivial.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Goat [Wolf; Goat; Cabbage]
H0: In Goat [Goat; Cabbage]
In Goat [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage = Goat /\ In Cabbage [Goat] \/
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  right.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage <> Goat /\
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
Cabbage <> Goat
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] discriminate.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
In Cabbage [Wolf; Cabbage] /\ ~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] split.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
In Cabbage [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
H: In Cabbage [Wolf; Goat; Cabbage]
H0: In Cabbage [Goat; Cabbage]
H1: In Cabbage [Cabbage]
~ In Cabbage [Goat]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] [] auto_not_in.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
NoEats [Wolf; Cabbage]
r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []
  auto with local.r: list Object
Hw: In Wolf r
Hg: In Goat r
Hc: In Cabbage r
RiverCrossing Right [Wolf; Goat; Cabbage] []

  (* initial state: everyone on the left bank *)
  apply initial; repeat auto with local.
Qed.

End SecondAttempt.

Conclusions and Issues

In the end, I was surprised that I was able to produce something that at least resembled a model and proof to the problem. I thought I’d need much more to even begin dealing with this puzzle, especially after failing to find an example solution.

But there are still some issues that I cannot address on my own, given my current knowledge.

I’m not sure if there is another “hole” in my logic, as the first time everything fit into place but was wrong.
The RiverCrossing predicate and the solution still seem overly complicated. I feel that they should be shorter and cleaner…
Both proofs are backwards. I’d like to somehow start from the initial state and build my proof towards the desired goal. I guess one way is to “reverse” the constructors in RiverCrossing and start from the initial state in the solution goal. But that seems wrong.
I still need to specify the initial left and right river banks on the steps that carry an object. I expected that I could use eapply or eauto and let Coq infer those later, yet that didn’t work out. This is kinda annoying.
If I were to use bullets when building the proof steps, each new step would get nested deeper and deeper, making it harder to read. So I just separated them the way I did. I’d love to know how to structure proofs of this form in a more elegant way…

I shared this problem in the Coq Zulip chat asking for advice, but unfortunately, at the time of writing, no one has replied yet. Maybe someone will shed light on those issues someday, and I hope to learn enough to address them in the (distant) future…

Wolf, Goat and Cabbage puzzle, in Coq

Introduction

Basic definitions

First attempt (problematic!)

Second attempt

Conclusions and Issues