@[reducible, inline]

abbrev Data.Map (k : Type u) (v : Type w) [Ord k] : Type (max u w)

An ordered finite map from keys k to values v, backed by a red-black tree. $$\text{Map}(k, v) \cong \text{RBMap}(k, v, \text{compare})$$ Provides $O(\log n)$ lookup, insert, and delete.

Equations

• Data.Map k v = Lean.RBMap k v compare

@[inline]

def Data.Map.empty {k : Type u} {v : Type w} [Ord k] : Map k v

The empty map. $$\text{empty} = \emptyset$$

Equations

• Data.Map.empty = Lean.RBMap.empty

@[inline]

def Data.Map.singleton {k : Type u} {v : Type w} [Ord k] (key : k) (val : v) : Map k v

A map with a single key-value pair. $$\text{singleton}(k, v) = \{k \mapsto v\}$$

Equations

• Data.Map.singleton key val = Lean.RBMap.empty.insert key val

@[inline]

def Data.Map.fromList {k : Type u} {v : Type w} [Ord k] (l : List (k × v)) : Map k v

Build a map from an association list. Later entries override earlier ones for duplicate keys. $$\text{fromList}([(k_1,v_1),\ldots,(k_n,v_n)])$$

Equations

• Data.Map.fromList l = Lean.RBMap.ofList l

@[inline]

def Data.Map.lookup {k : Type u} {v : Type w} [Ord k] (key : k) (m : Map k v) : Option v

Look up a key. $$\text{lookup}(k, m) = \begin{cases} \text{some}(v) & \text{if } k \mapsto v \in m \\ \text{none} & \text{otherwise} \end{cases}$$

Equations

• Data.Map.lookup key m = Lean.RBMap.find? m key

@[inline]

def Data.Map.findWithDefault {k : Type u} {v : Type w} [Ord k] (dflt : v) (key : k) (m : Map k v) : v

Look up a key, returning a default if absent. $$\text{findWithDefault}(d, k, m) = \begin{cases} v & \text{if } k \mapsto v \in m \\ d & \text{otherwise} \end{cases}$$

Equations

• Data.Map.findWithDefault dflt key m = Lean.RBMap.findD m key dflt

@[inline]

def Data.Map.member {k : Type u} {v : Type w} [Ord k] (key : k) (m : Map k v) : Bool

Test whether a key is in the map. $$\text{member}(k, m) \iff k \in \text{dom}(m)$$

Equations

• Data.Map.member key m = Lean.RBMap.contains m key

@[inline]

def Data.Map.null {k : Type u} {v : Type w} [Ord k] (m : Map k v) : Bool

Is the map empty? $$\text{null}(m) \iff m = \emptyset$$

Equations

• m.null = Lean.RBMap.isEmpty m

@[inline]

def Data.Map.size' {k : Type u} {v : Type w} [Ord k] (m : Map k v) : Nat

The number of entries. $$\text{size}(m) = |m|$$

Equations

• m.size' = Lean.RBMap.size m

@[inline]

def Data.Map.insert' {k : Type u} {v : Type w} [Ord k] (key : k) (val : v) (m : Map k v) : Map k v

Insert a key-value pair. If the key already exists, the value is replaced. $$\text{insert}(k, v, m) = m[k \mapsto v]$$

Equations

• Data.Map.insert' key val m = Lean.RBMap.insert m key val

@[inline]

def Data.Map.delete {k : Type u} {v : Type w} [Ord k] (key : k) (m : Map k v) : Map k v

Delete a key from the map. $$\text{delete}(k, m) = m \setminus \{k\}$$

Equations

• Data.Map.delete key m = Lean.RBMap.erase m key

def Data.Map.adjust {k : Type u} {v : Type w} [Ord k] (f : v → v) (key : k) (m : Map k v) : Map k v

Adjust the value at a key, if present. $$\text{adjust}(f, k, m) = \begin{cases} m[k \mapsto f(v)] & \text{if } k \mapsto v \in m \\ m & \text{otherwise} \end{cases}$$

