Documentation

Projects.AP.Alts.Alt1.Equiv

@[simp]

theorem AP.Alt₁.Point.x_toAlt {p : Point} :

p.toAlt.x = p.x

@[simp]

theorem AP.Alt₁.Point.y_toAlt {p : Point} :

p.toAlt.y = p.y

@[simp]

theorem AP.Alt₁.Point.toAlt_mk {x y : ℤ} :

{ x := x, y := y }.toAlt = { x := x, y := y }

@[simp]

theorem AP.Alt₁.Point.x_ofAlt {p : PointZ} :

(ofAlt p).x = p.x

@[simp]

theorem AP.Alt₁.Point.y_ofAlt {p : PointZ} :

(ofAlt p).y = p.y

@[simp]

theorem AP.Alt₁.Point.ofAlt_mk {x y : ℤ} :

ofAlt { x := x, y := y } = { x := x, y := y }

@[simp]

theorem AP.Alt₁.ofAlt_dist {p₁ p₂ : PointZ} :

dist (Point.ofAlt p₁) (Point.ofAlt p₂) = (Point.dist p₁ p₂).toNat

theorem AP.Alt₁.dist_eq_alt {p₁ p₂ : Point} :

dist p₁ p₂ = (Point.dist p₁.toAlt p₂.toAlt).toNat

@[simp]

theorem AP.Alt₁.Game.act_iff {pw : ℕ} {g : Game pw} :

g.act ↔ g.s.act

@[simp]

theorem AP.Alt₁.Board.pw_toAlt {b : Board} {pw : ℕ} {aTurn : Bool} {hist : List PointZ} :

(b.toAlt pw aTurn hist).pw = pw

@[simp]

theorem AP.Alt₁.Board.taken_toAlt {b : Board} {pw : ℕ} {aTurn : Bool} {hist : List PointZ} :

(b.toAlt pw aTurn hist).taken = Set'.ofSet ((fun (x : Point) => x.toAlt) '' (Set.univ \ b.squares))

@[simp]

theorem AP.Alt₁.Board.aPos_toAlt {b : Board} {pw : ℕ} {aTurn : Bool} {hist : List PointZ} :

(b.toAlt pw aTurn hist).aPos = b.A.toAlt

@[simp]

theorem AP.Alt₁.Board.aTurn_toAlt {b : Board} {pw : ℕ} {aTurn : Bool} {hist : List PointZ} :

(b.toAlt pw aTurn hist).aTurn = aTurn

@[simp]

theorem AP.Alt₁.Board.hist_toAlt {b : Board} {pw : ℕ} {aTurn : Bool} {hist : List PointZ} :

(b.toAlt pw aTurn hist).hist = hist

@[simp]

theorem AP.Alt₁.State.pw_toAlt {s : State} {pw : ℕ} {hist : List PointZ} :

(s.toAlt pw hist).pw = pw

@[simp]

theorem AP.Alt₁.State.taken_toAlt {s : State} {pw : ℕ} {hist : List PointZ} :

(s.toAlt pw hist).taken = Set'.ofSet ((fun (x : Point) => x.toAlt) '' (Set.univ \ s.board.squares))

@[simp]

theorem AP.Alt₁.State.aPos_toAlt {s : State} {pw : ℕ} {hist : List PointZ} :

(s.toAlt pw hist).aPos = s.board.A.toAlt

@[simp]

theorem AP.Alt₁.State.aTurn_toAlt {s : State} {pw : ℕ} {hist : List PointZ} :

(s.toAlt pw hist).aTurn = s.aTurn

@[simp]

theorem AP.Alt₁.State.hist_toAlt {s : State} {pw : ℕ} {hist : List PointZ} :

(s.toAlt pw hist).hist = hist

@[simp]

theorem AP.Alt₁.State.board_ofAlt {s : AP.State} {act : Prop} {hist : List Board} :

(ofAlt s act hist).board = Board.ofAlt s

@[simp]

theorem AP.Alt₁.State.history_ofAlt {s : AP.State} {act : Prop} {hist : List Board} :

(ofAlt s act hist).history = hist

@[simp]

theorem AP.Alt₁.State.act_ofAlt {s : AP.State} {act : Prop} {hist : List Board} :

(ofAlt s act hist).act ↔ act

@[simp]

theorem AP.Alt₁.State.aTurn_mk {b : Board} {hist : List Board} {act : Prop} :

{ board := b, history := hist, act := act }.aTurn = decide (Odd hist.length)

@[simp]

theorem AP.Alt₁.toAlt_state₀ {pw : ℕ} {hist : List PointZ} :

state₀.toAlt pw hist = (AP.initState pw 0).setHist hist

@[simp]

theorem AP.Alt₁.Point.toAlt_ofAlt {p : PointZ} :

(ofAlt p).toAlt = p

@[simp]

theorem AP.Alt₁.Point.ofAlt_toAlt {p : Point} :

ofAlt p.toAlt = p

@[simp]

theorem AP.Alt₁.Board.squares_ofAlt {s : AP.State} :

(ofAlt s).squares = Set.univ \ Point.ofAlt '' s.taken.toSet

@[simp]

theorem AP.Alt₁.Board.a_ofAlt {s : AP.State} :

(ofAlt s).A = Point.ofAlt s.aPos

@[simp]

theorem AP.Alt₁.Board.ofAlt_init {s : AP.State} :

