Zulip Chat Archive

Stream: general

Topic: undead


view this post on Zulip Kevin Buzzard (Aug 23 2018 at 10:35):

"Undead" is a game from [Simon Tatham's portable puzzle collection] (https://www.chiark.greenend.org.uk/~sgtatham/puzzles/). These games are perfect information one player puzzle games, and often solving a level completely (for me at least, in most of these games) involves finding a constructive proof that there is precisely one solution to the level. I'm probably going to supervise a masters project this coming academic year on games like this, so I thought it was about time I understood what I could do with them in Lean.

Here's a [pic of an undead level] (http://wwwf.imperial.ac.uk/~buzzard/xena/blog/undead_initial.png). The diagonal lines in some squares are (two-sided) mirrors. The vacant squares need to be each filled with exactly one of a vampire, ghost or zombie. There are 9 vacant squares and we're told at the top that we need to fill them with three ghosts, three vampires and three zombies. The numbers around the outside of the board are the number of monsters you can see if you look into the board from where the number is, with the caveat that you can't see a ghost directly and you can't see a vampire through a mirror. So for example, the zero on the top row, second from the left, indicates that you can't see the monster in the top left hand corner through a mirror, so it must be a vampire, and the 3 at the left of the top row indicates that exactly one of the monsters in the first column is a ghost (because you can only see three of the four monsters in that column).

This sort of game is really easy to model in Lean; like mathematics, it seems to fit very gracefully into the language of dependent type theory. The nine empty squares can be thought of as 9 variables of type square (or type monster or whatever), the 16 numbers and three totals give 19 equations involving these variables, and the two main claims here are (1) that there's a solution to the equations and (2) it's unique.

Here is a formalisation of the level in Lean, plus some preliminary lemmas.

https://gist.github.com/kbuzzard/53712d672a894d7b158a512f7aa5f836

The lemmas reduce the problem to the following position:

(and actually a little further because I worked out something about a7 after taking that screenshot). The search space initially has size 3^9, which is a bit big perhaps for Lean, but the lemmas I prove about the solution reduce the space to something like 2^7 * 3, which sounds a bit more reasonable. I think I'd now like to brute force it and get a proof that there's a unique solution, plus a description of the solution, but I'm not sure how to do that in Lean. I have these random facts like "variable a6 isn't a vampire" but I am not sure how to write the procedural code in Lean which will save me from generating a gazillion cases with a6 being a vampire. The issue is that I want to do cases on all 8 remaining variables at once, but for the variables where I've proved something I want to immediately eliminate all cases which contradict what I've proved. Am I making sense? I just want to solve the level now, in Lean, without running out of memory, and ideally I'd like to output the solution. I feel like I've done the lion's share of the work now but I've not quite finished.

view this post on Zulip Sean Leather (Aug 23 2018 at 10:47):

@[derive decidable_eq]

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 10:48):

Oh yeah that was it :-) I derived it myself :-) I think I'd find it easier to remember that if I understood what was going on there. Is this the same as @[simp]? It doesn't look like it.

view this post on Zulip Sean Leather (Aug 23 2018 at 10:50):

init/meta/derive.lean says: “Attribute that can automatically derive typeclass instances.”

view this post on Zulip Sean Leather (Aug 23 2018 at 10:51):

Maybe that note will also help me remember the syntax. I don't use it very often, so I have to keep looking for it. But if I know that it's an attribute, I know it must be in @[...].

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 19:18):

I'm working on square 7. After the line cases a₂;cases a₃;cases a₅;cases h₇;cases h₁₅, in tactic mode, it's difficult for me to see what happened. Each of the a's has three possibilities, so after the three cases tactics there are now 27 goals. But for most of them (I think) there is a contradiction with assumptions h7 and h15, so after that entire line is processed we are back to one goal (unless I have misunderstood Lean's output). However I don't seem to be able to read off which of the cases we are in. Is there a trick for me to track which of the 27 branches survived?

view this post on Zulip Chris Hughes (Aug 23 2018 at 19:47):

