noncomputable def Sokoban.State.boxesReachable (s : State) : Set' PointZ

Equations

• s.boxesReachable = s.points.filter fun (p : PointZ) => decide (∃ (s' : Sokoban.State), Sokoban.sys.Reachable s s' ∧ p ∈ s'.boxes)

noncomputable def Sokoban.State.trBox (s : State) : PointZ

Equations

• s.trBox = s.boxesReachable.headMap! fun (p : PointZ) => p * { x := -1, y := 1 }

noncomputable def Sokoban.State.BoxPushed (s s' : State) : Prop

Equations

• s.BoxPushed s' = ((∃ (p : Sokoban.Move), Sokoban.sys.tr s p = some s') ∧ s'.boxes ≠ s.boxes)

@[simp]

theorem Sokoban.boxes_subset_boxesReachable {s : State} : s.boxes ⊆ s.boxesReachable

@[simp]

theorem Sokoban.boxesReachable_eq_empty_iff {s : State} [hs : sys.WF s] : s.boxesReachable = ∅ ↔ s.boxes = ∅

theorem Sokoban.trBox_spec_aux {s : State} [hs : sys.WF s] (h : s.boxes ≠ ∅) : s.trBox ∈ s.boxesReachable ∧ ∀ p ∈ s.boxesReachable, s.trBox.y ≤ p.y ∧ (s.trBox.y = p.y → p.x ≤ s.trBox.x)

@[simp]

theorem Sokoban.trBox_mem_iff {s : State} [hs : sys.WF s] : s.trBox ∈ s.boxesReachable ↔ s.boxes ≠ ∅

@[simp]

theorem Sokoban.trBox_mem {s : State} [hs : sys.WF s] (h : s.boxes ≠ ∅) : s.trBox ∈ s.boxesReachable

theorem Sokoban.trBox_spec' {s : State} [hs : sys.WF s] (h : s.boxes ≠ ∅) (p : PointZ) : p ∈ s.boxesReachable → s.trBox.y ≤ p.y ∧ (s.trBox.y = p.y → p.x ≤ s.trBox.x)

theorem Sokoban.trBox_spec {s : State} {p : PointZ} [hs : sys.WF s] (h : s.boxes ≠ ∅) (hp : p ∈ s.boxesReachable) : s.trBox.y ≤ p.y ∧ (s.trBox.y = p.y → p.x ≤ s.trBox.x)

theorem Sokoban.points_eq_of_reachable {s s' : State} (h : sys.Reachable s s') : s'.points = s.points

theorem Sokoban.mem_points_of_mem_boxesReachable {s : State} {p : PointZ} (h : p ∈ s.boxesReachable) : p ∈ s.points

theorem Sokoban.boxesReachable_subseq_of_reachable {s s' : State} (h : sys.Reachable s s') : s'.boxesReachable ⊆ s.boxesReachable

theorem Sokoban.size_boxesReachable_le_of_reachable {s s' : State} (h : sys.Reachable s s') : s'.boxesReachable.size ≤ s.boxesReachable.size

theorem Sokoban.exi_tr_of_boxPushed {s s' : State} (h : s.BoxPushed s') : ∃ (p : Move), sys.tr s p = some s'

theorem Sokoban.boxes_ne_of_boxPushed {s s' : State} (h : s.BoxPushed s') : s'.boxes ≠ s.boxes

theorem Sokoban.reachable_of_boxPushed {s s' : State} (h : s.BoxPushed s') : sys.Reachable s s'

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

theorem Sokoban.player'_mem_boxes_of_tr_and_boxes_ne {s s' : State} {p : Move} (h₁ : sys.tr s p = some s') (h₂ : s'.boxes ≠ s.boxes) : s'.player ∈ s.boxes

theorem Sokoban.player'_mem_boxes_of_boxPushed {s s' : State} (h : s.BoxPushed s') : s'.player ∈ s.boxes

theorem Sokoban.mem_boxesReachable_iff {s : State} {p : PointZ} : p ∈ s.boxesReachable ↔ ∃ (s' : State), sys.Reachable s s' ∧ p ∈ s'.boxes

theorem Sokoban.exi_boxPushed_of_boxes_ne {s s' : State} (h₁ : sys.Reachable s s') (h₂ : s'.boxes ≠ s.boxes) : ∃ (s₁ : State) (s₂ : State), sys.Reachable s s₁ ∧ s₁.BoxPushed s₂ ∧ sys.Reachable s₂ s'