Documentation

Projects.Sokoban.Basic

theorem Sokoban.get_iff {s : State} {p : PointZ} {d : Tile} :

s.Get p d ↔ Map.get? p s.grid = some d

theorem Sokoban.get'_iff {s : State} {d : Tile} :

s.Get' d ↔ ∃ (p : PointZ), Map.get? p s.grid = some d

theorem Sokoban.get?_grid_eq_some_iff {s : State} {p : PointZ} {d : Tile} :

Map.get? p s.grid = some d ↔ s.Get p d

theorem Sokoban.State.Get.eq_of {s : State} {p : PointZ} {d₁ d₂ : Tile} (h₁ : s.Get p d₁) (h₂ : s.Get p d₂) :

d₁ = d₂

theorem Sokoban.State.Get.get' {s : State} {p : PointZ} {d : Tile} [hd : s.Get p d] :

s.Get' d

theorem Sokoban.State.Get.wf {s : State} {p : PointZ} {d : Tile} [hs : s.WF] [hd : s.Get p d] :

d.WF

theorem Sokoban.State.Get'.wf {s : State} {d : Tile} [hs : s.WF] [hd : s.Get' d] :

d.WF

theorem Sokoban.State.Get.mem {s : State} {p : PointZ} {d : Tile} [hd : s.Get p d] :

@[simp]

theorem Sokoban.sys_initial_iff {s : State} :

sys.Initial s ↔ s.WF

theorem Sokoban.sys_tr_eq {s : State} :

sys.tr s = s.move

@[simp]

theorem Sokoban.width_movePlayer {s : State} {p₁ : PointZ} :

(s.movePlayer p₁).width = s.width

@[simp]

theorem Sokoban.height_movePlayer {s : State} {p₁ : PointZ} :

(s.movePlayer p₁).height = s.height

@[simp]

theorem Sokoban.player_movePlayer {s : State} {p₁ : PointZ} :

(s.movePlayer p₁).player = p₁

@[simp]

theorem Sokoban.width_moveBox {s : State} {p₁ p₂ : PointZ} :

(s.moveBox p₁ p₂).width = s.width

@[simp]

theorem Sokoban.height_moveBox {s : State} {p₁ p₂ : PointZ} :

(s.moveBox p₁ p₂).height = s.height

@[simp]

theorem Sokoban.player_moveBox {s : State} {p₁ p₂ : PointZ} :

(s.moveBox p₁ p₂).player = s.player

@[simp]

theorem Sokoban.mem_grid_movePlayer {s : State} {p₁ p : PointZ} :

p ∈ (s.movePlayer p₁).grid ↔ p ∈ s.grid

@[simp]

theorem Sokoban.mem_grid_moveBox {s : State} {p₁ p₂ p : PointZ} :

p ∈ (s.moveBox p₁ p₂).grid ↔ p ∈ s.grid

@[simp]

theorem Sokoban.get?_grid_movePlayer {s : State} {p₁ p : PointZ} :

Map.get? p (s.movePlayer p₁).grid = Option.map (fun (d : Tile) => if p₁ = p then { player := true, box := d.box, target := d.target, wall := d.wall } else if s.player = p then { player := false, box := d.box, target := d.target, wall := d.wall } else d) (Map.get? p s.grid)

@[simp]

theorem Sokoban.get?_grid_moveBox {s : State} {p₁ p₂ p : PointZ} :

Map.get? p (s.moveBox p₁ p₂).grid = Option.map (fun (d : Tile) => if p₂ = p then { player := d.player, box := true, target := d.target, wall := d.wall } else if p₁ = p then { player := d.player, box := false, target := d.target, wall := d.wall } else d) (Map.get? p s.grid)

@[simp]

theorem Sokoban.get_movePlayer {s : State} {p₁ p : PointZ} {d : Tile} :

