Parity games

InductivePlayers of a parity game#✓fully proved

A parity game has exactly two players, the even player and the odd player.

The even player is the one who wins the plays whose largest priority occurring infinitely often is even, and the odd player the one who wins those where it is odd.

inductive Player where
  /-- The player who wins plays whose maximal recurring priority is even. -/
  | even
  /-- The player who wins plays whose maximal recurring priority is odd. -/
  | odd
  deriving DecidableEq, Repr
Used by 54
Used byVerifier's positional strategies make a game move at Verifier positions that have one · Segments of canonical plays through fragment positions are bespoke plays · Owners in the totalized fragment game · Owner of an embedded position in the totalized fragment game · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Fragment parity game · Wins is the winning region of the fragment game · Sequences that stay at the win state are won by the even player · Sequences that stay at the lose state are won by the odd player · Attractor · The attractor stabilizes after as many stages as there are positions · Attractor stages · Attractor operator · Attractor strategy · The attractor strategy moves into the stage from its controllable predecessor · The attractor strategy reaches the target from an attractor stage · The attractor strategy reaches the target from the attractor · The attractor lies in every closed set · Plays conforming to a strategy · Controllable predecessor · Traps disjoint from a set avoid its attractor · The winning regions of the two players are disjoint · Every player is \(p\) or the opponent of \(p\) · Forcing a visit to a set · The attractor strategy forces a visit · Trap for a player · The complement of an attractor is a trap · Winning regions are traps for the opponent · Joint successor of two strategies · Characterization of the attractor · Opponent moves stay in the winning region · A winning strategy's move stays in the winning region · Positional strategies exist · No strategy forces a visit from outside the attractor · No play is won by both players · Winning strategies keep winning along allowed moves · Opponent · Outcome of two positional strategies · Parity game · Positional strategy in a parity game · The parity game of a serial encoded game · Trap strategy · The trap strategy avoids the target · The trap strategy stays in the trap · The attractor is a fixed point · Winning region of a parity game · Parity winning condition of a player · Winning strategy from a position · Winner of a play in a parity game · Winning is prefix independent · Bounded priorities give every play a winner

DefinitionOpponent#✓fully proved

The opponent of a player of a parity game is the other player: the opponent of the even player is the odd player, and the opponent of the odd player is the even player.

def opponent : Player → Player
  | even => odd
  | odd => even
Uses 1 · Used by 13
Statement usesPlayers of a parity game
Used byTerminal losing positions are not won by the even player · The winning regions of the two players are disjoint · Every player is \(p\) or the opponent of \(p\) · Winning regions are traps for the opponent · Joint successor of two strategies · Opponent moves stay in the winning region · No strategy forces a visit from outside the attractor · No play is won by both players · Outcome of two positional strategies · Trap strategy · The trap strategy avoids the target · The trap strategy stays in the trap · Bounded priorities give every play a winner

TheoremEvery player is \(p\) or the opponent of \(p\)#✓fully proved

For all players \(p\) and \(q\) of a parity game, \(q = p\) or \(q\) is the opponent of \(p\).

theorem eq_or_eq_opponent (p q : Player) : q = p ∨ q = p.opponent
Uses 2 · Used by 4
Statement usesPlayers of a parity game · Opponent
Used byThe winning regions of the two players are disjoint · Winning regions are traps for the opponent · No strategy forces a visit from outside the attractor · The trap strategy stays in the trap

DefinitionParity winning condition of a player#✓fully proved

A player wins an infinite sequence of natural-number priorities when the sequence satisfies that player's parity condition: the even player wins it when the largest priority occurring infinitely often exists and is even, and the odd player wins it when the largest priority occurring infinitely often exists and is odd.

def Wins : Player → ωSequence ℕ → Prop
  | even, ps => ParityEven ps
  | odd, ps => ParityOdd ps
Uses 3 · Used by 1
Statement usesPlayers of a parity game · Even max-parity condition · Odd max-parity condition
Used byWinner of a play in a parity game

StructureParity game#✓fully proved

A parity game on a type of positions consists of an owner for each position, which is one of the two players, a move relation between positions, where the owner of \(v\) may move from \(v\) to \(w\) when \(v\) is related to \(w\), and a natural-number priority for each position, such that every position has at least one move (there are no dead ends).

As in the usual infinite-play model, the absence of dead ends means that both players always have positional strategies.

structure ParityGame (Pos : Type*) where
  /-- The player choosing the move at each position. -/
  owner : Pos → Player
  /-- The moves: `Move v w` iff the owner of `v` may move from `v` to `w`. -/
  Move : Pos → Pos → Prop
  /-- The priority of each position. -/
  priority : Pos → ℕ
  /-- Every position has a move. -/
  serial : ∀ v, ∃ w, Move v w
Uses 1 · Used by 45
Statement usesPlayers of a parity game
Used byVerifier's positional strategies make a game move at Verifier positions that have one · Segments of canonical plays through fragment positions are bespoke plays · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · The fragment game's winning region is contained in Wins · Fragment parity game · Attractor · The attractor stabilizes after as many stages as there are positions · Attractor stages · Attractor operator · Attractor strategy · The attractor strategy moves into the stage from its controllable predecessor · The attractor strategy reaches the target from an attractor stage · The attractor strategy reaches the target from the attractor · The attractor lies in every closed set · Plays conforming to a strategy · Controllable predecessor · Traps disjoint from a set avoid its attractor · The winning regions of the two players are disjoint · Forcing a visit to a set · The attractor strategy forces a visit · Plays of a parity game · Trap for a player · The complement of an attractor is a trap · Winning regions are traps for the opponent · Joint successor of two strategies · Characterization of the attractor · Opponent moves stay in the winning region · A winning strategy's move stays in the winning region · Positional strategies exist · No strategy forces a visit from outside the attractor · No play is won by both players · Winning strategies keep winning along allowed moves · Outcome of two positional strategies · Positional strategy in a parity game · The parity game of a serial encoded game · Trap strategy · The trap strategy avoids the target · The trap strategy stays in the trap · The attractor is a fixed point · Winning region of a parity game · Winning strategy from a position · Winner of a play in a parity game · Winning is prefix independent · Bounded priorities give every play a winner

DefinitionPlays of a parity game#✓fully proved

An infinite sequence of positions \(\pi_0, \pi_1, \dots\) of a parity game is a play if for every \(i\) there is a move from \(\pi_i\) to \(\pi_{i+1}\).

