Lean 4.19

6 files changed, 15 insertions, 18 deletions

diff --git a/LeanAStar/Basic.lean b/LeanAStar/Basic.lean
index a2920f1..f4b972e 100644
--- a/LeanAStar/Basic.lean
+++ b/LeanAStar/Basic.lean
@@ -143,7 +143,7 @@ protected instance {α : Type u} [AStarNode α Costs] [LawfulBEq α] : LawfulBEq
 def findLowestCosts {α : Type u} [AStarNode α Costs] [Add Costs] [LawfulBEq α] (starts : List (StartPoint (α := α))) : Option Costs :=
   let openSet := BinaryHeap.ofList ⟨OpenSetEntry.le_trans, OpenSetEntry.le_total⟩ $ starts.map λ{start, initial_costs}↦
     {node := start, accumulated_costs := initial_costs, estimated_total_costs:= AStarNode.remaining_costs_heuristic start : LeanAStar.OpenSetEntry α}
-  LeanAStar.findPath_Aux openSet Std.HashSet.empty
+  LeanAStar.findPath_Aux openSet Std.HashSet.emptyWithCapacity
 
 /-- Helper to not only get the lowest costs, but also the shortest path. Could be implemented more efficient. -/
 def findShortestPath {α : Type u} [AStarNode α Costs] [Add Costs] [LawfulBEq α] (starts : List (StartPoint (α := α))) : Option (Costs × List α) :=
diff --git a/LeanAStar/Finite.lean b/LeanAStar/Finite.lean
index 4c1455f..302e3b1 100644
--- a/LeanAStar/Finite.lean
+++ b/LeanAStar/Finite.lean
@@ -102,8 +102,8 @@ theorem Finite.forall_nth {α : Type u} [Finite α] (p : α → Prop) (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⟩
+  | 0 => Std.HashSet.emptyWithCapacity
+  | l+1 => set_worker Std.HashSet.emptyWithCapacity ⟨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
@@ -148,7 +148,7 @@ theorem Finite.set_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [La
   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)
+    have h₂ := Finite.set_worker_contains _ a Std.HashSet.emptyWithCapacity o (by omega)
     simp[h₁] at h₂
     assumption
 
@@ -196,5 +196,5 @@ theorem Finite.set_size_eq_cardinality (α : Type u) [Finite α] [BEq α] [Hasha
   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]
+    have := Finite.set_worker_size α Std.HashSet.emptyWithCapacity ⟨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_emptyWithCapacity, Nat.zero_add, Nat.succ_eq_add_one]
diff --git a/LeanAStar/HashSet.lean b/LeanAStar/HashSet.lean
index c73216e..87f351a 100644
--- a/LeanAStar/HashSet.lean
+++ b/LeanAStar/HashSet.lean
@@ -12,13 +12,13 @@ theorem erase_not_mem_of_not_mem {α : Type u} [BEq α] [Hashable α] [LawfulBEq
   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
+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.emptyWithCapacity  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]
+    have h₃ : (Finite.set.set_worker α emptyWithCapacity ⟨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 =>
@@ -73,10 +73,10 @@ protected theorem size_le_finite_worker_size (α : Type u) [Finite α] [BEq α]
         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₆ : (Finite.set.set_worker α emptyWithCapacity ⟨m, Nat.lt_of_succ_lt h₂⟩).size = emptyWithCapacity.size + m + 1 :=
+      Finite.set_worker_size α emptyWithCapacity ⟨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 α emptyWithCapacity ⟨m+1,h₂⟩).size = emptyWithCapacity.size + (m + 1) + 1 :=
+      Finite.set_worker_size α emptyWithCapacity ⟨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₇]
diff --git a/lake-manifest.json b/lake-manifest.json
index 723a9b7..be02118 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "60832223e03e50cbffca8bc90b1dec40b48f1f14",
+   "rev": "93c883d5332469d90a4f1c42d45c66e2b6a89eb8",
    "name": "BinaryHeap",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lakefile.toml b/lakefile.toml
index 957dbdd..c252c82 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,13 +6,10 @@ testDriver = "LeanAStarTest"
 [[lean_lib]]
 name = "LeanAStar"
 
-[[lean_lib]]
-name = "LeanAStarTest"
-
 [[lean_exe]]
 name = "LeanAStarTest"
 
 [[require]]
 name = "BinaryHeap"
 git = "http://git.grois.info/BinaryHeap"
-revision = "60832223e03e50cbffca8bc90b1dec40b48f1f14"
\ No newline at end of file
+revision = "93c883d5332469d90a4f1c42d45c66e2b6a89eb8"
\ No newline at end of file
diff --git a/lean-toolchain b/lean-toolchain
index 9f78e65..a0922e9 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.18.0
+leanprover/lean4:4.19.0