Conway's Angel Problem

Stream: new members

[Patrick Johnson]

Considering suggestions from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/First.20contribution, seems like there is not much of a need for verified algorithms in Lean 3. Since I still want to contribute something, and being encouraged by Yaël's advice that "useless" theorems are welcome too, I decided to start formalizing the proof of Conway's Angel problem, strictly following this paper.

Would you like to take a look at my initial draft (definitions and the main theorem statement)? Is there anything I should fix wrt notation or naming conventions before I proceed? Note: In the definitions, "angel" is called "player₁" and "devil" is called "player₂" because it sounds more neutral. Did I make some trivial mistake in the definitions?

[Eric Wieser]

An initial comment; what you've called the Manhattan distance is not the usual definition

[Patrick Johnson]

Ah, right. Fixed. I think "Moore neighborhood distance" is a more appropriate name.

[Yaël Dillies]

angel and devil are definitely more memorable names than player₁, player₂! Do not feel like you need to be neutral. This is standard nomenclature.

[David Wärn]

With these definitions, there is actually no strategy for either player and the main theorem is trivially false. Do you see why?

lemma oops : is_empty Strategy₁ :=
{ false := begin
    intro strat,
    set p := strat.fn ⟨default _, ∅, default _, default _⟩,
    have : p ∈ reachable_tiles _, apply strat.h,
    exact this.1,
  end }

I think it would be very nice to see a formal proof that an angel of power 2 wins, but don't expect it to be easy.

[Patrick Johnson]

@David Wärn Good catch! Fixed. That's the exact reason why I asked for a revision before I proceed with the proof. Four eyes are better than two.

[Patrick Johnson]

Update: I refactored the entire file. Some quick feedback would be nice. Does it look good so far?

[Yaël Dillies]

I would advise you not to define so many new types: Point and Moveprobably don't need to exist. Instead of getting whose turn it is through a parity condition, it's easier to make that data a field of Board.

[Patrick Johnson]

Instead of getting whose turn it is through a parity condition, it's easier to make that data a field of Board.

Yeah, I already tried that, but things get horribly complicated. The idea is that the Board is intended to be a raw data structure that should not be "trusted". The board is defined in terms of the list of moves, so the turn field needs to be computed anyway. The function is_turn_a is used by other functions that are not "aware" of the Board type.

I would advise you not to define so many new types: Point and Moveprobably don't need to exist.

Is abbreviation better, or should I explicitly write option (ℤ × ℤ) everywhere?

[Yaël Dillies]

You could just write option (ℤ × ℤ) everywhere.

[David Wärn]

Usually the best way to see if your definitions are correct is to try to prove things about them. It's hard to know what the best definitions are from the start. Even if your definitions are mathematically correct they may be difficult to work with.

I think you should consider working in a more abstract setting. At best it will make your proofs both more readable and more general. Here's one possible notion of an infinite 2-player game: you have a type S of states together with functions angel_moves, devil_moves : S -> set S. Then you can inductively define which elements of {angel, devil} x S are devil-wins (under 'normal play conditions'): if (devil, s') is a devil-win for every s' \in angel_moves s then (angel, s) is a devil-win, and if (angel, s') is a devil-win for some s' \in devil_moves s then (devil, s) is a devil-win.

The advantage of this definition is that you don't have to talk about 'global' strategies, and inductive definitions are easy to work with in Lean. And if you want to connect it with 'does player X have a winning strategy' this should be easy. In the end, instead of proving only your someone_has_win_st you will basically have proved determinacy for open infinite games.

[Patrick Johnson]

@David Wärn That's a good idea. Is this what you have in mind?

[David Wärn]

Yes, exactly! But you should obviously feel free to experiment with different definitions. You might like also to define some sort of structure game := ... (this stuff on 'nice devils' could maybe be phrased in terms of a sort of 'equivalence' between games?). Note also that this 'compactness argument' behind Lemma 2.1 can be phrased in terms of inductive props: you can define another predicate expressing that a state is a devil-win in at most n moves, and prove by devil-win-induction that any devil-win is a devil-win in at most n moves for some n : nat (assuming the f₁ s are all finite).