def IsPlay (π : ωSequence Pos) : Prop :=
  ∀ i, G.Move (π i) (π (i + 1))
Uses 1 · Used by 15
Statement usesParity game
Used bySegments of canonical plays through fragment positions are bespoke plays · Plays of the totalized fragment game stay at the losing state · Plays of the totalized fragment game stay at the winning state · Terminal losing positions are not won by the even player · Winning Verifier strategies transfer to the fragment game · The attractor strategy reaches the target from an attractor stage · The attractor strategy reaches the target from the attractor · The winning regions of the two players are disjoint · Forcing a visit to a set · The attractor strategy forces a visit · No strategy forces a visit from outside the attractor · Winning strategies keep winning along allowed moves · The trap strategy avoids the target · The trap strategy stays in the trap · Winning strategy from a position

DefinitionWinner of a play in a parity game#✓fully proved

Let \(G\) be a parity game, write \(\Omega(v)\) for the priority of a position \(v\), and let \(p\) be a player. An infinite sequence \(\pi = \pi_0 \pi_1 \pi_2 \dots\) of positions of \(G\) is won by \(p\) when its priority sequence \(\Omega(\pi_0) \Omega(\pi_1) \Omega(\pi_2) \dots\) satisfies the parity condition of \(p\): among the priorities occurring infinitely often there is a largest one, and it is even if \(p\) is the even player and odd if \(p\) is the odd player.

The definition applies to every infinite sequence of positions, whether or not it follows the moves of \(G\).

def WonBy (p : Player) (π : ωSequence Pos) : Prop :=
  p.Wins (π.map G.priority)
Uses 3 · Used by 10
Statement usesParity game · Players of a parity game · Parity winning condition of a player
Used byTerminal losing positions are not won by the even player · Winning Verifier strategies transfer to the fragment game · Sequences that stay at the win state are won by the even player · Sequences that stay at the lose state are won by the odd player · The winning regions of the two players are disjoint · No play is won by both players · Winning strategies keep winning along allowed moves · Winning strategy from a position · Winning is prefix independent · Bounded priorities give every play a winner

StructurePositional strategy in a parity game#✓fully proved

A positional (memoryless) strategy for player p: a choice of successor at each position, legal at the positions p owns. Its values elsewhere are irrelevant.

structure PositionalStrategy (p : Player) where
  /-- The chosen successor. -/
  next : Pos → Pos
  /-- At positions owned by `p`, the chosen successor is a legal move. -/
  legal : ∀ v, G.owner v = p → G.Move v (next v)
Uses 2 · Used by 25
Statement usesParity game · Players of a parity game
Used byVerifier's positional strategies make a game move at Verifier positions that have one · Segments of canonical plays through fragment positions are bespoke plays · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · The fragment game's winning region is contained in Wins · Wins is the winning region of the fragment game · Attractor strategy · The attractor strategy moves into the stage from its controllable predecessor · The attractor strategy reaches the target from an attractor stage · Plays conforming to a strategy · The winning regions of the two players are disjoint · Forcing a visit to a set · Winning regions are traps for the opponent · Joint successor of two strategies · Characterization of the attractor · Opponent moves stay in the winning region · A winning strategy's move stays in the winning region · Positional strategies exist · No strategy forces a visit from outside the attractor · Winning strategies keep winning along allowed moves · Outcome of two positional strategies · Trap strategy · The trap strategy stays in the trap · Winning region of a parity game · Winning strategy from a position

TheoremPositional strategies exist#✓fully proved

In a parity game, every player has a positional strategy, since every position has a move.

theorem nonempty_positionalStrategy (p : Player) : Nonempty (G.PositionalStrategy p)
Uses 3
Statement usesParity game · Positional strategy in a parity game · Players of a parity game

DefinitionPlays conforming to a strategy#✓fully proved

Let \(\sigma\) be a positional strategy of player \(p\) in a parity game. An infinite sequence of positions \(\pi_0, \pi_1, \dots\) (not necessarily a play) conforms to \(\sigma\) if \(\pi_{i+1} = \sigma(\pi_i)\) for every \(i\) such that \(p\) owns \(\pi_i\).

def Conforms {p : Player} (σ : G.PositionalStrategy p) (π : ωSequence Pos) : Prop :=
  ∀ i, G.owner (π i) = p → π (i + 1) = σ.next (π i)
Uses 3 · Used by 13
Statement usesParity game · Positional strategy in a parity game · Players of a parity game
Used bySegments of canonical plays through fragment positions are bespoke plays · Terminal losing positions are not won by the even player · Winning Verifier strategies transfer to the fragment game · The attractor strategy reaches the target from an attractor stage · The attractor strategy reaches the target from the attractor · The winning regions of the two players are disjoint · Forcing a visit to a set · The attractor strategy forces a visit · No strategy forces a visit from outside the attractor · Winning strategies keep winning along allowed moves · The trap strategy avoids the target · The trap strategy stays in the trap · Winning strategy from a position

DefinitionWinning strategy from a position#✓fully proved

Let \(p\) be a player of a parity game. A positional strategy \(\sigma\) of \(p\) wins from a position \(v\) when every play starting at \(v\) that conforms to \(\sigma\) (at every position owned by \(p\), the play moves to the successor chosen by \(\sigma\)) is won by \(p\).

def WinsFrom {p : Player} (σ : G.PositionalStrategy p) (v : Pos) : Prop :=
  ∀ π, G.IsPlay π → π 0 = v → Conforms σ π → G.WonBy p π
Uses 6 · Used by 10
Statement usesParity game · Plays conforming to a strategy · Plays of a parity game · Positional strategy in a parity game · Winner of a play in a parity game · Players of a parity game
Used byTerminal losing positions are not won by the even player · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Wins is the winning region of the fragment game · The winning regions of the two players are disjoint · Winning regions are traps for the opponent · Opponent moves stay in the winning region · A winning strategy's move stays in the winning region · Winning strategies keep winning along allowed moves · Winning region of a parity game

DefinitionWinning region of a parity game#✓fully proved

The positions from which player p has a winning positional strategy.

def WinningRegion (p : Player) : Set Pos :=
  { v | ∃ σ : G.PositionalStrategy p, WinsFrom σ v }
Uses 4 · Used by 7
Statement usesParity game · Positional strategy in a parity game · Winning strategy from a position · Players of a parity game
Used byTerminal losing positions are not won by the even player · The fragment game's winning region is contained in Wins · Wins is the winning region of the fragment game · The winning regions of the two players are disjoint · Winning regions are traps for the opponent · Opponent moves stay in the winning region · A winning strategy's move stays in the winning region

