structure Sokoban.Tile : Type

• player : Bool
• box : Bool
• target : Bool
• wall : Bool

theorem Sokoban.Tile.ext {x y : Tile} (player : x.player = y.player) (box : x.box = y.box) (target : x.target = y.target) (wall : x.wall = y.wall) : x = y

theorem Sokoban.Tile.ext_iff {x y : Tile} : x = y ↔ x.player = y.player ∧ x.box = y.box ∧ x.target = y.target ∧ x.wall = y.wall

@[instance_reducible]

instance Sokoban.instInhabitedTile : Inhabited Tile

Equations

• Sokoban.instInhabitedTile = { default := Sokoban.instInhabitedTile.default }

@[instance_reducible]

instance Sokoban.instDecidableEqTile : DecidableEq Tile

Equations

• Sokoban.instDecidableEqTile = Sokoban.instDecidableEqTile.decEq

def Sokoban.instDecidableEqTile.decEq (x✝ x✝¹ : Tile) : Decidable (x✝ = x✝¹)

Equations

• Sokoban.instDecidableEqTile.decEq { player := a, box := a_1, target := a_2, wall := a_3 } { player := b, box := b_1, target := b_2, wall := b_3 } = 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 ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Sokoban.instFintypeTile : Fintype Tile

Equations

• Sokoban.instFintypeTile = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × (_ : Bool) × Bool) Sokoban.Tile.proxyTypeEquiv

structure Sokoban.State : Type

• width : ℕ
• height : ℕ
• grid : Map PointZ Tile
• player : PointZ
• unsolvedNum : ℕ

theorem Sokoban.State.ext_iff {x y : State} : x = y ↔ x.width = y.width ∧ x.height = y.height ∧ x.grid = y.grid ∧ x.player = y.player ∧ x.unsolvedNum = y.unsolvedNum

theorem Sokoban.State.ext {x y : State} (width : x.width = y.width) (height : x.height = y.height) (grid : x.grid = y.grid) (player : x.player = y.player) (unsolvedNum : x.unsolvedNum = y.unsolvedNum) : x = y

@[instance_reducible]

instance Sokoban.instInhabitedState : Inhabited State

Equations

• Sokoban.instInhabitedState = { default := Sokoban.instInhabitedState.default }

@[instance_reducible]

instance Sokoban.instDecidableEqState : DecidableEq State

Equations

• Sokoban.instDecidableEqState = Sokoban.instDecidableEqState.decEq

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

Equations

• Sokoban.instDecidableEqState.decEq { width := a, height := a_1, grid := a_2, player := a_3, unsolvedNum := a_4 } { width := b, height := b_1, grid := b_2, player := b_3, unsolvedNum := 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 ⋯

@[reducible, inline]

abbrev Sokoban.Move : Type

Equations

• Sokoban.Move = Dir

def Sokoban.State.points (s : State) : Set' PointZ

Equations

• s.points = s.grid.keysSet

def Sokoban.State.boxes (s : State) : Set' PointZ

Equations

• s.boxes = s.points.filter fun (p : PointZ) => (Map.get! p s.grid).box

def Sokoban.State.targets (s : State) : Set' PointZ

Equations

• s.targets = s.points.filter fun (p : PointZ) => (Map.get! p s.grid).target

class Sokoban.State.Get (s : State) (p : PointZ) (d : outParam Tile) : Prop

• h : Map.get? p s.grid = some d

class Sokoban.State.Get' (s : State) (d : Tile) : Prop

• h : ∃ (p : PointZ), s.Get p d

class Sokoban.Tile.WF (d : Tile) : Prop

• tw : [d.target, d.wall].atMostOne = true
• pbw : [d.player, d.box, d.wall].atMostOne = true

class Sokoban.State.WF (s : State) : Prop

• mem_grid_iff_bounds {p : PointZ} : p ∈ s.grid ↔ 0 ≤ p.x ∧ 0 ≤ p.y ∧ p.x < ↑s.width ∧ p.y < ↑s.height
• wf_get {d : Tile} : s.Get' d → d.WF
• player_mem : s.player ∈ s.grid
• tile_player_iff {p : PointZ} {d : Tile} : s.Get p d → (d.player = true ↔ s.player = p)
• unsolvedNum_eq : s.unsolvedNum = List.countP (fun (d : Tile) => d.box && !d.target) s.grid.values
• size_boxes_eq_size_targets : s.boxes.size = s.targets.size

def Sokoban.State.movePlayer (s : State) (p : PointZ) : State

Equations

• s.movePlayer p = { width := s.width, height := s.height, grid := s.grid.modifyMany [(s.player, fun (d : Sokoban.Tile) => { player := false, box := d.box, target := d.target, wall := d.wall }), (p, fun (d : Sokoban.Tile) => { player := true, box := d.box, target := d.target, wall := d.wall })], player := p, unsolvedNum := s.unsolvedNum }

def Sokoban.State.moveBox (s : State) (p₁ p₂ : PointZ) : State

Equations

• s.moveBox p₁ p₂ = { width := s.width, height := s.height, grid := s.grid.modifyMany [(p₁, fun (d : Sokoban.Tile) => { player := d.player, box := false, target := d.target, wall := d.wall }), (p₂, fun (d : Sokoban.Tile) => { player := d.player, box := true, target := d.target, wall := d.wall })], player := s.player, unsolvedNum := (s.unsolvedNum + if (Map.get! p₁ s.grid).target = true then 1 else 0) - if (Map.get! p₂ s.grid).target = true then 1 else 0 }

def Sokoban.State.move (s : State) (m : Move) : Option State

Equations

• s.move m = do let d₁ ← Map.get? (s.player + Dir.point m) s.grid guard ((!d₁.wall) = true) if (!d₁.box) = true then some (s.movePlayer (s.player + Dir.point m)) else have p₂ := s.player + Dir.point m + Dir.point m; do let d₂ ← Map.get? p₂ s.grid guard ((!(d₂.box || d₂.wall)) = true) some ((s.moveBox (s.player + Dir.point m) p₂).movePlayer (s.player + Dir.point m))

def Sokoban.State.solved (s : State) : Bool

Equations

• s.solved = s.grid.all fun (x : PointZ) (d : Sokoban.Tile) => decide (d.target = true → d.box = true)

def Sokoban.sys : System State Move

Equations

• Sokoban.sys = { initial := {s : Sokoban.State | s.WF}, tr := Sokoban.State.move }