structure AP.State : Type

• pw : ℕ
• taken : Set' PointZ
• aPos : PointZ
• aTurn : Bool
• hist : List PointZ

theorem AP.State.ext_iff {x y : State} : x = y ↔ x.pw = y.pw ∧ x.taken = y.taken ∧ x.aPos = y.aPos ∧ x.aTurn = y.aTurn ∧ x.hist = y.hist

theorem AP.State.ext {x y : State} (pw : x.pw = y.pw) (taken : x.taken = y.taken) (aPos : x.aPos = y.aPos) (aTurn : x.aTurn = y.aTurn) (hist : x.hist = y.hist) : x = y

@[instance_reducible]

instance AP.instDecidableEqState : DecidableEq State

Equations

• AP.instDecidableEqState = AP.instDecidableEqState.decEq

def AP.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

• AP.instDecidableEqState.decEq { pw := a, taken := a_1, aPos := a_2, aTurn := a_3, hist := a_4 } { pw := b, taken := b_1, aPos := b_2, aTurn := b_3, hist := b_4 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ if h : a_2 = b_2 then h ▸ if h : a_3 = b_3 then h ▸ if h : a_4 = b_4 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯

structure AP.AStrat : Type

• mk' :: (
• f : State → PointZ
• )

theorem AP.AStrat.ext {x y : AStrat} (f : x.f = y.f) : x = y

theorem AP.AStrat.ext_iff {x y : AStrat} : x = y ↔ x.f = y.f

structure AP.DStrat : Type

• mk' :: (
• f : State → PointZ
• )

theorem AP.DStrat.ext {x y : DStrat} (f : x.f = y.f) : x = y

theorem AP.DStrat.ext_iff {x y : DStrat} : x = y ↔ x.f = y.f

structure AP.Strat : Type

• a : AStrat
• d : DStrat

theorem AP.Strat.ext {x y : Strat} (a : x.a = y.a) (d : x.d = y.d) : x = y

theorem AP.Strat.ext_iff {x y : Strat} : x = y ↔ x.a = y.a ∧ x.d = y.d

def AP.initState (pw : ℕ) (aPos : PointZ) : State

Equations

• AP.initState pw aPos = { pw := pw, taken := ∅, aPos := aPos, aTurn := false, hist := [aPos] }

def AP.State.aMove (s : State) (p : PointZ) : Option State

Equations

• s.aMove p = do guard (s.aPos ≠ p) guard (p ∉ s.taken) guard (Point.dist p s.aPos ≤ ↑s.pw) pure { pw := s.pw, taken := s.taken, aPos := p, aTurn := s.aTurn, hist := s.hist }

def AP.State.dMove (s : State) (p : PointZ) : Option State

Equations

• s.dMove p = do guard (s.aPos ≠ p) guard (p ∉ s.taken) pure { pw := s.pw, taken := s.taken.insert p, aPos := s.aPos, aTurn := s.aTurn, hist := s.hist }

def AP.State.move (s : State) (p : PointZ) : Option State

Equations

• s.move p = if s.aTurn = true then do let s' ← s.aMove p (fun (s' : AP.State) => pure { pw := s'.pw, taken := s'.taken, aPos := s'.aPos, aTurn := decide ¬s.aTurn = true, hist := p :: s.hist }) s' else do let s' ← s.dMove p (fun (s' : AP.State) => pure { pw := s'.pw, taken := s'.taken, aPos := s'.aPos, aTurn := decide ¬s.aTurn = true, hist := p :: s.hist }) s'

def AP.sys : System State PointZ

Equations

• AP.sys = { initial := {s : AP.State | ∃ (pw : ℕ) (p : PointZ), AP.initState pw p = s}, tr := AP.State.move }

class AP.AStrat.WF (a : AStrat) : Prop

• h {s : State} [sys.WF s] : sys.hasTr s → s.aTurn = true → sys.validTr s (a.f s)

class AP.DStrat.WF (d : DStrat) : Prop

• h {s : State} [sys.WF s] : sys.hasTr s → s.aTurn = false → sys.validTr s (d.f s)

def AP.Strat.f (st : Strat) (s : State) : PointZ

Equations

• st.f s = if s.aTurn = true then st.a.f s else st.d.f s

class AP.Strat.WF (st : Strat) : Prop

• h {s : State} [sys.WF s] : sys.hasTr s → sys.validTr s (st.f s)

def AP.State.aWins (s : State) (st : Strat) : Prop

Equations

• s.aWins st = ∀ (n : ℕ), (AP.sys.simulate st.f s n).2 = 0

def AP.State.dWins (s : State) (st : Strat) : Prop

Equations

• s.dWins st = ∃ (n : ℕ), (AP.sys.simulate st.f s n).2 ≠ 0

def AP.State.aHws (s : State) : Prop

Equations

• s.aHws = ∃ (a : AP.AStrat), a.WF ∧ ∀ (d : AP.DStrat), d.WF → s.aWins { a := a, d := d }

def AP.State.dHws (s : State) : Prop

Equations

• s.dHws = ∃ (d : AP.DStrat), d.WF ∧ ∀ (a : AP.AStrat), a.WF → s.dWins { a := a, d := d }

def AP.aHwsPw (pw : ℕ) : Prop

Equations

• AP.aHwsPw pw = ∀ (p : PointZ), (AP.initState pw p).aHws

def AP.dHwsPw (pw : ℕ) : Prop

Equations

• AP.dHwsPw pw = ∀ (p : PointZ), (AP.initState pw p).dHws