TheoremBounded priorities give every play a winner#✓fully proved

Let \(p\) be a player of a parity game in which every position has priority at most \(d\), for some natural number \(d\). Then every infinite sequence of positions, in particular every play, is won by \(p\) or by the opponent of \(p\).

theorem wonBy_or_wonBy_opponent {d : ℕ} (hd : ∀ v, G.priority v ≤ d) (p : Player)
    (π : ωSequence Pos) : G.WonBy p π ∨ G.WonBy p.opponent π
Uses 8
Statement usesParity game · Winner of a play in a parity game · Players of a parity game · Opponent
Proof usesLargest infinitely occurring value · Even max-parity condition · Odd max-parity condition · Bounded sequences have a largest infinitely occurring value

TheoremNo play is won by both players#✓fully proved

In a parity game, for every player \(p\), no infinite sequence of positions (play or not) is won both by \(p\) and by the opponent of \(p\).

theorem not_wonBy_and_wonBy_opponent (p : Player) (π : ωSequence Pos) :
    ¬ (G.WonBy p π ∧ G.WonBy p.opponent π)
Uses 7 · Used by 2
Statement usesParity game · Winner of a play in a parity game · Players of a parity game · Opponent
Proof usesLargest infinitely occurring value · Even max-parity condition · Odd max-parity condition
Used byTerminal losing positions are not won by the even player · The winning regions of the two players are disjoint

TheoremWinning is prefix independent#✓fully proved

Let \(p\) be a player of a parity game, \(\pi = (\pi_0, \pi_1, \dots)\) an infinite sequence of positions and \(j\) a natural number. Then the sequence \((\pi_j, \pi_{j+1}, \dots)\), obtained by dropping the first \(j\) positions of \(\pi\), is won by \(p\) if and only if \(\pi\) is won by \(p\).

theorem wonBy_drop_iff (p : Player) (π : ωSequence Pos) (j : ℕ) :
    G.WonBy p (π.drop j) ↔ G.WonBy p π
Uses 7 · Used by 1
Statement usesParity game · Winner of a play in a parity game · Players of a parity game
Proof usesLargest infinitely occurring value · Even max-parity condition · Odd max-parity condition · Prefix independence of the largest infinitely occurring value
Used byWinning strategies keep winning along allowed moves

DefinitionJoint successor of two strategies#✓fully proved

Let \(\sigma\) be a positional strategy of player \(p\) and \(\tau\) a positional strategy of the opponent of \(p\) in a parity game. The joint successor of a position \(v\) is \(\sigma(v)\) if \(p\) owns \(v\), and \(\tau(v)\) otherwise.

def jointNext {p : Player} (σ : G.PositionalStrategy p)
    (τ : G.PositionalStrategy p.opponent) (v : Pos) : Pos :=
  if G.owner v = p then σ.next v else τ.next v
Uses 4 · Used by 3
Statement usesParity game · Positional strategy in a parity game · Players of a parity game · Opponent
Used byThe winning regions of the two players are disjoint · No strategy forces a visit from outside the attractor · Outcome of two positional strategies

DefinitionOutcome of two positional strategies#✓fully proved

Let \(p\) be a player of a parity game, \(\sigma\) a positional strategy of \(p\) and \(\tau\) a positional strategy of the opponent of \(p\). The outcome of \(\sigma\) and \(\tau\) from a position \(v\) is the infinite sequence of positions \(v_0, v_1, v_2, \dots\) with \(v_0 = v\) in which \(v_{i+1}\) is the successor chosen by \(\sigma\) at \(v_i\) if \(p\) owns \(v_i\), and the successor chosen by \(\tau\) at \(v_i\) otherwise. It is the play from \(v\) in which \(p\) follows \(\sigma\) and the opponent follows \(\tau\).

def outcome {p : Player} (σ : G.PositionalStrategy p) (τ : G.PositionalStrategy p.opponent)
    (v : Pos) : ωSequence Pos :=
  ωSequence.iterate (jointNext σ τ) v
Uses 5 · Used by 2
Statement usesParity game · Positional strategy in a parity game · Joint successor of two strategies · Players of a parity game · Opponent
Used byThe winning regions of the two players are disjoint · No strategy forces a visit from outside the attractor

TheoremThe winning regions of the two players are disjoint#✓fully proved

In a parity game, for every player \(p\), no position lies both in the winning region of \(p\) and in the winning region of the opponent of \(p\).

theorem disjoint_winningRegion (p : Player) :
    Disjoint (G.WinningRegion p) (G.WinningRegion p.opponent)
Uses 13
Statement usesParity game · Winning region of a parity game · Players of a parity game · Opponent
Proof usesPlays conforming to a strategy · Plays of a parity game · Positional strategy in a parity game · Winning strategy from a position · Winner of a play in a parity game · Joint successor of two strategies · No play is won by both players · Outcome of two positional strategies · Every player is \(p\) or the opponent of \(p\)

TheoremWinning strategies keep winning along allowed moves#✓fully proved

In a parity game, let \(\sigma\) be a positional strategy of player \(p\) that wins from a position \(v\), and let \(w\) be a position with a move from \(v\) to \(w\) such that \(w = \sigma(v)\) if \(p\) owns \(v\). Then \(\sigma\) wins from \(w\).

theorem WinsFrom.of_move {v w : Pos} (h : WinsFrom σ v) (hmove : G.Move v w)
    (hσ : G.owner v = p → w = σ.next v) : WinsFrom σ w
Uses 8 · Used by 2
Statement usesParity game · Positional strategy in a parity game · Winning strategy from a position · Players of a parity game
Proof usesPlays conforming to a strategy · Plays of a parity game · Winner of a play in a parity game · Winning is prefix independent
Used byOpponent moves stay in the winning region · A winning strategy's move stays in the winning region

TheoremOpponent moves stay in the winning region#✓fully proved

In a parity game, let \(v\) be a position in the winning region of player \(p\) that is owned by the opponent of \(p\). Then every position \(w\) with a move from \(v\) to \(w\) is in the winning region of \(p\).

theorem move_mem_winningRegion {v w : Pos} (hv : v ∈ G.WinningRegion p)
    (hown : G.owner v = p.opponent) (hmove : G.Move v w) : w ∈ G.WinningRegion p
Uses 7 · Used by 2
Statement usesParity game · Winning region of a parity game · Players of a parity game · Opponent
Proof usesPositional strategy in a parity game · Winning strategy from a position · Winning strategies keep winning along allowed moves
Used byThe fragment game's winning region is contained in Wins · Winning regions are traps for the opponent

