diff options
Diffstat (limited to 'LeanAStar/HashSet.lean')
| -rw-r--r-- | LeanAStar/HashSet.lean | 12 |
1 files changed, 6 insertions, 6 deletions
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₇] |