[Patrick Johnson]

Progress update: I have abstracted most of the lemmas to a more general form. The loses is an inductive set of states at which player₂ has a winning strategy and wins are all other states (a state is a prod of bool and Board, where tt means player₁'s turn and ff means player₂'s turn). Inductive set states s₀ is the set of all states s that can be reached from state s₀ and the number of moves needed to reach s. There are bunch of lemmas proving the relation between those inductive types (many of the lemmas still have sorries, unfortunately).

Then we define a Strategy to be a subset of all available moves at any game state (with some additional constraints). We then prove some relations between strategies. We also introduce two different definitions of a notion that a player has a winning strategy: 1) directly using wins and supplying the set of all available moves for both players and 2) showing that there exists a specific strategy of one player that wins against any specific strategy of the other player. I'm working on proving that those two definitions are equivalent.

I need advices regarding the following questions:

• What is the right way to go with lemmas of the form A ↔ ¬B and B ↔ ¬A? Should I have two lemmas, or just one of them, or should I use xor instead of ↔?
• How to properly use sections? I have a bunch of definitions that depend on the same types of parameters. Is what I have right now the correct way to do this? Is it a good idea to have a nested sections like this?
• Should I separate the abstract definitions of a 2-player game to a new file, and have angel-devil game in another file?
• Since we prefer small PRs, what portion of the current lemmas (once become sorry-free) are suitable for the first PR?

Note: all those abbreviations and notations in the file are temporary.

[Stuart Presnell]

Is the material in set_theory/game/ useful to you here?

[David Wärn]

Stuart Presnell said:

Is the material in set_theory/game/ useful to you here?

I don't think it will apply directly since docs#pgame only describes well-founded games.

[Patrick Johnson]

set_theory/game/ is not suitable for this type of infinite games (I think) and I already have more than 500 lines of code, so I'll go with the current definitions anyway.

I understand that the Angel Problem is not very useful to mathlib, which explains the community's lack of interest. But since this is supposed to be my first contribution to mathlib, I would really like if some of the maintainers can answer the questions from my previous comment, especially the one related to PR. The lemmas that are currently in the file are going to be finished soon (which will complete the general proof of the determinacy of open games). What should be included in my first PR?

[Kevin Buzzard]

Try to make it 150 lines max. The best way to get the maintainers' attention is to make the PR

[Kevin Buzzard]

I think plenty of them don't even read this stream so may well not even see this message

[Yaël Dillies]

My problem currently is that I do not buy this.
Patrick Johnson said:

set_theory/game/ is not suitable for this type of infinite games

and I don't want you to duplicate theory that already exists. The thing is that I don't know enough myself to decide on that matter, so maybe finding a reference that talks about the relation between the angel problem and combinatorial games would help?

[Arthur Paulino]

Practical example:
If you check #PR reviews, you'll notice how Kyle split his contributions on "walks, trails, paths" in parts. He's currently on part 3 and there's even more to come :+1:

[Yaël Dillies]

Patrick Johnson said:

I understand that the Angel Problem is not very useful to mathlib, which explains the community's lack of interest.

Also, the angel problem is very cool and how dare you say this.

[David Wärn]

The problem with the material in set_theory/game/ is that it's based on docs#pgame which is defined inductively. This means that whenever two players 'play' a pgame, eventually they will reach a state where there is no available move. The Angel and Devil game is not of this form: the angel and devil can keep playing forever. So I think we need a more general notion of (infinite) game. (Would it be possible to define a coinductive analogue of pgame?)

[Yaël Dillies]

That's what I had at the back of my mind too. Pretty we can, although I wouldn't claim I can :grinning:

[David Wärn]

Patrick Johnson said:

I need advices regarding the following questions:

• What is the right way to go with lemmas of the form A ↔ ¬B and B ↔ ¬A? Should I have two lemmas, or just one of them, or should I use xor instead of ↔?

Declaring new lemmas is cheap. Iff-lemmas are nice because you can use them for rewriting. If you want to be able to rewrite A to ¬B and B to ¬A it can be a good idea to have new lemmas. Note there is also docs#iff_not_comm

