Documentation

Mathlib.Data.Finmap

Finite maps over Multiset #

Multisets of sigma types #

def Multiset.keys {α : Type u} {β : αType v} (s : Multiset (Sigma β)) :

Multiset of keys of an association multiset.

Equations
@[simp]
theorem Multiset.coe_keys {α : Type u} {β : αType v} {l : List (Sigma β)} :
(↑l).keys = l.keys
@[simp]
theorem Multiset.keys_zero {α : Type u} {β : αType v} :
keys 0 = 0
@[simp]
theorem Multiset.keys_cons {α : Type u} {β : αType v} {a : α} {b : β a} {s : Multiset (Sigma β)} :
(a, b ::ₘ s).keys = a ::ₘ s.keys
@[simp]
theorem Multiset.keys_singleton {α : Type u} {β : αType v} {a : α} {b : β a} :
def Multiset.NodupKeys {α : Type u} {β : αType v} (s : Multiset (Sigma β)) :

NodupKeys s means that s has no duplicate keys.

Equations
@[simp]
theorem Multiset.coe_nodupKeys {α : Type u} {β : αType v} {l : List (Sigma β)} :
theorem Multiset.nodup_keys {α : Type u} {β : αType v} {m : Multiset ((a : α) × β a)} :
theorem Multiset.NodupKeys.nodup_keys {α : Type u} {β : αType v} {m : Multiset ((a : α) × β a)} :

Alias of the reverse direction of Multiset.nodup_keys.

theorem Multiset.NodupKeys.nodup {α : Type u} {β : αType v} {m : Multiset ((a : α) × β a)} (h : m.NodupKeys) :

Finmap #

structure Finmap {α : Type u} (β : αType v) :
Type (max u v)

Finmap β is the type of finite maps over a multiset. It is effectively a quotient of AList β by permutation of the underlying list.

def AList.toFinmap {α : Type u} {β : αType v} (s : AList β) :

The quotient map from AList to Finmap.

Equations
theorem AList.toFinmap_eq {α : Type u} {β : αType v} {s₁ s₂ : AList β} :
s₁.toFinmap = s₂.toFinmap s₁.entries.Perm s₂.entries
@[simp]
theorem AList.toFinmap_entries {α : Type u} {β : αType v} (s : AList β) :
def List.toFinmap {α : Type u} {β : αType v} [DecidableEq α] (s : List (Sigma β)) :

Given l : List (Sigma β), create a term of type Finmap β by removing entries with duplicate keys.

Equations
theorem Finmap.nodup_entries {α : Type u} {β : αType v} (f : Finmap β) :

Lifting from AList #

def Finmap.liftOn {α : Type u} {β : αType v} {γ : Type u_1} (s : Finmap β) (f : AList βγ) (H : ∀ (a b : AList β), a.entries.Perm b.entriesf a = f b) :
γ

Lift a permutation-respecting function on AList to Finmap.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finmap.liftOn_toFinmap {α : Type u} {β : αType v} {γ : Type u_1} (s : AList β) (f : AList βγ) (H : ∀ (a b : AList β), a.entries.Perm b.entriesf a = f b) :
s.toFinmap.liftOn f H = f s
def Finmap.liftOn₂ {α : Type u} {β : αType v} {γ : Type u_1} (s₁ s₂ : Finmap β) (f : AList βAList βγ) (H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries.Perm a₂.entriesb₁.entries.Perm b₂.entriesf a₁ b₁ = f a₂ b₂) :
γ

Lift a permutation-respecting function on 2 ALists to 2 Finmaps.

Equations
@[simp]
theorem Finmap.liftOn₂_toFinmap {α : Type u} {β : αType v} {γ : Type u_1} (s₁ s₂ : AList β) (f : AList βAList βγ) (H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries.Perm a₂.entriesb₁.entries.Perm b₂.entriesf a₁ b₁ = f a₂ b₂) :
s₁.toFinmap.liftOn₂ s₂.toFinmap f H = f s₁ s₂

Induction #

theorem Finmap.induction_on {α : Type u} {β : αType v} {C : Finmap βProp} (s : Finmap β) (H : ∀ (a : AList β), C a.toFinmap) :
C s
theorem Finmap.induction_on₂ {α : Type u} {β : αType v} {C : Finmap βFinmap βProp} (s₁ s₂ : Finmap β) (H : ∀ (a₁ a₂ : AList β), C a₁.toFinmap a₂.toFinmap) :
C s₁ s₂
theorem Finmap.induction_on₃ {α : Type u} {β : αType v} {C : Finmap βFinmap βFinmap βProp} (s₁ s₂ s₃ : Finmap β) (H : ∀ (a₁ a₂ a₃ : AList β), C a₁.toFinmap a₂.toFinmap a₃.toFinmap) :
C s₁ s₂ s₃

extensionality #