TheoremA winning strategy's move stays in the winning region#✓fully proved

In a parity game, let \(\sigma\) be a positional strategy of player \(p\) that wins from a position \(v\) owned by \(p\). Then the successor \(\sigma(v)\) chosen by \(\sigma\) is in the winning region of \(p\).

theorem next_mem_winningRegion {v : Pos} {σ : G.PositionalStrategy p} (hσ : WinsFrom σ v)
    (hown : G.owner v = p) : σ.next v ∈ G.WinningRegion p
Uses 6 · Used by 2
Statement usesParity game · Positional strategy in a parity game · Winning region of a parity game · Winning strategy from a position · Players of a parity game
Proof usesWinning strategies keep winning along allowed moves
Used byThe fragment game's winning region is contained in Wins · Winning regions are traps for the opponent

DefinitionControllable predecessor#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(X\) a set of positions. The controllable predecessor \(\mathrm{cpre}_p(X)\) of \(X\) for \(p\) is the set of positions \(v\) such that either \(v\) is owned by \(p\) and some move from \(v\) leads into \(X\), or \(v\) is not owned by \(p\) and every move from \(v\) leads into \(X\).

def cpre (p : Player) (X : Set Pos) : Set Pos :=
  { v | (G.owner v = p ∧ ∃ w, G.Move v w ∧ w ∈ X) ∨ (G.owner v ≠ p ∧ ∀ w, G.Move v w → w ∈ X) }
Uses 2 · Used by 9
Statement usesParity game · Players of a parity game
Used byThe attractor stabilizes after as many stages as there are positions · Attractor operator · The attractor strategy moves into the stage from its controllable predecessor · The attractor strategy reaches the target from an attractor stage · The attractor lies in every closed set · Traps disjoint from a set avoid its attractor · The complement of an attractor is a trap · The trap strategy avoids the target · The attractor is a fixed point

DefinitionAttractor operator#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions. The attractor operator of \(T\) for \(p\) is the monotone map on sets of positions sending \(X\) to \(T \cup \mathrm{cpre}_p(X)\), where \(\mathrm{cpre}_p\) is the controllable predecessor for \(p\).

def attractorStep (p : Player) (T : Set Pos) : Set Pos →o Set Pos where
  toFun X := T ∪ G.cpre p X
  monotone' _ _ h := Set.union_subset_union_right T (G.cpre_mono p h)
Uses 3 · Used by 7
Statement usesParity game · Controllable predecessor · Players of a parity game
Used byAttractor · The attractor stabilizes after as many stages as there are positions · Attractor stages · The attractor strategy moves into the stage from its controllable predecessor · The attractor strategy reaches the target from an attractor stage · The attractor lies in every closed set · The attractor is a fixed point

DefinitionAttractor#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions. The attractor of \(T\) for \(p\) is the least fixed point of the attractor operator \(X \mapsto T \cup \mathrm{cpre}_p(X)\) on sets of positions, where \(\mathrm{cpre}_p\) is the controllable predecessor for \(p\).

def attractor (p : Player) (T : Set Pos) : Set Pos :=
  OrderHom.lfp (G.attractorStep p T)
Uses 3 · Used by 10
Statement usesParity game · Attractor operator · Players of a parity game
Used byThe attractor stabilizes after as many stages as there are positions · The attractor strategy reaches the target from the attractor · The attractor lies in every closed set · Traps disjoint from a set avoid its attractor · The attractor strategy forces a visit · The complement of an attractor is a trap · Characterization of the attractor · No strategy forces a visit from outside the attractor · The trap strategy avoids the target · The attractor is a fixed point

DefinitionAttractor stages#✓fully proved

Let \(G\) be a parity game, \(p\) a player, \(T\) a set of positions and \(n\) a natural number. The \(n\)-th attractor stage \(S_n\) of \(T\) for \(p\) is the set obtained by applying the attractor operator \(X \mapsto T \cup \mathrm{cpre}_p(X)\) \(n\) times to \(\emptyset\), where \(\mathrm{cpre}_p\) is the controllable predecessor for \(p\); thus \(S_0 = \emptyset\) and \(S_{n+1} = T \cup \mathrm{cpre}_p(S_n)\).

The \(n\)-th stage consists of the positions from which \(p\) can force a visit to \(T\) within fewer than \(n\) moves.

def attractorStage (p : Player) (T : Set Pos) (n : ℕ) : Set Pos :=
  (G.attractorStep p T)^[n] ∅
Uses 3 · Used by 5
Statement usesParity game · Attractor operator · Players of a parity game
Used byThe attractor stabilizes after as many stages as there are positions · Attractor strategy · The attractor strategy moves into the stage from its controllable predecessor · The attractor strategy reaches the target from an attractor stage · The attractor strategy reaches the target from the attractor

TheoremThe attractor is a fixed point#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions, and let \(A\) be the attractor of \(T\) for \(p\). Then \(T \cup \mathrm{cpre}_p(A) = A\), where \(\mathrm{cpre}_p(A)\) is the controllable predecessor of \(A\) for \(p\); that is, \(A\) is a fixed point of the attractor operator \(X \mapsto T \cup \mathrm{cpre}_p(X)\).

theorem union_cpre_attractor : T ∪ G.cpre p (G.attractor p T) = G.attractor p T
Uses 5 · Used by 3
Statement usesParity game · Attractor · Controllable predecessor · Players of a parity game
Proof usesAttractor operator
Used byThe attractor stabilizes after as many stages as there are positions · The complement of an attractor is a trap · The trap strategy avoids the target

TheoremThe attractor lies in every closed set#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions. If a set \(X\) of positions satisfies \(T \cup \mathrm{cpre}_p(X) \subseteq X\), where \(\mathrm{cpre}_p\) is the controllable predecessor for \(p\), then the attractor of \(T\) for \(p\) is contained in \(X\).

theorem attractor_subset_of {X : Set Pos} (h : T ∪ G.cpre p X ⊆ X) : G.attractor p T ⊆ X
Uses 5 · Used by 2
Statement usesParity game · Attractor · Controllable predecessor · Players of a parity game
Proof usesAttractor operator
Used byThe attractor stabilizes after as many stages as there are positions · Traps disjoint from a set avoid its attractor

TheoremThe attractor stabilizes after as many stages as there are positions#✓fully proved

