Move AStar into a separte library and use it for Day17-1

7 files changed, 61 insertions, 450 deletions

diff --git a/Common.lean b/Common.lean
index ee60dfb..6b0e329 100644
--- a/Common.lean
+++ b/Common.lean
@@ -10,7 +10,4 @@ import Common.Parsing
 import Common.Nat
 import Common.Substring
 import Common.BitVec
-import Common.Finite
-import Common.Countable
-import Common.HashSet
 import Common.Function
diff --git a/Common/Countable.lean b/Common/Countable.lean
deleted file mode 100644
index e19db99..0000000
--- a/Common/Countable.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-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
deleted file mode 100644
index 95f90a0..0000000
--- a/Common/Finite.lean
+++ /dev/null
@@ -1,186 +0,0 @@
-import Std.Data.HashSet
-import Common.Nat
-
-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.tuple_enumerate {α : Type u} [Finite α] {β : Type v} [Finite β] (x : α × β) : Fin ((Finite.cardinality α) * (Finite.cardinality β)) :=
-  let (a, b) := x
-  let idxa := (Finite.enumerate a)
-  let idxb := (Finite.enumerate b)
-  let idx := idxa.val + (Finite.cardinality α) * idxb.val
-  have h : idx < (Finite.cardinality α) * (Finite.cardinality β) :=
-    Nat.two_d_coordinate_to_index_lt_size idxa.isLt idxb.isLt
-  ⟨idx,h⟩
-
-def Finite.tuple_nth {α : Type u} [Finite α] {β : Type v} [Finite β] (idx : Fin ((Finite.cardinality α) * (Finite.cardinality β))) :=
-  let idxav := idx % (Finite.cardinality α)
-  let idxbv := idx / (Finite.cardinality α)
-  have h₁ : Finite.cardinality α > 0 :=
-    if h : 0 = Finite.cardinality α then
-      have : cardinality α * cardinality β = 0 := h.subst (motive := λx↦x*cardinality β = 0) $ Nat.zero_mul (cardinality β)
-      (Fin.cast this idx).elim0
-    else
-      Nat.pos_of_ne_zero (Ne.symm h)
-  let idxa : Fin (Finite.cardinality α) := ⟨idxav, Nat.mod_lt _ h₁⟩
-  let idxb : Fin (Finite.cardinality β):= ⟨idxbv, Nat.div_lt_of_lt_mul idx.isLt⟩
-  (Finite.nth idxa, Finite.nth idxb)
-
-theorem Finite.tuple_nth_inverse_enumerate {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite.tuple_nth (α := α) (β := β) ∘ Finite.tuple_enumerate (α := α) (β := β) = id := by
-  unfold Finite.tuple_enumerate Finite.tuple_nth
-  funext
-  simp
-  congr
-  case h.e_fst x =>
-    simp[Nat.mod_eq_of_lt]
-    rw[←Function.comp_apply (f := Finite.nth) (x := x.fst), Finite.nth_inverse_enumerate]
-    rfl
-  case h.e_snd x =>
-    have h₁ : (↑(Finite.enumerate x.fst) + (Finite.cardinality α) * ↑(Finite.enumerate x.snd)) / Finite.cardinality α = ↑(Finite.enumerate x.snd) := by
-      rw[Nat.add_mul_div_left]
-      simp[Nat.div_eq_of_lt]
-      exact Nat.zero_lt_of_lt (Finite.enumerate x.fst).isLt
-    simp[h₁]
-    rw[←Function.comp_apply (f := Finite.nth) (x := x.snd), Finite.nth_inverse_enumerate]
-    rfl
-
-theorem Finite.tuple_enumerate_inerse_nth {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite.tuple_enumerate (α := α) (β := β) ∘ Finite.tuple_nth (α := α) (β := β) = id := by
-  funext
-  unfold Finite.tuple_enumerate Finite.tuple_nth
-  simp
-  rename_i x
-  rw[Fin.eq_mk_iff_val_eq]
-  simp
-  rw[←Function.comp_apply (f := Finite.enumerate), Finite.enumerate_inverse_nth]
-  rw[←Function.comp_apply (f := Finite.enumerate), Finite.enumerate_inverse_nth]
-  simp[Nat.mod_add_div]
-
-instance {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite (Prod α β) where
-  cardinality := (Finite.cardinality α) * (Finite.cardinality β)
-  enumerate := Finite.tuple_enumerate
-  nth := Finite.tuple_nth
-  enumerate_inverse_nth := Finite.tuple_enumerate_inerse_nth
-  nth_inverse_enumerate := Finite.tuple_nth_inverse_enumerate
-
-theorem Finite.forall_nth {α : Type u} [Finite α] (p : α → Prop) (h₁ : ∀(o : Fin (Finite.cardinality α)), p (Finite.nth o)) : ∀(a : α), p a := λa↦
-  have : p ((nth ∘ enumerate) a) := Function.comp_apply.substr $ h₁ (Finite.enumerate a)
-  Finite.nth_inverse_enumerate.subst (motive := λx ↦ p (x a)) this
-
-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
deleted file mode 100644
index 3271121..0000000
--- a/Common/HashSet.lean
+++ /dev/null
@@ -1,123 +0,0 @@
-import Std.Data.HashSet
-import Common.Finite
-
-
-open Std.HashSet
-namespace Std.HashSet
-
-theorem erase_not_mem {α : Type u} [BEq α] [Hashable α] [LawfulBEq α] (set : HashSet α) (a : α) : a ∉ (set.erase a) := by
-  simp only [HashSet.mem_iff_contains, HashSet.contains_erase, beq_self_eq_true, Bool.not_true, Bool.false_and, Bool.false_eq_true, not_false_eq_true]
-
-theorem erase_not_mem_of_not_mem {α : Type u} [BEq α] [Hashable α] [LawfulBEq α] (set : HashSet α) {a : α} (b : α) (h₁ : a ∉ set) : a ∉ (set.erase b) := by
-  intro h₂
-  rw[HashSet.mem_erase] at h₂
-  exact absurd h₂.right h₁
-
-protected theorem size_le_finite_worker_size (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) (_h₁ : ∀(o : Fin (Finite.cardinality α)) (_h : o > n), Finite.nth o ∉ set), set.size ≤ (Finite.set.set_worker α HashSet.empty  n).size := by
-  intros set n h₁
-  cases n
-  case mk n h₂ =>
-  cases n
-  case zero =>
-    have h₃ : (Finite.set.set_worker α empty ⟨0,h₂⟩).size = 1 := by simp[Finite.set.set_worker, HashSet.size_insert]
-    rw[h₃]
-    cases h₄ : set.contains (Finite.nth ⟨0,h₂⟩)
-    case false =>
-      have h₅ : ∀(o : Fin (Finite.cardinality α)), Finite.nth o ∉ set := by
-        simp[←Bool.not_eq_true, ←HashSet.mem_iff_contains] at h₄
-        intro o
-        cases o
-        case mk o ho =>
-        cases o
-        case zero => exact h₄
-        case succ oo => exact h₁ ⟨oo+1, ho⟩ (Nat.succ_pos oo)
-      have h₆ : ∀(a : α), a∉set := Finite.forall_nth (λx ↦ x∉set) h₅
-      have h₇ : set.isEmpty = true := HashSet.isEmpty_iff_forall_not_mem.mpr h₆
-      have h₈ : true = (set.size == 0) := HashSet.isEmpty_eq_size_eq_zero.subst h₇.symm
-      have h₈ : set.size = 0 := beq_iff_eq.mp h₈.symm
-      rw[h₈]
-      exact Nat.zero_le _
-    case true =>
-      --show that the set from which we erase (nth 0) has size 0, just like in case false.
-      --then show that, since we removed one element, set.size equals 1.
-      let rset := set.erase $ Finite.nth ⟨0,h₂⟩
-      have h₅ : (Finite.nth ⟨0,h₂⟩) ∉ rset := erase_not_mem set (Finite.nth ⟨0,h₂⟩)
-      have h₆ : ∀(o : Fin (Finite.cardinality α)), Finite.nth o ∉ rset := by
-        intro o
-        cases o
-        case mk o ho =>
-        cases o
-        case zero => exact h₅
-        case succ oo => exact erase_not_mem_of_not_mem set _ $ h₁ ⟨oo+1, ho⟩ (Nat.succ_pos oo)
-      have h₇ : ∀(a : α), a∉rset := Finite.forall_nth (λx ↦ x∉rset) h₆
-      have h₈ : rset.isEmpty = true := HashSet.isEmpty_iff_forall_not_mem.mpr h₇
-      have h₉ : true = (rset.size == 0) := HashSet.isEmpty_eq_size_eq_zero.subst h₈.symm
-      have h₉ : rset.size = 0 := beq_iff_eq.mp h₉.symm
-      have h₁₀ : set.size ≤ rset.size + 1 := HashSet.size_le_size_erase
-      rw[h₉, Nat.zero_add] at h₁₀
-      assumption
-  case succ m =>
-    --erase (nth m) from the set and recurse.
-    --then show that the current set can only be larger by 1, and therefore fulfills the goal
-    --HashSet.size_le_size_erase
-    let rset := set.erase $ Finite.nth ⟨m+1,h₂⟩
-    have h₃ : (Finite.nth ⟨m+1,h₂⟩) ∉ rset := erase_not_mem set (Finite.nth ⟨m+1,h₂⟩)
-    have h₄ : ∀(o : Fin (Finite.cardinality α)) (h₄ : o > ⟨m,Nat.lt_of_succ_lt h₂⟩), Finite.nth o ∉ rset := by
-      intros o h₄
-      cases o
-      case mk o h₅ =>
-      cases h₆ : o == (m+1) <;> simp at h₆
-      case true =>
-        simp only[h₆]
-        exact erase_not_mem set $ Finite.nth ⟨m+1, h₂⟩
-      case false =>
-        have h₆ : o > m+1 := by simp at h₄; omega
-        exact erase_not_mem_of_not_mem _ _ (h₁ ⟨o,h₅⟩ h₆)
-    have h₅ := Std.HashSet.size_le_finite_worker_size α rset ⟨m, Nat.lt_of_succ_lt h₂⟩ h₄
-    have h₆ : (Finite.set.set_worker α empty ⟨m, Nat.lt_of_succ_lt h₂⟩).size = empty.size + m + 1 :=
-      Finite.set_worker_size α empty ⟨m, Nat.lt_of_succ_lt h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
-    have h₇ : (Finite.set.set_worker α empty ⟨m+1,h₂⟩).size = empty.size + (m + 1) + 1 :=
-      Finite.set_worker_size α empty ⟨m+1,h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
-    have h₈ := HashSet.size_le_size_erase (m := set) (k:=Finite.nth ⟨m+1,h₂⟩)
-    simp[h₆] at h₅
-    simp[h₇]
-    exact Nat.le_trans h₈ (Nat.succ_le_succ h₅)
-
-theorem size_le_finite_set_size {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) : set.size ≤ (Finite.set α).size := by
-  unfold Finite.set
-  split
-  case h_1 h₁ =>
-    if h : set.isEmpty then
-      have := HashSet.isEmpty_eq_size_eq_zero (m := set)
-      simp[h] at this
-      simp[this]
-    else
-      have := HashSet.isEmpty_eq_false_iff_exists_mem.mp (Bool.eq_false_iff.mpr h)
-      cases this
-      case intro x hx =>
-        let xx := Finite.enumerate x
-        exact (Fin.cast h₁ xx).elim0
-  case h_2 l h =>
-    exact Std.HashSet.size_le_finite_worker_size α set ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λa hx ↦
-      by
-      have h₁ := a.isLt
-      simp_arith[h] at h₁
-      have h₂ : a > l := Fin.lt_iff_val_lt_val.mp hx
-      exact absurd h₁ (Nat.not_le.mpr h₂)
-    )
-
-theorem size_le_finite_cardinality {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) : set.size ≤ Finite.cardinality α :=
-  (Finite.set_size_eq_cardinality α).subst (size_le_finite_set_size set)
-
-theorem size_lt_finite_cardinality_of_not_mem {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) (h₁ : ∃(a : α), a ∉ set) : set.size < Finite.cardinality α := by
-  have h₂ : set.size ≤ Finite.cardinality α := size_le_finite_cardinality set
-  cases h₁
-  case intro e h₁ =>
-  let iset := set.insert e
-  have h₂ : iset.size = set.size + 1 := by
-    have := HashSet.size_insert (m := set) (k := e)
-    simp[h₁] at this
-    assumption
-  have h₃ : iset.size ≤ Finite.cardinality α := size_le_finite_cardinality iset
-  rw[h₂] at h₃
-  exact Nat.lt_of_succ_le h₃
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index d878639..d68a313 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -2,7 +2,7 @@
 
 import Common.List
 import Common.Nat
-import Common.Finite
+import LeanAStar.Finite
 
 namespace Parsing
 
diff --git a/Day17.lean b/Day17.lean
index 11a92f2..769474b 100644
--- a/Day17.lean
+++ b/Day17.lean
@@ -1,6 +1,7 @@
 import Common
 import Std.Data.HashSet
 import BinaryHeap
+import LeanAStar
 
 namespace Day17
 
@@ -91,9 +92,9 @@ private def StepsInDirection.next (s : StepsInDirection) (h₁ : s ≠ .Three) :
 
 private structure PathNode (heatLossMap : HeatLossMap) where
   coordinate : heatLossMap.Coordinate
-  accumulatedCosts : Nat
   currentDirection : Direction
   takenSteps : StepsInDirection
+deriving BEq, Hashable
 
 private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heatLossMap) :=
   match node.coordinate.y, node.currentDirection, node.takenSteps with
@@ -106,7 +107,6 @@ private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heat
     let coordinate := {x := node.coordinate.x, y := ⟨y, Nat.lt_of_succ_lt h₁⟩}
     some {
       coordinate,
-      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
       currentDirection := .Up,
       takenSteps,
       }
@@ -114,7 +114,6 @@ private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heat
     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,
     }