theorem Finmap.ext {α : Type u} {β : αType v} {s t : Finmap β} :
s.entries = t.entriess = t
theorem Finmap.ext_iff {α : Type u} {β : αType v} {s t : Finmap β} :
@[simp]
theorem Finmap.ext_iff' {α : Type u} {β : αType v} {s t : Finmap β} :

mem #

instance Finmap.instMembership {α : Type u} {β : αType v} :

The predicate a ∈ s means that s has a value associated to the key a.

Equations
theorem Finmap.mem_def {α : Type u} {β : αType v} {a : α} {s : Finmap β} :
@[simp]
theorem Finmap.mem_toFinmap {α : Type u} {β : αType v} {a : α} {s : AList β} :

keys #

def Finmap.keys {α : Type u} {β : αType v} (s : Finmap β) :

The set of keys of a finite map.

Equations
@[simp]
theorem Finmap.keys_val {α : Type u} {β : αType v} (s : AList β) :
@[simp]
theorem Finmap.keys_ext {α : Type u} {β : αType v} {s₁ s₂ : AList β} :
s₁.toFinmap.keys = s₂.toFinmap.keys s₁.keys.Perm s₂.keys
theorem Finmap.mem_keys {α : Type u} {β : αType v} {a : α} {s : Finmap β} :
a s.keys a s

empty #

instance Finmap.instEmptyCollection {α : Type u} {β : αType v} :

The empty map.

Equations
instance Finmap.instInhabited {α : Type u} {β : αType v} :
Equations
@[simp]
theorem Finmap.empty_toFinmap {α : Type u} {β : αType v} :
@[simp]
theorem Finmap.toFinmap_nil {α : Type u} {β : αType v} [DecidableEq α] :
theorem Finmap.notMem_empty {α : Type u} {β : αType v} {a : α} :
a
@[deprecated Finmap.notMem_empty (since := "2025-05-23")]
theorem Finmap.not_mem_empty {α : Type u} {β : αType v} {a : α} :
a

Alias of Finmap.notMem_empty.

@[simp]
theorem Finmap.keys_empty {α : Type u} {β : αType v} :

singleton #

def Finmap.singleton {α : Type u} {β : αType v} (a : α) (b : β a) :

The singleton map.

Equations
@[simp]
theorem Finmap.keys_singleton {α : Type u} {β : αType v} (a : α) (b : β a) :
@[simp]
theorem Finmap.mem_singleton {α : Type u} {β : αType v} (x y : α) (b : β y) :
x singleton y b x = y
instance Finmap.decidableEq {α : Type u} {β : αType v} [DecidableEq α] [(a : α) → DecidableEq (β a)] :
Equations

lookup #

def Finmap.lookup {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
Option (β a)

Look up the value associated to a key in a map.

Equations
@[simp]
theorem Finmap.lookup_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
@[simp]
theorem Finmap.dlookup_list_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : List (Sigma β)) :
@[simp]
theorem Finmap.lookup_empty {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
theorem Finmap.lookup_isSome {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Finmap β} :
theorem Finmap.lookup_eq_none {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Finmap β} :
lookup a s = none as
theorem Finmap.mem_lookup_iff {α : Type u} {β : αType v} [DecidableEq α] {s : Finmap β} {a : α} {b : β a} :
theorem Finmap.lookup_eq_some_iff {α : Type u} {β : αType v} [DecidableEq α] {s : Finmap β} {a : α} {b : β a} :
@[simp]
theorem Finmap.sigma_keys_lookup {α : Type u} {β : αType v} [DecidableEq α] (s : Finmap β) :
(s.keys.sigma fun (i : α) => (lookup i s).toFinset) = { val := s.entries, nodup := }
@[simp]
theorem Finmap.lookup_singleton_eq {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} :
instance Finmap.instDecidableMem {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
Equations
theorem Finmap.mem_iff {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Finmap β} :
a s ∃ (b : β a), lookup a s = some b
theorem Finmap.mem_of_lookup_eq_some {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} (h : lookup a s = some b) :
a s
theorem Finmap.ext_lookup {α : Type u} {β : αType v} [DecidableEq α] {s₁ s₂ : Finmap β} :
(∀ (x : α), lookup x s₁ = lookup x s₂)s₁ = s₂
def Finmap.keysLookupEquiv {α : Type u} {β : αType v} [DecidableEq α] :
Finmap β { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true i f.1 }

An equivalence between Finmap β and pairs (keys : Finset α, lookup : ∀ a, Option (β a)) such that (lookup a).isSome ↔ a ∈ keys.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finmap.keysLookupEquiv_apply_coe_fst {α : Type u} {β : αType v} [DecidableEq α] (s : Finmap β) :
(↑(keysLookupEquiv s)).1 = s.keys
@[simp]
theorem Finmap.keysLookupEquiv_apply_coe_snd {α : Type u} {β : αType v} [DecidableEq α] (s : Finmap β) (i : α) :
(↑(keysLookupEquiv s)).2 i = lookup i s
@[simp]
theorem Finmap.keysLookupEquiv_symm_apply_keys {α : Type u} {β : αType v} [DecidableEq α] (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true i f.1 }) :
(keysLookupEquiv.symm f).keys = (↑f).1
@[simp]
theorem Finmap.keysLookupEquiv_symm_apply_lookup {α : Type u} {β : αType v} [DecidableEq α] (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true i f.1 }) (a : α) :
lookup a (keysLookupEquiv.symm f) = (↑f).2 a