Let \(G\) be a parity game with finitely many positions, \(N\) of them, let \(p\) be a player and \(T\) a set of positions. Then the attractor of \(T\) for \(p\) equals the \(N\)-th attractor stage of \(T\) for \(p\), that is, the result of applying the attractor operator \(X \mapsto T \cup \mathrm{cpre}_p(X)\) \(N\) times to \(\emptyset\), where \(\mathrm{cpre}_p\) is the controllable predecessor for \(p\).

theorem attractor_eq_attractorStage_card [Finite Pos] :
    G.attractor p T = G.attractorStage p T (Nat.card Pos)
Uses 8 · Used by 1
Statement usesParity game · Attractor · Attractor stages · Players of a parity game
Proof usesAttractor operator · The attractor lies in every closed set · Controllable predecessor · The attractor is a fixed point
Used byThe attractor strategy reaches the target from the attractor

DefinitionAttractor strategy#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions. The attractor strategy of \(p\) for \(T\) is the positional strategy of \(p\) that at a position \(v\) moves to a successor of \(v\) lying in the \(n\)-th attractor stage of \(T\) for \(p\), for the least \(n\) for which \(v\) has such a successor, and to an arbitrary successor of \(v\) if no successor of \(v\) lies in any attractor stage.

noncomputable def attractorStrategy : G.PositionalStrategy p where
  next v :=
    if h : ∃ n w, G.Move v w ∧ w ∈ G.attractorStage p T n then (Nat.find_spec h).choose
    else (G.serial v).choose
  legal v _ := by
    split_ifs with h
    · exact (Nat.find_spec h).choose_spec.1
    · exact (G.serial v).choose_spec
Uses 4 · Used by 5
Statement usesParity game · Positional strategy in a parity game · Attractor stages · Players of a parity game
Used byThe attractor strategy moves into the stage from its controllable predecessor · The attractor strategy reaches the target from an attractor stage · The attractor strategy reaches the target from the attractor · The attractor strategy forces a visit · Characterization of the attractor

TheoremThe attractor strategy moves into the stage from its controllable predecessor#✓fully proved

Let \(G\) be a parity game, \(p\) a player, \(T\) a set of positions, \(n\) a natural number and \(S_n\) the \(n\)-th attractor stage of \(T\) for \(p\). If a position \(v\) owned by \(p\) lies in the controllable predecessor \(\mathrm{cpre}_p(S_n)\) of \(S_n\) for \(p\), then the successor that the attractor strategy of \(p\) for \(T\) chooses at \(v\) lies in \(S_n\).

theorem attractorStrategy_next_mem {n : ℕ} {v : Pos}
    (hv : v ∈ G.cpre p (G.attractorStage p T n)) (hown : G.owner v = p) :
    (G.attractorStrategy p T).next v ∈ G.attractorStage p T n
Uses 7 · Used by 1
Statement usesParity game · Positional strategy in a parity game · Attractor stages · Attractor strategy · Controllable predecessor · Players of a parity game
Proof usesAttractor operator
Used byThe attractor strategy reaches the target from an attractor stage

TheoremThe attractor strategy reaches the target from an attractor stage#✓fully proved

Let \(G\) be a parity game, \(p\) a player, \(T\) a set of positions and \(n\) a natural number. If \(\pi\) is a play of \(G\) that conforms to the attractor strategy of \(p\) for \(T\) and whose initial position \(\pi_0\) lies in the \(n\)-th attractor stage of \(T\) for \(p\), then \(\pi_i \in T\) for some \(i < n\).

theorem attractorStrategy_reaches (n : ℕ) {π : ωSequence Pos} (hπ : G.IsPlay π)
    (hconf : Conforms (G.attractorStrategy p T) π) (h0 : π 0 ∈ G.attractorStage p T n) :
    ∃ i < n, π i ∈ T
Uses 10 · Used by 1
Statement usesParity game · Plays conforming to a strategy · Plays of a parity game · Attractor stages · Attractor strategy · Players of a parity game
Proof usesPositional strategy in a parity game · Attractor operator · The attractor strategy moves into the stage from its controllable predecessor · Controllable predecessor
Used byThe attractor strategy reaches the target from the attractor

DefinitionForcing a visit to a set#✓fully proved

Let \(G\) be a parity game, \(p\) a player, \(\sigma\) a positional strategy of \(p\), \(T\) a set of positions and \(v\) a position. The strategy \(\sigma\) forces a visit to \(T\) from \(v\) when every play \(\pi\) of \(G\) with \(\pi_0 = v\) that conforms to \(\sigma\) visits \(T\), that is, \(\pi_i \in T\) for some \(i \in \mathbb{N}\).

def ForcesReach {p : Player} (σ : G.PositionalStrategy p) (T : Set Pos) (v : Pos) : Prop :=
  ∀ π, G.IsPlay π → π 0 = v → Conforms σ π → ∃ i, π i ∈ T
Uses 5 · Used by 3
Statement usesParity game · Plays conforming to a strategy · Plays of a parity game · Positional strategy in a parity game · Players of a parity game
Used byThe attractor strategy forces a visit · Characterization of the attractor · No strategy forces a visit from outside the attractor

TheoremThe attractor strategy reaches the target from the attractor#✓fully proved

Let \(G\) be a parity game with finitely many positions, \(N\) of them, let \(p\) be a player and \(T\) a set of positions. If \(\pi\) is a play of \(G\) that conforms to the attractor strategy of \(p\) for \(T\) and whose initial position \(\pi_0\) lies in the attractor of \(T\) for \(p\), then \(\pi_i \in T\) for some \(i < N\).

theorem attractorStrategy_reaches_of_mem_attractor [Finite Pos] {π : ωSequence Pos}
    (hπ : G.IsPlay π) (hconf : Conforms (G.attractorStrategy p T) π)
    (h0 : π 0 ∈ G.attractor p T) : ∃ i < Nat.card Pos, π i ∈ T
Uses 9 · Used by 1
Statement usesParity game · Plays conforming to a strategy · Plays of a parity game · Attractor · Attractor strategy · Players of a parity game
Proof usesAttractor stages · The attractor strategy reaches the target from an attractor stage · The attractor stabilizes after as many stages as there are positions
Used byThe attractor strategy forces a visit

TheoremThe attractor strategy forces a visit#✓fully proved

Let \(G\) be a parity game with finitely many positions, \(p\) a player and \(T\) a set of positions. From every position \(v\) of the attractor of \(T\) for \(p\), the attractor strategy of \(p\) for \(T\) forces a visit to \(T\): every play from \(v\) conforming to it visits \(T\).