Prove it's equivalent to proving ∃! (a₁ ∈ [vampire, ghost]) (a₂ ∈ [ghost, zmobie]) ... and use dec_trivial. You might have to guide simp a bit, and prove lemmas like a ! = zombie iff a = vampire or a = ghost

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 19:50):

Actually I am now confused about whether I have even done what I think I've done. Is this a bug? What happens if you type this into a Lean file:

inductive square
| vampire : square
| ghost : square
| zombie : square

theorem test (a b c d : square) : false :=
begin
  cases a;cases b,
  cases c;cases d,
  repeat {sorry}
end

and then put your cursor just after the end comma in the cases a;cases b, line? I expect to see 9 goals but I only see one. Typing "sorry" makes the next one appear :-) Typing a few sorries eventually sorts things out and then it's back to 9 goals.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 19:52):

Even weirder:

inductive square
| vampire : square
| ghost : square
| zombie : square

theorem test (a b c d : square) : false :=
begin
  cases a;cases b,
  sorry,
  sorry,
  cases c;cases d,
  repeat {sorry}
end

After the b, there are 9 cases, after the next sorry there are 8, and after the next one it drops to one. The others are still there, they're just not being displayed for some reason.


view this post on Zulip Chris Hughes (Aug 23 2018 at 19:55):

It seems to be being parsed as this

theorem test (a b c d : square) : false :=
begin
  cases a; {cases b,
  cases c; cases d,
  repeat {sorry}},
end

view this post on Zulip Chris Hughes (Aug 23 2018 at 19:56):

Actually not quite.

view this post on Zulip Gabriel Ebner (Aug 23 2018 at 19:58):

I think the ; just messes up the information on the current line. If you put skip, on another line it shows the expected number of goals.

view this post on Zulip Gabriel Ebner (Aug 23 2018 at 20:00):

Information about the goal is stored in a very unstructured form at the moment: essentially there is a function tactic.save_info which stores the corresponding string at a user-specified position (= line/column pair, and yes this can be almost anywhere..).

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 20:07):

If you put skip then on the line before the skip it displays correctly. So perhaps it's the second semicolon which is causing the confusion.

view this post on Zulip Gabriel Ebner (Aug 23 2018 at 20:10):

Yes, the semicolon seems to break the goal output between the surrounding commas. If you add a skip, then you add a comma which keeps the breakage away.

view this post on Zulip Patrick Massot (Aug 23 2018 at 20:55):

I've noticed repeatedly that using semi-colon is very confusing in this way

view this post on Zulip Patrick Massot (Aug 23 2018 at 20:56):

About the general problem, isn't something that could be handled entirely by the type class system? It looks like problem designed for solving using prolog.

view this post on Zulip Andrew Ashworth (Aug 23 2018 at 21:08):

i believe sebastian solved the n-queens problem using type classes

view this post on Zulip Andrew Ashworth (Aug 23 2018 at 21:10):

this is really an abuse of inference I think :)

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:12):

Prove it's equivalent to proving ∃! (a₁ ∈ [vampire, ghost]) (a₂ ∈ [ghost, zmobie]) ... and use dec_trivial. You might have to guide simp a bit, and prove lemmas like a ! = zombie iff a = vampire or a = ghost

So how does dec_trivial work? Does it look at hypotheses? Why doesn't this work:

@[derive decidable_eq]
inductive square
| vampire : square
| ghost : square
| zombie : square

open square

lemma thing :  a : square, a = vampire  a = ghost  a = zombie := dec_trivial -- fails

It looks pretty decidably trivial to me. How can I make this work?

view this post on Zulip Chris Hughes (Aug 23 2018 at 21:12):

Prove fintype square

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:15):

@[derive fintype]?

view this post on Zulip Kenny Lau (Aug 23 2018 at 21:17):

look at my three elsewhere lol

view this post on Zulip Patrick Massot (Aug 23 2018 at 21:17):

What is this derive? I see this from time to time but never know what it means

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:19):

What I wrote doesn't work.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:19):

