def AP.State.aPos₀ (s : State) : PointZ

Equations

• s.aPos₀ = s.hist.getLast?.getd

def AP.State.aMoves (s : State) : List PointZ

Equations

• s.aMoves = List.filter (fun (b : PointZ) => decide (AP.sys.validTr s b)) (Point.nbhd s.aPos ↑s.pw)

def AP.State.aHasMove (s : State) : Bool

Equations

• s.aHasMove = decide (s.aMoves ≠ [])

def AP.State.hasMove (s : State) : Bool

Equations

• s.hasMove = if s.aTurn = true then s.aHasMove else true

def AP.State.setHist (s : State) (hist : List PointZ) : State

Equations

• s.setHist hist = { pw := s.pw, taken := s.taken, aPos := s.aPos, aTurn := s.aTurn, hist := hist }

def AP.State.setPw (s : State) (pw : ℕ) : State

Equations

• s.setPw pw = { pw := pw, taken := s.taken, aPos := s.aPos, aTurn := s.aTurn, hist := s.hist }

def AP.State.chooseAMove (s : State) : PointZ

Equations

• s.chooseAMove = (List.filter (fun (b : PointZ) => decide (AP.sys.validTr s b)) (Point.nbhd s.aPos ↑s.pw)).head?.getD 0

def AP.State.chooseDMove (s : State) : PointZ

Equations

• s.chooseDMove = (insert s.aPos s.taken).max! + { x := 1, y := 0 }

def AP.State.chooseMove (s : State) : PointZ

Equations

• s.chooseMove = if s.aTurn = true then s.chooseAMove else s.chooseDMove

def AP.State.decideWF (s : State) : Bool

Equations

• s.decideWF = decide (AP.sys.trs (AP.initState s.pw s.aPos₀) s.hist.reverse.tail = (s, []))

def AP.State.decideAState (s : State) : Bool

Equations

• s.decideAState = (s.decideWF && s.aTurn)

def AP.State.decideDState (s : State) : Bool

Equations

• s.decideDState = (s.decideWF && !s.aTurn)

def AP.mkStratFn (f : State → Option PointZ) (s : State) : PointZ

Equations

• AP.mkStratFn f s = (fun (x : Option PointZ) => x.getD s.chooseMove) do let p ← f s guard (AP.sys.validTr s p) pure p

def AP.AStrat.mk (f : State → Option PointZ) : AStrat

Equations

• AP.AStrat.mk f = { f := AP.mkStratFn f }

def AP.DStrat.mk (f : State → Option PointZ) : DStrat

Equations

• AP.DStrat.mk f = { f := AP.mkStratFn f }

theorem AP.AStrat.wf_def {a : AStrat} : a.WF ↔ ∀ {s : State} [sys.WF s], sys.hasTr s → s.aTurn = true → sys.validTr s (a.f s)

theorem AP.DStrat.wf_def {d : DStrat} : d.WF ↔ ∀ {s : State} [sys.WF s], sys.hasTr s → s.aTurn = false → sys.validTr s (d.f s)

theorem AP.Strat.wf_def {st : Strat} : st.WF ↔ ∀ {s : State} [sys.WF s], sys.hasTr s → sys.validTr s (st.f s)

theorem AP.Strat.wf_iff {st : Strat} : st.WF ↔ st.a.WF ∧ st.d.WF

theorem AP.Strat.WF.wf_a {st : Strat} [hst : st.WF] : st.a.WF

theorem AP.Strat.WF.wf_d {st : Strat} [hst : st.WF] : st.d.WF

@[simp]

instance AP.instWFAOfWF {st : Strat} [hst : st.WF] : st.a.WF

@[simp]

instance AP.instWFDOfWF {st : Strat} [hst : st.WF] : st.d.WF

@[instance_reducible]

instance AP.instInhabitedState : Inhabited State

Equations

• AP.instInhabitedState = { default := AP.initState 0 0 }

@[simp]

theorem AP.State.default_def : default = initState 0 0

@[simp]

instance AP.instWFStatePointZSysDefault : sys.WF default

class AP.AState (s : State) : Prop

• wf : sys.WF s
• turn : s.aTurn = true

class AP.DState (s : State) : Prop

• wf : sys.WF s
• turn : s.aTurn = false

theorem AP.AState.iff {s : State} : AState s ↔ sys.WF s ∧ s.aTurn = true

theorem AP.DState.iff {s : State} : DState s ↔ sys.WF s ∧ s.aTurn = false

@[simp]

instance AP.instWFStatePointZSysOfAState {sa : State} [ha : AState sa] : sys.WF sa

@[simp]

instance AP.instWFStatePointZSysOfDState {sd : State} [hd : DState sd] : sys.WF sd

@[simp]

theorem AP.AState.turn' {s : State} [hs : AState s] : s.aTurn = true

@[simp]

theorem AP.DState.turn' {s : State} [hs : DState s] : s.aTurn = false

