Payoff-free reachability

Finite transition reachability for Arena, together with reachability from a ControlledGame root. The relation records existence of a path; it makes no finiteness, acyclicity, or decidability assumption.

Main definitions

• Arena.Reachable — finite transition reachability between Arena states.
• ControlledGame.IsReachable — reachability from a controlled game's root.

inductive Arena.Reachable (A : Arena) : A.State → A.State → Prop

A state t is reachable from s if a finite legal path leads from s to t.

• refl {A : Arena} (s : A.State) : A.Reachable s s
• step {A : Arena} {s t : A.State} (a : A.Action s) (h : A.Reachable (A.next s a) t) : A.Reachable s t

theorem Arena.Reachable.trans {A : Arena} {s t u : A.State} (h₁ : A.Reachable s t) (h₂ : A.Reachable t u) : A.Reachable s u

Reachability is transitive.

theorem Arena.Reachable.step' {A : Arena} {s t : A.State} (h : A.Reachable s t) (action : A.Action t) : A.Reachable s (A.next t action)

Taking one legal action extends a reachable path.

def ControlledGame.IsReachable {N : Type u_1} (G : ControlledGame N) (state : G.State) : Prop

A state is reachable in a controlled game if it is reachable from its distinguished initial state.

Equations

• G.IsReachable state = G.Reachable G.init state

theorem ControlledGame.isReachable_init {N : Type u_1} (G : ControlledGame N) : G.IsReachable G.init

The initial state is reachable.

theorem ControlledGame.IsReachable.next {N : Type u_1} {G : ControlledGame N} {state : G.State} (h : G.IsReachable state) (action : G.Action state) : G.IsReachable (G.next state action)

A legal successor of a reachable state is reachable.