Continue Day17

7 files changed, 450 insertions, 8 deletions

diff --git a/Common.lean b/Common.lean
index becafd3..4432bcd 100644
--- a/Common.lean
+++ b/Common.lean
@@ -10,3 +10,6 @@ import Common.Parsing
 import Common.Nat
 import Common.Substring
 import Common.BitVec
+import Common.Finite
+import Common.Countable
+import Common.HashSet
diff --git a/Common/Countable.lean b/Common/Countable.lean
new file mode 100644
index 0000000..e19db99
--- /dev/null
+++ b/Common/Countable.lean
@@ -0,0 +1,9 @@
+import Common.Finite
+
+class Countable (α : Type u) where
+  enumerate : α → Nat
+  injective {a b : α} : enumerate a = enumerate b → a = b
+
+instance {α : Type u} [Finite α] : Countable α where
+  enumerate := Fin.val ∘ Finite.enumerate
+  injective :=  Finite.injective ∘ Fin.val_inj.mp
diff --git a/Common/Finite.lean b/Common/Finite.lean
new file mode 100644
index 0000000..25041a8
--- /dev/null
+++ b/Common/Finite.lean
@@ -0,0 +1,123 @@
+import Std.Data.HashSet
+
+class Finite (α : Type u) where
+  cardinality : Nat
+  enumerate : α → Fin cardinality
+  nth : Fin cardinality → α
+  nth_inverse_enumerate : nth ∘ enumerate = id
+  enumerate_inverse_nth : enumerate ∘ nth = id
+
+theorem Finite.surjective {α : Type u} [Finite α] {a b : Fin (Finite.cardinality α)} : nth a = nth b → a = b := λh₃ ↦
+  have h₁ := Finite.enumerate_inverse_nth (α := α)
+  have h₄ := congrArg enumerate h₃
+  have h₂ : ∀(x : Fin (Finite.cardinality α)), (enumerate ∘ nth) x = x := λ_↦h₁.substr rfl
+  have h₅ := Function.comp_apply.subst (h₂ a).symm
+  have h₆ := Function.comp_apply.subst (h₂ b).symm
+  h₅.substr $ h₆.substr h₄
+
+theorem Finite.injective {α : Type u} [Finite α] {a b : α} : enumerate a = enumerate b → a = b := λh₁↦
+  have h₂ := Finite.nth_inverse_enumerate (α := α)
+  have h₃ := congrArg nth h₁
+  have h₄ : ∀(x : α), (nth ∘ enumerate) x = x := λ_↦h₂.substr rfl
+  have h₅ := Function.comp_apply.subst (h₄ a).symm
+  have h₆ := Function.comp_apply.subst (h₄ b).symm
+  h₅.substr $ h₆.substr h₃
+
+def Finite.set (α : Type u) [Finite α] [BEq α] [Hashable α] : Std.HashSet α :=
+  match h: (Finite.cardinality α) with
+  | 0 => Std.HashSet.empty
+  | l+1 => set_worker Std.HashSet.empty ⟨l,h.substr (p := λx ↦ l < x) $ Nat.lt.base l⟩
+where set_worker (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) : Std.HashSet α :=
+  let e := Finite.nth n
+  let set := set.insert e
+  match n with
+  | ⟨0,_⟩ => set
+  | ⟨m+1,h₁⟩ => set_worker set ⟨m, Nat.lt_of_succ_lt h₁⟩
+
+protected theorem Finite.set_worker_contains_self' (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] (a : α) (oldSet : Std.HashSet α) (h₁ : oldSet.contains a) (n : Fin (Finite.cardinality α)) : (Finite.set.set_worker α oldSet n).contains a := by
+  cases n
+  case mk n h₂ =>
+    induction n generalizing oldSet
+    case zero => unfold set.set_worker; simp[h₁]
+    case succ m hm =>
+      unfold set.set_worker
+      exact hm (oldSet.insert (nth ⟨m + 1, h₂⟩)) (by simp[h₁]) (Nat.lt_of_succ_lt h₂)
+
+protected theorem Finite.set_worker_contains_self (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α) (set : Std.HashSet α), (Finite.set.set_worker α set (Finite.enumerate a)).contains a := by
+  intros a oldSet
+  unfold set.set_worker
+  rw[←Function.comp_apply (f := nth), Finite.nth_inverse_enumerate, id_def]
+  split
+  case h_1 => apply Std.HashSet.contains_insert_self
+  case h_2 =>
+    apply Finite.set_worker_contains_self'
+    exact Std.HashSet.contains_insert_self
+
+protected theorem Finite.set_worker_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α) (set : Std.HashSet α) (o : Nat) (h₁ : Finite.enumerate a + o < Finite.cardinality α), (Finite.set.set_worker α set ⟨Finite.enumerate a + o, h₁⟩).contains a := by
+  intros a oldSet offset h₁
+  induction offset generalizing oldSet
+  case zero =>
+    exact Finite.set_worker_contains_self _ _ _
+  case succ p hi =>
+    unfold set.set_worker
+    simp
+    have : ↑(enumerate a) + p < cardinality α := Nat.lt_of_succ_lt $ (Nat.add_assoc (enumerate a) p 1).substr h₁
+    exact hi (oldSet.insert (nth ⟨↑(enumerate a) + (p + 1), h₁⟩)) this
+
+theorem Finite.set_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α), (Finite.set α).contains a := λa ↦ by
+    unfold set
+    split
+    case h_1 h => exact (Fin.cast h $ Finite.enumerate a).elim0
+    case h_2 l h =>
+      let o := l - enumerate a
+      have h₁ : (Finite.enumerate a).val + o = l := by omega
+      have h₂ := Finite.set_worker_contains _ a Std.HashSet.empty o (by omega)
+      simp[h₁] at h₂
+      assumption
+
+protected theorem Finite.set_worker_size (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α]
+: ∀(set : Std.HashSet α) (n : Fin (Finite.cardinality α)) (_ : ∀(x : Fin (Finite.cardinality α)) (_ : x ≤ n),
+   ¬set.contains (Finite.nth x)), (Finite.set.set_worker α set n).size = set.size + n + 1
+:= by
+  intros set n h₂
+  simp at h₂
+  unfold Finite.set.set_worker
+  cases n
+  case mk n h₁ =>
+    split
+    case h_1 m isLt he =>
+      simp at he
+      simp[Std.HashSet.size_insert, Std.HashSet.mem_iff_contains, h₂, he]
+    case h_2 m isLt he =>
+      simp
+      have h₄ : m < n := have : n = m.succ := Fin.val_eq_of_eq he; this.substr (Nat.lt_succ_self m)
+      have h₅ : ∀ (x : Fin (cardinality α)), x ≤ ⟨m, Nat.lt_of_succ_lt isLt⟩ → ¬(set.insert (nth ⟨n, h₁⟩)).contains (nth x) = true := by
+        simp
+        intros x hx
+        constructor
+        case right => exact h₂ x (Nat.le_trans hx (Nat.le_of_lt h₄))
+        case left =>
+          have h₅ : x ≠ ⟨n, h₁⟩ := Fin.ne_of_val_ne $ Nat.ne_of_lt $ Nat.lt_of_le_of_lt hx h₄
+          have h₆ := Finite.surjective (α := α) (a := x) (b := ⟨n,h₁⟩)
+          exact Ne.symm (h₅ ∘ h₆)
+      have h₃ := Finite.set_worker_size α (set.insert (nth ⟨n, h₁⟩)) ⟨m, Nat.lt_of_succ_lt isLt⟩ (h₅)
+      rw[h₃]
+      simp at he
+      simp[he, Std.HashSet.size_insert]
+      split
+      case isFalse => rw[Nat.add_assoc, Nat.add_comm 1 m]
+      case isTrue hx =>
+        subst n
+        have h₂ := h₂ ⟨m+1,h₁⟩ (Fin.le_refl _)
+        have hx := Std.HashSet.mem_iff_contains.mp hx
+        exact absurd hx (Bool.eq_false_iff.mp h₂)
+termination_by _ n => n.val
+
+theorem Finite.set_size_eq_cardinality (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : (Finite.set α).size = Finite.cardinality α := by
+  unfold set
+  split
+  case h_1 h => exact Std.HashSet.size_empty.substr h.symm
+  case h_2 l h =>
+    rewrite(occs := .pos [3])[h]
+    have := Finite.set_worker_size α Std.HashSet.empty ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λx _↦Bool.eq_false_iff.mp (Std.HashSet.contains_empty (a:=Finite.nth x)))
+    simp only [this, Std.HashSet.size_empty, Nat.zero_add]
diff --git a/Common/HashSet.lean b/Common/HashSet.lean
new file mode 100644
index 0000000..1845443
--- /dev/null
+++ b/Common/HashSet.lean
@@ -0,0 +1,9 @@
+import Std.Data.HashSet
+import Common.Finite
+
+open Std.HashSet
+namespace Std.HashSet
+
+theorem finite_size {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) : set.size ≤ Finite.cardinality α := by
+
+  sorry
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 637f807..ebc5589 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -24,6 +24,18 @@ structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where
 instance {grid : RectangularGrid Element} : BEq grid.Coordinate where
   beq := λa b ↦ a.x == b.x && a.y == b.y
 