theorem forcesReach_attractorStrategy [Finite Pos] {v : Pos} (hv : v ∈ G.attractor p T) :
    G.ForcesReach (G.attractorStrategy p T) T v
Uses 8 · Used by 1
Statement usesParity game · Forcing a visit to a set · Attractor · Attractor strategy · Players of a parity game
Proof usesPlays conforming to a strategy · Plays of a parity game · The attractor strategy reaches the target from the attractor
Used byCharacterization of the attractor

DefinitionTrap for a player#✓fully proved

Let \(G\) be a parity game and \(p\) a player. A set \(U\) of positions is a trap for \(p\) when, for every position \(v \in U\), every move from \(v\) leads into \(U\) if \(v\) belongs to \(p\), and some move from \(v\) leads into \(U\) if \(v\) does not belong to \(p\). Thus \(p\) cannot force the play out of \(U\).

def IsTrap (U : Set Pos) : Prop :=
  ∀ v ∈ U, (G.owner v = p → ∀ w, G.Move v w → w ∈ U) ∧ (G.owner v ≠ p → ∃ w, G.Move v w ∧ w ∈ U)
Uses 2 · Used by 4
Statement usesParity game · Players of a parity game
Used byTraps disjoint from a set avoid its attractor · The complement of an attractor is a trap · Winning regions are traps for the opponent · The trap strategy stays in the trap

TheoremThe complement of an attractor is a trap#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions. The complement of the attractor of \(T\) for \(p\) is a trap for \(p\).

theorem isTrap_compl_attractor : G.IsTrap p (G.attractor p T)ᶜ
Uses 6 · Used by 1
Statement usesParity game · Trap for a player · Attractor · Players of a parity game
Proof usesControllable predecessor · The attractor is a fixed point
Used byThe trap strategy avoids the target

TheoremTraps disjoint from a set avoid its attractor#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions. If a set \(U\) of positions is a trap for \(p\) and is disjoint from \(T\), then \(U\) is disjoint from the attractor of \(T\) for \(p\).

Since the complement of the attractor is itself a trap for \(p\) disjoint from \(T\), it is the largest such trap.

theorem IsTrap.disjoint_attractor {U : Set Pos} (hU : G.IsTrap p U) (hT : Disjoint U T) :
    Disjoint U (G.attractor p T)
Uses 6
Statement usesParity game · Trap for a player · Attractor · Players of a parity game
Proof usesThe attractor lies in every closed set · Controllable predecessor

DefinitionTrap strategy#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(U\) a set of positions. The trap strategy for \(U\) is the positional strategy of the opponent of \(p\) that, at each position \(v\), moves to some position \(w \in U\) with a move from \(v\) to \(w\) if there is one, and to an arbitrary position reachable from \(v\) in one move otherwise.

noncomputable def trapStrategy (U : Set Pos) : G.PositionalStrategy p.opponent where
  next v := if h : ∃ w, G.Move v w ∧ w ∈ U then h.choose else (G.serial v).choose
  legal v _ := by
    split_ifs with h
    · exact h.choose_spec.1
    · exact (G.serial v).choose_spec
Uses 4 · Used by 3
Statement usesParity game · Positional strategy in a parity game · Players of a parity game · Opponent
Used byNo strategy forces a visit from outside the attractor · The trap strategy avoids the target · The trap strategy stays in the trap

TheoremThe trap strategy stays in the trap#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(U\) a trap for \(p\). If \(\pi\) is a play with \(\pi_0 \in U\) that conforms to the trap strategy of the opponent of \(p\) for \(U\), then \(\pi_i \in U\) for every \(i \in \mathbb{N}\).

theorem IsTrap.trapStrategy_stays {U : Set Pos} (hU : G.IsTrap p U) {π : ωSequence Pos}
    (hπ : G.IsPlay π) (hconf : Conforms (G.trapStrategy p U) π) (h0 : π 0 ∈ U) (i : ℕ) :
    π i ∈ U
Uses 9 · Used by 1
Statement usesParity game · Plays conforming to a strategy · Plays of a parity game · Trap for a player · Trap strategy · Players of a parity game · Opponent
Proof usesPositional strategy in a parity game · Every player is \(p\) or the opponent of \(p\)
Used byThe trap strategy avoids the target

TheoremThe trap strategy avoids the target#✓fully proved

Let \(G\) be a parity game, \(p\) a player, \(T\) a set of positions and \(A\) the attractor of \(T\) for \(p\). If \(\pi\) is a play starting at a position outside \(A\) that conforms to the trap strategy of the opponent of \(p\) for the complement of \(A\), then \(\pi_i \notin T\) for every \(i \in \mathbb{N}\).

theorem trapStrategy_avoids {v : Pos} (hv : v ∉ G.attractor p T) {π : ωSequence Pos}
    (hπ : G.IsPlay π) (h0 : π 0 = v) (hconf : Conforms (G.trapStrategy p (G.attractor p T)ᶜ) π)
    (i : ℕ) : π i ∉ T
Uses 11 · Used by 1
Statement usesParity game · Plays conforming to a strategy · Plays of a parity game · Attractor · Trap strategy · Players of a parity game · Opponent
Proof usesThe trap strategy stays in the trap · Controllable predecessor · The complement of an attractor is a trap · The attractor is a fixed point
Used byNo strategy forces a visit from outside the attractor

TheoremNo strategy forces a visit from outside the attractor#✓fully proved

Let \(G\) be a parity game, \(p\) a player and \(T\) a set of positions. If a position \(v\) is not in the attractor of \(T\) for \(p\), then no positional strategy of \(p\) forces a visit to \(T\) from \(v\).

theorem not_forcesReach_of_notMem_attractor {v : Pos} (hv : v ∉ G.attractor p T)
    (σ : G.PositionalStrategy p) : ¬ G.ForcesReach σ T v
Uses 13 · Used by 1
Statement usesParity game · Forcing a visit to a set · Positional strategy in a parity game · Attractor · Players of a parity game
Proof usesPlays conforming to a strategy · Plays of a parity game · Joint successor of two strategies · Outcome of two positional strategies · Trap strategy · The trap strategy avoids the target · Every player is \(p\) or the opponent of \(p\) · Opponent
Used byCharacterization of the attractor

TheoremCharacterization of the attractor#✓fully proved

Let \(G\) be a parity game with finitely many positions, \(p\) a player and \(T\) a set of positions. A position \(v\) lies in the attractor of \(T\) for \(p\) if and only if some positional strategy of \(p\) forces a visit to \(T\) from \(v\).