failed to find a derive handler for 'fintype'

view this post on Zulip Andrew Ashworth (Aug 23 2018 at 21:26):

I believe the derive stuff is user-written extensions that add functionality to a type. like @[derive decidable_eq] adds an automatically generated instance saying that the type is decidable

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:29):

definition finset_square : finset square :=
{ val := [vampire,ghost,zombie],
  nodup := begin
    repeat {constructor,intro a,cases a,repeat {exact dec_trivial}},
    constructor,
  end
}

instance : fintype square := {
  elems := finset_square,
  complete := λ x,by cases x;exact dec_trivial
}

:-)

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:30):

I reckon that could be automated...

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:31):

instance : fintype three :=
{ elems := {A, B, C},
  complete := λ x, by cases x; simp }

Kenny's three

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:39):

import data.fintype

@[derive decidable_eq]
inductive square
| vampire : square
| ghost : square
| zombie : square

open square

instance : fintype square := {
  elems := {vampire,ghost,zombie},
  complete := λ x,by cases x;exact dec_trivial
}

open square

lemma thing2 : ∃! a : square, a = vampire := dec_trivial -- fails

That looks pretty trivial too. Error is

failed to synthesize type class instance for
⊢ decidable (∃! (a : square), a = vampire)

view this post on Zulip Kenny Lau (Aug 23 2018 at 21:40):

you need to import something iirc

view this post on Zulip Chris Hughes (Aug 23 2018 at 21:40):

unfold exists_unique first

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:45):

rofl I just tried it for the actual problem and I got this error: https://gist.github.com/kbuzzard/84dbdf0fab4b96148099f49ac4f1770e . I think I've seen this before when you do exists_unique with multiple variables, it unfolds to something quite unwieldy.

view this post on Zulip Patrick Massot (Aug 23 2018 at 21:46):

nice goal!

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:46):

example : ∃! (a b c : ), a + b + c = 0 :=
begin
  unfold exists_unique,
/-
∃ (x : ℕ),
    (∃ (x_1 : ℕ),
         (∃ (x_2 : ℕ), x + x_1 + x_2 = 0 ∧ ∀ (y : ℕ), x + x_1 + y = 0 → y = x_2) ∧
           ∀ (y : ℕ),
             (∃ (x_1 : ℕ), x + y + x_1 = 0 ∧ ∀ (y_1 : ℕ), x + y + y_1 = 0 → y_1 = x_1) → y = x_1) ∧
      ∀ (y : ℕ),
        (∃ (x : ℕ),
           (∃ (x_1 : ℕ), y + x + x_1 = 0 ∧ ∀ (y_1 : ℕ), y + x + y_1 = 0 → y_1 = x_1) ∧
             ∀ (y_1 : ℕ),
               (∃ (x : ℕ), y + y_1 + x = 0 ∧ ∀ (y_2 : ℕ), y + y_1 + y_2 = 0 → y_2 = x) → y_1 = x) →
        y = x
-/
  sorry
end

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:47):

Does it have to do that? Why not just "exists a b c, a + b + c = 0 and forall a' b' c', a' + b' + c' = 0 implies a=a' and b=b' and c=c'"?

view this post on Zulip Chris Hughes (Aug 23 2018 at 21:53):

It's parsed as a load of nested exists_uniques. I imagine your definition is quite hard to write

view this post on Zulip Reid Barton (Aug 23 2018 at 21:55):

Wait, does it even mean the right thing then?

view this post on Zulip Reid Barton (Aug 23 2018 at 21:57):

Isn't this "there exists a unique a such that there exists a unique b such that ...", but maybe for some other a there's multiple b's which would work, and so there isn't actually a unique (a,b,c)

view this post on Zulip Reid Barton (Aug 23 2018 at 22:04):

Say P x y holds if and only if (x, y) is (1, 2) or (3, 4) or (3, 5). Then ∃! x y, P x y = ∃! x, ∃! y, P x y is true because ∃! y, P x y holds only for x = 1.

view this post on Zulip Reid Barton (Aug 23 2018 at 22:05):

