Zulip Chat Archive

Stream: maths

Topic: wolf goat cabbage


view this post on Zulip Johan Commelin (Aug 31 2019 at 08:13):

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

view this post on Zulip Johan Commelin (Aug 31 2019 at 08:14):

Would the game theory PR help here?

view this post on Zulip Johan Commelin (Aug 31 2019 at 08:15):

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

view this post on Zulip 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".

view this post on Zulip Johan Commelin (Aug 31 2019 at 08:17):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 31 2019 at 08:40):

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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 31 2019 at 09:28):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 31 2019 at 13:25):

@Mario Carneiro Wow, thanks a lot!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 31 2019 at 13:55):

s/solution_from/position/g

view this post on Zulip Johan Commelin (Aug 31 2019 at 13:55):

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

view this post on Zulip 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

view this post on Zulip 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}

view this post on Zulip Keeley Hoek (Aug 31 2019 at 14:43):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 31 2019 at 17:27):

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

view this post on Zulip Patrick Massot (Aug 31 2019 at 17:30):

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

view this post on Zulip Johan Commelin (Aug 31 2019 at 17:31):

Aaah, I forgot about that one...

view this post on Zulip 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?

view this post on Zulip Reid Barton (Aug 31 2019 at 17:40):

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

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jeremy Avigad (Aug 31 2019 at 18:06):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Aug 31 2019 at 20:49):

Wow! Just wow!

view this post on Zulip Johan Commelin (Aug 31 2019 at 20:50):

This makes "no goals" so depressing...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 11 2019 at 13:28):

that sounds like incredible.pm

view this post on Zulip Wojciech Nawrocki (Oct 11 2019 at 13:39):

Yes. Thank you!

view this post on Zulip 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')
-/

view this post on Zulip 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

view this post on Zulip 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⟩

view this post on Zulip 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.

view this post on Zulip 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