Angel and Devil: infinite-board game and strategies
DefinitionAngelDevil_GameInteger lattice game with Devil-first rounds, passing, history-dependent strategies, legal survival, Nice Devil restrictions, unbounded escape, and confinement of every finite safe prefix. Conventions follow Sections 1-2, Definitions 2.2, 2.3, 2.5 and equation (2).
import Std
/-! The convention is Mathe's paper: Devil moves first, may pass, and may
eat any square (including the occupied square); only subsequent landing on
an eaten square loses. Zero-length Angel moves are allowed by Definition 2.5.
Histories are stored oldest first. Strategies are total also off legal play.
-/
namespace AngelDevil
abbrev Point := Int × Int
def origin : Point := (0, 0)
def Jump (p : Nat) (u v : Point) : Prop :=
-(p : Int) ≤ v.1 - u.1 ∧ v.1 - u.1 ≤ (p : Int) ∧
-(p : Int) ≤ v.2 - u.2 ∧ v.2 - u.2 ≤ (p : Int)
def InBox (N : Nat) (v : Point) : Prop := Jump N origin v
def Journey (p : Nat) (h : List Point) : Prop :=
h.head? = some origin ∧
∀ (i : Nat) (u v : Point), h[i]? = some u → h[i+1]? = some v → Jump p u v
abbrev DevilStrategy := List Point → Option Point
abbrev AngelStrategy := List Point → List (Option Point) → Point
structure State where
visited : List Point
burned : List (Option Point)
def initial : State := ⟨[origin], []⟩
def current (s : State) : Point := s.visited.getLastD origin
def step (A : AngelStrategy) (D : DevilStrategy) (s : State) : State :=
let burned := s.burned ++ [D s.visited]
⟨s.visited ++ [A s.visited burned], burned⟩
def play (A : AngelStrategy) (D : DevilStrategy) : Nat → State
| 0 => initial
| n+1 => step A D (play A D n)
def Survives (p : Nat) (A : AngelStrategy) (D : DevilStrategy) : Prop :=
∀ n, Jump p (current (play A D n)) (current (play A D (n+1))) ∧
some (current (play A D (n+1))) ∉ (play A D (n+1)).burned
def AngelWins (p : Nat) : Prop := ∃ A, ∀ D, Survives p A D
/- Definition 2.2, as made explicit by equation (2): the origin and every
square reachable from a position before the last one are protected. -/
def Nice (p : Nat) (D : DevilStrategy) : Prop :=
∀ h, Journey p h → ∀ z, D h = some z →
z ≠ origin ∧ ∀ v ∈ h.dropLast, ¬ Jump p v z
def Escapes (A : AngelStrategy) (D : DevilStrategy) : Prop :=
∀ N : Nat, ∃ n : Nat, ¬ InBox N (current (play A D n))
def NiceAngelWins (p : Nat) : Prop :=
∃ A, ∀ D, Nice p D → Survives p A D ∧ Escapes A D
def NiceCanConfine (p N : Nat) : Prop :=
∃ D, Nice p D ∧ ∀ A n,
(∀ m, m < n →
Jump p (current (play A D m)) (current (play A D (m+1))) ∧
some (current (play A D (m+1))) ∉ (play A D (m+1)).burned) →
InBox N (current (play A D n))
end AngelDevil
Read-back
What the Lean code literally says, in plain math · gpt-6
Points are pairs of integers, with origin o = (0,0). For every natural number p (including zero), a jump from u to v means that each coordinate of v − u lies inclusively between −p and p; staying still is allowed, and for p = 0 it is the only jump. The box of natural radius N is the set of points whose two coordinates lie in [−N,N], so radius zero gives {o}. A journey of power p is a finite nonempty list beginning at o whose consecutive entries are jumps of power p; the one-entry list [o] is a journey, repetitions are allowed, and indices for which either consecutive entry is absent impose no constraint. A Devil strategy is any total function from finite point lists to an optional point, with no point meaning a pass; an Angel strategy is any total function from a finite point list and a finite list of optional points to a point. These functions are defined even on empty, inconsistent, or otherwise illegal histories. A state consists of these two lists, without invariants; its current point is the last point in its first list, or o if that list is empty. Starting with point list [o] and empty optional-point list, each round first appends the Devil's response to the existing point list to the optional-point list, then appends the Angel's response to the old point list and this extended optional-point list to the point list. This recursion defines play for every natural number of rounds, even after an illegal move. The Angel survives with power p against a Devil precisely when, in every round starting at round zero, its new point is a jump of power p from its preceding point and is unequal to every point the Devil has selected up through that round. Repeated selections, passes, and selection of the occupied point are otherwise allowed; selecting the occupied point alone does not invalidate a round if the Angel leaves it legally. AngelWins(p) means that a single Angel strategy survives against every Devil strategy. A Devil is nice at power p precisely when on every journey of power p, every point it selects is different from o and is not a jump of power p from any entry before the last entry of that journey; passing imposes no restriction, non-journey inputs impose no restriction, and on [o] only selection of o is forbidden. Escaping means that for every natural N there is a natural round n at which the current point lies outside the box of radius N; this does not require eventually remaining outside that box. NiceAngelWins(p) means that one Angel strategy both survives and escapes against every nice Devil. NiceCanConfine(p,N) means that one nice Devil has the following property for every Angel strategy and every natural n: if each of the first n rounds has a jump of power p and a new point unequal to every point selected by the Devil up through that round, the current point after n rounds belongs to the box of radius N. This condition includes finite legal prefixes that have no infinite legal continuation; for n = 0 its premise is vacuous and its conclusion is the true assertion that o belongs to the box.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.