But I'm sure what you really wanted is ∃! p, P p.1 p.2.

view this post on Zulip Patrick Massot (Aug 23 2018 at 22:06):

That's a pretty nasty trap

view this post on Zulip Sebastian Ullrich (Aug 23 2018 at 22:08):

makes note to remove this "feature" as soon as possible

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 22:13):

I think I once tried to prove exactly the goal above and decided at the end of it that it seemed to be an extremely roundabout way of saying the correct thing.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 22:17):

I think it unfolds to something more complicated than what Reid is suggesting.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 22:17):

In particular I'm suggesting that Chris' comment is oversimplifying the matter.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 22:18):

Here's an example of an intermediate goal that you have to prove when proving the exists_unique statement above:

y : ℕ,
h : ∃ (x : ℕ), 0 + y + x = 0 ∧ ∀ (y_1 : ℕ), 0 + y + y_1 = 0 → y_1 = x
⊢ y = 0

view this post on Zulip Reid Barton (Aug 23 2018 at 22:20):

This is after you set a and b to 0, right?

view this post on Zulip Reid Barton (Aug 23 2018 at 22:21):

You shouldn't be given the ∀ (y_1 : ℕ), 0 + y + y_1 = 0 → y_1 = x part of the hypothesis

view this post on Zulip Reid Barton (Aug 23 2018 at 22:21):

I think. Actually staring at this is making me confused.

view this post on Zulip Reid Barton (Aug 23 2018 at 22:22):

But in general, the way that Lean interprets ∃! x y, ... is as ∃! x, ∃! y, ..., right?

view this post on Zulip Mario Carneiro (Aug 23 2018 at 22:29):

Description: An alternate definition of double existential uniqueness (see 2eu4 2371). A mistake sometimes made in the literature is to use ∃!𝑥∃!𝑦 to mean "exactly one 𝑥 and exactly one 𝑦." (For example, see Proposition 7.53 of [TakeutiZaring] p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining ∀𝑥∃* 𝑦𝜑 as an additional condition. The correct definition apparently has never been published. (∃* means "exists at most one.")

http://us.metamath.org/mpeuni/2eu5.html

view this post on Zulip Reid Barton (Aug 23 2018 at 22:29):

You want to prove (0, 0, 0) is the unique solution (let's say). Then you ought to be able to prove

y : ,
h :  (x : ), 0 + y + x = 0
 y = 0

view this post on Zulip Mario Carneiro (Aug 23 2018 at 22:31):

the simplest way to assert multiple existential uniqueness is to claim unique existence of a triple

view this post on Zulip Mario Carneiro (Aug 23 2018 at 22:34):

also: why are you using lean as a sat solver? It's not particularly smart for this

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:07):

@Kenny Lau you might like this challenge:

example (p :     Prop) :
( m n, p m n  ( b c : , p b c  b = m  c = n))  ∃! m n : , p m n := sorry

Mario -- did I get this right? I just spent 15 minutes on it and failed to do one way; I don't want to waste Kenny's time.

I'm using Lean as a whatever-you-said because I'm trying to figure out what can and can't and should be done using Lean when it comes to puzzles like this.

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:12):

as Reid points out, as well as the quote I gave, that theorem is false

view this post on Zulip Reid Barton (Aug 23 2018 at 23:16):

There are other tools out there which are a better fit for these kinds of constraint satisfaction problems. One of which even shares an author with Lean.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:16):

right, I just went back to it and figured that it couldn't possibly be provable.

view this post on Zulip Reid Barton (Aug 23 2018 at 23:16):

However, you can't beat the convenience of already knowing the input language.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:16):

In which case I don't understand what this exists_unique even means.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:18):

I could solve this undead puzzle in python just with some dull loop. I was trying to work out what Lean could offer me that python couldn't.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:19):

So Lean really does do what Chris says? "There exists a unique x such that there exists a unique y such that..."? That's not what I would have guessed from the notation.

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:25):