+instance {grid : RectangularGrid Element} : LawfulBEq grid.Coordinate where
+  rfl := λ{a} ↦ by
+    unfold BEq.beq instBEqCoordinate
+    simp only [beq_self_eq_true, Bool.and_self]
+  eq_of_beq := λ{a b} h₁ ↦ by
+    unfold BEq.beq instBEqCoordinate at h₁
+    simp only [Bool.and_eq_true, beq_iff_eq] at h₁
+    cases a
+    cases b
+    simp at h₁ ⊢
+    assumption
+
 instance {grid : RectangularGrid Element} : Hashable grid.Coordinate where
   hash := λa ↦ Hashable.hash (a.x, a.y)
 
diff --git a/Day17.lean b/Day17.lean
index 496b40c..602ae39 100644
--- a/Day17.lean
+++ b/Day17.lean
@@ -1,4 +1,6 @@
 import Common
+import Std.Data.HashSet
+import BinaryHeap
 
 namespace Day17
 
@@ -38,7 +40,7 @@ private inductive Direction
 | Right
 | Down
 | Left
-deriving BEq
+deriving BEq, Hashable
 
 instance : LawfulBEq Direction where
   rfl := λ{x} ↦ by cases x <;> rfl
@@ -48,6 +50,11 @@ private inductive StepsInDirection
 | One
 | Two
 | Three