theorem mem_attractor_iff [Finite Pos] {v : Pos} :
    v ∈ G.attractor p T ↔ ∃ σ : G.PositionalStrategy p, G.ForcesReach σ T v
Uses 8
Statement usesParity game · Forcing a visit to a set · Positional strategy in a parity game · Attractor · Players of a parity game
Proof usesAttractor strategy · The attractor strategy forces a visit · No strategy forces a visit from outside the attractor

TheoremWinning regions are traps for the opponent#✓fully proved

In a parity game \(G\), the winning region of a player \(p\), the set of positions from which \(p\) has a winning positional strategy, is a trap for the opponent of \(p\).

theorem isTrap_winningRegion : G.IsTrap p.opponent (G.WinningRegion p)
Uses 10
Statement usesParity game · Trap for a player · Winning region of a parity game · Players of a parity game · Opponent
Proof usesPositional strategy in a parity game · Winning strategy from a position · Opponent moves stay in the winning region · A winning strategy's move stays in the winning region · Every player is \(p\) or the opponent of \(p\)

StructureEncoded parity game#✓fully proved

An encoded finite parity game on the \(n\) positions \(0, \dots, n - 1\) consists of an owner for each position, given as a Boolean (false for the even player, true for the odd player), a move relation, given as a Boolean-valued \(n \times n\) matrix, and a priority for each position, given as a natural number.

No seriality is assumed: a position may have no move, since restricted subgames need not be serial on the whole arena.

structure EncodedParityGame (n : ℕ) where
  /-- The owner of each position: `false` for even, `true` for odd. -/
  owner : Fin n → Bool
  /-- The move matrix: `move v w = true` iff there is a move from `v` to `w`. -/
  move : Fin n → Fin n → Bool
  /-- The priority of each position. -/
  priority : Fin n → ℕ
Used by 15
Used byAttractor inside a set of positions · Controllable predecessor inside a set of positions · Dual parity game · Positions of maximal priority · Maximal priority on a set of positions · Priority compression · Compressed priority · Bound on compressed priorities · Priority compression preserves and reflects the order of priorities · Priority compression preserves parity · Rank of a priority in a parity game · Monotonicity of priority ranks · Priority ranks are below the number of priorities · Strict monotonicity of priority ranks · The parity game of a serial encoded game

DefinitionThe parity game of a serial encoded game#✓fully proved

Let \(G\) be an encoded parity game on the positions \(\{0, \dots, n-1\}\) in which every position has a move to some position. The associated parity game has the same positions, moves and priorities, and a position is owned by the odd player if \(G\) assigns it to the odd player and by the even player otherwise; every position has a move by the hypothesis on \(G\).

def toParityGame (hser : ∀ v, ∃ w, G.move v w = true) : ParityGame (Fin n) where
  owner v := if G.owner v then Player.odd else Player.even
  Move v w := G.move v w = true
  priority := G.priority
  serial v := by
    obtain ⟨w, hw⟩ := hser v
    exact ⟨w, hw⟩
Uses 3
Statement usesEncoded parity game · Parity game · Players of a parity game

DefinitionDual parity game#✓fully proved

The dual of an encoded parity game \(G\) is the encoded parity game with the same positions and moves in which every position is owned by the other player than in \(G\) and has priority one more than in \(G\).

Since incrementing priorities flips every parity, the even player wins the dual game exactly where the odd player wins the original.

def dualGame : EncodedParityGame n where
  owner v := !G.owner v
  move := G.move
  priority v := G.priority v + 1
Uses 1
Statement usesEncoded parity game

DefinitionControllable predecessor inside a set of positions#✓fully proved

Let \(G\) be an encoded parity game, \(p\) a player (encoded as a Boolean: false for even, true for odd), and \(U\), \(X\) sets of positions. The controllable predecessor of \(X\) for \(p\) inside \(U\) is the set of positions \(v \in U\) such that either \(v\) is owned by \(p\) and some move of \(G\) goes from \(v\) to a position of \(U \cap X\), or \(v\) is not owned by \(p\) and every move of \(G\) from \(v\) to a position of \(U\) ends in \(X\).

Moves leaving \(U\) are ignored; in particular a position of \(U\) not owned by \(p\) with no move into \(U\) belongs to the set.

def cpreIn (p : Bool) (U X : Finset (Fin n)) : Finset (Fin n) :=
  U.filter fun v =>
    (if G.owner v = p then
      (List.finRange n).any fun w =>
        decide (w ∈ U) && G.move v w && decide (w ∈ X)
    else
      (List.finRange n).all fun w =>
        (!decide (w ∈ U)) || (!G.move v w) || decide (w ∈ X)) = true
Uses 1 · Used by 1
Statement usesEncoded parity game
Used byAttractor inside a set of positions

DefinitionAttractor inside a set of positions#✓fully proved

Let \(G\) be an encoded parity game on \(n\) positions, \(p\) a player (encoded as a Boolean: false for even, true for odd), and \(T\), \(U\) sets of positions. The attractor of \(T\) for \(p\) inside \(U\) is the set obtained from \(\emptyset\) by applying \(n\) times the map \(X \mapsto (T \cap U) \cup \mathrm{CPre}_p^U(X)\), where \(\mathrm{CPre}_p^U(X)\) is the controllable predecessor of \(X\) for \(p\) inside \(U\).

def attractorIn (p : Bool) (T U : Finset (Fin n)) : Finset (Fin n) :=
  (fun X => (T ∩ U) ∪ cpreIn G p U X)^[n] ∅
Uses 2
Statement usesEncoded parity game · Controllable predecessor inside a set of positions

DefinitionRank of a priority in a parity game#✓fully proved

The rank of a priority p among the distinct priorities occurring in the game: the number of distinct priorities q < p that occur.

def priorityRank (p : ℕ) : ℕ :=
  ((Finset.univ : Finset (Fin n)).image G.priority).filter (· < p) |>.card
Uses 1 · Used by 7
Statement usesEncoded parity game
Used byCompressed priority · Bound on compressed priorities · Priority compression preserves and reflects the order of priorities · Priority compression preserves parity · Monotonicity of priority ranks · Priority ranks are below the number of priorities · Strict monotonicity of priority ranks

DefinitionCompressed priority#✓fully proved

Let \(G\) be an encoded parity game on the positions \(\{0, \dots, n-1\}\). The compressed priority of a natural number \(p\) is \(2r + (p \bmod 2)\), where \(r\) is the rank of \(p\) in \(G\): the number of distinct priorities \(q < p\) that occur in \(G\).

