## Stream: maths

### Topic: wolf goat cabbage

#### Johan Commelin (Aug 31 2019 at 08:13):

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

#### Johan Commelin (Aug 31 2019 at 08:14):

Would the game theory PR help here?

#### Johan Commelin (Aug 31 2019 at 08:15):

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

#### Johan Commelin (Aug 31 2019 at 08:16):

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 (Aug 31 2019 at 08:17):

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

#### Mario Carneiro (Aug 31 2019 at 08:38):

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 (Aug 31 2019 at 08:40):

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

#### Mario Carneiro (Aug 31 2019 at 08:41):

(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 (Aug 31 2019 at 09:23):

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 (Aug 31 2019 at 09:28):

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

#### Mario Carneiro (Aug 31 2019 at 09:39):

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 (Aug 31 2019 at 09:40):

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

#### Johan Commelin (Aug 31 2019 at 13:25):

@Mario Carneiro Wow, thanks a lot!

#### Johan Commelin (Aug 31 2019 at 13:25):

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

#### Johan Commelin (Aug 31 2019 at 13:44):

(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 (Aug 31 2019 at 13:55):

s/solution_from/position/g

#### Johan Commelin (Aug 31 2019 at 13:55):

notation left_shore :=  tt
notation right_shore := ff


#### Johan Commelin (Aug 31 2019 at 13:55):

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 (Aug 31 2019 at 13:56):

With tactic states like:

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


#### Keeley Hoek (Aug 31 2019 at 14:43):

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

#### Jeremy Avigad (Aug 31 2019 at 16:55):

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 (Aug 31 2019 at 17:27):

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

#### Patrick Massot (Aug 31 2019 at 17:30):

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

#### Johan Commelin (Aug 31 2019 at 17:31):

Aaah, I forgot about that one...

#### Jeremy Avigad (Aug 31 2019 at 17:38):

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 (Aug 31 2019 at 17:40):

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

#### Jeremy Avigad (Aug 31 2019 at 17:40):

(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 (Aug 31 2019 at 17:42):

@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 (Aug 31 2019 at 18:00):

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 (Aug 31 2019 at 18:01):

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 (Aug 31 2019 at 18:06):

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

#### Kevin Buzzard (Aug 31 2019 at 18:17):

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 (Aug 31 2019 at 20:44):

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!

Wow! Just wow!

#### Johan Commelin (Aug 31 2019 at 20:50):

This makes "no goals" so depressing...

#### Johan Commelin (Aug 31 2019 at 20:52):

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

#### Johan Commelin (Aug 31 2019 at 20:53):

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 (Aug 31 2019 at 21:18):

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 (Sep 01 2019 at 02:26):

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 (Oct 11 2019 at 11:45):

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 (Oct 11 2019 at 13:28):

that sounds like incredible.pm

Yes. Thank you!

#### Bryan Gin-ge Chen (Oct 11 2019 at 13:47):

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 (Oct 11 2019 at 13:53):

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 (Oct 11 2019 at 13:54):

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 (Oct 11 2019 at 13:58):

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

#### Bryan Gin-ge Chen (Oct 11 2019 at 13:59):

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

Last updated: May 11 2021 at 16:22 UTC