+deriving BEq, Hashable
+
+instance : LawfulBEq StepsInDirection where
+  rfl := λ{x} ↦ by cases x <;> rfl
+  eq_of_beq := λ {a b} ↦ by cases a <;> cases b <;> simp <;> rfl
 
 private def StepsInDirection.next (s : StepsInDirection) (h₁ : s ≠ .Three) : StepsInDirection :=
   match s with
@@ -63,14 +70,293 @@ private structure PathNode (heatLossMap : HeatLossMap) where
 private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heatLossMap) :=
   match node.coordinate.y, node.currentDirection, node.takenSteps with
   | ⟨0,_⟩, _, _ => none
-  | _, Direction.Up, StepsInDirection.Three => none
-  | ⟨y,h₂⟩, Direction.Up, steps@h₁:StepsInDirection.One | ⟨y,h₂⟩, Direction.Up, steps@h₁:StepsInDirection.Two =>
-    have : steps ≠ .Three := λx ↦ StepsInDirection.noConfusion (x.subst h₁.symm)
-    sorry
-  | ⟨y,h₂⟩, _, _ => sorry
+  | ⟨_+1,_⟩, .Down, _ => none -- can't go back
+  | ⟨_+1,_⟩, .Up, .Three => none
+  | ⟨y+1,h₁⟩, .Up, steps@h₂:.One | ⟨y+1,h₁⟩, .Up, steps@h₂:.Two =>
+    have : steps ≠ .Three := λh₃ ↦ StepsInDirection.noConfusion (h₃.subst h₂.symm)
+    let takenSteps := steps.next this
+    let coordinate := {x := node.coordinate.x, y := ⟨y, Nat.lt_of_succ_lt h₁⟩}
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Up,
+      takenSteps,
+      }
+  | ⟨y+1,h₁⟩, .Left, _ | ⟨y+1,h₁⟩, .Right, _ =>
+    let coordinate := { x := node.coordinate.x, y := ⟨y, Nat.lt_of_succ_lt h₁⟩}
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Up,
+      takenSteps := .One,
+    }
+
+--since I made mistakes, rather add verification
+private theorem PathNode.goUp_goes_up (node result : PathNode heatLossMap) (h₁ : some result = node.goUp?) : result.currentDirection = .Up := by
+  unfold PathNode.goUp? at h₁
+  split at h₁ <;> simp_all
+private theorem PathNode.goUp_y_pred (node result : PathNode heatLossMap) (h₁ : some result = node.goUp?) : result.coordinate.y.val.succ = node.coordinate.y.val := by
+  unfold PathNode.goUp? at h₁
+  split at h₁ <;> simp_all
+
+private def PathNode.goLeft? (node : PathNode heatLossMap) : Option (PathNode heatLossMap) :=
+  match node.coordinate.x, node.currentDirection, node.takenSteps with
+  | ⟨0,_⟩, _, _ => none
+  | ⟨_+1,_⟩, .Right, _ => none -- can't go back
+  | ⟨_+1,_⟩, .Left, .Three => none
+  | ⟨x+1,h₁⟩, .Left, steps@h₂:.One | ⟨x+1,h₁⟩, .Left, steps@h₂:.Two =>
+    have : steps ≠ .Three := λh₃ ↦ StepsInDirection.noConfusion (h₃.subst h₂.symm)
+    let takenSteps := steps.next this
+    let coordinate := { x := ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y }
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Left
+      takenSteps
+    }
+  | ⟨x+1,h₁⟩, .Up, _ | ⟨x+1,h₁⟩, .Down, _ =>
+    let coordinate := { x := ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y }
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Left
+      takenSteps := .One
+    }
+
+--since I made mistakes, rather add verification
+private theorem PathNode.goLeft_goes_left (node result : PathNode heatLossMap) (h₁ : some result = node.goLeft?) : result.currentDirection = .Left := by
+  unfold PathNode.goLeft? at h₁
+  split at h₁ <;> simp_all
+private theorem PathNode.goLeft_x_pred (node result : PathNode heatLossMap) (h₁ : some result = node.goLeft?) : result.coordinate.x.val.succ = node.coordinate.x.val := by
+  unfold PathNode.goLeft? at h₁
+  split at h₁ <;> simp_all
+
+private def PathNode.goDown? (node : PathNode heatLossMap) : Option (PathNode heatLossMap) :=
+  match node.coordinate.y.rev, node.currentDirection, node.takenSteps with
+  | ⟨0,_⟩, _, _ => none
+  | ⟨_+1,_⟩, .Up, _ => none -- can't go back
+  | ⟨_+1,_⟩, .Down, .Three => none
+  | ⟨y+1,h₁⟩, .Down, steps@h₂:.One | ⟨y+1,h₁⟩, .Down, steps@h₂:.Two =>
+    have : steps ≠ .Three := λh₃ ↦ StepsInDirection.noConfusion (h₃.subst h₂.symm)
+    let takenSteps := steps.next this
+    let coordinate := {x := node.coordinate.x, y := Fin.rev ⟨y, Nat.lt_of_succ_lt h₁⟩}
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Down,
+      takenSteps,
+      }
+  | ⟨y+1,h₁⟩, .Left, _ | ⟨y+1,h₁⟩, .Right, _  =>
+    let coordinate := { x := node.coordinate.x, y := Fin.rev ⟨y, Nat.lt_of_succ_lt h₁⟩}
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Down,
+      takenSteps := .One,
+    }
+
+--since I made mistakes, rather add verification
+private theorem PathNode.goDown_goes_down (node result : PathNode heatLossMap) (h₁ : some result = node.goDown?) : result.currentDirection = .Down := by
+  unfold PathNode.goDown? at h₁
+  split at h₁ <;> simp_all
+private theorem PathNode.goDown_y_succ (node result : PathNode heatLossMap) (h₁ : some result = node.goDown?) : result.coordinate.y.val = node.coordinate.y.val.succ := by
+  unfold PathNode.goDown? at h₁
+  split at h₁ <;> simp at h₁
+  all_goals
+    simp_all[Fin.rev]
+    omega
+
+private def PathNode.goRight? (node : PathNode heatLossMap) : Option (PathNode heatLossMap) :=
+  match node.coordinate.x.rev, node.currentDirection, node.takenSteps with
+  | ⟨0,_⟩, _, _ => none
+  | ⟨_+1,_⟩, .Left, _ => none -- can't go back
+  | ⟨_+1,_⟩, .Right, .Three => none
+  | ⟨x+1,h₁⟩, .Right, steps@h₂:.One | ⟨x+1,h₁⟩, .Right, steps@h₂:.Two =>
+    have : steps ≠ .Three := λh₃ ↦ StepsInDirection.noConfusion (h₃.subst h₂.symm)
+    let takenSteps := steps.next this
+    let coordinate := {x := Fin.rev ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y}
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Right,
+      takenSteps,
+      }
+  | ⟨x+1,h₁⟩, .Down, _ | ⟨x+1,h₁⟩, .Up, _  =>
+    let coordinate := {x := Fin.rev ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y}
+    some {
+      coordinate,
+      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
+      currentDirection := .Right,
+      takenSteps := .One,
+    }
+
+--since I made mistakes, rather add verification
+private theorem PathNode.goRightt_goes_right (node result : PathNode heatLossMap) (h₁ : some result = node.goRight?) : result.currentDirection = .Right := by
+  unfold PathNode.goRight? at h₁
+  split at h₁ <;> simp_all
+private theorem PathNode.goRight_x_succ (node result : PathNode heatLossMap) (h₁ : some result = node.goRight?) : result.coordinate.x.val = node.coordinate.x.val.succ := by
+  unfold PathNode.goRight? at h₁
+  split at h₁ <;> simp at h₁
+  all_goals
+    simp_all[Fin.rev]
+    omega
 
 private def PathNode.getNeighbours (node : PathNode heatLossMap) : List (PathNode heatLossMap) :=