ofAlt s.init = { squares := Set.univ, A := Point.ofAlt s.aPos₀ }

theorem AP.Alt₁.State.toAlt_ofAlt {s : AP.State} {act : Prop} {pw : ℕ} {hist₁ : List Board} {hist₂ : List PointZ} (h : Odd hist₁.length ↔ s.aTurn = true) :

(ofAlt s act hist₁).toAlt pw hist₂ = (s.setPw pw).setHist hist₂

@[simp]

theorem AP.Alt₁.State.board_setHist {s : State} {hist : List Board} :

(s.setHist hist).board = s.board

@[simp]

theorem AP.Alt₁.State.history_setHist {s : State} {hist : List Board} :

(s.setHist hist).history = hist

@[simp]

theorem AP.Alt₁.State.act_setHist {s : State} {hist : List Board} :

(s.setHist hist).act = s.act

theorem AP.Alt₁.Board.ofAlt_toAlt {s : State} {pw : ℕ} {hist : List PointZ} (h₁ : s.FinSq) :

ofAlt (s.toAlt pw hist) = s.board

theorem AP.Alt₁.State.ofAlt_toAlt {s : State} {pw : ℕ} {hist₁ : List PointZ} {hist₂ : List Board} (h₁ : s.FinSq) :

ofAlt (s.toAlt pw hist₁) s.act hist₂ = s.setHist hist₂

@[simp]

theorem AP.Alt₁.Game.not_aWinsAt_iff {pw : ℕ} {g : Game pw} :

¬g.AWins ↔ g.DWins

@[simp]

theorem AP.Alt₁.Game.not_dWinsAt_iff {pw : ℕ} {g : Game pw} :

¬g.DWins ↔ g.AWins

@[simp]

theorem AP.Alt₁.dMoveValid_none {b : Board} :

DMoveValid b none

@[simp]

instance AP.Alt₁.A.nonempty {pw : ℕ} :

Nonempty (A pw)

@[simp]

instance AP.Alt₁.D.nonempty :

@[instance_reducible]

noncomputable instance AP.Alt₁.instInhabitedA {pw : ℕ} :

Inhabited (A pw)

Equations

AP.Alt₁.instInhabitedA = inferInstance

@[instance_reducible]

noncomputable instance AP.Alt₁.instInhabitedD :

Equations

AP.Alt₁.instInhabitedD = inferInstance

@[simp]

theorem AP.Alt₁.board_state₀ :

state₀.board = board₀

@[simp]

theorem AP.Alt₁.squares_board₀ :

board₀.squares = Set.univ

@[simp]

theorem AP.Alt₁.a_board₀ :

board₀.A = { x := 0, y := 0 }

@[simp]

theorem AP.Alt₁.aTurn_state₀ :

state₀.aTurn = false

@[simp]

theorem AP.Alt₁.toAlt_board₀_not_aTurn {pw : ℕ} {hist : List PointZ} :

board₀.toAlt pw false hist = (AP.initState pw 0).setHist hist

@[instance_reducible]

instance AP.Alt₁.instInhabitedBoard :

Inhabited Board

Equations

AP.Alt₁.instInhabitedBoard = { default := AP.Alt₁.board₀ }

@[instance_reducible]

instance AP.Alt₁.instInhabitedState :

Inhabited State

Equations

AP.Alt₁.instInhabitedState = { default := AP.Alt₁.state₀ }

@[simp]

theorem AP.Alt₁.toAltH_state₀ {pw : ℕ} :

state₀.toAltH pw = AP.initState pw 0

@[simp]

theorem AP.Alt₁.toAltH_board₀ {pw : ℕ} :

board₀.toAltH pw false = AP.initState pw 0

@[simp]

instance AP.Alt₁.initial_toAltH_state₀ {pw : ℕ} :

sys.Initial (state₀.toAltH pw)

@[simp]

theorem AP.Alt₁.aHws_toAltH_state₀ {pw : ℕ} :

(state₀.toAltH pw).aHws ↔ aHwsPw pw

@[simp]

theorem AP.Alt₁.dHws_toAltH_state₀ {pw : ℕ} :

(state₀.toAltH pw).dHws ↔ dHwsPw pw

@[simp]

theorem AP.Alt₁.Game.play_zero {pw : ℕ} {g : Game pw} :

g.play 0 = g

@[simp]

theorem AP.Alt₁.Game.s_initGame {pw : ℕ} {a : A pw} {d : D} {s : State} :

(initGame a d s).s = s

@[simp]

theorem AP.Alt₁.Game.act_initGame {pw : ℕ} {a : A pw} {d : D} {s : State} :

(initGame a d s).s.act = s.act

@[simp]

theorem AP.Alt₁.act_state₀ :

theorem AP.Alt₁.State.dwn_eq {pw : ℕ} {s : State} :

s.dwn pw = (s.toAltH pw).dwn

@[simp]

theorem AP.Alt₁.Game.play_succ {pw : ℕ} {g : Game pw} {n : ℕ} :

g.play (n + 1) = (g.play n).playMove

theorem AP.Alt₁.Game.play_succ' {pw : ℕ} {g : Game pw} {n : ℕ} :

g.play (n + 1) = g.playMove.play n

@[simp]

theorem AP.Alt₁.Game.state_setState {pw : ℕ} {g : Game pw} {s : State} :

(g.setState s).s = s

@[simp]

