feat: additional collection operations

Co-authored-by: Mac Malone <tydeu@hatpress.net>

src/Init/Data/Array/Basic.lean

@@ -10,7 +10,7 @@ import Init.Data.Fin.Basic
 import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
-import Init.Util
+import Init.GetElem
 universe u v w
 
 namespace Array
@@ -59,6 +59,8 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 

src/Init/Data/Array/Subarray.lean

@@ -32,6 +32,8 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
+
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/ByteArray/Basic.lean

@@ -52,9 +52,13 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
+
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩

src/Init/Data/Fin/Basic.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
-import Init.Data.Nat.Div
 import Init.Data.Nat.Bitwise.Basic
-import Init.Coe
 
 open Nat
 
@@ -170,9 +168,3 @@ theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1
 theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := h
 
 end Fin
-
-instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
-  getElem xs i h := getElem xs i.1 h
-
-macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

src/Init/Data/FloatArray/Basic.lean

@@ -58,9 +58,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
+
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
+
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/List/Basic.lean

@@ -7,6 +7,7 @@ prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
+
 set_option linter.missingDocs true -- keep it documented
 open Decidable List
 
@@ -54,15 +55,6 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 namespace List
 
-instance : GetElem (List α) Nat α fun as i => i < as.length where
-  getElem as i h := as.get ⟨i, h⟩
-
-@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
-  rfl
-
-@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
-  rfl
-
 theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n := by
   induction as generalizing n with
   | nil  => simp [length, lengthTRAux]
@@ -520,11 +512,6 @@ def drop : Nat → List α → List α
 @[simp] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
 
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
-  match as, i with
-  | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
-
 /--
 `O(min n |xs|)`. Returns the first `n` elements of `xs`, or the whole list if `n` is too large.
 * `take 0 [a, b, c, d, e] = []`

src/Init/GetElem.lean

