feat: unbundle array size constraint from hash map bucket array

Std.lean

@@ -93,7 +93,6 @@ import Std.Tactic.OpenPrivate
 import Std.Tactic.PermuteGoals
 import Std.Tactic.PrintDependents
 import Std.Tactic.PrintPrefix
-import Std.Tactic.Relation.Rfl
 import Std.Tactic.SeqFocus
 import Std.Tactic.ShowUnused
 import Std.Tactic.SqueezeScope

Std/Classes/BEq.lean

@@ -16,8 +16,3 @@ class PartialEquivBEq (α) [BEq α] : Prop where
   symm : (a : α) == b → b == a
   /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
   trans : (a : α) == b → b == c → a == c
-
-@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α]
-    (a b : α) : (a == b) = false ↔ a ≠ b := by
-  rw [ne_eq, ← beq_iff_eq a b]
-  cases a == b <;> decide

Std/CodeAction/Attr.lean

@@ -124,7 +124,7 @@ initialize
           if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
           modifyEnv (tacticSeqCodeActionExt.addEntry · (decl, ← mkTacticSeqCodeAction decl))
         else
-          let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
+          let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
           if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
           modifyEnv (tacticCodeActionExt.addEntry · (⟨decl, args⟩, ← mkTacticCodeAction decl))
       | _ => pure ()

Std/CodeAction/Deprecated.lean

@@ -29,8 +29,8 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   let mut i := 0
   let doc ← readDoc
   let mut msgs := #[]
-  for diag in snap.interactiveDiags do
-    if let some #[.deprecated] := diag.tags? then
+  for m in snap.msgLog.msgs do
+    if m.data.isDeprecationWarning then
       if h : _ then
         msgs := msgs.push (snap.cmdState.messages.msgs[i])
     i := i + 1

Std/Data/Array/Basic.lean

@@ -161,11 +161,11 @@ namespace Subarray
 The empty subarray.
 -/
 protected def empty : Subarray α where
-  as := #[]
+  array := #[]
   start := 0
   stop := 0
-  h₁ := Nat.le_refl 0
-  h₂ := Nat.le_refl 0
+  start_le_stop := Nat.le_refl 0
+  stop_le_array_size := Nat.le_refl 0
 
 instance : EmptyCollection (Subarray α) :=
   ⟨Subarray.empty⟩
@@ -198,7 +198,7 @@ def popHead? (as : Subarray α) : Option (α × Subarray α) :=
       let tail :=
         { as with
           start := as.start + 1
-          h₁ := Nat.le_of_lt_succ $ Nat.succ_lt_succ h  }
+          start_le_stop := Nat.le_of_lt_succ $ Nat.succ_lt_succ h }
       some (head, tail)
     else
       none

Std/Data/Array/Lemmas.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Mario Carneiro, Gabriel Ebner
 -/
-import Std.Data.Nat.Lemmas
 import Std.Data.List.Lemmas
 import Std.Data.Array.Init.Lemmas
 import Std.Data.Array.Basic