theorem AP.Alt₁.Game.act_setState {pw : ℕ} {g : Game pw} {s : State} :

(g.setState s).s.act ↔ s.act

@[simp]

theorem AP.Alt₁.Game.act_applyDMove {s : State} {m : DMove} :

(applyDMove s m).act ↔ s.act

@[simp]

theorem AP.Alt₁.Game.act_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} :

(playDMoveAt g h).s.act

theorem AP.Alt₁.Game.playMove_eq {pw : ℕ} {g : Game pw} :

g.playMove = if hs : g.s.act then playAMoveAt (playDMoveAt g hs) else g

theorem AP.Alt₁.Game.playMove_eq_of_not_act {pw : ℕ} {g : Game pw} (h : ¬g.s.act) :

theorem AP.Alt₁.Game.play_eq_of_not_act {pw : ℕ} {g : Game pw} {n : ℕ} (h : ¬g.s.act) :

g.play n = g

@[simp]

theorem AP.Alt₁.State.act_finish {s : State} :

@[simp]

theorem AP.Alt₁.Game.act_finish {pw : ℕ} {g : Game pw} :

¬g.finish.s.act

@[simp]

theorem AP.Alt₁.Game.playMove_finish {pw : ℕ} {g : Game pw} :

g.finish.playMove = g.finish

@[simp]

theorem AP.Alt₁.Game.play_finish {pw : ℕ} {g : Game pw} {n : ℕ} :

g.finish.play n = g.finish

@[simp]

theorem AP.Alt₁.a_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} :

(playDMoveAt g h).a = g.a

@[simp]

theorem AP.Alt₁.a_initGame {pw : ℕ} {a : A pw} {d : D} {s : State} :

(initGame a d s).a = a

@[simp]

theorem AP.Alt₁.d_initGame {pw : ℕ} {a : A pw} {d : D} {s : State} :

(initGame a d s).d = d

@[simp]

theorem AP.Alt₁.State.aTurn_applyMove {s : State} {m : Board} :

(applyMove s m).aTurn = !s.aTurn

@[simp]

theorem AP.Alt₁.State.aTurn_applyDMove {s : State} {m : DMove} :

(applyDMove s m).aTurn = !s.aTurn

@[simp]

theorem AP.Alt₁.aTurn_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} :

(playDMoveAt g h).s.aTurn = !g.s.aTurn

@[simp]

theorem AP.Alt₁.applyDMoveB_none {b : Board} :

applyDMoveB b none = b

@[simp]

theorem AP.Alt₁.State.board_applyMove {s : State} {b : Board} :

(applyMove s b).board = b

@[simp]

theorem AP.Alt₁.State.history_applyMove {s : State} {b : Board} :

(applyMove s b).history = s.history ++ [s.board]

@[simp]

theorem AP.Alt₁.State.act_applyMove {s : State} {b : Board} :

(applyMove s b).act ↔ s.act

@[simp]

theorem AP.Alt₁.applyDMove_none {s : State} :

applyDMove s none = s.setHist (s.history ++ [s.board])

@[simp]

theorem AP.Alt₁.State.aTurn_setHist {s : State} {hist : List Board} :

(s.setHist hist).aTurn = decide (Odd hist.length)

theorem AP.Alt₁.State.toAltH_setHist {pw : ℕ} {s : State} {hist : List Board} (ht : s.aTurn = decide (Odd hist.length)) :

(s.setHist hist).toAltH pw = s.toAltH pw

theorem AP.Alt₁.State.wf_iff {pw : ℕ} {s : State} :

WF pw s ↔ ∃ (a : A pw) (d : D) (n : ℕ) (g : Game pw), (initGame a d state₀).play n = g ∧ (g.s = s ∨ ∃ (h : g.s.act), (playDMoveAt g h).s = s)

@[simp]