theorem AP.State.validTr_iff_of_aTurn {s : State} {p : PointZ} (ht : s.aTurn = true) : sys.validTr s p ↔ s.aPos ≠ p ∧ p ∉ s.taken ∧ Point.dist p s.aPos ≤ ↑s.pw

theorem AP.State.validTr_iff_of_not_aTurn {s : State} {p : PointZ} (ht : s.aTurn = false) : sys.validTr s p ↔ s.aPos ≠ p ∧ p ∉ s.taken

theorem AP.AState.validTr_iff {s : State} [hs : AState s] {p : PointZ} : sys.validTr s p ↔ s.aPos ≠ p ∧ p ∉ s.taken ∧ Point.dist p s.aPos ≤ ↑s.pw

theorem AP.DState.validTr_iff {s : State} [hs : DState s] {p : PointZ} : sys.validTr s p ↔ s.aPos ≠ p ∧ p ∉ s.taken

theorem AP.State.validTr_chooseDMove {s : State} (ht : s.aTurn = false) : sys.validTr s s.chooseDMove

@[simp]

theorem AP.DState.validTr_chooseDMove {s : State} [hs : DState s] : sys.validTr s s.chooseDMove

theorem AP.State.hasTr_of_not_aTurn {s : State} (ht : s.aTurn = false) : sys.hasTr s

@[simp]

theorem AP.DState.hasTr {s : State} [hs : DState s] : sys.hasTr s

theorem AP.State.hasTr_iff_of_aTurn {s : State} (ht : s.aTurn = true) : sys.hasTr s ↔ ∃ (p : PointZ), s.aPos ≠ p ∧ p ∉ s.taken ∧ Point.dist p s.aPos ≤ ↑s.pw

theorem AP.AState.hasTr_iff {s : State} [hs : AState s] : sys.hasTr s ↔ ∃ (p : PointZ), s.aPos ≠ p ∧ p ∉ s.taken ∧ Point.dist p s.aPos ≤ ↑s.pw

theorem AP.State.aHasMove_of_hasTr {s : State} (ht : s.aTurn = true) (h : sys.hasTr s) : s.aHasMove = true

theorem AP.State.hasTr_of_aHasMove {s : State} (ht : s.aTurn = true) (h : s.aHasMove = true) : sys.hasTr s

theorem AP.State.hasTr_iff_aHasMove {s : State} (ht : s.aTurn = true) : sys.hasTr s ↔ s.aHasMove = true

theorem AP.State.WF.ind_turn {P : State → Prop} (h₁ : ∀ (s : State), AState s → P s) (h₂ : ∀ (s : State), DState s → P s) {s : State} (hs : sys.WF s) : P s

theorem AP.State.hasTr_iff_hasMove {s : State} : sys.hasTr s ↔ s.hasMove = true

@[instance_reducible]

instance AP.instDecidableHasTrStatePointZSys {s : State} : Decidable (sys.hasTr s)

Equations

• AP.instDecidableHasTrStatePointZSys = decidable_of_iff' (s.hasMove = true) ⋯

@[simp]

theorem AP.State.pw_setHist {s : State} {hist : List PointZ} : (s.setHist hist).pw = s.pw

@[simp]

theorem AP.State.aPos_setHist {s : State} {hist : List PointZ} : (s.setHist hist).aPos = s.aPos

@[simp]

theorem AP.State.aTurn_setHist {s : State} {hist : List PointZ} : (s.setHist hist).aTurn = s.aTurn

@[simp]

theorem AP.State.taken_setHist {s : State} {hist : List PointZ} : (s.setHist hist).taken = s.taken

@[simp]

theorem AP.State.hist_setHist {s : State} {hist : List PointZ} : (s.setHist hist).hist = hist

@[simp]

theorem AP.State.setHist_setHist {s : State} {hist₁ hist₂ : List PointZ} : (s.setHist hist₁).setHist hist₂ = s.setHist hist₂

@[simp]

theorem AP.State.setHist_eq_self_iff {s : State} {hist : List PointZ} : s.setHist hist = s ↔ s.hist = hist

@[simp]

theorem AP.State.setHist_hist_self_eq_self {s : State} : s.setHist s.hist = s

@[simp]