Equations

• Data.Map.adjust f key m = match Lean.RBMap.find? m key with | some val => Lean.RBMap.insert m key (f val) | none => m

def Data.Map.union {k : Type u} {v : Type w} [Ord k] (m1 m2 : Map k v) : Map k v

Left-biased union of two maps. Keys in both maps take the value from the first (left) map. $$\text{union}(m_1, m_2) = m_1 \cup m_2 \quad (\text{left-biased})$$

Equations

• m1.union m2 = Lean.RBMap.mergeBy (fun (x : k) (v1 x_1 : v) => v1) m1 m2

def Data.Map.unionWith {k : Type u} {v : Type w} [Ord k] (f : v → v → v) (m1 m2 : Map k v) : Map k v

Union with a combining function. $$\text{unionWith}(f, m_1, m_2)[k] = \begin{cases} f(v_1, v_2) & \text{if } k \mapsto v_1 \in m_1 \text{ and } k \mapsto v_2 \in m_2 \\ v_1 & \text{if } k \in m_1 \text{ only} \\ v_2 & \text{if } k \in m_2 \text{ only} \end{cases}$$

Equations

• Data.Map.unionWith f m1 m2 = Lean.RBMap.mergeBy (fun (x : k) (v1 v2 : v) => f v1 v2) m1 m2

def Data.Map.intersection {k : Type u} {v : Type w} [Ord k] (m1 m2 : Map k v) : Map k v

Intersection of two maps, keeping values from the first. $$\text{intersection}(m_1, m_2) = \{k \mapsto v \mid k \mapsto v \in m_1, k \in \text{dom}(m_2)\}$$

Equations

• m1.intersection m2 = Lean.RBMap.intersectBy (fun (x : k) (v1 x_1 : v) => v1) m1 m2

def Data.Map.intersectionWith {k : Type u} {v : Type w} [Ord k] (f : v → v → v) (m1 m2 : Map k v) : Map k v

Intersection with a combining function. $$\text{intersectionWith}(f, m_1, m_2)[k] = f(v_1, v_2) \text{ for } k \in \text{dom}(m_1) \cap \text{dom}(m_2)$$

Equations

• Data.Map.intersectionWith f m1 m2 = Lean.RBMap.intersectBy (fun (x : k) (v1 v2 : v) => f v1 v2) m1 m2

def Data.Map.difference {k : Type u} {v : Type w} [Ord k] (m1 m2 : Map k v) : Map k v

Difference of two maps. $$\text{difference}(m_1, m_2) = \{k \mapsto v \mid k \mapsto v \in m_1, k \notin \text{dom}(m_2)\}$$

Equations

• m1.difference m2 = Lean.RBMap.filter (fun (key : k) (x : v) => !Lean.RBMap.contains m2 key) m1

@[inline]

def Data.Map.foldlWithKey {k : Type u} {v : Type w} [Ord k] {α : Type u_1} (f : α → k → v → α) (init : α) (m : Map k v) : α

Left fold over key-value pairs in ascending key order. $$\text{foldlWithKey}(f, z, m) = f(\ldots f(f(z, k_1, v_1), k_2, v_2) \ldots, k_n, v_n)$$

Equations

• Data.Map.foldlWithKey f init m = Lean.RBMap.fold f init m

@[inline]

def Data.Map.foldrWithKey {k : Type u} {v : Type w} [Ord k] {α : Type u_1} (f : k → v → α → α) (init : α) (m : Map k v) : α

Right fold over key-value pairs in ascending key order. $$\text{foldrWithKey}(f, z, m) = f(k_1, v_1, f(k_2, v_2, \ldots f(k_n, v_n, z)))$$

Equations

• Data.Map.foldrWithKey f init m = Lean.RBMap.revFold (fun (acc : α) (key : k) (val : v) => f key val acc) init m

def Data.Map.mapValues {k : Type u} {v : Type w} [Ord k] {w : Type u_1} (f : v → w) (m : Map k v) : Map k w