@@ -138,7 +137,6 @@ private def PathNode.goLeft? (node : PathNode heatLossMap) : Option (PathNode he
     let coordinate := { x := ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y }
     some {
       coordinate,
-      accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate],
       currentDirection := .Left
       takenSteps
     }
@@ -146,7 +144,6 @@ private def PathNode.goLeft? (node : PathNode heatLossMap) : Option (PathNode he
     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
     }
@@ -170,7 +167,6 @@ private def PathNode.goDown? (node : PathNode heatLossMap) : Option (PathNode he
     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,
       }
@@ -178,7 +174,6 @@ private def PathNode.goDown? (node : PathNode heatLossMap) : Option (PathNode he
     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,
     }
@@ -205,7 +200,6 @@ private def PathNode.goRight? (node : PathNode heatLossMap) : Option (PathNode h
     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,
       }
@@ -213,7 +207,6 @@ private def PathNode.goRight? (node : PathNode heatLossMap) : Option (PathNode h
     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,
     }
@@ -242,20 +235,6 @@ private def PathNode.estimateMinimumCostToGoal (node : PathNode heatLossMap) : N
   }
   (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⟩,
@@ -263,134 +242,81 @@ private def PathNode.isGoal (node : PathNode heatLossMap) : Bool :=
   }
   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