replace #

def Finmap.replace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) :

Replace a key with a given value in a finite map. If the key is not present it does nothing.

Equations
@[simp]
theorem Finmap.replace_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : AList β) :
@[simp]
theorem Finmap.keys_replace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) :
(replace a b s).keys = s.keys
@[simp]
theorem Finmap.mem_replace {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {b : β a} {s : Finmap β} :
a' replace a b s a' s

foldl #

def Finmap.foldl {α : Type u} {β : αType v} {δ : Type w} (f : δ(a : α) → β aδ) (H : ∀ (d : δ) (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂), f (f d a₁ b₁) a₂ b₂ = f (f d a₂ b₂) a₁ b₁) (d : δ) (m : Finmap β) :
δ

Fold a commutative function over the key-value pairs in the map

Equations
def Finmap.any {α : Type u} {β : αType v} (f : (x : α) → β xBool) (s : Finmap β) :

any f s returns true iff there exists a value v in s such that f v = true.

Equations
def Finmap.all {α : Type u} {β : αType v} (f : (x : α) → β xBool) (s : Finmap β) :

all f s returns true iff f v = true for all values v in s.

Equations

erase #

def Finmap.erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :

Erase a key from the map. If the key is not present it does nothing.

Equations
@[simp]
theorem Finmap.erase_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
@[simp]
theorem Finmap.keys_erase_toFinset {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
@[simp]
theorem Finmap.keys_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
(erase a s).keys = s.keys.erase a
@[simp]
theorem Finmap.mem_erase {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {s : Finmap β} :
a' erase a s a' a a' s
theorem Finmap.notMem_erase_self {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Finmap β} :
aerase a s
@[deprecated Finmap.notMem_erase_self (since := "2025-05-23")]
theorem Finmap.not_mem_erase_self {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Finmap β} :
aerase a s

Alias of Finmap.notMem_erase_self.

@[simp]
theorem Finmap.lookup_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
lookup a (erase a s) = none
@[simp]
theorem Finmap.lookup_erase_ne {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {s : Finmap β} (h : a a') :
lookup a (erase a' s) = lookup a s
theorem Finmap.erase_erase {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {s : Finmap β} :
erase a (erase a' s) = erase a' (erase a s)

sdiff #

def Finmap.sdiff {α : Type u} {β : αType v} [DecidableEq α] (s s' : Finmap β) :

sdiff s s' consists of all key-value pairs from s and s' where the keys are in s or s' but not both.

Equations
instance Finmap.instSDiff {α : Type u} {β : αType v} [DecidableEq α] :
Equations

insert #

def Finmap.insert {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) :

Insert a key-value pair into a finite map, replacing any existing pair with the same key.

Equations
@[simp]
theorem Finmap.insert_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : AList β) :
theorem Finmap.entries_insert_of_notMem {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} :
as(insert a b s).entries = a, b ::ₘ s.entries
@[deprecated Finmap.entries_insert_of_notMem (since := "2025-05-23")]
theorem Finmap.entries_insert_of_not_mem {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} :
as(insert a b s).entries = a, b ::ₘ s.entries

Alias of Finmap.entries_insert_of_notMem.

@[deprecated Finmap.entries_insert_of_not_mem (since := "2024-12-14")]
theorem Finmap.insert_entries_of_neg {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} :
as(insert a b s).entries = a, b ::ₘ s.entries

Alias of Finmap.entries_insert_of_notMem.


Alias of Finmap.entries_insert_of_notMem.

@[simp]
theorem Finmap.mem_insert {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {b' : β a'} {s : Finmap β} :
a insert a' b' s a = a' a s
@[simp]
theorem Finmap.lookup_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} (s : Finmap β) :
lookup a (insert a b s) = some b
@[simp]
theorem Finmap.lookup_insert_of_ne {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {b : β a} (s : Finmap β) (h : a' a) :
lookup a' (insert a b s) = lookup a' s
@[simp]
theorem Finmap.insert_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b b' : β a} (s : Finmap β) :
insert a b' (insert a b s) = insert a b' s
theorem Finmap.insert_insert_of_ne {α : Type u} {β : αType v} [DecidableEq α] {a a' : α} {b : β a} {b' : β a'} (s : Finmap β) (h : a a') :
insert a' b' (insert a b s) = insert a b (insert a' b' s)
theorem Finmap.toFinmap_cons {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)) :
(a, b :: xs).toFinmap = insert a b xs.toFinmap
theorem Finmap.mem_list_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (xs : List (Sigma β)) :
a xs.toFinmap ∃ (b : β a), a, b xs
@[simp]
theorem Finmap.insert_singleton_eq {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b b' : β a} :
insert a b (singleton a b') = singleton a b

extract #

def Finmap.extract {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
Option (β a) × Finmap β

Erase a key from the map, and return the corresponding value, if found.

Equations
@[simp]
theorem Finmap.extract_eq_lookup_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
extract a s = (lookup a s, erase a s)

union #

def Finmap.union {α : Type u} {β : αType v} [DecidableEq α] (s₁ s₂ : Finmap β) :

s₁ ∪ s₂ is the key-based union of two finite maps. It is left-biased: if there exists an a ∈ s₁, lookup a (s₁ ∪ s₂) = lookup a s₁.

Equations
instance Finmap.instUnion {α : Type u} {β : αType v} [DecidableEq α] :
Equations
@[simp]
theorem Finmap.mem_union {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} :
a s₁ s₂ a s₁ a s₂
@[simp]
theorem Finmap.union_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (s₁ s₂ : AList β) :
s₁.toFinmap s₂.toFinmap = (s₁ s₂).toFinmap
theorem Finmap.keys_union {α : Type u} {β : αType v} [DecidableEq α] {s₁ s₂ : Finmap β} :
(s₁ s₂).keys = s₁.keys s₂.keys
@[simp]
theorem Finmap.lookup_union_left {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} :
a s₁lookup a (s₁ s₂) = lookup a s₁
@[simp]
theorem Finmap.lookup_union_right {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} :
as₁lookup a (s₁ s₂) = lookup a s₂
theorem Finmap.lookup_union_left_of_not_in {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s₁ s₂ : Finmap β} (h : as₂) :
lookup a (s₁ s₂) = lookup a s₁
@[simp]
theorem Finmap.mem_lookup_union' {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β} :
lookup a (s₁ s₂) = some b b lookup a s₁ as₁ b lookup a s₂

simp-normal form of mem_lookup_union

theorem Finmap.mem_lookup_union {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β} :
b lookup a (s₁ s₂) b lookup a s₁ as₁ b lookup a s₂
theorem Finmap.mem_lookup_union_middle {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ s₃ : Finmap β} :
b lookup a (s₁ s₃)as₂b lookup a (s₁ s₂ s₃)
theorem Finmap.insert_union {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β} :
insert a b (s₁ s₂) = insert a b s₁ s₂
theorem Finmap.union_assoc {α : Type u} {β : αType v} [DecidableEq α] {s₁ s₂ s₃ : Finmap β} :
s₁ s₂ s₃ = s₁ (s₂ s₃)
@[simp]
theorem Finmap.empty_union {α : Type u} {β : αType v} [DecidableEq α] {s₁ : Finmap β} :
s₁ = s₁
@[simp]
theorem Finmap.union_empty {α : Type u} {β : αType v} [DecidableEq α] {s₁ : Finmap β} :
s₁ = s₁
theorem Finmap.erase_union_singleton {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) (h : lookup a s = some b) :
erase a s singleton a b = s

Disjoint #

def Finmap.Disjoint {α : Type u} {β : αType v} (s₁ s₂ : Finmap β) :

Disjoint s₁ s₂ holds if s₁ and s₂ have no keys in common.

Equations
  • s₁.Disjoint s₂ = xs₁, xs₂
theorem Finmap.disjoint_empty {α : Type u} {β : αType v} (x : Finmap β) :
theorem Finmap.Disjoint.symm {α : Type u} {β : αType v} (x y : Finmap β) (h : x.Disjoint y) :
theorem Finmap.Disjoint.symm_iff {α : Type u} {β : αType v} (x y : Finmap β) :
theorem Finmap.disjoint_union_left {α : Type u} {β : αType v} [DecidableEq α] (x y z : Finmap β) :
theorem Finmap.disjoint_union_right {α : Type u} {β : αType v} [DecidableEq α] (x y z : Finmap β) :
theorem Finmap.union_comm_of_disjoint {α : Type u} {β : αType v} [DecidableEq α] {s₁ s₂ : Finmap β} :
s₁.Disjoint s₂s₁ s₂ = s₂ s₁
theorem Finmap.union_cancel {α : Type u} {β : αType v} [DecidableEq α] {s₁ s₂ s₃ : Finmap β} (h : s₁.Disjoint s₃) (h' : s₂.Disjoint s₃) :
s₁ s₃ = s₂ s₃ s₁ = s₂