Wolf, goat and cabbage puzzle in Coq

river_crossing.v

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

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

  (* step 6 : [G] <- [W; C] => [G] || [W; C] *)
  apply goLeftAlone.
  (* proof that Wolf doesn't eat Cabbage *)
  apply NoEatsMore. apply NoEatsOne. trivial.

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

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

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

  (* step 2 : [W; C] <- [G] => [W; C] || [G] *)
  apply goLeftAlone.
  (* proof that Goat doesn't eat itself *)
  apply NoEatsOne.

  (* step 1 : [W; G; C] -G> [] => [W; C] || [G] *)
  apply goRight with (o := Goat) (l := [Wolf; Goat; Cabbage]) (r := []).
  (* Goat in initial left bank *)
  simpl; right; left; reflexivity.
  (* Goat not in final left bank *)
  intros contra; inversion contra; inversion H; inversion H0.
  (* Goat in final right bank *)
  apply in_eq.
  (* proof that Wolf doesn't eat Cabbage *)
  apply NoEatsMore. apply NoEatsOne. trivial.

  (* initial state: everyone on the left bank *)
  apply initial.
  (* Wolf on the initial left bank *)
  simpl; left; reflexivity.
  (* Goat on the initial left bank *)
  simpl; right; left; reflexivity.
  (* Cabbage on the initial left bank *)
  simpl; right; right; left; reflexivity.
Qed.

Hint Constructors Object : local.
Hint Constructors Direction : local.
Hint Constructors NoEats : local.
Hint Resolve eats : local.
Hint Unfold eats : local.
Hint Constructors RiverCrossing : local.
Hint Unfold In : local.
Hint Resolve in_nil : local.
Hint Resolve in_eq : local.
Hint Resolve ex_intro : local.

Theorem solution_auto : forall r,
    In Wolf r ->
    In Goat r ->
    In Cabbage r ->
    RiverCrossing Left [] r.
Proof.
  info_eauto with local.
Qed.

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

(* Second attempt *)
Module SecondAttempt.

(* this new definition seems more solid *)
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 RiverCrossing : local.

(* still... *)
(* - seems overly complicated *)
(* - proof is "backwards" *)
(* - needs to specify [l] and [r] every step *)
(* - proof gets nested and nested... how to structure it? *)

End SecondAttempt.