-  sorry
+  [node.goLeft?, node.goUp?, node.goRight?, node.goDown?].filterMap id
+
+private def PathNode.estimateMinimumCostToGoal (node : PathNode heatLossMap) : Nat :=
+  --costs cannot be lower than 1, so the minimum is just the Manhattan Distance
+  --this is a dumb estimate, only true if there is a perfect diagonal path, but should be good enough.
+  --also, it must never overestimate, sooo
+  let goal : heatLossMap.Coordinate := {
+    x := ⟨heatLossMap.width - 1, Nat.pred_lt_self heatLossMap.not_empty.left⟩,
+    y := ⟨heatLossMap.height - 1, Nat.pred_lt_self heatLossMap.not_empty.right⟩,
+  }
+  (goal.x - node.coordinate.x : Fin _).val + (goal.y - node.coordinate.y : Fin _).val
+
+private def PathNode.heuristics (node : PathNode heatLossMap) : Nat :=
+  node.estimateMinimumCostToGoal + node.accumulatedCosts
+
+private def PathNode.heuristicsLe (a b : PathNode heatLossMap) : Bool :=
+  Nat.ble a.heuristics b.heuristics
+
+theorem PathNode.heuristicsLe_transitive : BinaryHeap.transitive_le (PathNode.heuristicsLe (heatLossMap := heatLossMap)) :=
+  λa b c ↦ BinaryHeap.nat_ble_to_heap_transitive_le a.heuristics b.heuristics c.heuristics
+
+theorem PathNode.heuristicsLe_total : BinaryHeap.total_le (PathNode.heuristicsLe (heatLossMap := heatLossMap)) :=
+  λa b ↦ BinaryHeap.nat_ble_to_heap_le_total a.heuristics b.heuristics
+
+private theorem PathNode.heuristicsLe_total_and_transitive : BinaryHeap.TotalAndTransitiveLe (PathNode.heuristicsLe (heatLossMap := heatLossMap)) := ⟨PathNode.heuristicsLe_transitive, PathNode.heuristicsLe_total⟩
 