The compressed priority of \(p\) is congruent to \(p\) modulo \(2\). On the priorities that occur in \(G\), compression is injective and strictly increasing.

def priorityCompressed (p : ℕ) : ℕ :=
  2 * G.priorityRank p + (p % 2)
Uses 2 · Used by 1
Statement usesEncoded parity game · Rank of a priority in a parity game
Used byPriority compression

DefinitionPriority compression#✓fully proved

For an encoded parity game \(G\) on \(n\) positions, the compressed game has the same owners and moves as \(G\) and gives each position \(v\) the priority \(2r + (q \bmod 2)\), where \(q\) is the priority of \(v\) in \(G\) and \(r\) is the number of distinct priorities occurring in \(G\) that are smaller than \(q\).

Since at most \(n\) distinct priorities occur, every compressed priority is strictly below \(2n\).

def priorityCompress : EncodedParityGame n where
  owner := G.owner
  move := G.move
  priority v := G.priorityCompressed (G.priority v)
Uses 2 · Used by 3
Statement usesEncoded parity game · Compressed priority
Used byBound on compressed priorities · Priority compression preserves and reflects the order of priorities · Priority compression preserves parity

TheoremPriority ranks are below the number of priorities#✓fully proved

Let \(G\) be an encoded parity game, and for a natural number \(p\) let the rank of \(p\) be the number of distinct priorities \(q < p\) that occur in \(G\). For every position \(v\) of \(G\), the rank of the priority of \(v\) is strictly less than the number of distinct priorities that occur in \(G\).

The priorities below the priority of \(v\) form a proper subset of the occurring priorities, since the priority of \(v\) occurs but is not below itself.

theorem priorityRank_lt_card {v : Fin n} :
    G.priorityRank (G.priority v) <
      ((Finset.univ : Finset (Fin n)).image G.priority).card
Sources
  • M. Jurdziński, "Small progress measures for solving parity games", Proceedings of STACS 2000, LNCS 1770, 290-301.
Uses 2 · Used by 1
Statement usesEncoded parity game · Rank of a priority in a parity game
Used byBound on compressed priorities

TheoremStrict monotonicity of priority ranks#✓fully proved

Let \(G\) be an encoded parity game, and for a natural number \(p\) let the rank of \(p\) be the number of distinct priorities \(q < p\) that occur in \(G\). If \(v\) and \(w\) are positions of \(G\) and the priority of \(w\) is strictly less than the priority of \(v\), then the rank of the priority of \(w\) is strictly less than the rank of the priority of \(v\).

The priority of \(w\) is counted in the rank of the priority of \(v\) but not in its own rank.

theorem priorityRank_lt_of_lt {v w : Fin n} (h : G.priority w < G.priority v) :
    G.priorityRank (G.priority w) < G.priorityRank (G.priority v)
Sources
  • M. Jurdziński, "Small progress measures for solving parity games", Proceedings of STACS 2000, LNCS 1770, 290-301.
Uses 2 · Used by 1
Statement usesEncoded parity game · Rank of a priority in a parity game
Used byPriority compression preserves and reflects the order of priorities

TheoremMonotonicity of priority ranks#✓fully proved

Let \(G\) be an encoded parity game, and for a natural number \(p\) let the rank of \(p\) be the number of distinct priorities \(q < p\) that occur in \(G\). If \(v\) and \(w\) are positions of \(G\) and the priority of \(w\) is at most the priority of \(v\), then the rank of the priority of \(w\) is at most the rank of the priority of \(v\).

theorem priorityRank_le_of_le {v w : Fin n} (h : G.priority w ≤ G.priority v) :
    G.priorityRank (G.priority w) ≤ G.priorityRank (G.priority v)
Sources
  • M. Jurdziński, "Small progress measures for solving parity games", Proceedings of STACS 2000, LNCS 1770, 290-301.
Uses 2
Statement usesEncoded parity game · Rank of a priority in a parity game

TheoremBound on compressed priorities#✓fully proved

For an encoded parity game \(G\) on \(n\) positions, every priority of the priority-compressed game of \(G\) is strictly less than \(2n\).

This holds because at most \(n\) distinct priorities occur in \(G\).

theorem priorityCompressed_lt {v : Fin n} :
    (G.priorityCompress).priority v < 2 * n
Uses 4
Statement usesEncoded parity game · Priority compression
Proof usesRank of a priority in a parity game · Priority ranks are below the number of priorities

TheoremPriority compression preserves and reflects the order of priorities#✓fully proved

For an encoded parity game \(G\) and positions \(v\), \(w\), the priority of \(v\) is smaller than the priority of \(w\) in the priority-compressed game of \(G\) if and only if it is smaller in \(G\).

theorem priorityCompressed_lt_iff {v w : Fin n} :
    (G.priorityCompress).priority v < (G.priorityCompress).priority w ↔
      G.priority v < G.priority w
Uses 4
Statement usesEncoded parity game · Priority compression
Proof usesRank of a priority in a parity game · Strict monotonicity of priority ranks

TheoremPriority compression preserves parity#✓fully proved

For an encoded parity game \(G\) and every position \(v\), the priority of \(v\) in the priority-compressed game of \(G\) has the same parity as the priority of \(v\) in \(G\).

theorem priorityCompressed_mod_two {v : Fin n} :
    (G.priorityCompress).priority v % 2 = G.priority v % 2
Uses 3
Statement usesEncoded parity game · Priority compression
Proof usesRank of a priority in a parity game

DefinitionMaximal priority on a set of positions#✓fully proved

For an encoded parity game \(G\) and a set \(U\) of positions, the maximal priority on \(U\) is the largest priority of \(G\) at a position of \(U\), or \(0\) if \(U\) is empty.

def maxPriorityIn (U : Finset (Fin n)) : ℕ :=
  U.sup G.priority
Uses 1 · Used by 1
Statement usesEncoded parity game
Used byPositions of maximal priority

DefinitionPositions of maximal priority#✓fully proved

For an encoded parity game \(G\) and a set \(U\) of positions, the positions of maximal priority in \(U\) are the positions \(v \in U\) whose priority equals the maximal priority of \(G\) on \(U\).

def maxPositionsIn (U : Finset (Fin n)) : Finset (Fin n) :=
  U.filter fun v => G.priority v = maxPriorityIn G U
Uses 2
Statement usesEncoded parity game · Maximal priority on a set of positions
59 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.