mathlib3 documentation

data.finmap

Finite maps over multiset #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 β)} :
def multiset.nodupkeys {α : Type u} {β : α Type v} (s : multiset (sigma β)) :
Prop

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.

Instances for finmap
def alist.to_finmap {α : Type u} {β : α Type v} (s : alist β) :

The quotient map from alist to finmap.

Equations
theorem alist.to_finmap_eq {α : Type u} {β : α Type v} {s₁ s₂ : alist β} :
s₁.to_finmap = s₂.to_finmap s₁.entries ~ s₂.entries
@[simp]
theorem alist.to_finmap_entries {α : Type u} {β : α Type v} (s : alist β) :
def list.to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (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.lift_on {α : Type u} {β : α Type v} {γ : Type u_1} (s : finmap β) (f : alist β γ) (H : (a b : alist β), a.entries ~ b.entries f a = f b) :
γ

Lift a permutation-respecting function on alist to finmap.

Equations
@[simp]
theorem finmap.lift_on_to_finmap {α : Type u} {β : α Type v} {γ : Type u_1} (s : alist β) (f : alist β γ) (H : (a b : alist β), a.entries ~ b.entries f a = f b) :
s.to_finmap.lift_on f H = f s
def finmap.lift_on₂ {α : Type u} {β : α Type v} {γ : Type u_1} (s₁ s₂ : finmap β) (f : alist β alist β γ) (H : (a₁ b₁ a₂ b₂ : alist β), a₁.entries ~ a₂.entries b₁.entries ~ b₂.entries f a₁ b₁ = f a₂ b₂) :
γ

Lift a permutation-respecting function on 2 alists to 2 finmaps.

Equations
@[simp]
theorem finmap.lift_on₂_to_finmap {α : Type u} {β : α Type v} {γ : Type u_1} (s₁ s₂ : alist β) (f : alist β alist β γ) (H : (a₁ b₁ a₂ b₂ : alist β), a₁.entries ~ a₂.entries b₁.entries ~ b₂.entries f a₁ b₁ = f a₂ b₂) :
s₁.to_finmap.lift_on₂ s₂.to_finmap f H = f s₁ s₂

induction #

theorem finmap.induction_on {α : Type u} {β : α Type v} {C : finmap β Prop} (s : finmap β) (H : (a : alist β), C a.to_finmap) :
C s
theorem finmap.induction_on₂ {α : Type u} {β : α Type v} {C : finmap β finmap β Prop} (s₁ s₂ : finmap β) (H : (a₁ a₂ : alist β), C a₁.to_finmap a₂.to_finmap) :
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₁.to_finmap a₂.to_finmap a₃.to_finmap) :
C s₁ s₂ s₃

extensionality #

@[ext]
theorem finmap.ext {α : Type u} {β : α Type v} {s t : finmap β} :
@[simp]
theorem finmap.ext_iff {α : Type u} {β : α Type v} {s t : finmap β} :

mem #

@[protected, instance]
def finmap.has_mem {α : Type u} {β : α Type v} :
has_mem α (finmap β)

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_to_finmap {α : 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₁.to_finmap.keys = s₂.to_finmap.keys s₁.keys ~ s₂.keys
theorem finmap.mem_keys {α : Type u} {β : α Type v} {a : α} {s : finmap β} :
a s.keys a s

empty #

@[protected, instance]
def finmap.has_emptyc {α : Type u} {β : α Type v} :

The empty map.

Equations
@[protected, instance]
def finmap.inhabited {α : Type u} {β : α Type v} :
Equations
@[simp]
theorem finmap.empty_to_finmap {α : Type u} {β : α Type v} :
@[simp]
theorem finmap.to_finmap_nil {α : Type u} {β : α Type v} [decidable_eq α] :
theorem finmap.not_mem_empty {α : Type u} {β : α Type v} {a : α} :
@[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) :
@[protected, instance]
def finmap.has_decidable_eq {α : Type u} {β : α Type v} [decidable_eq α] [Π (a : α), decidable_eq (β a)] :
Equations

lookup #

def finmap.lookup {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : finmap β) :
option (β a)

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

Equations
@[simp]
theorem finmap.lookup_to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : alist β) :
@[simp]
theorem finmap.lookup_list_to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : list (sigma β)) :
@[simp]
theorem finmap.lookup_empty {α : Type u} {β : α Type v} [decidable_eq α] (a : α) :
theorem finmap.lookup_is_some {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s : finmap β} :
theorem finmap.lookup_eq_none {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s : finmap β} :
theorem finmap.mem_lookup_iff {α : Type u} {β : α Type v} [decidable_eq α] {f : finmap β} {a : α} {b : β a} :
theorem finmap.lookup_eq_some_iff {α : Type u} {β : α Type v} [decidable_eq α] {f : finmap β} {a : α} {b : β a} :