@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Util
+
+@[never_extract]
+private def outOfBounds [Inhabited α] : α :=
+  panic! "index out of bounds"
+
+/--
+The class `GetElem cont idx elem dom` implements the `xs[i]` notation.
+When you write this, given `xs : cont` and `i : idx`, Lean looks for an instance
+of `GetElem cont idx elem dom`. Here `elem` is the type of `xs[i]`, while
+`dom` is whatever proof side conditions are required to make this applicable.
+For example, the instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
+
+The proof side-condition `dom xs i` is automatically dispatched by the
+`get_elem_tactic` tactic, which can be extended by adding more clauses to
+`get_elem_tactic_trivial`.
+-/
+class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
+  /--
+  The syntax `arr[i]` gets the `i`'th element of the collection `arr`.
+  If there are proof side conditions to the application, they will be automatically
+  inferred by the `get_elem_tactic` tactic.
+
+  The actual behavior of this class is type-dependent,
+  but here are some important implementations:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`:
+    does array indexing with no bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list,
+    with proof side goal `i < l.length`.
+  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
+    no side goal (returns `.missing` out of range)
+
+  There are other variations on this syntax:
+  * `arr[i]`: proves the proof side goal by `get_elem_tactic`
+  * `arr[i]!`: panics if the side goal is false
+  * `arr[i]?`: returns `none` if the side goal is false
+  * `arr[i]'h`: uses `h` to prove the side goal
+  -/
+  getElem (xs : cont) (i : idx) (h : dom xs i) : elem
+
+  getElem? (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
+    if h : _ then some (getElem xs i h) else none
+
+  getElem! [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem (getElem getElem! getElem?)
+
+@[inherit_doc getElem]
+syntax:max term noWs "[" withoutPosition(term) "]" : term
+macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
+
+@[inherit_doc getElem]
+syntax term noWs "[" withoutPosition(term) "]'" term:max : term
+macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
+
+/--
+The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
+returns `none` if `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
+
+/--
+The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
+panics `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
+
+class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
+
+  getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
+
+export LawfulGetElem (getElem?_def getElem!_def)
+
+theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
+  rw [getElem?_def]
+  exact dif_pos h
+
+theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
+  rw [getElem?_def]
+  exact dif_neg h
+
+theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
+    c[i]! = c[i]'h := by
+  simp only [getElem!_def, getElem?_def, h]
+
+theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
+  simp only [getElem!_def, getElem?_def, h]
+
+namespace Fin
+
+instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
+  getElem xs i h := getElem xs i.1 h
+  getElem? xs i := getElem? xs i.val
+  getElem! xs i := getElem! xs i.val
+
+instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+      LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
+
+  getElem?_def _c _i _d := h.getElem?_def ..
+  getElem!_def _c _i _d := h.getElem!_def ..
+
+@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+    a[i] = a[i.1] := rfl
+
+@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+    [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
+
+@[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
+
+macro_rules
+  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)
+
+end Fin
+
+namespace List
+
+instance : GetElem (List α) Nat α fun as i => i < as.length where
+  getElem as i h := as.get ⟨i, h⟩
+
+instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
+
+@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
+  rfl
+
+@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
+  rfl
+
+theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+  match as, i with
+  | _::_, 0   => rfl
+  | _::_, i+1 => get_drop_eq_drop _ i _
+
+end List
+
+namespace Array
+
+instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
+  getElem xs i h := xs.get ⟨i, h⟩
+
+instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
+
+end Array
+
+namespace Lean.Syntax
+
+instance : GetElem Syntax Nat Syntax fun _ _ => True where
+  getElem stx i _ := stx.getArg i
+
+instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
+
+end Lean.Syntax

src/Init/Meta.lean

@@ -1227,14 +1227,6 @@ instance : Coe (Lean.Term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where
 
 end Lean.Syntax
 
-set_option linter.unusedVariables.funArgs false in
-/--
-  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
-  the given tactic.
-  Like `optParam`, this gadget only affects elaboration.
-  For example, the tactic will *not* be invoked during type class resolution. -/
-abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α
-
 /-! # Helper functions for manipulating interpolated strings -/
 
 namespace Lean.Syntax

src/Init/Prelude.lean

@@ -2533,43 +2533,6 @@ def panic {α : Type u} [Inhabited α] (msg : String) : α :=
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
 attribute [nospecialize] Inhabited
 
-/--
-The class `GetElem cont idx elem dom` implements the `xs[i]` notation.
-When you write this, given `xs : cont` and `i : idx`, Lean looks for an instance
-of `GetElem cont idx elem dom`. Here `elem` is the type of `xs[i]`, while
-`dom` is whatever proof side conditions are required to make this applicable.
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
-
-The proof side-condition `dom xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
--/
-class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
-  /--
-  The syntax `arr[i]` gets the `i`'th element of the collection `arr`.
-  If there are proof side conditions to the application, they will be automatically
-  inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent,
-  but here are some important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`:
-    does array indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list,
-    with proof side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]`: proves the proof side goal by `get_elem_tactic`
-  * `arr[i]!`: panics if the side goal is false
-  * `arr[i]?`: returns `none` if the side goal is false
-  * `arr[i]'h`: uses `h` to prove the side goal
-  -/
-  getElem (xs : cont) (i : idx) (h : dom xs i) : elem
-
-export GetElem (getElem)
-
 /--
 `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
 with elements from `α`. This type has special support in the runtime.
@@ -2627,9 +2590,6 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
-instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
-
 /--
 Push an element onto the end of an array. This is amortized O(1) because
 `Array α` is internally a dynamic array.
@@ -3884,9 +3844,6 @@ def getArg (stx : Syntax) (i : Nat) : Syntax :=
   | Syntax.node _ _ args => args.getD i Syntax.missing
   | _                    => Syntax.missing
 
-instance : GetElem Syntax Nat Syntax fun _ _ => True where
-  getElem stx i _ := stx.getArg i
-
 /-- Gets the list of arguments of the syntax node, or `#[]` if it's not a `node`. -/
 def getArgs (stx : Syntax) : Array Syntax :=
   match stx with

src/Init/Tactics.lean

@@ -1493,16 +1493,16 @@ macro "get_elem_tactic" : tactic =>
   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
    )
 
-@[inherit_doc getElem]
-syntax:max term noWs "[" withoutPosition(term) "]" : term
-macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
-
-@[inherit_doc getElem]
-syntax term noWs "[" withoutPosition(term) "]'" term:max : term
-macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
 /--
 Searches environment for definitions or theorems that can be substituted in
 for `exact?% to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
+
+set_option linter.unusedVariables.funArgs false in
+/--
+  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
+  the given tactic.
+  Like `optParam`, this gadget only affects elaboration.
+  For example, the tactic will *not* be invoked during type class resolution. -/
+abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α

src/Init/Util.lean

@@ -73,19 +73,6 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 @[implemented_by withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
 
-@[never_extract]
-private def outOfBounds [Inhabited α] : α :=
-  panic! "index out of bounds"
-
-@[inline] def getElem! [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
-  if h : _ then getElem xs i h else outOfBounds
-
-@[inline] def getElem? [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
-  if h : _ then some (getElem xs i h) else none
-
-macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
-macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
-
 /--
   Marks given value and its object graph closure as multi-threaded if currently
   marked single-threaded. This will make reference counter updates atomic and

src/Lean/Data/AssocList.lean

@@ -54,17 +54,34 @@ def mapVal (f : β → δ) : AssocList α β → AssocList α δ
   | nil        => nil
   | cons k v t => cons k (f v) (mapVal f t)
 
-def findEntry? [BEq α] (a : α) : AssocList α β → Option (α × β)
+/-- Auxiliary for `List.reverse`. `List.reverseAux l r = l.reverse ++ r`, but it is defined directly. -/
+def reverseAux : AssocList α β → AssocList α β → AssocList α β
+  | nil,   r => r
+  | cons k v l, r => reverseAux l (cons k v r)
+
+def reverse (as : AssocList α β) : AssocList α β := reverseAux as nil
+
+@[inline]
+def mapValM {m : Type u → Type v} [Monad m] {α : Type u} {β γ : Type _} (f : β → m γ) (as : AssocList α β) : m (AssocList α γ) :=
+  let rec @[specialize] loop
+    | nil,         bs => pure bs.reverse
+    | cons k v as, bs => do loop as (cons k (← f v) bs)
+  loop as nil
+
+def getEntry? [BEq α] (a : α) : AssocList α β → Option (α × β)
   | nil         => none
   | cons k v es => match k == a with
     | true  => some (k, v)
-    | false => findEntry? a es
+    | false => getEntry? a es
 
-def find? [BEq α] (a : α) : AssocList α β → Option β
+def get? [BEq α] (a : α) : AssocList α β → Option β
   | nil         => none
   | cons k v es => match k == a with
     | true  => some v
-    | false => find? a es
+    | false => get? a es
+
+@[deprecated getEntry?] def findEntry? [BEq α] : α → AssocList α β → Option (α × β) := getEntry?
+@[deprecated getEntry?] def find? [BEq α] : α → AssocList α β → Option β := get?
 
 def contains [BEq α] (a : α) : AssocList α β → Bool
   | nil         => false

src/Lean/Data/HashMap.lean

@@ -4,13 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
+import Init.Data.Array.Lemmas
 import Init.Data.Nat.Power2
 import Lean.Data.AssocList
+
 namespace Lean
 
 def HashMapBucket (α : Type u) (β : Type v) :=
   { b : Array (AssocList α β) // b.size.isPowerOfTwo }
 
+@[inline] def HashMapBucket.mapVal (f : β → γ) (m : HashMapBucket α β) : HashMapBucket α γ :=
+  match m with
+  | ⟨a, p⟩ => ⟨a.map (fun l => l.mapVal f), by rw [Array.size_map]; exact p⟩
+
 def HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) : HashMapBucket α β :=
   ⟨ data.val.uset i d h,
     by erw [Array.size_set]; apply data.property ⟩
@@ -64,17 +70,20 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
 @[inline] def forM {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : HashMapImp α β) : m PUnit :=
   forBucketsM h.buckets f
 
-def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
+def getEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
   match m with
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].findEntry? a
+    buckets.val[i].getEntry? a
 
-def find? [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
+def get? [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
   match m with
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].find? a
+    buckets.val[i].get? a
+
+@[deprecated getEntry?] def findEntry? [BEq α] [Hashable α] : HashMapImp α β → α → Option (α × β) := getEntry?
+@[deprecated get?] def find? [BEq α] [Hashable α] : HashMapImp α β → α →  Option β := get?
 
 def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
   match m with
@@ -124,6 +133,9 @@ def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α
     if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
     else m
 
+@[inline] def map (f : β → γ) (m : HashMapImp α β) : HashMapImp α γ :=
+  { size := m.size, buckets := m.buckets.mapVal f }
+
 inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
   | mkWff     : ∀ n,                    WellFormed (mkHashMapImp n)
   | insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
@@ -167,25 +179,32 @@ def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
   match m with
   | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
 
-@[inline] def findEntry? (m : HashMap α β) (a : α) : Option (α × β) :=
+@[inline] def getEntry? (m : HashMap α β) (a : α) : Option (α × β) :=
   match m with
-  | ⟨ m, _ ⟩ => m.findEntry? a
+  | ⟨ m, _ ⟩ => m.getEntry? a
 
-@[inline] def find? (m : HashMap α β) (a : α) : Option β :=
+@[inline] def get? (m : HashMap α β) (a : α) : Option β :=
   match m with
-  | ⟨ m, _ ⟩ => m.find? a
+  | ⟨ m, _ ⟩ => m.get? a
 
-@[inline] def findD (m : HashMap α β) (a : α) (b₀ : β) : β :=
-  (m.find? a).getD b₀
+@[inline] def getD (m : HashMap α β) (a : α) (b₀ : β) : β :=
+  (m.get? a).getD b₀
 
-@[inline] def find! [Inhabited β] (m : HashMap α β) (a : α) : β :=
-  match m.find? a with
+@[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
+  match m.get? a with
   | some b => b
   | none   => panic! "key is not in the map"
 
+@[deprecated getEntry?] def findEntry? : HashMap α β → α → Option (α × β) := getEntry?
+@[deprecated get?] def find? : HashMap α β → α → Option β := get?
+@[deprecated getD] def findD : HashMap α β →  α → β → β := getD
+@[deprecated get!] def find! [Inhabited β] : HashMap α β → α → β := get!
+
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
+instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a
@@ -229,6 +248,10 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
       match m.find? p.fst with
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
+
+instance [Repr α] [Repr β] : Repr (HashMap α β) where
+  reprPrec m prec := Repr.addAppParen ("Lean.HashMap.ofList " ++ repr m.toList) prec
+
 end Lean.HashMap
 
 /--

src/Lean/Data/NameMap.lean

@@ -29,7 +29,16 @@ def insert (m : NameMap α) (n : Name) (a : α) := RBMap.insert m n a
 
 def contains (m : NameMap α) (n : Name) : Bool := RBMap.contains m n
 
-@[inline] def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n
+@[inline] def get? (m : NameMap α) (n : Name) : Option α := RBMap.get? m n
+@[inline] def getD (m : NameMap α) (n : Name) (v : α) : α := RBMap.getD m n v
+@[inline] def get! [Inhabited α] (m : NameMap α) (n : Name) : α := RBMap.get! m n
+
+@[deprecated get?] def find? (m : NameMap α) (n : Name) : Option α := get? m n
+
+protected def ofList (l : List (Name × α)) : NameMap α := RBMap.fromList l _
+
+instance [Repr α] : Repr (NameMap α) where
+  reprPrec m prec := Repr.addAppParen ("Lean.NameMap.ofList " ++ repr m.toList) prec
 
 instance : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (RBMap ..) ..)

src/Lean/Data/PersistentArray.lean

@@ -71,6 +71,8 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
+instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
+
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -154,6 +154,8 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
+instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 

src/Lean/Data/PrefixTree.lean

@@ -32,7 +32,7 @@ partial def insert (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k
     | PrefixTreeNode.Node _ m, [] =>
       PrefixTreeNode.Node (some val) m -- overrides old value
     | PrefixTreeNode.Node v m, k :: ks =>
-      let t := match RBNode.find cmp m k with
+      let t := match RBNode.get cmp m k with
         | none   => insertEmpty ks
         | some t => loop t ks
       PrefixTreeNode.Node v (RBNode.insert cmp m k t)
@@ -43,7 +43,7 @@ partial def find? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k :
   let rec loop
     | PrefixTreeNode.Node val _, [] => val
     | PrefixTreeNode.Node _   m, k :: ks =>
-      match RBNode.find cmp m k with
+      match RBNode.get cmp m k with
       | none   => none
       | some t => loop t ks
   loop t k
@@ -59,7 +59,7 @@ partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α
   let rec find : List α → PrefixTreeNode α β → σ → m σ
     | [],    t, d => fold t d
     | k::ks, PrefixTreeNode.Node _ m, d =>
-      match RBNode.find cmp m k with
+      match RBNode.get cmp m k with
       | none   => pure init
       | some t => find ks t d
   find k t init

src/Lean/Data/RBMap.lean

@@ -190,22 +190,26 @@ end Erase
 section Membership
 variable (cmp : α → α → Ordering)
 
-@[specialize] def findCore : RBNode α β → (k : α) → Option (Sigma (fun k => β k))
+@[specialize] def getCore : RBNode α β → (k : α) → Option (Sigma (fun k => β k))
   | leaf,             _ => none
   | node _ a ky vy b, x =>
     match cmp x ky with
-    | Ordering.lt => findCore a x
-    | Ordering.gt => findCore b x
+    | Ordering.lt => getCore a x
+    | Ordering.gt => getCore b x
     | Ordering.eq => some ⟨ky, vy⟩
 
-@[specialize] def find {β : Type v} : RBNode α (fun _ => β) → α → Option β
+@[inline] def get {β : Type v} : RBNode α (fun _ => β) → α → Option β
   | leaf,             _ => none
   | node _ a ky vy b, x =>
     match cmp x ky with
-    | Ordering.lt => find a x
-    | Ordering.gt => find b x
+    | Ordering.lt => get a x
+    | Ordering.gt => get b x
     | Ordering.eq => some vy
 
+@[deprecated getCore] def findCore (n : RBNode α β) (k : α) : Option (Sigma (fun k => β k)) := n.getCore cmp k
+
+@[deprecated get] def find {β : Type v} (n : RBNode α (fun _ => β)) (k : α) : Option β := n.get cmp k
+
 @[specialize] def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β)
   | leaf,             _, lb => lb
   | node _ a ky vy b, x, lb =>
@@ -321,14 +325,26 @@ instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
   | []        => mkRBMap ..
   | ⟨k,v⟩::xs => (ofList xs).insert k v
 
-@[inline] def findCore? : RBMap α β cmp → α → Option (Sigma (fun (_ : α) => β))
-  | ⟨t, _⟩, x => t.findCore cmp x
+@[inline] def getCore? : RBMap α β cmp → α → Option (Sigma (fun (_ : α) => β))
+  | ⟨t, _⟩, x => t.getCore cmp x
 
-@[inline] def find? : RBMap α β cmp → α → Option β
-  | ⟨t, _⟩, x => t.find cmp x
+@[inline] def get? : RBMap α β cmp → α → Option β
+  | ⟨t, _⟩, x => t.get cmp x
 
-@[inline] def findD (t : RBMap α β cmp) (k : α) (v₀ : β) : β :=
-  (t.find? k).getD v₀
+@[inline] def getD (t : RBMap α β cmp) (k : α) (v : β) : β :=
+  (t.get? k).getD v
+
+/-- Attempts to find the value with key `k : α` in `t` and panics if there is no such key. -/
+@[inline] def get! [Inhabited β] (t : RBMap α β cmp) (k : α) : β :=
+  match t.get? k with
+  | some b => b
+  | none   => panic! "key is not in the map"
+
+@[deprecated getCore?] def findCore? : RBMap α β cmp → α → Option (Sigma (fun (_ : α) => β)) := getCore?
+@[deprecated get?] def find? : RBMap α β cmp → α → Option β := get?
+@[deprecated getD] def findD (t : RBMap α β cmp) (k : α) (v₀ : β) : β := t.getD k v₀
+/-- Attempts to find the value with key `k : α` in `t` and panics if there is no such key. -/
+@[deprecated get!] def find! [Inhabited β] (t : RBMap α β cmp) (k : α) : β := t.get! k
 
 /-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`,
     if it exists. -/
@@ -370,12 +386,6 @@ def maxDepth (t : RBMap α β cmp) : Nat :=
   | some p => p
   | none   => panic! "map is empty"
 
-/-- Attempts to find the value with key `k : α` in `t` and panics if there is no such key. -/
-@[inline] def find! [Inhabited β] (t : RBMap α β cmp) (k : α) : β :=
-  match t.find? k with
-  | some b => b
-  | none   => panic! "key is not in the map"
-
 /-- Merges the maps `t₁` and `t₂`, if a key `a : α` exists in both,
 then use `mergeFn a b₁ b₂` to produce the new merged value. -/
 def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : RBMap α β cmp) : RBMap α β cmp :=

src/Lean/Data/RBTree.lean

@@ -79,11 +79,13 @@ instance [Repr α] : Repr (RBTree α cmp) where
   | []    => mkRBTree ..
   | x::xs => (ofList xs).insert x
 
-@[inline] def find? (t : RBTree α cmp) (a : α) : Option α :=
-  match RBMap.findCore? t a with
+@[inline] def get? (t : RBTree α cmp) (a : α) : Option α :=
+  match RBMap.getCore? t a with
   | some ⟨a, _⟩ => some a
   | none        => none
 
+@[deprecated get?] def find? (t : RBTree α cmp) (a : α) : Option α := get? t a
+
 @[inline] def contains (t : RBTree α cmp) (a : α) : Bool :=
   (t.find? a).isSome
 
@@ -100,7 +102,7 @@ def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp :=
   RBMap.any t (fun a _ => p a)
 
 def subset (t₁ t₂ : RBTree α cmp) : Bool :=
-  t₁.all fun a => (t₂.find? a).toBool
+  t₁.all fun a => (t₂.get? a).toBool
 
 def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
   subset t₁ t₂ && subset t₂ t₁

src/Lean/Meta/Canonicalizer.lean

@@ -56,7 +56,7 @@ structure State where
   -- We use `HashMapImp` to ensure we don't have to tag `State` as `unsafe`.
   cache      : HashMapImp ExprVisited Key := mkHashMapImp
   /--
-  Given a key `k` and `keyToExprs.find? k = some es`, we have that all `es` share key `k`, and
+  Given a key `k` and `keyToExprs.get? k = some es`, we have that all `es` share key `k`, and
   are not definitionally equal modulo the transparency setting used. -/
   keyToExprs : HashMapImp Key (List Expr) := mkHashMapImp
 
@@ -78,7 +78,7 @@ private def shareCommon (a : α) : CanonM α :=
     (a, { keys, cache, keyToExprs })
 
 private partial def mkKey (e : Expr) : CanonM Key := do
-  if let some key := unsafe (← get).cache.find? { e } then
+  if let some key := unsafe (← get).cache.get? { e } then
     return key
   else
     let key ← match e with
@@ -125,7 +125,7 @@ private partial def mkKey (e : Expr) : CanonM Key := do
 def canon (e : Expr) : CanonM Expr := do
   let k ← mkKey e
   -- Find all expressions canonicalized before that have the same key.
-  if let some es' := unsafe (← get).keyToExprs.find? k then
+  if let some es' := unsafe (← get).keyToExprs.get? k then
     withTransparency (← read) do
       for e' in es' do
         -- Found an expression `e'` that is definitionally equal to `e` and share the same key.

src/Lean/Util/HasConstCache.lean

@@ -12,7 +12,7 @@ structure HasConstCache (declName : Name) where
   cache : HashMapImp Expr Bool := mkHashMapImp
 
 unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declName) Bool := do
-  if let some r := (← get).cache.find? (beq := ⟨ptrEq⟩) e then
+  if let some r := (← get).cache.get? (beq := ⟨ptrEq⟩) e then
     return r
   else
     match e with