Map a function over all values. $$\text{map}(f, m)[k] = f(m[k])$$

Equations

• Data.Map.mapValues f m = Lean.RBMap.fold (fun (acc : Data.Map k w) (key : k) (val : v) => Lean.RBMap.insert acc key (f val)) Lean.RBMap.empty m

def Data.Map.mapWithKey {k : Type u} {v : Type w} [Ord k] {w : Type u_1} (f : k → v → w) (m : Map k v) : Map k w

Map a function over all key-value pairs. $$\text{mapWithKey}(f, m)[k] = f(k, m[k])$$

Equations

• Data.Map.mapWithKey f m = Lean.RBMap.fold (fun (acc : Data.Map k w) (key : k) (val : v) => Lean.RBMap.insert acc key (f key val)) Lean.RBMap.empty m

def Data.Map.mapKeys {k : Type u} {v : Type w} [Ord k] {k₂ : Type u_1} [Ord k₂] (f : k → k₂) (m : Map k v) : Map k₂ v

Map a function over all keys. The resulting map may be smaller if the function maps distinct keys to the same value (last wins). $$\text{mapKeys}(f, m) = \text{fromList}([(f(k), v) \mid k \mapsto v \in m])$$

Equations

• Data.Map.mapKeys f m = Lean.RBMap.fold (fun (acc : Data.Map k₂ v) (key : k) (val : v) => Lean.RBMap.insert acc (f key) val) Lean.RBMap.empty m

@[inline]

def Data.Map.filterWithKey {k : Type u} {v : Type w} [Ord k] (p : k → v → Bool) (m : Map k v) : Map k v

Filter entries by a predicate on keys and values. $$\text{filterWithKey}(p, m) = \{k \mapsto v \mid k \mapsto v \in m, p(k, v)\}$$

Equations

• Data.Map.filterWithKey p m = Lean.RBMap.filter p m

@[inline]

def Data.Map.toList' {k : Type u} {v : Type w} [Ord k] (m : Map k v) : List (k × v)

Convert the map to a list of key-value pairs in ascending key order. $$\text{toList}(m) = [(k_1, v_1), \ldots, (k_n, v_n)]$$ where $k_1 < \cdots < k_n$.

Equations

• m.toList' = Lean.RBMap.toList m

@[inline]

def Data.Map.toAscList {k : Type u} {v : Type w} [Ord k] (m : Map k v) : List (k × v)

Convert the map to an ascending list (same as toList for an ordered map). $$\text{toAscList} = \text{toList}$$

Equations

• m.toAscList = Lean.RBMap.toList m

def Data.Map.keys {k : Type u} {v : Type w} [Ord k] (m : Map k v) : List k

The list of all keys in ascending order. $$\text{keys}(m) = [k_1, \ldots, k_n]$$ where $k_1 < \cdots < k_n$.

Equations

• m.keys = Lean.RBMap.fold (fun (acc : List k) (key : k) (x : v) => acc ++ [key]) [] m

def Data.Map.elems {k : Type u} {v : Type w} [Ord k] (m : Map k v) : List v

The list of all values in ascending key order. $$\text{elems}(m) = [v_1, \ldots, v_n]$$ ordered by their corresponding keys.

Equations

• m.elems = Lean.RBMap.fold (fun (acc : List v) (x : k) (val : v) => acc ++ [val]) [] m

def Data.Map.restrictKeys {k : Type u} {v : Type w} [Ord k] (m : Map k v) (ks : List k) : Map k v

Restrict a map to only the keys in the given list. $$\text{restrictKeys}(m, ks) = \{k \mapsto v \mid k \mapsto v \in m, k \in ks\}$$

Equations

• m.restrictKeys ks = Lean.RBMap.filter (fun (key : k) (x : v) => (List.foldl (fun (s : Lean.RBMap k Unit compare) (key : k) => s.insert key ()) Lean.RBMap.empty ks).contains key) m