• How to properly use sections? I have a bunch of definitions that depend on the same types of parameters. Is what I have right now the correct way to do this? Is it a good idea to have a nested sections like this?

I don't think there's any problem with nested sections, but usually we use variables over parameters (at least when you write definitions which can be useful outside of the section, you should try to make sure they are easy to use even outside the section, and this becomes less clear when you rely on parameters). You can reduce the number of variables / parameters by bundling your B, F₁, and F₂ in one structure game := ....

• Should I separate the abstract definitions of a 2-player game to a new file, and have angel-devil game in another file?

Yes. I would suggest to put the material on general games in set_theory/game and the material specific to the angel problem in archive/.

• Since we prefer small PRs, what portion of the current lemmas (once become sorry-free) are suitable for the first PR?

I would suggest starting with a PR defining infinite games (and maybe some notion of winning / losing positions). But it can make sense to wait to PR until you know that you got the basic definitions 'right' / that they are easy to work.

[Patrick Johnson]

A quick update: I am currently working on formalizing theorem 2.6 from the paper, all definitions and theorems so far are almost sorry-free. There are only two non-trivial sorries: in the theorems asserting that if a player can always force a win, then he has a winning strategy. It needs to be proved using some sort of geodesic arborescence on quivers, using two mutually recursive transitive closures (thanks @David Wärn for suggestion), which is, I think, far beyond the scope of formalizing the proof of the Angel problem. I will get back to these two theorems after I formalize the main theorem. I'm still not sure when to open a PR. Each new lemma I prove, I realize some of my definitions needs to be fixed or even completely rewritten. So I will probably open a PR after I formalize theorem 3.2 from the paper (at that point I hope my definitions will converge to some stable point).

But maybe we can use set_theory/game/, if we change the definition of the angel-devil game a bit. Instead of letting them play forever, the first move of the devil must be to pick a natural number n, which represents his promise that he will catch the angel in at most n moves. After n moves, if the angel is not caught, the devil loses. This is equivalent to the original angel-devil game (guaranteed by theorem 2.1), but all games end after a finite number of moves. I haven't tried to implement this yet, just want to check what do mathematicians think. Would this approach work and is it the right way to go?

(repo link for convenience)

[David Wärn]

I expect the material in set_theory/game which applies to the angel-devil game is basic enough that it's easier to reimplement it for your situation. mathlib should have some notion of infinite game anyway.

[David Wärn]

There is a proliferation of definitions starting from your Strategy, and they don't all seem to make sense (Strategy does not look like a function, and you shouldn't define winning strategies in terms of wins). I would suggest that you work only with wins and loses. If you like you could prove that they are equivalent to existence of some more explicit notion of winning strategy, but this shouldn't get in the way of proving the main result. Alternatively, if you want to work more closely to Máthé's paper, you can abandon wins and loses and use Máthé's notion of strategy

[Patrick Johnson]