(s.movePlayer p₁).Get p d ↔ ∃ (d' : Tile), s.Get p d' ∧ (if p₁ = p then { player := true, box := d'.box, target := d'.target, wall := d'.wall } else if s.player = p then { player := false, box := d'.box, target := d'.target, wall := d'.wall } else d') = d

@[simp]

theorem Sokoban.get_moveBox {s : State} {p₁ p₂ p : PointZ} {d : Tile} :

(s.moveBox p₁ p₂).Get p d ↔ ∃ (d' : Tile), s.Get p d' ∧ (if p₂ = p then { player := d'.player, box := true, target := d'.target, wall := d'.wall } else if p₁ = p then { player := d'.player, box := false, target := d'.target, wall := d'.wall } else d') = d

@[simp]

theorem Sokoban.unsolvedNum_move_player {s : State} {p : PointZ} :

(s.movePlayer p).unsolvedNum = s.unsolvedNum

theorem Sokoban.moveBox_movePlayer {s : State} {p₁ p₂ p₃ : PointZ} :

(s.movePlayer p₁).moveBox p₂ p₃ = (s.moveBox p₂ p₃).movePlayer p₁

theorem Sokoban.movePlayer_moveBox {s : State} {p₁ p₂ p₃ : PointZ} :

(s.moveBox p₁ p₂).movePlayer p₃ = (s.movePlayer p₃).moveBox p₁ p₂

theorem Sokoban.tr_eq_some_iff {s s' : State} (t : Move) :

sys.tr s t = some s' ↔ have p_dif := Dir.point t; have p₁ := s.player + p_dif; have p₂ := p₁ + p_dif; have s₁ := s.movePlayer p₁; ∃ (d₁ : Tile), s.Get p₁ d₁ ∧ (!d₁.wall) = true ∧ if (!d₁.box) = true then s₁ = s' else ∃ (d₂ : Tile), s.Get p₂ d₂ ∧ d₂.box = false ∧ d₂.wall = false ∧ s₁.moveBox p₁ p₂ = s'

theorem Sokoban.State.Get.player_eq {s : State} {p : PointZ} {d : Tile} [hs : s.WF] (hd : s.Get p d) :

s.player = p ↔ d.player = true

theorem Sokoban.State.Get.player_iff {s : State} {p : PointZ} {d : Tile} [hs : s.WF] (hd : s.Get p d) :

d.player = decide (s.player = p)

theorem Sokoban.State.Get.player_of_get_player {s : State} {d : Tile} [hs : s.WF] (hd : s.Get s.player d) :

d.player = true

theorem Sokoban.State.Get.not_box_and_not_wall_of_get_player {s : State} {d : Tile} [hs : s.WF] (hd : s.Get s.player d) :

d.box = false ∧ d.wall = false

@[simp]

theorem Sokoban.countP_box_target_movePlayer {s : State} {p : PointZ} :

List.countP (fun (d : Tile) => d.box && !d.target) (s.movePlayer p).grid.values = List.countP (fun (d : Tile) => d.box && !d.target) s.grid.values

@[simp]

theorem Sokoban.get?_grid_of_get {s : State} {p : PointZ} {d : Tile} [h : s.Get p d] :

Map.get? p s.grid = some d

@[simp]

theorem Sokoban.get!_grid_of_get {s : State} {p : PointZ} {d : Tile} [h : s.Get p d] :

Map.get! p s.grid = d

@[simp]

theorem Sokoban.mem_grid_of_get {s : State} {p : PointZ} {d : Tile} [h : s.Get p d] :

@[simp]

theorem Sokoban.points_moveBox {s : State} {p₁ p₂ : PointZ} :

(s.moveBox p₁ p₂).points = s.points

@[simp]

theorem Sokoban.mem_points_of_get {s : State} {p : PointZ} {d : Tile} [h : s.Get p d] :

theorem Sokoban.mem_points_iff_exi_get {s : State} {p : PointZ} :

p ∈ s.points ↔ ∃ (d : Tile), s.Get p d

theorem Sokoban.boxes_moveBox {s : State} {p₁ p₂ : PointZ} {d₁ d₂ : Tile} [h₁ : s.Get p₁ d₁] [h₂ : s.Get p₂ d₂] :

(s.moveBox p₁ p₂).boxes = (s.boxes.erase p₁).insert p₂

theorem Sokoban.eq_of_get_and_get {s : State} {p : PointZ} {d₁ d₂ : Tile} [h₁ : s.Get p d₁] [h₂ : s.Get p d₂] :

d₁ = d₂

theorem Sokoban.size_boxes_moveBox {s : State} {p₁ p₂ : PointZ} {d₁ d₂ : Tile} [h₁ : s.Get p₁ d₁] [h₂ : s.Get p₂ d₂] (h₃ : d₁.box = true) (h₄ : d₂.box = false) :

(s.moveBox p₁ p₂).boxes.size = s.boxes.size

@[simp]

theorem Sokoban.points_movePlayer {s : State} {p : PointZ} :

(s.movePlayer p).points = s.points

@[simp]

theorem Sokoban.box_get!_grid_movePlayer {s : State} {p p₁ : PointZ} :

(Map.get! p₁ (s.movePlayer p).grid).box = (Map.get! p₁ s.grid).box

@[simp]

theorem Sokoban.boxes_movePlayer {s : State} {p : PointZ} :

(s.movePlayer p).boxes = s.boxes

@[simp]

theorem Sokoban.target_get!_grid_movePlayer {s : State} {p p₁ : PointZ} :

(Map.get! p₁ (s.movePlayer p).grid).target = (Map.get! p₁ s.grid).target

@[simp]

theorem Sokoban.targets_movePlayer {s : State} {p : PointZ} :

(s.movePlayer p).targets = s.targets

@[simp]

theorem Sokoban.target_get!_grid_moveBox {s : State} {p₁ p₂ p : PointZ} :

(Map.get! p (s.moveBox p₁ p₂).grid).target = (Map.get! p s.grid).target

@[simp]

theorem Sokoban.targets_moveBox {s : State} {p₁ p₂ : PointZ} :

(s.moveBox p₁ p₂).targets = s.targets

theorem Sokoban.sys_wf_iff {s : State} :

sys.WF s ↔ s.WF

theorem Sokoban.wf_of_reachable {s s' : State} [hs : s.WF] (hr : sys.Reachable s s') :

s'.WF

@[simp]

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

s.player ∈ s.grid

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

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

instance Sokoban.instNeZeroNatWidthOfWF {s : State} [hs : s.WF] :

instance Sokoban.instNeZeroNatHeightOfWF {s : State} [hs : s.WF] :

NeZero s.height

theorem Sokoban.width_and_height_eq_of_reachable {s₀ s : State} [hs₀ : s₀.WF] (h : sys.Reachable s₀ s) :

s.width = s₀.width ∧ s.height = s₀.height

theorem Sokoban.width_eq_of_reachable {s₀ s : State} [hs₀ : s₀.WF] (h : sys.Reachable s₀ s) :

s.width = s₀.width

theorem Sokoban.height_eq_of_reachable {s₀ s : State} [hs₀ : s₀.WF] (h : sys.Reachable s₀ s) :

s.height = s₀.height

theorem Sokoban.mem_grid_iff_of_reachable {s₀ s : State} [hs₀ : s₀.WF] {p : PointZ} (h : sys.Reachable s₀ s) :

p ∈ s.grid ↔ p ∈ s₀.grid

theorem Sokoban.targets_eq_of_tr {s s' : State} {p : Move} (h : sys.tr s p = some s') :

s'.targets = s.targets

theorem Sokoban.targets_eq_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') :

s'.targets = s.targets

theorem Sokoban.size_boxes_eq_of_tr {s s' : State} {p : Move} (h : sys.tr s p = some s') :

s'.boxes.size = s.boxes.size

theorem Sokoban.size_boxes_eq_of_reachable {s s' : State} [hs : sys.WF s] (h : sys.Reachable s s') :

s'.boxes.size = s.boxes.size

theorem Sokoban.mem_points_of_mem_boxes {s : State} {p : PointZ} (h : p ∈ s.boxes) :