wolf goat cabbage

Stream: maths

[Johan Commelin]

Can we formalise the wolf-goat-cabbage problem, and its solution? As nice as possible...

[Johan Commelin]

Would the game theory PR help here?

[Johan Commelin]

I would like to have a tactic proof that works as an actual game.

[Johan Commelin]

So that my kids can write the tactic carry_in_boat wolf, and it will fail with the error message: "Can't do that, the goat would eat the cabbage".

[Johan Commelin]

And the tactic state should reflect in a clean way where all the protagonists are.

[Mario Carneiro]

You mean like this?

import data.list.defs

namespace list

instance decidable_chain₂ {α R} [decidable_rel R] (a : α) (l : list α) : decidable (chain R a l) :=
begin
  induction l generalizing a,
  exact is_true chain.nil,
  exactI decidable_of_iff' _ chain_cons
end

instance decidable_chain'₂ {α R} [decidable_rel R] (l : list α) : decidable (chain' R l) :=
by cases l; dunfold chain'; apply_instance

end list

namespace WGC

@[derive decidable_eq]
structure state := (wolf goat cabbage farmer : bool)

def valid (s : state) :=
¬ (s.wolf = s.goat ∧ s.farmer ≠ s.wolf) ∧
¬ (s.goat = s.cabbage ∧ s.farmer ≠ s.goat)

instance : decidable_pred valid | s := by unfold valid; apply_instance

def step (s₁ s₂ : state) :=
s₁.farmer ≠ s₂.farmer ∧
((s₁.wolf = s₂.wolf ∧ s₁.goat = s₂.goat ∧ s₁.cabbage = s₂.cabbage) ∨
 (s₁.wolf = s₂.wolf ∧ s₁.goat = s₂.goat ∧ s₁.cabbage = s₁.farmer ∧ s₂.cabbage = s₂.farmer) ∨
 (s₁.wolf = s₂.wolf ∧ s₁.goat = s₁.farmer ∧ s₂.goat = s₂.farmer ∧ s₁.cabbage = s₂.cabbage) ∨
 (s₁.wolf = s₁.farmer ∧ s₂.wolf = s₂.farmer ∧ s₁.cabbage = s₂.cabbage ∧ s₁.goat = s₂.goat))

instance : decidable_rel step | s₁ s₂ := by unfold step; apply_instance

def path : list state :=
[⟨ff, ff, ff, ff⟩,
 ⟨ff, tt, ff, tt⟩,
 ⟨ff, tt, ff, ff⟩,
 ⟨ff, tt, tt, tt⟩,
 ⟨ff, ff, tt, ff⟩,
 ⟨tt, ff, tt, tt⟩,
 ⟨tt, ff, tt, ff⟩,
 ⟨tt, tt, tt, tt⟩]

theorem path_start : path.head' = some ⟨ff, ff, ff, ff⟩ := rfl
theorem path_end : path.last' = some ⟨tt, tt, tt, tt⟩ := rfl
theorem path_step : list.chain' step path := dec_trivial
theorem path_valid : ∀ s ∈ path, valid s := dec_trivial

end WGC

[Mario Carneiro]

Ah, I guess I'm not meeting your secondary objectives...

[Mario Carneiro]

(PS: I had to fix some broken definitions of the decidable instances for chain and chain' here, caused by improper use of simp in a decidability proof.)

[Mario Carneiro]

Here's a more gamey version:

import data.list.basic

namespace list

instance decidable_chain₂ {α R} [decidable_rel R] (a : α) (l : list α) : decidable (chain R a l) :=
begin
  induction l generalizing a,
  exact is_true chain.nil,
  exactI decidable_of_iff' _ chain_cons
end

instance decidable_chain'₂ {α R} [decidable_rel R] (l : list α) : decidable (chain' R l) :=
by cases l; dunfold chain'; apply_instance

end list

namespace WGC

structure state := (wolf goat cabbage farmer : bool)

def valid (s : state) :=
¬ (s.wolf = s.goat ∧ s.farmer ≠ s.wolf) ∧
¬ (s.goat = s.cabbage ∧ s.farmer ≠ s.goat)

instance : decidable_pred valid | s := by unfold valid; apply_instance

def step (s₁ s₂ : state) :=
s₁.farmer ≠ s₂.farmer ∧
((s₁.wolf = s₂.wolf ∧ s₁.goat = s₂.goat ∧ s₁.cabbage = s₂.cabbage) ∨
 (s₁.wolf = s₂.wolf ∧ s₁.goat = s₂.goat ∧ s₁.cabbage = s₁.farmer ∧ s₂.cabbage = s₂.farmer) ∨
 (s₁.wolf = s₂.wolf ∧ s₁.goat = s₁.farmer ∧ s₂.goat = s₂.farmer ∧ s₁.cabbage = s₂.cabbage) ∨
 (s₁.wolf = s₁.farmer ∧ s₂.wolf = s₂.farmer ∧ s₁.cabbage = s₂.cabbage ∧ s₁.goat = s₂.goat))

