Wolf/goat/cabbage, or fox/chicken/grain, or river crossing puzzle in Coq, with automation

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

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

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

Example ex1 :
  ~ (In Goat [Wolf; Cabbage]).
Proof.
  intros contra.
  simpl in contra.
  repeat (destruct contra as [contra | contra]; try discriminate; try apply contra).
Qed.

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

Example ex2 :
  ~ (In Goat [Wolf; Cabbage]).
Proof.
  jauto.
Qed.

Example ex3 :
  ~ (In Goat []).
Proof.
  auto_not_in.
Qed.

Example ex4 :
  In Goat [Cabbage; Wolf] -> False.
Proof.
  intros.
  not_in_absurd H.
Qed.

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

  apply goRight with (l := [Goat]) (r := [Wolf; Cabbage]).
  exists Goat.
  try repeat (split; jauto).
  destruct ol; intros H; not_in_absurd H.
  left. split. trivial. assumption.
  destruct or; try discriminate; not_in_absurd H.
  destruct or; try discriminate; not_in_absurd H.
  assumption. assumption. constructor.

  apply goLeftAlone.
  auto with local.

  apply goRight with (l := [Goat; Cabbage]) (r := [Wolf]).
  exists Cabbage.
  try repeat (split; jauto).
  destruct ol; intros H; not_in_absurd H.
  right. split. discriminate. split. auto with local. auto_not_in.
  left. split. trivial. auto with local.
  destruct or; try discriminate; not_in_absurd H.
  destruct or; try discriminate; not_in_absurd H.
  auto with local. constructor.

  apply goLeft with (l := [Cabbage]) (r := [Wolf; Goat]).
  exists Goat.
  try repeat (split; jauto).
  destruct or; intros H; not_in_absurd H.
  right. split. discriminate. split. auto with local. auto_not_in.
  left. split. trivial. auto with local.
  destruct ol; try discriminate; not_in_absurd H.
  auto with local.

  apply goRight with (l := [Wolf; Cabbage]) (r := [Goat]).
  exists Wolf.
  try repeat (split; jauto).
  destruct ol; intros H; not_in_absurd H.
  left. split. trivial. auto with local.
  right. split. discriminate. split. auto with local. auto_not_in.
  destruct or; try discriminate; not_in_absurd H.
  auto with local.

  apply goLeftAlone.
  auto with local.

  apply goRight with (l := [Wolf; Goat; Cabbage]) (r := []).
  exists Goat.
  try repeat (split; jauto).
  destruct ol; intros H; not_in_absurd H.
  right. split. discriminate. split. auto with local. auto_not_in.
  left. split. trivial. auto with local.
  right. split. discriminate. split. auto with local. auto_not_in.
  auto with local.

  apply initial; repeat auto with local.
Qed.