+instance : LawfulBEq (PathNode heatLossMap) where
   rfl := λ {a} ↦
     match a with
-    | {coordinate, direction, steps} => by
-      unfold BEq.beq instBEqClosedSetEntry
+    | {coordinate, currentDirection, takenSteps} => by
+      unfold BEq.beq instBEqPathNode
       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₁
+    unfold BEq.beq instBEqPathNode at h₁
     cases a
     cases b
     simp! at h₁
     simp[h₁]
 
-private def ClosedSetEntry.toTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry heatLossMap) → (heatLossMap.Coordinate × Direction × StepsInDirection)
-| {coordinate, direction, steps} => (coordinate, direction, steps)
+private def PathNode.toTuple : (PathNode heatLossMap) → (heatLossMap.Coordinate × Direction × StepsInDirection)
+| {coordinate, currentDirection, takenSteps} => (coordinate, currentDirection, takenSteps)
 
-private def ClosedSetEntry.ofTuple {heatLossMap : HeatLossMap} : (heatLossMap.Coordinate × Direction × StepsInDirection) → (ClosedSetEntry heatLossMap)
-| (coordinate, direction, steps) => {coordinate, direction, steps}
+private def PathNode.ofTuple  : (heatLossMap.Coordinate × Direction × StepsInDirection) → (PathNode heatLossMap)
+| (coordinate, currentDirection, takenSteps) => {coordinate, currentDirection, takenSteps}
 
