# Zulip Chat Archive

## 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!

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

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

#### Wojciech Nawrocki (Oct 11 2019 at 13:39):

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