Documentation

Projects.Sokoban.Card

theorem Sokoban.point_eq_of_fin {s : State} [hs : s.WF] {p : PointZ} (h : p ∈ s.grid) :

p = { x := ↑↑p.x.toFin, y := ↑↑p.y.toFin }

theorem Sokoban.x_toFin_width_eq_iff' {s : State} [hs : s.WF] {p₁ p₂ : PointZ} (h₁ : p₁ ∈ s.grid) (h₂ : p₂ ∈ s.grid) :

p₁.x.toFin = p₂.x.toFin ↔ p₁.x = p₂.x

theorem Sokoban.y_toFin_width_eq_iff' {s : State} [hs : s.WF] {p₁ p₂ : PointZ} (h₁ : p₁ ∈ s.grid) (h₂ : p₂ ∈ s.grid) :

p₁.y.toFin = p₂.y.toFin ↔ p₁.y = p₂.y

theorem Sokoban.x_toFin_width_eq_iff {n : ℕ} [hn : NeZero n] {s₁ s₂ : State} [hs₁ : s₁.WF] [hs₂ : s₂.WF] {p₁ p₂ : PointZ} (hw₁ : s₁.width = n) (hw₂ : s₂.width = n) (h₁ : p₁ ∈ s₁.grid) (h₂ : p₂ ∈ s₂.grid) :

p₁.x.toFin = p₂.x.toFin ↔ p₁.x = p₂.x

theorem Sokoban.y_toFin_width_eq_iff {n : ℕ} [hn : NeZero n] {s₁ s₂ : State} [hs₁ : s₁.WF] [hs₂ : s₂.WF] {p₁ p₂ : PointZ} (hw₁ : s₁.height = n) (hw₂ : s₂.height = n) (h₁ : p₁ ∈ s₁.grid) (h₂ : p₂ ∈ s₂.grid) :

p₁.y.toFin = p₂.y.toFin ↔ p₁.y = p₂.y

structure Sokoban.Card.FinState (w h : ℕ) [NeZero w] [NeZero h] :

grid : Map (Fin w × Fin h) Tile
player : Fin w × Fin h

Instances For

@[instance_reducible]

instance Sokoban.Card.instFintypeFinState {w✝ h✝ : ℕ} {inst✝ : NeZero w✝} {inst✝¹ : NeZero h✝} :

Fintype (FinState w✝ h✝)

Equations

Sokoban.Card.instFintypeFinState = Fintype.ofEquiv ((_ : Map (Fin w✝ × Fin h✝) Sokoban.Tile) × Fin w✝ × Fin h✝) (Sokoban.Card.FinState.proxyTypeEquiv w✝ h✝)

def Sokoban.Card.fn (s₀ : State) [hs : s₀.WF] (s : State) :

FinState s₀.width s₀.height

Equations

Sokoban.Card.fn s₀ s = { grid := Map.range fun (p : Fin s₀.width × Fin s₀.height) => Map.get! { x := ↑↑p.1, y := ↑↑p.2 } s.grid, player := (s.player.x.toFin, s.player.y.toFin) }

Instances For

theorem Sokoban.nonneg_x_of_get {s : State} {x y : ℤ} {d : Tile} [hs : s.WF] [h : s.Get { x := x, y := y } d] :

0 ≤ x

theorem Sokoban.nonneg_y_of_get {s : State} {x y : ℤ} {d : Tile} [hs : s.WF] [h : s.Get { x := x, y := y } d] :

0 ≤ y

theorem Sokoban.x_lt_width_of_get {s : State} {x y : ℤ} {d : Tile} [hs : s.WF] [h : s.Get { x := x, y := y } d] :

x < ↑s.width

theorem Sokoban.y_lt_height_of_get {s : State} {x y : ℤ} {d : Tile} [hs : s.WF] [h : s.Get { x := x, y := y } d] :

y < ↑s.height

theorem Sokoban.toFin_eq_of_get? {s s' : State} {p : PointZ} {d : Tile} [hs : s.WF] [hs' : s'.WF] (h₁ : sys.Reachable s s') (h₂ : Map.get? p s'.grid = some d) :

{ x := ↑↑p.x.toFin, y := ↑↑p.y.toFin } = p

theorem Sokoban.finite_reachable {s : State} [hs : s.WF] :

{s' : State | sys.Reachable s s'}.Finite