-private theorem ClosedSetEntry.toTuple_inv_ofTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry.toTuple (heatLossMap := heatLossMap)) ∘ ClosedSetEntry.ofTuple = id := rfl
-private theorem ClosedSetEntry.ofTuple_inv_toTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry.ofTuple (heatLossMap := heatLossMap)) ∘ ClosedSetEntry.toTuple = id := rfl
+private theorem PathNode.toTuple_inv_ofTuple : (PathNode.toTuple (heatLossMap := heatLossMap)) ∘ PathNode.ofTuple = id := rfl
+private theorem PathNode.ofTuple_inv_toTuple : (PathNode.ofTuple (heatLossMap := heatLossMap)) ∘ PathNode.toTuple = id := rfl
 
-instance {heatLossMap : HeatLossMap} : Finite (ClosedSetEntry heatLossMap) where
+instance : Finite (PathNode heatLossMap) where
   cardinality := Finite.cardinality (heatLossMap.Coordinate × Direction × StepsInDirection)
-  enumerate := Finite.enumerate ∘ ClosedSetEntry.toTuple
-  nth := ClosedSetEntry.ofTuple ∘ Finite.nth
+  enumerate := Finite.enumerate ∘ PathNode.toTuple
+  nth := PathNode.ofTuple ∘ Finite.nth
   enumerate_inverse_nth := by
     funext x
     rewrite[Function.comp_assoc]
     rewrite (occs := .pos [2]) [←Function.comp_assoc]