+private def PathNode.isGoal (node : PathNode heatLossMap) : Bool :=
+  let goal : heatLossMap.Coordinate := {
+    x := ⟨heatLossMap.width - 1, Nat.pred_lt_self heatLossMap.not_empty.left⟩,
+    y := ⟨heatLossMap.height - 1, Nat.pred_lt_self heatLossMap.not_empty.right⟩,
+  }
+  node.coordinate == goal
 
 end PathNode
+
+abbrev OpenSet (heatLossMap : HeatLossMap) := BinaryHeap (PathNode heatLossMap) PathNode.heuristicsLe
+
+private def HeatLossMap.start (heatLossMap : HeatLossMap) : List (PathNode heatLossMap) :=
+  let a : List (PathNode heatLossMap) := if h : heatLossMap.width > 1 then
+    let coordinate := {x := ⟨1,h⟩, y := ⟨0, heatLossMap.not_empty.right⟩ }
+    [{
+      coordinate,
+      accumulatedCosts := heatLossMap[coordinate],
+      currentDirection := .Right,
+      takenSteps := .One
+    }]
+  else
+    []
+  if h : heatLossMap.height > 1 then
+    let coordinate := {x := ⟨0, heatLossMap.not_empty.left⟩, y := ⟨1,h⟩}
+    {
+      coordinate,
+      accumulatedCosts := heatLossMap[coordinate]
+      currentDirection := .Down,
+      takenSteps := .One
+    } :: a
+  else
+    a
+
+private def OpenSet.start (heatLossMap : HeatLossMap) : OpenSet heatLossMap (heatLossMap.start.length) :=
+  --we cannot add the start tile directly - it's invalid state, as it doesn't have a direction
+  BinaryHeap.ofList PathNode.heuristicsLe_total_and_transitive heatLossMap.start
+
+private structure ClosedSetEntry (heatLossMap : HeatLossMap) where
+  coordinate : heatLossMap.Coordinate
+  direction : Direction
+  steps : StepsInDirection
+deriving BEq, Hashable
+
+instance {heatLossMap : HeatLossMap} : LawfulBEq (ClosedSetEntry heatLossMap) where
+  rfl := λ {a} ↦
+    match a with
+    | {coordinate, direction, steps} => by
+      unfold BEq.beq instBEqClosedSetEntry
+      simp! --no clue how to rename an unnamed function in the goal
+  eq_of_beq := λ{a b} h₁ ↦ by
+    unfold BEq.beq instBEqClosedSetEntry at h₁
+    cases a
+    cases b
+    simp! at h₁
+    simp[h₁]
+
+instance {heatLossMap : HeatLossMap} : Coe (PathNode heatLossMap) (ClosedSetEntry heatLossMap) where
+  coe := λ{coordinate, currentDirection, takenSteps, ..} ↦ {coordinate, direction := currentDirection, steps := takenSteps}
+
+abbrev ClosedSet (heatLossMap : HeatLossMap) := Std.HashSet (ClosedSetEntry heatLossMap)
+
+private def OpenSet.findFirstNotInClosedSet {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) : Option ((r : Nat) × PathNode heatLossMap × OpenSet heatLossMap r) :=
+  match n, openSet with
+  | 0, _ => none
+  | m+1, openSet =>
+    let (node, openSet) := openSet.pop
+    if closedSet.contains node then
+      findFirstNotInClosedSet openSet closedSet
+    else
+      some ⟨m, node, openSet⟩
+
+private theorem OpenSet.findFirstNotInClosedSet_not_in_closed_set {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) {result : (r : Nat) × PathNode heatLossMap × OpenSet heatLossMap r} (h₁ : openSet.findFirstNotInClosedSet closedSet = some result) : ¬closedSet.contains result.snd.fst := by
+  simp
+  unfold findFirstNotInClosedSet at h₁
+  split at h₁; contradiction
+  simp at h₁
+  split at h₁
+  case h_2.isTrue =>
+    have h₃ := findFirstNotInClosedSet_not_in_closed_set _ closedSet h₁
+    simp at h₃
+    assumption
+  case h_2.isFalse h₂ =>
+    simp at h₂ h₁
+    subst result
+    assumption
+
+private partial def HeatLossMap.findPath {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) : Option Nat :=
+  match h₁ : openSet.findFirstNotInClosedSet closedSet with
+  | none => none
+  | some ⟨_,(node, openSet)⟩ =>
+    if node.isGoal then
+      some node.accumulatedCosts
+    else
+      let neighbours := node.getNeighbours.filter (not ∘ closedSet.contains ∘ Coe.coe)
+      let newClosedSet := closedSet.insert node
+      let openSet := openSet.pushList neighbours
+      findPath openSet newClosedSet
+--termination_by (ClosedSet.full heatLossMap).size - closedSet.size
+--decreasing_by
+--  have h₃ := Std.HashSet.size_insert (m := closedSet) (k := { coordinate := node.coordinate, direction := node.currentDirection, steps := node.takenSteps })
+--  split at h₃
+--  case isTrue =>
+--    have := OpenSet.findFirstNotInClosedSet_not_in_closed_set _ _ h₁
+--    contradiction
+--  case isFalse oldOpenSet h₂ =>
+--    rw[h₃]
+--    have : closedSet.size < (ClosedSet.full heatLossMap).size := sorry --contradiction, h₂, ClosedSet.full_is_full, Std.HashSet.size_insert
+--    omega
+
+
+
+------------------------------------------------------------------------------------
+
+private def testData := "2413432311323
+3215453535623
+3255245654254
+3446585845452
+4546657867536
+1438598798454
+4457876987766
+3637877979653
+4654967986887
+4564679986453
+1224686865563
+2546548887735
+4322674655533"
+
+#eval parse testData
+
+#eval match parse testData with
+| .error _ => none
+| .ok m => HeatLossMap.findPath (OpenSet.start m) Std.HashSet.empty
diff --git a/lakefile.lean b/lakefile.lean
index ae32628..a3a080f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -32,4 +32,4 @@ lean_exe «aoc-2023» where
   supportInterpreter := true
 
 require BinaryHeap from git
-  "https://github.com/soulsource/BinaryHeap"@"9a4169ce63e9d1c0e3e909174cbc43bd53526ae4"
+  "https://github.com/soulsource/BinaryHeap"@"376e4bf573f754aa7cb8c5d6ed652f1efece3050"