A version of finmap.mem_lookup_iff with LHS in the simp-normal form.

@[simp]
theorem finmap.sigma_keys_lookup {α : Type u} {β : α Type v} [decidable_eq α] (f : finmap β) :
f.keys.sigma (λ (i : α), (finmap.lookup i f).to_finset) = {val := f.entries, nodup := _}
@[simp]
theorem finmap.lookup_singleton_eq {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} :
@[protected, instance]
def finmap.has_mem.mem.decidable {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : finmap β) :
Equations
theorem finmap.mem_iff {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s : finmap β} :
a s (b : β a), finmap.lookup a s = option.some b
theorem finmap.mem_of_lookup_eq_some {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {s : finmap β} (h : finmap.lookup a s = option.some b) :
a s
theorem finmap.ext_lookup {α : Type u} {β : α Type v} [decidable_eq α] {s₁ s₂ : finmap β} :
( (x : α), finmap.lookup x s₁ = finmap.lookup x s₂) s₁ = s₂
def finmap.keys_lookup_equiv {α : Type u} {β : α Type v} [decidable_eq α] :
finmap β {f // (i : α), ((f.snd i).is_some) i f.fst}

An equivalence between finmap β and pairs (keys : finset α, lookup : Π a, option (β a)) such that (lookup a).is_some ↔ a ∈ keys.

Equations
@[simp]
theorem finmap.keys_lookup_equiv_apply_coe_snd {α : Type u} {β : α Type v} [decidable_eq α] (f : finmap β) (i : α) :
@[simp]
theorem finmap.keys_lookup_equiv_symm_apply_keys {α : Type u} {β : α Type v} [decidable_eq α] (f : {f // (i : α), ((f.snd i).is_some) i f.fst}) :
@[simp]
theorem finmap.keys_lookup_equiv_symm_apply_lookup {α : Type u} {β : α Type v} [decidable_eq α] (f : {f // (i : α), ((f.snd i).is_some) i f.fst}) (a : α) :

replace #

def finmap.replace {α : Type u} {β : α Type v} [decidable_eq α] (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_to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) (s : alist β) :
@[simp]
theorem finmap.keys_replace {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) (s : finmap β) :
@[simp]
theorem finmap.mem_replace {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {b : β a} {s : finmap β} :
a' finmap.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 : α), β x bool) (s : finmap β) :

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

Equations
def finmap.all {α : Type u} {β : α Type v} (f : Π (x : α), β x bool) (s : finmap β) :

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

Equations

erase #

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

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

Equations
@[simp]
theorem finmap.erase_to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : alist β) :
@[simp]
theorem finmap.keys_erase_to_finset {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : alist β) :
@[simp]
theorem finmap.keys_erase {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : finmap β) :
@[simp]
theorem finmap.mem_erase {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {s : finmap β} :
a' finmap.erase a s a' a a' s
theorem finmap.not_mem_erase_self {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s : finmap β} :
@[simp]
theorem finmap.lookup_erase {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (s : finmap β) :
@[simp]
theorem finmap.lookup_erase_ne {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {s : finmap β} (h : a a') :
theorem finmap.erase_erase {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {s : finmap β} :

sdiff #

def finmap.sdiff {α : Type u} {β : α Type v} [decidable_eq α] (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
@[protected, instance]
def finmap.has_sdiff {α : Type u} {β : α Type v} [decidable_eq α] :
Equations

insert #

def finmap.insert {α : Type u} {β : α Type v} [decidable_eq α] (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_to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) (s : alist β) :
theorem finmap.insert_entries_of_neg {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {s : finmap β} :
a s (finmap.insert a b s).entries = a, b⟩ ::ₘ s.entries
@[simp]
theorem finmap.mem_insert {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {b' : β a'} {s : finmap β} :
a finmap.insert a' b' s a = a' a s
@[simp]
theorem finmap.lookup_insert {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} (s : finmap β) :
@[simp]
theorem finmap.lookup_insert_of_ne {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {b : β a} (s : finmap β) (h : a' a) :
@[simp]
theorem finmap.insert_insert {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b b' : β a} (s : finmap β) :
theorem finmap.insert_insert_of_ne {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {b : β a} {b' : β a'} (s : finmap β) (h : a a') :
theorem finmap.to_finmap_cons {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) (xs : list (sigma β)) :
theorem finmap.mem_list_to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (xs : list (sigma β)) :
a xs.to_finmap (b : β a), a, b⟩ xs
@[simp]
theorem finmap.insert_singleton_eq {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b b' : β a} :

extract #

def finmap.extract {α : Type u} {β : α Type v} [decidable_eq α] (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} [decidable_eq α] (a : α) (s : finmap β) :

union #

def finmap.union {α : Type u} {β : α Type v} [decidable_eq α] (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
@[protected, instance]
def finmap.has_union {α : Type u} {β : α Type v} [decidable_eq α] :
Equations
@[simp]
theorem finmap.mem_union {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s₁ s₂ : finmap β} :
a s₁ s₂ a s₁ a s₂
@[simp]
theorem finmap.union_to_finmap {α : Type u} {β : α Type v} [decidable_eq α] (s₁ s₂ : alist β) :
s₁.to_finmap s₂.to_finmap = (s₁ s₂).to_finmap
theorem finmap.keys_union {α : Type u} {β : α Type v} [decidable_eq α] {s₁ s₂ : finmap β} :
(s₁ s₂).keys = s₁.keys s₂.keys
@[simp]
theorem finmap.lookup_union_left {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s₁ s₂ : finmap β} :
a s₁ finmap.lookup a (s₁ s₂) = finmap.lookup a s₁
@[simp]
theorem finmap.lookup_union_right {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s₁ s₂ : finmap β} :
a s₁ finmap.lookup a (s₁ s₂) = finmap.lookup a s₂
theorem finmap.lookup_union_left_of_not_in {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s₁ s₂ : finmap β} (h : a s₂) :
finmap.lookup a (s₁ s₂) = finmap.lookup a s₁
@[simp]
theorem finmap.mem_lookup_union {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {s₁ s₂ : finmap β} :
b finmap.lookup a (s₁ s₂) b finmap.lookup a s₁ a s₁ b finmap.lookup a s₂
theorem finmap.mem_lookup_union_middle {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {s₁ s₂ s₃ : finmap β} :
b finmap.lookup a (s₁ s₃) a s₂ b finmap.lookup a (s₁ s₂ s₃)
theorem finmap.insert_union {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {s₁ s₂ : finmap β} :
finmap.insert a b (s₁ s₂) = finmap.insert a b s₁ s₂
theorem finmap.union_assoc {α : Type u} {β : α Type v} [decidable_eq α] {s₁ s₂ s₃ : finmap β} :
s₁ s₂ s₃ = s₁ (s₂ s₃)
@[simp]
theorem finmap.empty_union {α : Type u} {β : α Type v} [decidable_eq α] {s₁ : finmap β} :
s₁ = s₁
@[simp]
theorem finmap.union_empty {α : Type u} {β : α Type v} [decidable_eq α] {s₁ : finmap β} :
s₁ = s₁
theorem finmap.erase_union_singleton {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) (s : finmap β) (h : finmap.lookup a s = option.some b) :

disjoint #

def finmap.disjoint {α : Type u} {β : α Type v} (s₁ s₂ : finmap β) :
Prop

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

Equations
Instances for finmap.disjoint
theorem finmap.disjoint_empty {α : Type u} {β : α Type v} (x : finmap β) :
@[symm]
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} [decidable_eq α] (x y z : finmap β) :
theorem finmap.disjoint_union_right {α : Type u} {β : α Type v} [decidable_eq α] (x y z : finmap β) :
theorem finmap.union_comm_of_disjoint {α : Type u} {β : α Type v} [decidable_eq α] {s₁ s₂ : finmap β} :
s₁.disjoint s₂ s₁ s₂ = s₂ s₁
theorem finmap.union_cancel {α : Type u} {β : α Type v} [decidable_eq α] {s₁ s₂ s₃ : finmap β} (h : s₁.disjoint s₃) (h' : s₂.disjoint s₃) :
s₁ s₃ = s₂ s₃ s₁ = s₂