-    simp only[ClosedSetEntry.toTuple_inv_ofTuple, Function.id_comp, Finite.enumerate_inverse_nth]
+    simp only[PathNode.toTuple_inv_ofTuple, Function.id_comp, Finite.enumerate_inverse_nth]
   nth_inverse_enumerate := by
     funext x
     rewrite[Function.comp_assoc]
     rewrite (occs := .pos [2]) [←Function.comp_assoc]
-    simp only[Finite.nth_inverse_enumerate, Function.id_comp, ClosedSetEntry.ofTuple_inv_toTuple]
-
-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 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 (Finite.cardinality (ClosedSetEntry heatLossMap)) - 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 h₂ =>
-    rw[h₃]
-    have : closedSet.size < (Finite.cardinality (ClosedSetEntry heatLossMap)) := Std.HashSet.size_lt_finite_cardinality_of_not_mem closedSet ⟨_,h₂⟩
-    omega
+    simp only[Finite.nth_inverse_enumerate, Function.id_comp, PathNode.ofTuple_inv_toTuple]
+
+instance : LeanAStar.AStarNode (PathNode heatLossMap) where
+  Costs := Nat
+  costsLe := Nat.ble
+  costs_order := ⟨BinaryHeap.nat_ble_to_heap_transitive_le, BinaryHeap.nat_ble_to_heap_le_total⟩
+  remaining_costs_heuristic := PathNode.estimateMinimumCostToGoal
+  isGoal := PathNode.isGoal
+  getNeighbours := λn↦
+    let ns := n.getNeighbours
+    ns.map λn ↦ (n, heatLossMap[n.coordinate])
+end PathNode
+
+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,
+      currentDirection := .Right,
+      takenSteps := .One
+    }]
+  else
+    []
+  if h : heatLossMap.height > 1 then
+    let coordinate := {x := ⟨0, heatLossMap.not_empty.left⟩, y := ⟨1,h⟩}
+    {
+      coordinate,
+      currentDirection := .Down,
+      takenSteps := .One
+    } :: a
+  else
+    a
+
+private def HeatLossMap.startPoints (heatLossMap : HeatLossMap) : List (LeanAStar.StartPoint (PathNode heatLossMap)) :=
+  heatLossMap.start.map λx ↦ {start := x, initial_costs := heatLossMap[x.coordinate]}
 
 def part1 (heatLossMap : HeatLossMap) : Option Nat :=
-  heatLossMap.findPath (OpenSet.start heatLossMap) Std.HashSet.empty
+  have : Add Nat := inferInstance
+  LeanAStar.findLowestCosts heatLossMap.startPoints
 
 ------------------------------------------------------------------------------------
 
@@ -421,4 +347,7 @@ private def testData := "2413432311323
 
 #eval match parse testData with
 | .error _ => none
-| .ok m => HeatLossMap.findPath (OpenSet.start m) Std.HashSet.empty
+| .ok m =>
+  have : Add Nat := inferInstance
+  let r : Option Nat := LeanAStar.findLowestCosts m.startPoints
+  r
diff --git a/lakefile.lean b/lakefile.lean
index a3a080f..3c764e1 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -33,3 +33,6 @@ lean_exe «aoc-2023» where
 
 require BinaryHeap from git
   "https://github.com/soulsource/BinaryHeap"@"376e4bf573f754aa7cb8c5d6ed652f1efece3050"
+
+require «lean-astar» from git
+  "https://github.com/soulsource/lean-astar"@"3514e38cf48b611abc808b7de4c13862d3a4ede0"