theorem AP.Alt₁.Game.setState_initGame {pw : ℕ} {a : A pw} {d : D} {s s' : State} :

(initGame a d s).setState s' = initGame a d s'

@[simp]

theorem AP.Alt₁.Game.s_finish {pw : ℕ} {g : Game pw} :

g.finish.s = g.s.finish

@[simp]

theorem AP.Alt₁.State.aTurn_finish {s : State} :

s.finish.aTurn = s.aTurn

@[simp]

theorem AP.Alt₁.State.act_applyAMove {s : State} {b : AMove} :

(applyAMove s b).act ↔ s.act

@[simp]

theorem AP.Alt₁.State.aTurn_applyAMove {s : State} {b : AMove} :

(applyAMove s b).aTurn = !s.aTurn

theorem AP.Alt₁.Game.act_play_initGame_of_not_aTurn {pw : ℕ} {a : A pw} {d : D} {n : ℕ} {g : Game pw} {s : State} (h₁ : s.aTurn = false) (h₂ : s.act) (h₃ : (initGame a d s).play n = g) (h₄ : g.s.aTurn = false) :

@[simp]

theorem AP.Alt₁.Game.s_playAMoveAt'_eq_iff {pw : ℕ} {g₁ g₂ : Game pw} {h₁ : g₁.s.act} {h₂ : AHasValidMove pw g₁.s.board} {h₃ : g₂.s.act} {h₄ : AHasValidMove pw g₂.s.board} :

(playAMoveAt' g₁.a g₁ h₁ h₂).s = (playAMoveAt' g₂.a g₂ h₃ h₄).s ↔ applyAMove g₁.s (g₁.a.f g₁.s h₁ h₂).m = applyAMove g₂.s (g₂.a.f g₂.s h₃ h₄).m

@[simp]

theorem AP.Alt₁.Game.s_playDMoveAt_eq_iff {pw : ℕ} {g₁ g₂ : Game pw} {h₁ : g₁.s.act} {h₂ : g₂.s.act} :

(playDMoveAt g₁ h₁).s = (playDMoveAt g₂ h₂).s ↔ applyDMove g₁.s (g₁.d.f g₁.s h₁).m = applyDMove g₂.s (g₂.d.f g₂.s h₂).m

@[simp]

theorem AP.Alt₁.Game.a_finish {pw : ℕ} {g : Game pw} :

g.finish.a = g.a

@[simp]

theorem AP.Alt₁.Game.d_finish {pw : ℕ} {g : Game pw} :

g.finish.d = g.d

@[simp]

theorem AP.Alt₁.Game.a_setState {pw : ℕ} {g : Game pw} {s : State} :

(g.setState s).a = g.a

@[simp]

theorem AP.Alt₁.Game.d_setState {pw : ℕ} {g : Game pw} {s : State} :

(g.setState s).d = g.d

@[simp]

theorem AP.Alt₁.Game.a_playAMoveAt' {pw : ℕ} {g : Game pw} {a : A pw} {h₁ : g.s.act} {h₂ : AHasValidMove pw g.s.board} :

(playAMoveAt' a g h₁ h₂).a = g.a

@[simp]

theorem AP.Alt₁.Game.d_playAMoveAt' {pw : ℕ} {g : Game pw} {a : A pw} {h₁ : g.s.act} {h₂ : AHasValidMove pw g.s.board} :

(playAMoveAt' a g h₁ h₂).d = g.d

@[simp]

theorem AP.Alt₁.Game.a_playAMoveAt {pw : ℕ} {g : Game pw} :

(playAMoveAt g).a = g.a

@[simp]

theorem AP.Alt₁.Game.d_playAMoveAt {pw : ℕ} {g : Game pw} :

(playAMoveAt g).d = g.d

@[simp]

theorem AP.Alt₁.Game.a_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} :

(playDMoveAt g h).a = g.a

@[simp]

theorem AP.Alt₁.Game.d_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} :

(playDMoveAt g h).d = g.d

@[simp]

theorem AP.Alt₁.Game.a_playMove {pw : ℕ} {g : Game pw} :

g.playMove.a = g.a

@[simp]

theorem AP.Alt₁.Game.d_playMove {pw : ℕ} {g : Game pw} :

g.playMove.d = g.d

@[simp]

theorem AP.Alt₁.Game.a_play {pw : ℕ} {g : Game pw} {n : ℕ} :

(g.play n).a = g.a

@[simp]

theorem AP.Alt₁.Game.d_play {pw : ℕ} {g : Game pw} {n : ℕ} :

(g.play n).d = g.d

@[simp]

theorem AP.Alt₁.State.board_finish {s : State} :

s.finish.board = s.board

theorem AP.Alt₁.Game.s_playAMoveAt_eq_iff_of {pw : ℕ} {g₁ g₂ : Game pw} (h₁ : g₁.s.act ↔ g₂.s.act) (h₂ : AHasValidMove pw g₁.s.board ↔ AHasValidMove pw g₂.s.board) (h₁✝ : g₁.s.act) (h₂✝ : AHasValidMove pw g₁.s.board) (h₃ : g₂.s.act) (h₄ : AHasValidMove pw g₂.s.board) :

(playAMoveAt g₁).s = (playAMoveAt g₂).s ↔ applyAMove g₁.s (g₁.a.f g₁.s h₁✝ h₂✝).m = applyAMove g₂.s (g₂.a.f g₂.s h₃ h₄).m

theorem AP.Alt₁.Game.playAMoveAt_eq_of_neg {pw : ℕ} {g : Game pw} (h : ¬g.s.act ∨ ¬AHasValidMove pw g.s.board) :

playAMoveAt g = g.finish

theorem AP.Alt₁.Game.s_play_initGame_d_set_eq_of_ne {pw : ℕ} {a : A pw} {d : D} {s s₁ : State} {dRef : D} {n : ℕ} (h : ∀ k < n, ((initGame a d s).play k).s ≠ s₁) :

((initGame a (d.set s₁ dRef) s).play n).s = ((initGame a d s).play n).s

theorem AP.Alt₁.Game.act_of_act_playMove {pw : ℕ} {g : Game pw} (h : g.playMove.s.act) :

theorem AP.Alt₁.Game.act_of_act_play {pw : ℕ} {g : Game pw} {n : ℕ} (h : (g.play n).s.act) :

@[simp]

theorem AP.Alt₁.State.length_history_applyAMove {s : State} {m : AMove} :

(applyAMove s m).history.length = s.history.length + 1

@[simp]

theorem AP.Alt₁.State.length_history_applyDMove {s : State} {m : DMove} :

(applyDMove s m).history.length = s.history.length + 1

@[simp]

theorem AP.Alt₁.Game.length_history_playAMoveAt' {pw : ℕ} {g : Game pw} {a : A pw} {h₁ : g.s.act} {h₂ : AHasValidMove pw g.s.board} :

(playAMoveAt' a g h₁ h₂).s.history.length = g.s.history.length + 1

@[simp]

theorem AP.Alt₁.Game.length_history_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} :

(playDMoveAt g h).s.history.length = g.s.history.length + 1

@[simp]

theorem AP.Alt₁.State.history_finish {s : State} :

s.finish.history = s.history

theorem AP.Alt₁.Game.length_history_playMove_eq_of_act {pw : ℕ} {g : Game pw} (h : g.playMove.s.act) :

g.playMove.s.history.length = g.s.history.length + 2

theorem AP.Alt₁.Game.length_history_play_eq_of_act {pw : ℕ} {g : Game pw} {n : ℕ} (h : (g.play n).act) :

(g.play n).s.history.length = g.s.history.length + n * 2

@[simp]

theorem AP.Alt₁.Game.play_add {pw : ℕ} {g : Game pw} {n m : ℕ} :

g.play (n + m) = (g.play n).play m

theorem AP.Alt₁.Game.s_play_eq_iff_of_act {pw : ℕ} {g : Game pw} {n m : ℕ} (h : (g.play (max n m)).act) :

(g.play n).s = (g.play m).s ↔ n = m

@[simp]

theorem AP.Alt₁.history_state₀ :

state₀.history = []

@[simp]

theorem AP.Alt₁.Game.aTurn_playAMoveAt' {pw : ℕ} {g : Game pw} {a : A pw} {h₁ : g.s.act} {h₂ : AHasValidMove pw g.s.board} :

(playAMoveAt' a g h₁ h₂).s.aTurn = !g.s.aTurn

theorem AP.Alt₁.Game.aTurn_playMove_eq_of_act {pw : ℕ} {g : Game pw} (h : g.playMove.s.act) :

g.playMove.s.aTurn = g.s.aTurn

theorem AP.Alt₁.Game.aTurn_play_eq_of_act {pw : ℕ} {g : Game pw} {n : ℕ} (h : (g.play n).act) :

(g.play n).s.aTurn = g.s.aTurn

theorem AP.Alt₁.aState_iff' {pw : ℕ} {s : State} :

AState pw s ↔ State.WF pw s ∧ s.aTurn = true

theorem AP.Alt₁.dState_iff' {pw : ℕ} {s : State} :

DState pw s ↔ State.WF pw s ∧ s.aTurn = false

@[simp]

instance AP.Alt₁.aState_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} [hs : DState pw g.s] :

AState pw (playDMoveAt g h).s

theorem AP.Alt₁.Game.playAMoveAt_eq_of_not_act {pw : ℕ} {g : Game pw} (h : ¬g.s.act) :

playAMoveAt g = g.finish

theorem AP.Alt₁.Game.s_play_initGame_a_set_eq_of_ne {pw : ℕ} {a : A pw} {d : D} {s s₁ : State} {aRef : A pw} {n : ℕ} (h : ∀ k < n, ∀ (h : ((initGame a d s).play k).s.act), (playDMoveAt ((initGame a d s).play k) h).s ≠ s₁) :

((initGame (a.set s₁ aRef) d s).play n).s = ((initGame a d s).play n).s

theorem AP.Alt₁.Game.playAMoveAt_eq_of_pos {pw : ℕ} {g : Game pw} (h₁ : g.s.act) (h₂ : AHasValidMove pw g.s.board) :

playAMoveAt g = playAMoveAt' g.a g h₁ h₂

theorem AP.Alt₁.Game.act_of_act_playAMoveAt {pw : ℕ} {g : Game pw} (h : (playAMoveAt g).act) :

theorem AP.Alt₁.Game.aHasValidMove_of_act_playAMoveAt {pw : ℕ} {g : Game pw} (h : (playAMoveAt g).act) :

AHasValidMove pw g.s.board

theorem AP.Alt₁.Game.s_playAMoveAt_eq_iff_of_act_playAMoveAt {pw : ℕ} {g₁ g₂ : Game pw} (h₁ : (playAMoveAt g₁).act) (h₂ : (playAMoveAt g₂).act) :

(playAMoveAt g₁).s = (playAMoveAt g₂).s ↔ applyAMove g₁.s (g₁.a.f g₁.s ⋯ ⋯).m = applyAMove g₂.s (g₂.a.f g₂.s ⋯ ⋯).m

@[simp]

theorem AP.Alt₁.Game.act_playAMoveAt' {pw : ℕ} {g : Game pw} {a : A pw} {h₁ : g.s.act} {h₂ : AHasValidMove pw g.s.board} :

(playAMoveAt' a g h₁ h₂).act ↔ g.s.act

theorem AP.Alt₁.State.finish_eq_of_not_act {s : State} (h : ¬s.act) :

theorem AP.Alt₁.Game.finish_eq_of_not_act {pw : ℕ} {g : Game pw} (h : ¬g.s.act) :

@[simp]

theorem AP.Alt₁.dState_state₀ {pw : ℕ} :

DState pw state₀

@[simp]

theorem AP.Alt₁.AState.aTurn {pw : outParam ℕ} {s : State} [hs : AState pw s] :

@[simp]

theorem AP.Alt₁.DState.aTurn {pw : outParam ℕ} {s : State} [hs : DState pw s] :

s.aTurn = false

@[simp]

instance AP.Alt₁.wf_playAMoveAt {pw : ℕ} {g : Game pw} [hs : AState pw g.s] :

State.WF pw (playAMoveAt g).s

@[simp]

instance AP.Alt₁.Game.wf_playMove {pw : ℕ} {g : Game pw} [hs : DState pw g.s] :

State.WF pw g.playMove.s

theorem AP.Alt₁.Game.playAMoveAt_eq_of_act {pw : ℕ} {g : Game pw} (h : (playAMoveAt g).act) :

playAMoveAt g = playAMoveAt' g.a g ⋯ ⋯

theorem AP.Alt₁.Game.aTurn_playAMoveAt_of_act {pw : ℕ} {g : Game pw} (h : (playAMoveAt g).act) :

(playAMoveAt g).s.aTurn = !g.s.aTurn

theorem AP.Alt₁.dState_playAMoveAt_of_act {pw : ℕ} {g : Game pw} [hs : AState pw g.s] (h : (playAMoveAt g).s.act) :

DState pw (playAMoveAt g).s

theorem AP.Alt₁.Game.dState_playMove_of_act {pw : ℕ} {g : Game pw} [hs : DState pw g.s] (h : g.playMove.act) :

DState pw g.playMove.s

@[simp]

instance AP.Alt₁.Game.wf_play {pw : ℕ} {g : Game pw} {n : ℕ} [hs : DState pw g.s] :

State.WF pw (g.play n).s

theorem AP.Alt₁.Game.dState_play_of_act {pw : ℕ} {g : Game pw} {n : ℕ} [hs : DState pw g.s] (h : (g.play n).act) :

DState pw (g.play n).s

theorem AP.Alt₁.not_dHws_of_aHws {pw : ℕ} (h : AHws pw) :

theorem AP.Alt₁.not_aHws_of_dHws {pw : ℕ} (h : DHws pw) :

@[simp]

instance AP.Alt₁.State.wf_toAltH_state₀ {pw : ℕ} :

sys.WF (state₀.toAltH pw)

@[simp]

instance AP.Alt₁.State.wf_getd_toAltH?_state₀ {pw : ℕ} :

sys.WF (state₀.toAltH? pw).getd

@[simp]

theorem AP.Alt₁.State.even_length_history_of_dState {pw : ℕ} {s : State} [hs : DState pw s] :

Even s.history.length

@[simp]

theorem AP.Alt₁.State.not_odd_length_history_of_dState {pw : ℕ} {s : State} [hs : DState pw s] :

¬Odd s.history.length

@[simp]

theorem AP.Alt₁.State.aTurn_eq_of_DState {pw : ℕ} {s : State} [hs : DState pw s] :

s.aTurn = false

theorem AP.Alt₁.Board.getd_toAltH?_eq_toAlt_of {pw : ℕ} {t₁ t₂ : Bool} {b₁ b₂ : Board} (h : ∃ (s₁ : AP.State) (s₂ : AP.State), sys.WF s₁ ∧ sys.WF s₂ ∧ b₁.toAlt pw t₁ s₁.hist = s₁ ∧ b₂.toAlt pw t₂ s₂.hist = s₂ ∧ s₁ = s₂.setHist s₁.hist) :

∃ (hist : List PointZ), (b₁.toAltH? pw t₁).getd = b₂.toAlt pw t₂ hist

theorem AP.Alt₁.Board.toAlt_eq_setHist {s : State} {pw : ℕ} {t : Bool} {hist : List PointZ} (hist₁ : List PointZ) :

s.board.toAlt pw t hist = (s.board.toAlt pw t hist₁).setHist hist

theorem AP.Alt₁.Board.toAlt_eq_setHist_nil {s : State} {pw : ℕ} {t : Bool} {hist : List PointZ} :

s.board.toAlt pw t hist = (s.board.toAlt pw t []).setHist hist

theorem AP.Alt₁.State.exi_wf_toAlt_board_iff_exi_hist {pw : ℕ} {t : Bool} {s : State} :

(∃ (s₁ : AP.State), sys.WF s₁ ∧ s.board.toAlt pw t s₁.hist = s₁) ↔ ∃ (hist : List PointZ), sys.WF (s.board.toAlt pw t hist)

theorem AP.Alt₁.State.exi_hist_toAlt_board_of_wfCnd {pw : ℕ} {t : Bool} {s : State} (h : WFCnd (s.board.toAlt pw t [])) :

∃ (hist : List PointZ), sys.WF (s.board.toAlt pw t hist)

theorem AP.Alt₁.State.exi_wf_toAlt_board_of_wfCnd {pw : ℕ} {t : Bool} {s : State} (h : WFCnd (s.board.toAlt pw t [])) :

∃ (s₁ : AP.State), sys.WF s₁ ∧ s.board.toAlt pw t s₁.hist = s₁

@[simp]

theorem AP.Alt₁.Game.squares_board_playAMoveAt {pw : ℕ} {g : Game pw} :

(playAMoveAt g).s.board.squares = g.s.board.squares

theorem AP.Alt₁.State.finite_univ_diff_squares_of_play' {pw : ℕ} {a : A pw} {d : D} {n : ℕ} {g : Game pw} {s : State} (h₁ : (Set.univ \ s.board.squares).Finite) (h₂ : (initGame a d s).play n = g) :

(Set.univ \ g.s.board.squares).Finite

@[simp]

theorem AP.Alt₁.State.finite_univ_diff_squares_of_play {pw : ℕ} {a : A pw} {d : D} {n : ℕ} {g : Game pw} (h : (initGame a d state₀).play n = g) :

(Set.univ \ g.s.board.squares).Finite

@[simp]

theorem AP.Alt₁.State.finite_univ_diff_squares {s : State} {pw : ℕ} [hs : WF pw s] :

(Set.univ \ s.board.squares).Finite

@[simp]

theorem AP.Alt₁.State.finite_image_univ_diff_squares {s : State} {pw : ℕ} [hs : WF pw s] :

((fun (x : Point) => x.toAlt) '' (Set.univ \ s.board.squares)).Finite

@[simp]

theorem AP.Alt₁.State.mem_ofSet_image_univ_diff_squares {s : State} {pw : ℕ} {p : PointZ} [hs : WF pw s] :

p ∈ Set'.ofSet ((fun (x : Point) => x.toAlt) '' (Set.univ \ s.board.squares)) ↔ p ∈ (fun (x : Point) => x.toAlt) '' (Set.univ \ s.board.squares)

@[simp]

theorem AP.Alt₁.Point.toAlt_eq_iff {a b : Point} :

a.toAlt = b.toAlt ↔ a = b

@[simp]

theorem AP.Alt₁.wf_state₀ {pw : ℕ} :

State.WF pw state₀

theorem AP.Alt₁.Game.aTurn_playMove_iff {pw : ℕ} {g : Game pw} (ha : g.s.act) (ht : g.s.aTurn = false) :

g.playMove.s.aTurn = !decide g.playMove.act

theorem AP.Alt₁.Game.aTurn_play_iff {pw : ℕ} {g : Game pw} {n : ℕ} (ha : g.s.act) (ht : g.s.aTurn = false) :

(g.play n).s.aTurn = !decide (g.play n).act

@[simp]

theorem AP.Alt₁.Game.length_history_le_playAMoveAt {pw : ℕ} {g : Game pw} :

g.s.history.length ≤ (playAMoveAt g).s.history.length

@[simp]

theorem AP.Alt₁.Game.length_history_le_playDMoveAt {pw : ℕ} {g : Game pw} {h : g.s.act} :

g.s.history.length ≤ (playDMoveAt g h).s.history.length

@[simp]

theorem AP.Alt₁.Game.length_history_le_playMove {pw : ℕ} {g : Game pw} :

g.s.history.length ≤ g.playMove.s.history.length

@[simp]

theorem AP.Alt₁.Game.length_history_le_play {pw : ℕ} {g : Game pw} {n : ℕ} :

g.s.history.length ≤ (g.play n).s.history.length

theorem AP.Alt₁.Game.length_hist_play_le_of_le {pw : ℕ} {g : Game pw} {k n : ℕ} (h : k ≤ n) :

(g.play k).s.history.length ≤ (g.play n).s.history.length

@[simp]

theorem AP.Alt₁.Game.length_hist_lt_playMove_iff_act {pw : ℕ} {g : Game pw} :

g.s.history.length < g.playMove.s.history.length ↔ g.s.act

theorem AP.Alt₁.Game.length_hist_play_lt_of_lt_and_act {pw : ℕ} {g : Game pw} {k n : ℕ} (h₁ : k < n) (h₂ : (g.play k).act) :

(g.play k).s.history.length < (g.play n).s.history.length

@[simp]

theorem AP.Alt₁.Game.setState_inj {pw : ℕ} {g : Game pw} {s₁ s₂ : State} :

g.setState s₁ = g.setState s₂ ↔ s₁ = s₂

@[simp]

theorem AP.Alt₁.A.f_set_of_eq {pw : ℕ} {a a₀ : A pw} {s : State} :

(a.set s a₀).f s = a₀.f s

@[simp]

theorem AP.Alt₁.D.f_set_of_eq {d d₀ : D} {s : State} :

(d.set s d₀).f s = d₀.f s

@[simp]

theorem AP.Alt₁.Game.playAMoveAt'_set_of_eq {pw : ℕ} {g : Game pw} {a a₀ : A pw} {h₁ : g.s.act} {h₂ : AHasValidMove pw g.s.board} :

playAMoveAt' (a.set g.s a₀) g h₁ h₂ = playAMoveAt' a₀ g h₁ h₂

@[simp]

theorem AP.Alt₁.Game.playAMoveAt_initGame_a_set_of_eq {pw : ℕ} {a a₀ : A pw} {d : D} {s : State} :

(playAMoveAt (initGame (a.set s a₀) d s)).s = (playAMoveAt (initGame a₀ d s)).s

@[simp]

theorem AP.Alt₁.Game.playDMoveAt_initGame_d_set_of_eq {pw : ℕ} {a : A pw} {d d₀ : D} {s : State} {h : (initGame a (d.set s d₀) s).s.act} :

(playDMoveAt (initGame a (d.set s d₀) s) h).s = (playDMoveAt (initGame a d₀ s) h).s

@[simp]

theorem AP.Alt₁.Game.initGame_self {pw : ℕ} {g : Game pw} :

initGame g.a g.d g.s = g

theorem AP.Alt₁.Game.eq_initGame {pw : ℕ} {g : Game pw} :

g = initGame g.a g.d g.s

@[simp]

theorem AP.Alt₁.Game.s_playAMoveAt_congr {pw : ℕ} {g : Game pw} {d : D} :

(playAMoveAt (initGame g.a d g.s)).s = (playAMoveAt g).s

@[simp]

theorem AP.Alt₁.Game.s_playDMoveAt_congr {pw : ℕ} {g : Game pw} {a : A pw} {h : (initGame a g.d g.s).s.act} :

(playDMoveAt (initGame a g.d g.s) h).s = (playDMoveAt g h).s

theorem AP.Alt₁.Game.act_play_of_le {pw : ℕ} {g : Game pw} {n k : ℕ} (h₁ : (g.play n).act) (h₂ : k ≤ n) :

(g.play k).act

theorem AP.Alt₁.Game.wf_playAMoveAt' {pw : ℕ} {g : Game pw} [hs : State.WF pw g.s] (h : g.s.aTurn = true) :

State.WF pw (playAMoveAt g).s

theorem AP.Alt₁.Game.wf_playDMoveAt' {pw : ℕ} {g : Game pw} [hs : State.WF pw g.s] {hh : g.s.act} (h : g.s.aTurn = false) :

State.WF pw (playDMoveAt g hh).s

@[simp]

instance AP.Alt₁.Game.wf_playAMoveAt {pw : ℕ} {g : Game pw} [hs : AState pw g.s] :

State.WF pw (playAMoveAt g).s

@[simp]

instance AP.Alt₁.Game.wf_playDMoveAt {pw : ℕ} {g : Game pw} [hs : DState pw g.s] {hh : g.s.act} :

State.WF pw (playDMoveAt g hh).s

theorem AP.Alt₁.dState_play_initGame_of {pw : ℕ} {a : A pw} {d : D} {s : State} {n : ℕ} [hs : DState pw s] (h : ((initGame a d s).play n).s.act) :

DState pw ((initGame a d s).play n).s

theorem AP.Alt₁.State.invariant_of_wf {pw : ℕ} {s : State} {p : State → Prop} [hs : WF pw s] (h₁ : p state₀) (h₄ : ∀ ⦃s : State⦄, WF pw s → p s → p s.finish) (h₂ : ∀ ⦃s : State⦄ ⦃m : AMove⦄, WF pw s → AMoveValid pw s.board m → p s → p (applyAMove s m)) (h₃ : ∀ ⦃s : State⦄ ⦃m : DMove⦄, WF pw s → DMoveValid s.board m → p s → p (applyDMove s m)) :

p s

theorem AP.Alt₁.Board.invariant_of_wf {pw : ℕ} {s : State} {p : Board → Prop} [hs : State.WF pw s] (h₁ : p board₀) (h₂ : ∀ ⦃b : Board⦄ ⦃m : AMove⦄, AMoveValid pw b m → p b → p (applyAMoveB b m)) (h₃ : ∀ ⦃b : Board⦄ ⦃m : DMove⦄, DMoveValid b m → p b → p (applyDMoveB b m)) :

@[simp]

theorem AP.Alt₁.dMoveValid_some_iff {b : Board} {p : Point} :

DMoveValid b (some p) ↔ p ≠ b.A ∧ p ∈ b.squares

theorem AP.Alt₁.dMoveValid_iff {b : Board} {m : DMove} :

DMoveValid b m ↔ m = none ∨ ∃ (p : Point), m = some p ∧ p ≠ b.A ∧ p ∈ b.squares

@[simp]

theorem AP.Alt₁.Board.a_applyAMoveB {b : Board} {m : AMove} :

(applyAMoveB b m).A = m

@[simp]

theorem AP.Alt₁.Board.a_applyDMoveB {b : Board} {m : DMove} :

(applyDMoveB b m).A = b.A

@[simp]

theorem AP.Alt₁.Board.squares_applyAMoveB {b : Board} {m : AMove} :

(applyAMoveB b m).squares = b.squares

@[simp]

theorem AP.Alt₁.Board.squares_applyDMoveB {b : Board} {m : DMove} :

(applyDMoveB b m).squares = b.squares \ Option.elim m ∅ fun (x : Point) => {x}

theorem AP.Alt₁.State.a_mem_squares_of_wf {pw : ℕ} {s : State} [hs : WF pw s] :

s.board.A ∈ s.board.squares

@[simp]

theorem AP.Alt₁.squares_board_applyAMove {s : State} {m : AMove} :

(applyAMove s m).board.squares = s.board.squares

theorem AP.Alt₁.Game.lt_of_not_act_play {pw : ℕ} {g : Game pw} {n k : ℕ} (h₁ : (g.play k).s.act) (h₂ : ¬(g.play n).s.act) :

k < n

@[simp]

theorem AP.Alt₁.Game.state_playDMoveAt_ne_self {pw : ℕ} {g : Game pw} {h : g.s.act} :

(playDMoveAt g h).s ≠ g.s

@[simp]

theorem AP.Alt₁.Game.playDMoveAt_ne_self {pw : ℕ} {g : Game pw} {h : g.s.act} :

playDMoveAt g h ≠ g

@[simp]

theorem AP.Alt₁.Game.play_initGame_aTurn_eq_true_iff_not_act {pw : ℕ} {a : A pw} {d : D} {n : ℕ} :

((initGame a d state₀).play n).s.aTurn = true ↔ ¬((initGame a d state₀).play n).s.act

@[simp]

theorem AP.Alt₁.Game.play_initGame_aTurn_eq_false_iff_act {pw : ℕ} {a : A pw} {d : D} {n : ℕ} :

((initGame a d state₀).play n).s.aTurn = false ↔ ((initGame a d state₀).play n).s.act