example : ¬ ∀ (p : ℕ → ℕ → Prop),
  (∃ m n, p m n ∧ (∀ b c : ℕ, p b c → b = m ∧ c = n)) ↔ ∃! m n : ℕ, p m n :=
λ H, begin
  let p := λ m n, m = 0 → n = 0,
  have : ∃! m n : ℕ, p m n,
  { refine ⟨0, ⟨0, λ _, rfl, λ n h, h rfl⟩, λ m h, _⟩,
    rcases h with ⟨m', h₁, h₂⟩,
    by_contra h,
    have := h₂ 1 h.elim,
    rw ← h₂ 0 (λ _, rfl) at this,
    cases this },
  rcases (H _).2 this with ⟨m, n, h₁, h₂⟩,
  simpa [(h₂ 0 0 id).1.symm] using h₂ 1 1 id
end

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:25):

this is what all nested binders are unfolded to in lean

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:26):

in most cases it works brilliantly - forall, exists, indexed union, supremum, infinite sum... it is only exists unique which doesn't have a nice interpretation

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:29):

rofl

definition p (a b : ) := (a = 1  b = 1)  (a = 2  b = 3)  (a = 2  b = 4)

theorem silly : ∃! a b, p a b :=
begin
  existsi 1,
  split,
  existsi 1,
  split,
  left,exact dec_trivial,
  intros y,
  unfold p,
  simp,intro H,
  cases H,exact H,cases H,cases H,cases H_left,cases H,cases H_left,
  intros y Hy,
  unfold p at Hy,
  cases Hy with x Hx,
  cases Hx with H H1,
  cases H,exact H.left,
  cases H,cases H with Hy Hx,
  dsimp at H1,rw Hx at *,
  have H := H1 4,
  suffices : 4 = 3,
    revert this,exact dec_trivial,
  apply H,rw Hy,simp,
  cases H with Hy Hx,
  dsimp at H1,rw Hx at *,
  have H := H1 3,
  suffices : 3 = 4,
    revert this,exact dec_trivial,
  apply H,rw Hy,simp
end

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:30):

I had no idea ∃! meant that in Lean. That is for me a very surprising design decision. ∃! a b doesn't even mean the same as ∃! b a, right?

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:30):

no, they are not logically equivalent

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:30):

frankly the problem is that ∃! is a shitty binder notation

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:30):

wo

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:31):

w

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:31):

it's not monotone

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:31):

So in fact the thing I'm trying to prove with this undead thing is not even formulated correctly.

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:32):

like I said, the easy way to say this without having to think much is to use exists unique in a pair type

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:33):

I don't care what Lean thinks ∃! means. All I want to say is that there exists a unique 9-tuple with some property, and I've just realised that I'd better spell it out rather than using this terrifying notation.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:34):

I wonder if any of the mathematicians here can find a mathematician who thinks ∃! a b, p a b means anything other than what I suggested it meant above with that false lemma.

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:36):

I see. The reason this has happened is that Lean has one inbuilt system for dealing with multiple variables with one binder, and to put it bluntly it doesn't work with this one, so really perhaps a different system should be used for this one binder and that might be what Sebastian was saying. Maybe I've caught up at last.

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:41):

I wonder if any of the mathematicians here can find a mathematician who thinks ∃! a b, p a b means anything other than what I suggested it meant above with that false lemma.

Most mathematicians think ∃! a b, p a b means what you wrote. They also think that ∃! a, ∃! b, p a b encodes this statement, and they are wrong

view this post on Zulip Mario Carneiro (Aug 23 2018 at 23:42):

it is obvious once you give it more than a cursory examination, but it's one of those things that often escapes notice

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 23:46):

Most mathematicians think ∃! a b, p a b means what you wrote. They also think that ∃! a, ∃! b, p a b encodes this statement, and they are wrong

I don't think I'd ever even considered the concept ∃! a, ∃! b, p a b until this evening and I suspect that many mathematicians would also not have come across it. It looks very weird to me. Of course, hindsight is a wonderful thing...


Last updated: May 06 2021 at 22:13 UTC