instance : decidable_rel step | s₁ s₂ := by unfold step; apply_instance

def solution_from (s : state) :=
{p : list state // p.head' = some s ∧
  p.last' = some ⟨tt, tt, tt, tt⟩ ∧
  list.chain' step p ∧
  ∀ s' ∈ p, valid s'}

def finish : solution_from ⟨tt, tt, tt, tt⟩ :=
⟨[⟨tt, tt, tt, tt⟩], dec_trivial⟩

def solution_from.step {s₁} (s₂)
  (H₁ : valid s₁) (H₂ : step s₁ s₂)
  (p : solution_from s₂) : solution_from s₁ :=
⟨s₁ :: p.1, begin
  rcases p.2 with ⟨h₁, h₂, h₃, h₄⟩,
  cases p.1 with a l; cases h₁,
  exact ⟨rfl, h₂, list.chain.cons H₂ h₃,
    list.forall_mem_cons.2 ⟨H₁, h₄⟩⟩
end⟩

section
open tactic tactic.interactive interactive lean.parser

meta def negate : expr → tactic expr
| `(tt) := return `(ff)
| `(ff) := return `(tt)
| _ := fail "invalid goal"

meta def carry_in_boat (n : parse ident) : tactic unit := do
  `(solution_from ⟨%%w, %%g, %%c, %%f⟩) ← target | fail "invalid goal",
  f' ← negate f,
  (w', g', c') ← match n with
  | `wolf := do
    when (¬ w =ₐ f) $ fail "Can't do that, the wolf is on the other side.",
    w' ← negate w,
    when (g =ₐ c ∧ ¬ g =ₐ f') $ fail "Can't do that, the goat would eat the cabbage.",
    return (w', g, c)
  | `goat := do
    when (¬ g =ₐ f) $ fail "Can't do that, the goat is on the other side.",
    g' ← negate g,
    return (w, g', c)
  | `cabbage := do
    when (¬ c =ₐ f) $ fail "Can't do that, the cabbage is on the other side.",
    c' ← negate c,
    when (w =ₐ g ∧ ¬ g =ₐ f') $ fail "Can't do that, the wolf would eat the goat.",
    return (w, g, c')
  | `nothing := do
    when (g =ₐ c ∧ ¬ g =ₐ f') $ fail "Can't do that, the goat would eat the cabbage.",
    when (w =ₐ g ∧ ¬ g =ₐ f') $ fail "Can't do that, the wolf would eat the goat.",
    return (w, g, c)
  | _ := fail "invalid choice"
  end,
  tactic.refine ``(solution_from.step
    ⟨%%w', %%g', %%c', %%f'⟩ dec_trivial dec_trivial _),
  tactic.try (exact `(finish))

run_cmd add_interactive [``carry_in_boat]
end

theorem solution : solution_from ⟨ff, ff, ff, ff⟩ :=
begin
  carry_in_boat goat,
  carry_in_boat nothing,
  carry_in_boat cabbage,
  carry_in_boat goat,
  carry_in_boat wolf,
  carry_in_boat nothing,
  carry_in_boat goat,
end

end WGC

[Mario Carneiro]

Manipulating the tactic state for a better display of the protagonists is more difficult though

[Mario Carneiro]

I don't think the game theory stuff would help, as it's primarily for two-player games and this is a one-player game

[Mario Carneiro]

unless you model the actions of the wolf and goat as an adversarial player rather than a constraint

[Johan Commelin]

@Mario Carneiro Wow, thanks a lot!

[Johan Commelin]

I'm only seeing it now, because we had an "emergency" swimming pool party, to keep the kids busy.

[Johan Commelin]

(PS: I had to fix some broken definitions of the decidable instances for chain and chain' here, caused by improper use of simp in a decidability proof.)

Do you mean "fix" in mathlib? Currently the dec_trivial in the proof of finish gives an error on my side. Are those fixes meant to fix that?

[Johan Commelin]

s/solution_from/position/g

[Johan Commelin]

notation `left_shore` :=  tt
notation `right_shore` := ff

[Johan Commelin]

theorem solution : position ⟨ff, ff, ff, ff⟩ :=
begin
  carry_in_boat goat,
  carry_in_boat nothing,
  carry_in_boat cabbage,
  carry_in_boat goat,
  carry_in_boat wolf,
  carry_in_boat nothing,
  carry_in_boat goat,
end

[Johan Commelin]

With tactic states like:

1 goal
⊢ position {wolf := right_shore, goat := left_shore, cabbage := left_shore, farmer := left_shore}

[Keeley Hoek]

I think we need a whole bunch of xyz := dec_trivial tests

[Jeremy Avigad]

This is a nice example. I think it should be in the archive folder. Even better: design a custom interactive tactic state that shows the state with little ASCII-art or unicode representations. That would be a great advertisement for kids.
We could have a whole library of Lean puzzles, like the 15 puzzle, or this one: https://www.cs.brandeis.edu/~storer/JimPuzzles/ZPAGES/zzzTrafficJam.html.

[Johan Commelin]

Is the tactic state customisable? :interrobang: :hushed: That sounds really cool!

[Patrick Massot]

Of course it is. Don't you use the Kevin tactic monad?

[Johan Commelin]

Aaah, I forgot about that one...

[Jeremy Avigad]

Yes, it is cool. You can change the way the state is displayed, add extra state, add instructions to be carried out after every command, etc. It is not well documented, but Leo put an example here: tests/interactive/my_tactic_class.lean. I used it here: https://github.com/avigad/embed/blob/master/src/interactive.lean. Seul Baek and Simon Hudon have also used it.
When even these little bits of customization are so much fun, can you imagine what things will be like with Lean 4?

[Reid Barton]

Sort of related is https://github.com/A1kmm/proofsweeper

[Jeremy Avigad]

(Seul, Simon, and I all used to it implement a "proof system with a proof system", e.g. https://github.com/avigad/embed/blob/master/src/examples.lean.)

[Jeremy Avigad]

@Reid Barton Cool. I have been told that the video game industry is much bigger than the film industry. We need to make ITP even more like playing video games.

[Kevin Buzzard]

I keep meaning to finish my blog post explaining how my favourite computer game used to be the Zelda series but now it's the Lean series.

[Kevin Buzzard]

OTOH it took me a year to understand how to play Lean; ideally it should take rather less long than that. I think it's striking that I haven't played any Zelda for well over a year now though.

[Jeremy Avigad]

We need avatars that can traverse fiber bundles and do battle with singular measures.

[Kevin Buzzard]

I definitely think about maths in a much more geometric way then lean and I'm sure that this is even more true for the geometers

[Bryan Gin-ge Chen]

This seemed like a good use-case for the Observable editor:

https://observablehq.com/d/5d494b42d8ce39e8

It should be possible to create some buttons (in a "custom footer") that allow users to click to insert / edit carry_in_boat XX lines and also to create graphics for the errors as well. I'll hold off on more changes for now in case the Lean code is updated (and also since it's dinnertime). Feel free to suggest ideas!

[Johan Commelin]

Wow! Just wow!

[Johan Commelin]

This makes "no goals" so depressing...

[Johan Commelin]

Maybe you should compensate for it by having confetti all over the screen, and playing some victory tune.

[Johan Commelin]

This is the solution that I created with my kids this morning: https://weblog.commelin.net/wp-content/uploads/2019/08/wgc_80.gif

[Kevin Buzzard]

That's great Bryan! But the solution at https://xkcd.com/1134/ doesn't work :-/

theorem solution : solution_from ⟨ff, ff, ff, ff⟩ :=
begin
  carry_in_boat goat,
  carry_in_boat nothing,
  carry_in_boat cabbage,
end

[Bryan Gin-ge Chen]

This makes "no goals" so depressing...

I updated the notebook so now it shows the end state as well as a :tada: emoji.

[Wojciech Nawrocki]

I recall that at Big Proof 2019 a few people were playing this online drag-n-drop proof game, where graph nodes are more or less inference rules. I was looking for it and for the life of me can't find it - does anyone remember the website name?

[Mario Carneiro]

that sounds like incredible.pm

[Wojciech Nawrocki]

Yes. Thank you!

[Bryan Gin-ge Chen]

I had forgotten about this. At some point I'd like to clean up my notebook and "publish" it on Observable. Before that, what's going on with this error I'm seeing in @Mario Carneiro 's code above? (I guess @Johan Commelin pointed this out too):

def finish : solution_from ⟨tt, tt, tt, tt⟩ :=
⟨[⟨tt, tt, tt, tt⟩], dec_trivial⟩
/-
failed to synthesize type class instance for
⊢ decidable
    (list.head' [{wolf := tt, goat := tt, cabbage := tt, farmer := tt}] =
         some {wolf := tt, goat := tt, cabbage := tt, farmer := tt} ∧
       list.last' [{wolf := tt, goat := tt, cabbage := tt, farmer := tt}] =
           some {wolf := tt, goat := tt, cabbage := tt, farmer := tt} ∧
         list.chain' step [{wolf := tt, goat := tt, cabbage := tt, farmer := tt}] ∧
           ∀ (s' : state), s' ∈ [{wolf := tt, goat := tt, cabbage := tt, farmer := tt}] → valid s')
-/

[Mario Carneiro]

that's odd. I guess I must have changed something relevant in data.list.basic when I was fiddling with those decidable instances

[Mario Carneiro]

it works if you put @[derive decidable_eq] on structure state, or if you replace the proof of finish with ⟨[⟨tt, tt, tt, tt⟩], rfl, rfl, dec_trivial⟩

[Bryan Gin-ge Chen]

Great! I wonder why later code that used finish still worked when it had the error.

[Bryan Gin-ge Chen]

Oh, maybe tactic.try doesn't care about missing instances.