diff options
Diffstat (limited to 'LeanAStar')
| -rw-r--r-- | LeanAStar/Basic.lean | 2 | ||||
| -rw-r--r-- | LeanAStar/Finite.lean | 10 | ||||
| -rw-r--r-- | LeanAStar/HashSet.lean | 12 |
3 files changed, 12 insertions, 12 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₇] |