instance AP.instAStateSetHistOfWFStatePointZSys {s : State} {hist : List PointZ} [hs : AState s] [hs' : sys.WF (s.setHist hist)] : AState (s.setHist hist)

@[simp]

instance AP.instDStateSetHistOfWFStatePointZSys {s : State} {hist : List PointZ} [hs : DState s] [hs' : sys.WF (s.setHist hist)] : DState (s.setHist hist)

@[simp]

theorem AP.State.pw_setPw {s : State} {pw : ℕ} : (s.setPw pw).pw = pw

@[simp]

theorem AP.State.aPos_setPw {s : State} {pw : ℕ} : (s.setPw pw).aPos = s.aPos

@[simp]

theorem AP.State.aTurn_setPw {s : State} {pw : ℕ} : (s.setPw pw).aTurn = s.aTurn

@[simp]

theorem AP.State.taken_setPw {s : State} {pw : ℕ} : (s.setPw pw).taken = s.taken

@[simp]

theorem AP.State.hist_setPw {s : State} {pw : ℕ} : (s.setPw pw).hist = s.hist

@[simp]

theorem AP.State.setPw_setPw {s : State} {pw₁ pw₂ : ℕ} : (s.setPw pw₁).setPw pw₂ = s.setPw pw₂

@[simp]

theorem AP.State.setPw_eq_self_iff {s : State} {pw : ℕ} : s.setPw pw = s ↔ s.pw = pw

@[simp]

theorem AP.State.setPw_pw_self_eq_self {s : State} : s.setPw s.pw = s

theorem AP.AState.validTr_of_le {s : State} [hs : AState s] {pw : ℕ} {p : PointZ} (h₁ : s.pw ≤ pw) (h₂ : sys.validTr s p) : sys.validTr (s.setPw pw) p

theorem AP.AState.hasTr_of_le {s : State} [hs : AState s] {pw : ℕ} (h₁ : s.pw ≤ pw) (h₂ : sys.hasTr s) : sys.hasTr (s.setPw pw)

@[simp]

theorem AP.State.not_aWins_iff {s : State} {st : Strat} : ¬s.aWins st ↔ s.dWins st

@[simp]

theorem AP.State.not_dWins_iff {s : State} {st : Strat} : ¬s.dWins st ↔ s.aWins st

theorem AP.AStrat.wf_iff {a : AStrat} : a.WF ↔ ∀ {s : State} [AState s], sys.hasTr s → sys.validTr s (a.f s)

theorem AP.DStrat.wf_iff {d : DStrat} : d.WF ↔ ∀ (s : State) [DState s], sys.validTr s (d.f s)

theorem AP.State.tr_eq_some_iff_of_aTurn {s s' : State} {p : PointZ} (ht : s.aTurn = true) : sys.tr s p = some s' ↔ (s.aPos ≠ p ∧ p ∉ s.taken ∧ Point.dist p s.aPos ≤ ↑s.pw) ∧ { pw := s.pw, taken := s.taken, aPos := p, aTurn := false, hist := p :: s.hist } = s'

theorem AP.State.tr_eq_some_iff_of_not_aTurn {s s' : State} {p : PointZ} (ht : s.aTurn = false) : sys.tr s p = some s' ↔ (s.aPos ≠ p ∧ p ∉ s.taken) ∧ { pw := s.pw, taken := s.taken.insert p, aPos := s.aPos, aTurn := true, hist := p :: s.hist } = s'

theorem AP.AState.tr_eq_some_iff {s s' : State} {p : PointZ} [hs : AState s] : sys.tr s p = some s' ↔ (s.aPos ≠ p ∧ p ∉ s.taken ∧ Point.dist p s.aPos ≤ ↑s.pw) ∧ { pw := s.pw, taken := s.taken, aPos := p, aTurn := false, hist := p :: s.hist } = s'

theorem AP.DState.tr_eq_some_iff {s s' : State} {p : PointZ} [hs : DState s] : sys.tr s p = some s' ↔ (s.aPos ≠ p ∧ p ∉ s.taken) ∧ { pw := s.pw, taken := s.taken.insert p, aPos := s.aPos, aTurn := true, hist := p :: s.hist } = s'

@[simp]

theorem AP.AState.strat_f_eq {sa : State} {st : Strat} [ha : AState sa] : st.f sa = st.a.f sa

@[simp]

theorem AP.DState.strat_f_eq {sd : State} {st : Strat} [hd : DState sd] : st.f sd = st.d.f sd

theorem AP.State.aWins_iff_mul_two {s : State} {st : Strat} : s.aWins st ↔ ∀ (n : ℕ), (sys.simulate st.f s (n * 2)).2 = 0

@[simp]

theorem AP.DState.tr_ne_none {sd : State} [hd : DState sd] {st : DStrat} [hst : st.WF] : sys.tr sd (st.f sd) ≠ none

@[simp]

instance AP.instSimFnStatePointZSysFOfWF {st : Strat} [hst : st.WF] : sys.SimFn st.f

theorem AP.AState.of_tr {sa sd : State} {p : PointZ} [hd : DState sd] (h : sys.tr sd p = some sa) : AState sa

theorem AP.DState.of_tr {sa sd : State} {p : PointZ} [ha : AState sa] (h : sys.tr sa p = some sd) : DState sd

theorem AP.AState.of_tr' {sa sd : State} {p : PointZ} [ha : sys.WF sa] [hd : DState sd] (h : sys.tr sa p = some sd) : AState sa

theorem AP.DState.of_tr' {sa sd : State} {p : PointZ} [hd : sys.WF sd] [ha : AState sa] (h : sys.tr sd p = some sa) : DState sd

@[simp]

theorem AP.AState.not_dState {sa : State} [ha : AState sa] : ¬DState sa

@[simp]

theorem AP.DState.not_aState {sd : State} [hd : DState sd] : ¬AState sd

instance AP.instWFMkOfWFOfWF {a : AStrat} {d : DStrat} [ha : a.WF] [hd : d.WF] : { a := a, d := d }.WF

@[simp]

instance AP.instWFMk'OfSimFnStatePointZSys {f : State → PointZ} [hf : sys.SimFn f] : { f := f }.WF

@[simp]

instance AP.instWFMk'OfSimFnStatePointZSys_1 {f : State → PointZ} [hf : sys.SimFn f] : { f := f }.WF

theorem AP.State.aState_or_dState {s : State} [hs : sys.WF s] : AState s ∨ DState s

theorem AP.AStrat.WF.validTr {s : State} [hs : AState s] {st : AStrat} [hst : st.WF] (h : sys.hasTr s) : sys.validTr s (st.f s)

@[simp]

theorem AP.DStrat.WF.validTr (s : State) [hs : DState s] {st : DStrat} [hst : st.WF] : sys.validTr s (st.f s)

theorem AP.AStrat.validTr {s : State} [hs : AState s] {st : AStrat} [hst : st.WF] (h : sys.hasTr s) : sys.validTr s (st.f s)

@[simp]

theorem AP.DStrat.validTr (s : State) [hs : DState s] {st : DStrat} [hst : st.WF] : sys.validTr s (st.f s)

theorem AP.Strat.WF.validTr {s : State} [hs : sys.WF s] {st : Strat} [hst : st.WF] (h : sys.hasTr s) : sys.validTr s (st.f s)

theorem AP.State.validTr_chooseAMove {s : State} (ht : s.aTurn = true) (h : sys.hasTr s) : sys.validTr s s.chooseAMove

@[simp]

theorem AP.AState.validTr_chooseAMove {s : State} [hs : AState s] (h : sys.hasTr s) : sys.validTr s s.chooseAMove

@[simp]

theorem AP.State.validTr_chooseMove {s : State} (h : sys.hasTr s) : sys.validTr s s.chooseMove

@[simp]

theorem AP.AState.chooseMove_eq {s : State} [hs : AState s] : s.chooseMove = s.chooseAMove

@[simp]

theorem AP.DState.chooseMove_eq {s : State} [hs : DState s] : s.chooseMove = s.chooseDMove

@[instance_reducible]

instance AP.instInhabitedAStrat : Inhabited AStrat

Equations

• AP.instInhabitedAStrat = { default := { f := AP.State.chooseAMove } }

@[instance_reducible]

instance AP.instInhabitedDStrat : Inhabited DStrat

Equations

• AP.instInhabitedDStrat = { default := { f := AP.State.chooseDMove } }

@[instance_reducible]

instance AP.instInhabitedStrat : Inhabited Strat

Equations

• AP.instInhabitedStrat = { default := { a := default, d := default } }

@[simp]

theorem AP.AStrat.default_def : default = { f := State.chooseAMove }

@[simp]

theorem AP.DStrat.default_def : default = { f := State.chooseDMove }

@[simp]

theorem AP.Strat.default_def : default = { a := { f := State.chooseAMove }, d := { f := State.chooseDMove } }

instance AP.instWFMk'ChooseAMove : { f := State.chooseAMove }.WF

instance AP.instWFMk'ChooseDMove : { f := State.chooseDMove }.WF

instance AP.instWFDefaultAStrat : default.WF

instance AP.instWFDefaultDStrat : default.WF

instance AP.instWFDefaultStrat : default.WF

theorem AP.pw_eq_of_tr {s s' : State} {p : PointZ} (h : sys.tr s p = some s') : s'.pw = s.pw

@[simp]

theorem AP.pw_initState {pw : ℕ} {p : PointZ} : (initState pw p).pw = pw

theorem AP.hist_eq_of_tr {s s' : State} {p : PointZ} (h : sys.tr s p = some s') : s'.hist = p :: s.hist

theorem AP.length_hist_eq_of_tr {s s₁ : State} {p : PointZ} (h : sys.tr s p = some s₁) : s₁.hist.length = s.hist.length + 1

theorem AP.hist_suffix_of_reachable {s₁ s₂ : State} (h : sys.Reachable s₁ s₂) : s₁.hist <:+ s₂.hist

theorem AP.not_reachable_of_not_hist_suffix {s₁ s₂ : State} (h : ¬s₁.hist <:+ s₂.hist) : ¬sys.Reachable s₁ s₂

theorem AP.length_hist_le_of_reachable {s₁ s₂ : State} (h : sys.Reachable s₁ s₂) : s₁.hist.length ≤ s₂.hist.length

theorem AP.hist_suffix_of_tr {s₁ s₂ : State} {p : PointZ} (h : sys.tr s₁ p = some s₂) : s₁.hist <:+ s₂.hist

theorem AP.length_hist_le_of_tr {s₁ s₂ : State} {p : PointZ} (h : sys.tr s₁ p = some s₂) : s₁.hist.length ≤ s₂.hist.length

@[simp]

theorem AP.hist_initState {pw : ℕ} {p : PointZ} : (initState pw p).hist = [p]

@[simp]

theorem AP.State.hist_ne_nil {s : State} [hs : sys.WF s] : s.hist ≠ []

@[simp]

theorem AP.Option.getD_eq_iget_iff {α : Type u_1} [ha : Inhabited α] {m : Option α} {x : α} : m.getD x = m.getd ↔ m.isSome = true ∨ x = default

theorem AP.State.aPos₀_eq_of_tr {s s' : State} {t : PointZ} [hs : sys.WF s] (h : sys.tr s t = some s') : s'.aPos₀ = s.aPos₀

theorem AP.State.aPos₀_eq_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') : s'.aPos₀ = s.aPos₀

@[simp]

theorem AP.initial_iff {s : State} : sys.Initial s ↔ initState s.pw s.aPos₀ = s

@[simp]

theorem AP.pw_trs {s : State} {ps : List PointZ} [hs : sys.WF s] : (sys.trs s ps).1.pw = s.pw

theorem AP.pw_eq_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') : s'.pw = s.pw

@[simp]

theorem AP.aPos₀_initState {pw : ℕ} {p : PointZ} : (initState pw p).aPos₀ = p

@[simp]

theorem AP.aPos_initState {pw : ℕ} {p : PointZ} : (initState pw p).aPos = p

@[simp]

theorem AP.taken_initState {pw : ℕ} {p : PointZ} : (initState pw p).taken = ∅

theorem AP.State.wf_iff' {s : State} : sys.WF s ↔ ∃ (ps : List PointZ), sys.trs (initState s.pw s.aPos₀) ps = (s, [])

@[simp]

instance AP.instInitialStatePointZSysInitState {pw : ℕ} {p : PointZ} : sys.Initial (initState pw p)

@[simp]

theorem AP.setPw_initState {p : PointZ} {pw₁ pw₂ : ℕ} : (initState pw₁ p).setPw pw₂ = initState pw₂ p

theorem AP.State.tr_setPw_eq_some_of {s s' : State} {pw : ℕ} {p : PointZ} [hs : sys.WF s] (h₁ : s.pw ≤ pw) (h₂ : sys.tr s p = some s') : sys.tr (s.setPw pw) p = some (s'.setPw pw)

theorem AP.State.trs_setPw_eq_of {s s' : State} {pw : ℕ} {ps : List PointZ} [hs : sys.WF s] (h₁ : s.pw ≤ pw) (h₂ : sys.trs s ps = (s', [])) : sys.trs (s.setPw pw) ps = (s'.setPw pw, [])

theorem AP.State.wf_setPw_of_le {s : State} {pw : ℕ} [hs : sys.WF s] (h : s.pw ≤ pw) : sys.WF (s.setPw pw)

theorem AP.DState.tr_setPw_eq {s : State} {p : PointZ} {pw : ℕ} [hs : DState s] : sys.tr (s.setPw pw) p = Option.map (fun (x : State) => x.setPw pw) (sys.tr s p)

@[simp]

theorem AP.hist_trs {s : State} {ps : List PointZ} [hs : sys.WF s] : (sys.trs s ps).1.hist = (List.take (ps.length - (sys.trs s ps).2.length) ps).reverse ++ s.hist

@[simp]

theorem AP.length_hist_eq_one_iff {s : State} [hs : sys.WF s] : s.hist.length = 1 ↔ initState s.pw s.aPos₀ = s

theorem AP.exi_prev_of_hist_eq_cons {s : State} {p : PointZ} {ps : List PointZ} [hs : sys.WF s] (h₁ : ps ≠ []) (h₂ : s.hist = p :: ps) : ∃ (s₀ : State), sys.WF s₀ ∧ sys.tr s₀ p = some s

@[simp]

theorem AP.aTurn_initState {pw : ℕ} {p : PointZ} : (initState pw p).aTurn = false

@[simp]

theorem AP.initState_eq_initState_iff {pw₁ : ℕ} {p₁ : PointZ} {pw₂ : ℕ} {p₂ : PointZ} : initState pw₁ p₁ = initState pw₂ p₂ ↔ pw₁ = pw₂ ∧ p₁ = p₂

@[simp]

theorem AP.hist_eq_singleton_iff {s : State} [hs : sys.WF s] {p : PointZ} : s.hist = [p] ↔ initState s.pw p = s ∧ s.aPos₀ = p

@[simp]

theorem AP.State.trs_reverse_hist_eq {s : State} [hs : sys.WF s] : sys.trs (initState s.pw s.aPos₀) s.hist.reverse.tail = (s, [])

theorem AP.State.eq_trs_reverse_hist {s : State} [hs : sys.WF s] : s = (sys.trs (initState s.pw s.aPos₀) s.hist.reverse.tail).1

theorem AP.State.wf_iff_decideWF {s : State} : sys.WF s ↔ s.decideWF = true

@[instance_reducible]

instance AP.instDecidableWFStatePointZSys {s : State} : Decidable (sys.WF s)

Equations

• AP.instDecidableWFStatePointZSys = match h : s.decideWF with | true => isTrue ⋯ | false => isFalse ⋯

@[simp]

theorem AP.State.decideWF_eq {s : State} : s.decideWF = decide (sys.WF s)

theorem AP.State.aState_iff_decideAState {s : State} : AState s ↔ s.decideAState = true

theorem AP.State.dState_iff_decideDState {s : State} : DState s ↔ s.decideDState = true

@[instance_reducible]

instance AP.instDecidableAState {s : State} : Decidable (AState s)

Equations

• AP.instDecidableAState = match h : s.decideAState with | true => isTrue ⋯ | false => isFalse ⋯

@[instance_reducible]

instance AP.instDecidableDState {s : State} : Decidable (DState s)

Equations

• AP.instDecidableDState = match h : s.decideDState with | true => isTrue ⋯ | false => isFalse ⋯

@[simp]

theorem AP.State.decideAState_eq {s : State} : s.decideAState = decide (AState s)

@[simp]

theorem AP.State.decideDState_eq {s : State} : s.decideDState = decide (DState s)

@[simp]

theorem AP.State.not_aState {s : State} [hs : sys.WF s] : ¬AState s ↔ DState s

@[simp]

theorem AP.State.not_dState {s : State} [hs : sys.WF s] : ¬DState s ↔ AState s

theorem AP.AState.validTr_of_aWins {s : State} {st : Strat} [hs : AState s] (h : s.aWins st) : sys.validTr s (st.a.f s)

theorem AP.AState.hasTr_of_aWins {s : State} {st : Strat} [hs : AState s] (h : s.aWins st) : sys.hasTr s

theorem AP.setPw_eq_comm {s₁ s₂ : State} : s₁.setPw s₂.pw = s₂ ↔ s₂.setPw s₁.pw = s₁

theorem AP.setHist_eq_comm {s₁ s₂ : State} : s₁.setHist s₂.hist = s₂ ↔ s₂.setHist s₁.hist = s₁

@[simp]

theorem AP.setHist_eq_setHist_iff {s : State} {hist₁ hist₂ : List PointZ} : s.setHist hist₁ = s.setHist hist₂ ↔ hist₁ = hist₂

@[simp]

theorem AP.State.aMove_setHist {s : State} {hist : List PointZ} {p : PointZ} : (s.setHist hist).aMove p = Option.map (fun (x : State) => x.setHist hist) (s.aMove p)

@[simp]

theorem AP.State.dMove_setHist {s : State} {hist : List PointZ} {p : PointZ} : (s.setHist hist).dMove p = Option.map (fun (x : State) => x.setHist hist) (s.dMove p)

@[simp]

theorem AP.State.move_setHist {s : State} {hist : List PointZ} {p : PointZ} : (s.setHist hist).move p = Option.map (fun (x : State) => x.setHist (p :: hist)) (s.move p)

@[simp]

theorem AP.State.tr_setHist {s : State} {hist : List PointZ} {p : PointZ} : sys.tr (s.setHist hist) p = Option.map (fun (x : State) => x.setHist (p :: hist)) (sys.tr s p)

@[simp]

theorem AP.State.validTr_setHist {s : State} {hist : List PointZ} : sys.validTr (s.setHist hist) = sys.validTr s

@[simp]

theorem AP.State.hasTr_setHist {s : State} {hist : List PointZ} : sys.hasTr (s.setHist hist) ↔ sys.hasTr s

@[simp]

theorem AP.State.chooseAMove_setHist {s : State} {hist : List PointZ} : (s.setHist hist).chooseAMove = s.chooseAMove

@[simp]

theorem AP.State.chooseDMove_setHist {s : State} {hist : List PointZ} : (s.setHist hist).chooseDMove = s.chooseDMove

theorem AP.State.setHist_eq_self_of {s : State} {hist : List PointZ} (h : s.hist = hist) : s.setHist hist = s

theorem AP.State.aTurn_eq_of_tr {s s' : State} {p : PointZ} (h : sys.tr s p = some s') : s'.aTurn = !s.aTurn

theorem AP.State.aTurn_eq_of_tr' {s s' : State} {p : PointZ} (h : sys.tr s p = some s') : s.aTurn = !s'.aTurn

theorem AP.AState.exi_prev {sa : State} [ha : AState sa] : ∃ (sd : State) (p : PointZ), DState sd ∧ sys.tr sd p = some sa

theorem AP.AState.taken_eq_of_tr {s s' : State} {p : PointZ} [hs : AState s] (h : sys.tr s p = some s') : s'.taken = s.taken

theorem AP.DState.taken_eq_of_tr {s s' : State} {p : PointZ} [hs : DState s] (h : sys.tr s p = some s') : s'.taken = s.taken.insert p

theorem AP.State.size_taken_eq_ite_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s') : s'.taken.size = s.taken.size + if s.aTurn = true then 0 else 1

theorem AP.State.length_hist_eq_size_taken_mul_two_add_ite {s : State} [hs : sys.WF s] : s.hist.length = s.taken.size * 2 + if s.aTurn = true then 0 else 1

theorem AP.State.length_hist_le_size_taken_mul_two_add_one {s : State} [hs : sys.WF s] : s.hist.length ≤ s.taken.size * 2 + 1

theorem AP.State.size_taken_mul_two_le_length_hist {s : State} [hs : sys.WF s] : s.taken.size * 2 ≤ s.hist.length

theorem AP.State.length_hist_le_two_of_pw_eq_zero {s : State} [hs : sys.WF s] (h : s.pw = 0) : s.hist.length ≤ 2

theorem AP.State.size_taken_le_one_of_pw_eq_zero {s : State} [hs : sys.WF s] (h : s.pw = 0) : s.taken.size ≤ 1

@[simp]

theorem AP.State.length_hist_le_one_iff {s : State} [hs : sys.WF s] : s.hist.length ≤ 1 ↔ s.hist.length = 1

@[simp]

theorem AP.State.not_aState_initState {pw : ℕ} {p : PointZ} : ¬AState (initState pw p)

@[simp]

theorem AP.AState.taken_ne_empty {s : State} [hs : AState s] : s.taken ≠ ∅

theorem AP.DState.exi_prev_of_mem_taken {s : State} {p₀ : PointZ} [hs : DState s] (h : p₀ ∈ s.taken) : ∃ (sa : State) (p : PointZ), AState sa ∧ sys.tr sa p = some s

theorem AP.DState.exi_prev_of_taken_ne_empty {s : State} [hs : DState s] (h : s.taken ≠ ∅) : ∃ (sa : State) (p : PointZ), AState sa ∧ sys.tr sa p = some s

theorem AP.State.aTurn_eq_of_simulate_eq {st : Strat} {s s₁ : State} {n r : ℕ} [hs : sys.WF s] (h : sys.simulate st.f s n = (s₁, r)) : s₁.aTurn = (s.aTurn == decide (Even (n - r)))

theorem AP.State.aTurn_eq_of_simulate_full_eq {st : Strat} {s s₁ : State} {n : ℕ} [hs : sys.WF s] (h : sys.simulate st.f s n = (s₁, 0)) : s₁.aTurn = (s.aTurn == decide (Even n))

theorem AP.State.simulate_congr_rel_full' {st st' : Strat} {r : State → State → Prop} {s s' s₁ : State} {n : ℕ} [hst : st.WF] [hst' : st'.WF] [hs : sys.WF s] [hs' : sys.WF s'] (h₁ : sys.simulate st.f s n = (s₁, 0)) (ht : s.aTurn = s'.aTurn) (h₂ : r s s') (h₃ : ∀ (sa sa' sd : State) [AState sa] [AState sa'] [DState sd], sys.tr sa (st.a.f sa) = some sd → r sa sa' → ∃ (sd' : State), sys.tr sa' (st'.a.f sa') = some sd' ∧ r sd sd') (h₄ : ∀ (sd sd' sa : State) [DState sd] [DState sd'] [AState sa], sys.tr sd (st.d.f sd) = some sa → r sd sd' → ∃ (sa' : State), sys.tr sd' (st'.d.f sd') = some sa' ∧ r sa sa') : ∃ (s₁' : State), sys.simulate st'.f s' n = (s₁', 0) ∧ r s₁ s₁'

theorem AP.State.simulate_congr_rel_full {st st' : Strat} {r : State → State → Prop} {s s' : State} {n : ℕ} [hst : st.WF] [hst' : st'.WF] [hs : sys.WF s] [hs' : sys.WF s'] (h₁ : (sys.simulate st.f s n).2 = 0) (ht : s.aTurn = s'.aTurn) (h₂ : r s s') (h₃ : ∀ (sa sa' sd : State) [AState sa] [AState sa'] [DState sd], sys.tr sa (st.a.f sa) = some sd → r sa sa' → ∃ (sd' : State), sys.tr sa' (st'.a.f sa') = some sd' ∧ r sd sd') (h₄ : ∀ (sd sd' sa : State) [DState sd] [DState sd'] [AState sa], sys.tr sd (st.d.f sd) = some sa → r sd sd' → ∃ (sa' : State), sys.tr sd' (st'.d.f sd') = some sa' ∧ r sa sa') : (sys.simulate st'.f s' n).2 = 0

theorem AP.AState.validTr_setPw_of_le {s : State} {pw : ℕ} {p : PointZ} [hs : sys.WF s] (h₁ : s.pw ≤ pw) (h₂ : sys.validTr s p) : sys.validTr (s.setPw pw) p

theorem AP.State.setPw_eq_self_of {s : State} {pw : ℕ} (h : s.pw = pw) : s.setPw pw = s

theorem AP.AState.setPw_of_le {s : State} {pw : ℕ} [hs : AState s] (h : s.pw ≤ pw) : AState (s.setPw pw)

theorem AP.DState.setPw_of_le {s : State} {pw : ℕ} [hs : DState s] (h : s.pw ≤ pw) : DState (s.setPw pw)

instance AP.instDStateInitState {pw : ℕ} {p : PointZ} : DState (initState pw p)

instance AP.instDStateSetPwInitState {pw pw' : ℕ} {p : PointZ} : DState ((initState pw p).setPw pw')

instance AP.instSimFnStatePointZSysMkStratFn {f : State → Option PointZ} : sys.SimFn (mkStratFn f)

instance AP.instWFMk {f : State → Option PointZ} : (AStrat.mk f).WF

instance AP.instWFMk_1 {f : State → Option PointZ} : (DStrat.mk f).WF

@[simp]

theorem AP.AStrat.f_mk {f : State → PointZ} : { f := f }.f = f

@[simp]

theorem AP.DStrat.f_mk {f : State → PointZ} : { f := f }.f = f

theorem AP.State.exi_tr_reachable_of_mem_dropLast_hist {s : State} {p : PointZ} [hs : sys.WF s] (h : p ∈ s.hist.dropLast) : ∃ (s₀ : State), sys.WF s₀ ∧ sys.validTr s₀ p ∧ sys.Reachable s₀ s

@[simp]

instance AP.instDStateOfInitialStatePointZSys {s : State} [hs : sys.Initial s] : DState s

theorem AP.wfTrans {p : PointZ} : sys.WFTrans p

@[simp]

instance AP.instWFTransStatePointZSys {p : PointZ} : sys.WFTrans p

theorem AP.State.hist_eq_snoc {s : State} [hs : sys.WF s] : s.hist = s.hist.dropLast ++ [s.aPos₀]

theorem AP.State.exi_hist_eq_snoc {s : State} [hs : sys.WF s] : ∃ (ps : List PointZ), s.hist = ps ++ [s.aPos₀]

instance AP.instWFStatePointZSysSetHist {s : State} {hist₁ hist₂ : List PointZ} [hs : sys.WF (s.setHist hist₂)] : sys.WF ((s.setHist hist₁).setHist hist₂)

instance AP.instWFStatePointZSysSetHistHist {s : State} [hs : sys.WF s] : sys.WF (s.setHist s.hist)

theorem AP.AState.aPos_eq_of_tr {s s' : State} {p : PointZ} [hs : AState s] (h : sys.tr s p = some s') : s'.aPos = p

theorem AP.DState.aPos_eq_of_tr {s s' : State} {p : PointZ} [hs : DState s] (h : sys.tr s p = some s') : s'.aPos = s.aPos

@[simp]

theorem AP.State.aPos_ne_chooseDMove {s : State} [hs : DState s] : s.aPos ≠ s.chooseDMove

@[simp]

theorem AP.State.chooseDMove_not_mem_taken {s : State} [hs : DState s] : s.chooseDMove ∉ s.taken

theorem AP.hist_eq_of_trs {s s₁ : State} {ps r : List PointZ} (h : sys.trs s ps = (s₁, r)) : s₁.hist = (List.take (ps.length - r.length) ps).reverse ++ s.hist

theorem AP.State.taken_subset_of_tr {s s' : State} {p : PointZ} [hs : sys.WF s] (h : sys.tr s p = some s') : s.taken ⊆ s'.taken

theorem AP.State.taken_subset_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') : s.taken ⊆ s'.taken

theorem AP.State.mem_taken_of_tr {s s' : State} {p p' : PointZ} [hs : sys.WF s] (h₁ : sys.tr s p = some s') (h₂ : p' ∈ s.taken) : p' ∈ s'.taken

theorem AP.State.mem_taken_of_reachable {s s' : State} {p : PointZ} [hs : sys.WF s] (h₁ : sys.Reachable s s') (h₂ : p ∈ s.taken) : p ∈ s'.taken

@[simp]

theorem AP.State.aPos_not_mem_taken {s : State} [hs : sys.WF s] : s.aPos ∉ s.taken

theorem AP.State.isSome_aMove_iff {s : State} {p : PointZ} : (s.aMove p).isSome = true ↔ s.aPos ≠ p ∧ p ∉ s.taken ∧ Point.dist p s.aPos ≤ ↑s.pw

theorem AP.DState.exi_aMove_of_taken_ne_empty {s : State} [hs : DState s] (h : s.taken ≠ ∅) : ∃ (p : PointZ), (s.aMove p).isSome = true

theorem AP.AState.size_taken_eq_one_of_pw_eq_zero {s : State} [hs : AState s] (h : s.pw = 0) : s.taken.size = 1

@[simp]

theorem AP.State.aPos₀_setHist {s : State} {hist : List PointZ} : (s.setHist hist).aPos₀ = hist.getLast?.getd

theorem AP.State.length_hist_eq_of_trs_eq {s s' : State} {ps r : List PointZ} (h : sys.trs s ps = (s', r)) : s'.hist.length = s.hist.length + ps.length - r.length

theorem AP.State.length_hist_eq_of_simulate_eq {s s' : State} {f : State → PointZ} {n r : ℕ} (h : sys.simulate f s n = (s', r)) : s'.hist.length = s.hist.length + n - r