Ok, I got rid of wins and loses and I use more intuitive notion of a strategy (haven't pushed to Github yet). Interestingly, proofs did not change too much.

But the main problem remains. How to prove that exactly one player has a winning strategy? If the angel has a winning strategy, then the devil does not (it's trivial and easy to prove). However, if the devil does not have a winning strategy, it seems very hard to prove that the angel has a winning strategy. This is beyond my math skills. I could formalize the proof if I had one on the paper, but I don't. They simply assume it's trivial and skip over it.

There must exist a winning strategy for one of the players. If the devil can force a win then it can do so in a finite number of moves. If the devil cannot force a win then there is always an action that the angel can take to avoid losing and a winning strategy for it is always to pick such a move. More abstractly, the "pay-off set" (i.e., the set of all plays in which the angel wins) is a closed set (in the natural topology on the set of all plays), and it is known that such games are determined. Of course, for any infinite game, if player 2 doesn't have a winning strategy, player 1 can always pick a move that leads to a position where player 2 doesn't have a winning strategy, but in some games, simply playing forever doesn't confer a win to player 1, so undetermined games may exist.

Especially, the statement "If the devil cannot force a win then there is always an action that the angel can take to avoid losing and a winning strategy for it is always to pick such a move" seems very unclear. I don't really find it obvious. Maybe they assume some other notion of a strategy? My understanding is that a strategy is a function from a game board to a game board, such that it represents a valid move of the angel/devil. Given an angel and a devil strategy, they play until the angel cannot move anymore. So, the game is determined by a pair of strategies. Angel wins in such game iff it is never trapped. Devil wins iff the angel is trapped after n moves for some n. A winning strategy for one player is a strategy which can win against any strategy of the other player. In pseudocode:

angel_hws := ∃ (a : angel), ∀ (d : devil), ∀ (n : ℕ), ¬angel_trapped_after_n_moves a d n
devil_hws := ∃ (d : devil), ∀ (a : angel), ∃ (n : ℕ), angel_trapped_after_n_moves a d n

And we want to prove ¬devil_hws → angel_hws. How is it supposed to be obvious? The assumption ¬devil_hws states that for any devil, there exists an angel that can win against that particular devil. And we are supposed to explicitly construct angel's strategy. The problem is, we don't know which devil we are playing against. We are aware of the history of moves, so we can reduce the set of possibilities, but we still don't know the opponent exactly. We can consult the assumption ¬devil_hws and ask what would be the next move is we were playing with some particular devil d, and the assumption (with the help of the axiom of choice) would tell us the next move, so we would be able to construct angel's strategy for any board based on the history of moves. But still, we don't know our opponent's strategy, and the intersection of all possibilities may be empty (the choice may pick different answer for each of the possible opponents), so how would we construct angel's strategy?

I'm just asking for an informal proof of the determinacy of open games. I can't find any detailed explanation in any of the related papers.

[Kevin Buzzard]

"If the devil cannot force a win then there is always an action that the angel can take to avoid losing and a winning strategy for it is always to pick such a move" sounds fine to me. What's the problem with it?

[Kevin Buzzard]

an informal proof of open determinacy goes like this. The easiest way to think of these infinite games is just to imagine that players are playing alternate moves which can be 0 or 1, building the binary expansion of a real number 0.a1d1a2d2... in [0,1], with a playing move a1 first, then d playing d1 then a playing a2 etc. Before the game starts we're given a subset S of [0,1] and you let the players play forever and then the angel wins if the resulting real number is in S. Because this is a crazy infinite thing, if you believe in the axiom of choice then you can make pathological sets S for which neither player has a winning strategy. However if S is sensible (e.g. open, or even Borel) then you can show that one player must have a winning strategy. For open sets the proof just goes like this: if an infinite play of the game ends up with a number s in S, then this element s of S has some epsilon such that (s-epsilon, s+epsilon) is a subset of S, and hence after a finite amount of time it was already guaranteed that the result of the game would be in S (because all the digits after some point don't change the final number by more than epsilon). So if the first player a has a strategy for S open, i.e. an algorithm which always wins however d plays, then for any play of the game there is a point at which a can announce "Ok I have now won even if we both now play randomly because all outcomes end up in S". Hence if a does not have a winning strategy then this means that there's a way for d to play such that a can never announce this, and if d plays in this way then the resulting limit point can't possibly be in S (because if it were then a would have won after a finite time).

With weirder S this argument doesn't work because you might never end up guaranteed to be in S but might end up in S at the end anyway.

[David Wärn]

I think you should define the angel-devil game in such a way that Devil wins when Angel no longer has a valid move. (There are two ways to achieve this. Either you allow Devil to capture the square which the angel stands on. Or you forbid Angel from standing still. I would recommend the former since it's simpler, but the latter seems to be traditional.) Then a winning strategy for Angel is just a strategy which always makes a valid move. If you use the wins s predicate, then you just prove that if it's Angel's turns and the current state is an Angel-win, then there is a valid move leading to a state which is also an Angel-win. If you pick such a move using exists.some, then you get a winning strategy. This is essentially equivalent to Kevin's argument, but expressed in a more Lean-friendly way.

Here's a sketch of how I would formalise infinite games and open determinacy.

Note that there is considerable ambiguity in the notion of "a strategy for an infinite game". Kevin has a minimalist notion of infinite game, which can be useful for proving abstract properties of general games, but makes it difficult to talk about specific games like the angel-devil game. The gist above instead uses a much more strongly-typed notion of infinite game. There's also ambiguity in the notion of a strategy. For example, must a strategy for white in chess have an answer to the question 'what do we do after 1. a4 e5'? Traditional notions of strategy would probably say 'yes', but the gist above says 'no' (you only need to know what to do after moves which you would actually choose), and it seems to me that when you describe explicit strategies you don't want to have to think about this question.

Often when you translate an informal argument to Lean, you want to switch to more Lean-friendly notions. For example, working with inductive types in Lean is usually straightforward, and proofs by induction (or coinduction!) more or less write themselves once you know what you're proving. In contrast, working with strategies defined as 'a function which takes as input a list of positions' sounds Lean-hard to me. That's why I would suggest working with the wins and loses predicates. It might be difficult to translate Máthé's argument in this language. You would want to rephrase the proofs as proofs by (co)induction, and define lots of different games (the game where the angel wins when they move sufficiently far from the origin, the nice devil game, the game with the runner). I would expect that the difficulty in translating the argument to this different language is outweighed by the alternative difficulty in working with Máthé's notion of strategy, but it's hard to say in advance.

(I left a comment at the bottom of the gist above about a coinductive definition of strategies for a general infinite game, which may help to make formal sense of the notion of 'strategy for an infinite game', but you shouldn't need this for the angel-devil game.)

[Patrick Johnson]

Thank you both. Kevin's number-theoretic approach is overcomplicated (we would need real numbers, binary encodings, limits, open sets, etc), I am definitely not going to take that approach.

David's approach seems more suitable for this problem, but that's still not what I'm looking for. In your sketch, you defined angel_win s as ¬devil_win s, and that's why your "determinacy" proof is trivial. I am talking about proving nonempty_angel_strat_iff_angel_win and the determinacy would be stated as nonempty_angel_strat_iff_empty_devil_strat.

But I think I got the general idea. I will try to use Mathe's notion of a strategy to prove determinacy.

[Patrick Johnson]

If anyone is wondering what the status of this project is (probably nobody is wondering, but I'll write this nonetheless). I decided not to formalize this paper in Lean, because I realized that dependent type theory cannot accurately express my intuition.

Instead, I started developing a set-theoretic theorem prover, which will be finished at the end of this year (hopefully). The proof of the angel problem will be the first big project I will formalize in that theorem prover, to put the expressiveness of the prover to the test. Of course, I need to develop a sufficient amount of math library first. After I fully formalize the paper, I will update this thread once again for the last time.

[Bulhwi Cha]

I have no idea what the angel problem is, but I look forward to seeing your theorem prover!

[Patrick Johnson]

Sure, here is our repository, but I suggest not trying to explore it until it's fully finished, since nothing is documented and everything is subject to change.

[Eric Wieser]

Can you elaborate on where dependent type theory was getting in the way?

[Patrick Johnson]

Just to be clear, I don't have anything against DTT. I would probably have finished formalizing this paper in Lean if I was persistent enough to do so. But, I realized it won't be fun for me, since I think set-theoretically and working (on a big project) in DTT is a pain for me. It's just a matter of taste.

To answer your question: Situations where DTT got in the way (among others):

• Coercions between ℕ ℤ ℚ ℝ
• Working with A being a subtype of B being a subtype of C being a subtype of ...
• Dependent rewrites yielding "motive not being type correct"

[Jireh Loreaux]

Maybe a stupid question, but to address your issues:

• Do you know about norm_cast?
• Often times there are better ways to work with things than continually using subtypes (of course, sometimes not)
• I think simp_rw can probably get past motive problems.

[Jireh Loreaux]

Of course, it's still fine if you prefer set-theoretic formalism to DTT.

[Patrick Johnson]

Yes, I know all that, but there are situations where none of that helps.

[Eric Wieser]

Thanks Patrick; I just wanted to check this wasn't the "x = yis a type error when x : A (i + j), y : A (j + i)" problem of DTT, or a new variant I haven't seen before.