def Data.Map.withoutKeys {k : Type u} {v : Type w} [Ord k] (m : Map k v) (ks : List k) : Map k v

Remove all keys in the given list from the map. $$\text{withoutKeys}(m, ks) = \{k \mapsto v \mid k \mapsto v \in m, k \notin ks\}$$

Equations

• m.withoutKeys ks = Lean.RBMap.filter (fun (key : k) (x : v) => !(List.foldl (fun (s : Lean.RBMap k Unit compare) (key : k) => s.insert key ()) Lean.RBMap.empty ks).contains key) m

def Data.Map.isSubmapOf {k : Type u} {v : Type w} [Ord k] [BEq v] (m1 m2 : Map k v) : Bool

Is m1 a submap of m2? Every key in m1 must be in m2 with an equal value. $$\text{isSubmapOf}(m_1, m_2) \iff \forall k \in \text{dom}(m_1),\; m_1[k] = m_2[k]$$

Equations

• m1.isSubmapOf m2 = Lean.RBMap.all m1 fun (key : k) (val : v) => match Lean.RBMap.find? m2 key with | some v2 => val == v2 | none => false

def Data.Map.lookupMin {k : Type u} {v : Type w} [Ord k] (m : Map k v) : Option (k × v)

The smallest key-value pair, or none if the map is empty. $$\text{lookupMin}(m) = \min_{k} \{(k, v) \mid k \mapsto v \in m\}$$

Equations

• m.lookupMin = Option.map (fun (x : (_ : k) × v) => match x with | ⟨key, val⟩ => (key, val)) m.val.min

def Data.Map.lookupMax {k : Type u} {v : Type w} [Ord k] (m : Map k v) : Option (k × v)

The largest key-value pair, or none if the map is empty. $$\text{lookupMax}(m) = \max_{k} \{(k, v) \mid k \mapsto v \in m\}$$

Equations

• m.lookupMax = Option.map (fun (x : (_ : k) × v) => match x with | ⟨key, val⟩ => (key, val)) m.val.max

@[implicit_reducible]

instance Data.Map.instEmptyCollection {k : Type u} {v : Type w} [Ord k] : EmptyCollection (Map k v)

Equations

• Data.Map.instEmptyCollection = { emptyCollection := Data.Map.empty }

@[implicit_reducible]

instance Data.Map.instInhabited {k : Type u} {v : Type w} [Ord k] : Inhabited (Map k v)

Equations

• Data.Map.instInhabited = { default := Data.Map.empty }

@[implicit_reducible]

instance Data.Map.instRepr {k : Type u} {v : Type w} [Ord k] [Repr k] [Repr v] : Repr (Map k v)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Map.instBEq {k : Type u} {v : Type w} [Ord k] [BEq k] [BEq v] : BEq (Map k v)

Equations

• Data.Map.instBEq = { beq := fun (m1 m2 : Data.Map k v) => Lean.RBMap.toList m1 == Lean.RBMap.toList m2 }

theorem Data.Map.null_empty {k : Type u} {v : Type w} [Ord k] : empty.null = true

The empty map has no entries. $$\text{null}(\emptyset) = \text{true}$$

theorem Data.Map.lookup_empty {k : Type u} {v : Type w} [Ord k] (key : k) : lookup key empty = none

Lookup on the empty map always returns none. $$\text{lookup}(k, \emptyset) = \text{none}$$

theorem Data.Map.size_empty {k : Type u} {v : Type w} [Ord k] : empty.size' = 0

The empty map has size zero. $$\text{size'}(\emptyset) = 0$$

theorem Data.Map.null_singleton {k : Type u} {v : Type w} [Ord k] (key : k) (val : v) : (singleton key val).null = false

A singleton map is not null. $$\text{null}(\text{singleton}(k, v)) = \text{false}$$

theorem Data.Map.member_empty {k : Type u} {v : Type w} [Ord k] (key : k) : member key empty = false

Membership in the empty map is always false. $$\text{member}(k, \emptyset) = \text{false}$$