@@ -20,12 +19,6 @@ import Std.Util.ProofWanted
 @[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
-theorem getElem?_pos [GetElem Cont Idx Elem Dom]
-    (a : Cont) (i : Idx) (h : Dom a i) [Decidable (Dom a i)] : a[i]? = a[i] := dif_pos h
-
-theorem getElem?_neg [GetElem Cont Idx Elem Dom]
-    (a : Cont) (i : Idx) (h : ¬Dom a i) [Decidable (Dom a i)] : a[i]? = none := dif_neg h
-
 @[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
 
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
@@ -93,13 +86,19 @@ theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := b
   rw [getElem?_pos, get_push_eq]
 
 theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
-  split
-  . next heq => rw [heq, getElem?_pos, get_push_eq]
-  · next hne =>
+  match Nat.lt_trichotomy i a.size with
+  | Or.inl g =>
+    have h1 : i < a.size + 1 := by omega
+    have h2 : i ≠ a.size := by omega
+    simp [getElem?, size_push, g, h1, h2, get_push_lt]
+  | Or.inr (Or.inl heq) =>
+    simp [heq, getElem?_pos, get_push_eq]
+  | Or.inr (Or.inr g) =>
     simp only [getElem?, size_push]
-    split <;> split <;> try simp only [*, get_push_lt]
-    · next p q => exact Or.elim (Nat.eq_or_lt_of_le (Nat.le_of_lt_succ p)) hne q
-    · next p q => exact p (Nat.lt.step q)
+    have h1 : ¬ (i < a.size ) := by omega
+    have h2 : ¬ (i < a.size + 1) := by omega
+    have h3 : i ≠ a.size := by omega
+    simp [h1, h2, h3]
 
 @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
   simp only [getElem?, Nat.lt_irrefl, dite_false]

Std/Data/Array/Match.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 F. G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
-import Std.Data.Nat.Lemmas
 
 namespace Array
 

Std/Data/Array/Merge.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Std.Data.Nat.Lemmas
-
 namespace Array
 
 /--

Std/Data/BinomialHeap/Basic.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Jannis Limperg, Mario Carneiro
 -/
 import Std.Classes.Order
 import Std.Control.ForInStep.Basic
-import Std.Data.Nat.Lemmas
 
 namespace Std
 namespace BinomialHeap

Std/Data/BitVec/Lemmas.lean

@@ -3,10 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/
-import Std.Data.Bool
-import Std.Data.Fin.Lemmas
-import Std.Data.Nat.Lemmas
-import Std.Util.ProofWanted
+import Std.Tactic.Alias
 
 namespace BitVec
 

Std/Data/HashMap/Basic.lean

@@ -18,21 +18,25 @@ class LawfulHashable (α : Type _) [BEq α] [Hashable α] : Prop where
 namespace Imp
 
 /--
-The bucket array of a `HashMap` is a nonempty array of `AssocList`s.
+The bucket array of a `HashMap` is an array of `AssocList`s.
 (This type is an internal implementation detail of `HashMap`.)
+All operations assume that the array is nonempty. This fact is part of `Buckets.WF`. We do not
+bundle it here for positivity reasons (see `test/collection_positivity.lean`).
 -/
-def Buckets (α : Type u) (β : Type v) := {b : Array (AssocList α β) // 0 < b.size}
+structure Buckets (α : Type u) (β : Type v) where mk' ::
+  /-- The array of `AssocList`s making up the bucket array. -/
+  b : Array (AssocList α β)
 
 namespace Buckets
 
 /-- Construct a new empty bucket array with the specified capacity. -/
-def mk (buckets := 8) (h : 0 < buckets := by decide) : Buckets α β :=
-  ⟨mkArray buckets .nil, by simp [h]⟩
+def mk (buckets := 8) : Buckets α β :=
+  ⟨mkArray buckets .nil⟩
 
 /-- Update one bucket in the bucket array with a new value. -/
 def update (data : Buckets α β) (i : USize)
     (d : AssocList α β) (h : i.toNat < data.1.size) : Buckets α β :=
-  ⟨data.1.uset i d h, (Array.size_uset ..).symm ▸ data.2⟩
+  ⟨data.1.uset i d h⟩
 
 /--
 The number of elements in the bucket array.
@@ -45,7 +49,7 @@ noncomputable def size (data : Buckets α β) : Nat := .sum (data.1.data.map (·
 
 /-- Map a function over the values in the map. -/
 @[specialize] def mapVal (f : α → β → γ) (self : Buckets α β) : Buckets α γ :=
-  ⟨self.1.map (.mapVal f), by simp [self.2]⟩
+  ⟨self.1.map (.mapVal f)⟩
 
 /--
 The well-formedness invariant for the bucket array says that every element hashes to its index
@@ -58,11 +62,15 @@ structure WF [BEq α] [Hashable α] (buckets : Buckets α β) : Prop where
   /-- Every element in a bucket should hash to its location. -/
   hash_self (i : Nat) (h : i < buckets.1.size) :
     buckets.1[i].All fun k _ => ((hash k).toUSize % buckets.1.size).toNat = i
+  /-- There must be at least one bucket. -/
+  size : 0 < buckets.1.size
 
 end Buckets
 end Imp
 
-/-- `HashMap.Imp α β` is the internal implementation type of `HashMap α β`. -/
+/-- `HashMap.Imp α β` is the implementation type of `HashMap α β` without the bundled
+    well-formedness constraint. Unlike `HashMap α β`, it is possible to use `HashMap.Imp α β` as a
+    constructor argument for an inductive type `β`, because `HashMap.Imp α β` is "positive". -/
 structure Imp (α : Type u) (β : Type v) where
   /-- The number of elements stored in the `HashMap`.
   We cache this both so that we can implement `.size` in `O(1)`, and also because we
@@ -81,16 +89,16 @@ A "load factor" of 0.75 is the usual standard for hash maps, so we return `capac
   capacity * 4 / 3
 
 /-- Constructs an empty hash map with the specified nonzero number of buckets. -/
-@[inline] def empty' (buckets := 8) (h : 0 < buckets := by decide) : Imp α β :=
-  ⟨0, .mk buckets h⟩
+@[inline] def empty' (buckets := 8) : Imp α β :=
+  ⟨0, .mk buckets⟩
 
 /-- Constructs an empty hash map with the specified target capacity. -/
 def empty (capacity := 0) : Imp α β :=
   let nbuckets := numBucketsForCapacity capacity
   let n : {n : Nat // 0 < n} :=
     if h : nbuckets = 0 then ⟨8, by decide⟩
     else ⟨nbuckets, Nat.zero_lt_of_ne_zero h⟩
-  empty' n n.2
+  empty' n
 
 /-- Calculates the bucket index from a hash value `u`. -/
 def mkIdx {n : Nat} (h : 0 < n) (u : USize) : {u : USize // u.toNat < n} :=
@@ -102,8 +110,10 @@ already in the array, which is appropriate when reinserting elements into the ar
 -/
 @[inline] def reinsertAux [Hashable α]
     (data : Buckets α β) (a : α) (b : β) : Buckets α β :=
-  let ⟨i, h⟩ := mkIdx data.2 (hash a |>.toUSize)
-  data.update i (.cons a b data.1[i]) h
+  if hd : 0 < data.1.size then
+    let ⟨i, h⟩ := mkIdx hd (hash a |>.toUSize)
+    data.update i (.cons a b data.1[i]) h
+  else data
 
 /-- Folds a monadic function over the elements in the map (in arbitrary order). -/
 @[inline] def foldM [Monad m] (f : δ → α → β → m δ) (d : δ) (map : Imp α β) : m δ :=
@@ -119,26 +129,32 @@ already in the array, which is appropriate when reinserting elements into the ar
 
 /-- Given a key `a`, returns a key-value pair in the map whose key compares equal to `a`. -/
 def findEntry? [BEq α] [Hashable α] (m : Imp α β) (a : α) : Option (α × β) :=
-  let ⟨_, buckets⟩ := m
-  let ⟨i, h⟩ := mkIdx buckets.2 (hash a |>.toUSize)
-  buckets.1[i].findEntry? a
+  if hm : 0 < m.2.1.size then
+    let ⟨_, buckets⟩ := m
+    let ⟨i, h⟩ := mkIdx hm (hash a |>.toUSize)
+    buckets.1[i].findEntry? a
+  else .none -- Will never happen for well-formed inputs
 
 /-- Looks up an element in the map with key `a`. -/
 def find? [BEq α] [Hashable α] (m : Imp α β) (a : α) : Option β :=
-  let ⟨_, buckets⟩ := m
-  let ⟨i, h⟩ := mkIdx buckets.2 (hash a |>.toUSize)
-  buckets.1[i].find? a
+  if hm : 0 < m.2.1.size then
+    let ⟨_, buckets⟩ := m
+    let ⟨i, h⟩ := mkIdx hm (hash a |>.toUSize)
+    buckets.1[i].find? a
+  else .none -- Will never happen for well-formed inputs
 
 /-- Returns true if the element `a` is in the map. -/
 def contains [BEq α] [Hashable α] (m : Imp α β) (a : α) : Bool :=
-  let ⟨_, buckets⟩ := m
-  let ⟨i, h⟩ := mkIdx buckets.2 (hash a |>.toUSize)
-  buckets.1[i].contains a
+  if hm : 0 < m.2.1.size then
+    let ⟨_, buckets⟩ := m
+    let ⟨i, h⟩ := mkIdx hm (hash a |>.toUSize)
+    buckets.1[i].contains a
+  else false -- Will never happen for well-formed inputs
 
 /-- Copies all the entries from `buckets` into a new hash map with a larger capacity. -/
 def expand [Hashable α] (size : Nat) (buckets : Buckets α β) : Imp α β :=
   let nbuckets := buckets.1.size * 2
-  { size, buckets := go 0 buckets.1 (.mk nbuckets (Nat.mul_pos buckets.2 (by decide))) }
+  { size, buckets := go 0 buckets.1 (.mk nbuckets) }
 where
   /-- Inner loop of `expand`. Copies elements `source[i:]` into `target`,
   destroying `source` in the process. -/
@@ -159,39 +175,45 @@ Inserts key-value pair `a, b` into the map.
 If an element equal to `a` is already in the map, it is replaced by `b`.
 -/
 @[inline] def insert [BEq α] [Hashable α] (m : Imp α β) (a : α) (b : β) : Imp α β :=
-  let ⟨size, buckets⟩ := m
-  let ⟨i, h⟩ := mkIdx buckets.2 (hash a |>.toUSize)
-  let bkt := buckets.1[i]
-  bif bkt.contains a then
-    ⟨size, buckets.update i (bkt.replace a b) h⟩
-  else
-    let size' := size + 1
-    let buckets' := buckets.update i (.cons a b bkt) h
-    if numBucketsForCapacity size' ≤ buckets.1.size then
-      { size := size', buckets := buckets' }
+  if hm : 0 < m.2.1.size then
+    let ⟨size, buckets⟩ := m
+    let ⟨i, h⟩ := mkIdx hm (hash a |>.toUSize)
+    let bkt := buckets.1[i]
+    bif bkt.contains a then
+      ⟨size, buckets.update i (bkt.replace a b) h⟩
     else
-      expand size' buckets'
+      let size' := size + 1
+      let buckets' := buckets.update i (.cons a b bkt) h
+      if numBucketsForCapacity size' ≤ buckets.1.size then
+        { size := size', buckets := buckets' }
+      else
+        expand size' buckets'
+  else m -- Will never happen for well-formed inputs
 
 /--
 Removes key `a` from the map. If it does not exist in the map, the map is returned unchanged.
 -/
 def erase [BEq α] [Hashable α] (m : Imp α β) (a : α) : Imp α β :=
-  let ⟨size, buckets⟩ := m
-  let ⟨i, h⟩ := mkIdx buckets.2 (hash a |>.toUSize)
-  let bkt := buckets.1[i]
-  bif bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩ else ⟨size, buckets⟩
+  if hm : 0 < m.2.1.size then
+    let ⟨size, buckets⟩ := m
+    let ⟨i, h⟩ := mkIdx hm (hash a |>.toUSize)
+    let bkt := buckets.1[i]
+    bif bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩ else ⟨size, buckets⟩
+  else m -- Will never happen for well-formed inputs
 
 /-- Map a function over the values in the map. -/
 @[inline] def mapVal (f : α → β → γ) (self : Imp α β) : Imp α γ :=
   { size := self.size, buckets := self.buckets.mapVal f }
 
 /-- Performs an in-place edit of the value, ensuring that the value is used linearly. -/
 def modify [BEq α] [Hashable α] (m : Imp α β) (a : α) (f : α → β → β) : Imp α β :=
-  let ⟨size, buckets⟩ := m
-  let ⟨i, h⟩ := mkIdx buckets.2 (hash a |>.toUSize)
-  let bkt := buckets.1[i]
-  let buckets := buckets.update i .nil h -- for linearity
-  ⟨size, buckets.update i (bkt.modify a f) ((Buckets.update_size ..).symm ▸ h)⟩
+  if hm : 0 < m.2.1.size then
+    let ⟨size, buckets⟩ := m
+    let ⟨i, h⟩ := mkIdx hm (hash a |>.toUSize)
+    let bkt := buckets.1[i]
+    let buckets := buckets.update i .nil h -- for linearity
+    ⟨size, buckets.update i (bkt.modify a f) ((Buckets.update_size ..).symm ▸ h)⟩
+  else m -- Will never happen for well-formed inputs
 
 /--
 Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` then
@@ -200,11 +222,7 @@ Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` the
 @[specialize] def filterMap {α : Type u} {β : Type v} {γ : Type w}
     (f : α → β → Option γ) (m : Imp α β) : Imp α γ :=
   let m' := m.buckets.1.mapM (m := StateT (ULift Nat) Id) (go .nil) |>.run ⟨0⟩ |>.run
-  have : m'.1.size > 0 := by
-    have := Array.size_mapM (m := StateT (ULift Nat) Id) (go .nil) m.buckets.1
-    simp [SatisfiesM_StateT_eq, SatisfiesM_Id_eq] at this
-    simp [this, Id.run, StateT.run, m.2.2, m']
-  ⟨m'.2.1, m'.1, this⟩
+  ⟨m'.2.1, ⟨m'.1⟩⟩
 where
   /-- Inner loop of `filterMap`. Note that this reverses the bucket lists,
   but this is fine since bucket lists are unordered. -/
@@ -230,15 +248,19 @@ inductive WF [BEq α] [Hashable α] : Imp α β → Prop where
     is lawful then every element hashes to its index. -/
   | mk : m.size = m.buckets.size → m.buckets.WF → WF m
   /-- The empty hash map is well formed. -/
-  | empty' : WF (empty' n h)
+  | empty' : 0 < n → WF (empty' n)
   /-- Inserting into a well formed hash map yields a well formed hash map. -/
   | insert : WF m → WF (insert m a b)
   /-- Removing an element from a well formed hash map yields a well formed hash map. -/
   | erase : WF m → WF (erase m a)
   /-- Replacing an element in a well formed hash map yields a well formed hash map. -/
   | modify : WF m → WF (modify m a f)
 
-theorem WF.empty [BEq α] [Hashable α] : WF (empty n : Imp α β) := by unfold empty; apply empty'
+theorem WF.empty [BEq α] [Hashable α] : WF (empty n : Imp α β) := by
+  dsimp only [Imp.empty]
+  split
+  · exact WF.empty' (by decide)
+  · next h => exact WF.empty' (Nat.pos_of_ne_zero h)
 
 end Imp
 

Std/Data/HashMap/Lemmas.lean

@@ -12,7 +12,7 @@ namespace Std.HashMap
 namespace Imp
 
 @[simp] theorem empty_buckets :
-    (empty : Imp α β).buckets = ⟨mkArray 8 AssocList.nil, by simp⟩ := rfl
+    (empty : Imp α β).buckets = ⟨mkArray 8 AssocList.nil⟩ := rfl
 
 @[simp] theorem empty_val [BEq α] [Hashable α] : (∅ : HashMap α β).val = Imp.empty := rfl