data.finmap - mathlib3 docs

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

s.lift_on f H = (quotient.lift_on s.entries (λ (l : list (sigma β)), {dom := l.nodupkeys, get := λ (nd : l.nodupkeys), f {entries := l, nodupkeys := nd}}) _).get _

source

@[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

source

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

s₁.lift_on₂ s₂ f H = s₁.lift_on (λ (l₁ : alist β), s₂.lift_on (f l₁) _) _

source

@[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₂

source

theorem finmap.induction_on {α : Type u} {β : α → Type v} {C : finmap β → Prop} (s : finmap β) (H : ∀ (a : alist β), C a.to_finmap) :

C s

source

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₂

source

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₃

source

@[ext]

theorem finmap.ext {α : Type u} {β : α → Type v} {s t : finmap β} :

s.entries = t.entries → s = t

source

@[simp]

theorem finmap.ext_iff {α : Type u} {β : α → Type v} {s t : finmap β} :

s.entries = t.entries ↔ s = t

source

@[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

finmap.has_mem = {mem := λ (a : α) (s : finmap β), a ∈ s.entries.keys}

source

theorem finmap.mem_def {α : Type u} {β : α → Type v} {a : α} {s : finmap β} :

a ∈ s ↔ a ∈ s.entries.keys

source

@[simp]

theorem finmap.mem_to_finmap {α : Type u} {β : α → Type v} {a : α} {s : alist β} :

a ∈ s.to_finmap ↔ a ∈ s

source

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

finset α

The set of keys of a finite map.

Equations

s.keys = {val := s.entries.keys, nodup := _}

source

@[simp]

theorem finmap.keys_val {α : Type u} {β : α → Type v} (s : alist β) :

s.to_finmap.keys.val = ↑(s.keys)

source

@[simp]

theorem finmap.keys_ext {α : Type u} {β : α → Type v} {s₁ s₂ : alist β} :

s₁.to_finmap.keys = s₂.to_finmap.keys ↔ s₁.keys ~ s₂.keys

source

theorem finmap.mem_keys {α : Type u} {β : α → Type v} {a : α} {s : finmap β} :

a ∈ s.keys ↔ a ∈ s

source

@[protected, instance]

def finmap.has_emptyc {α : Type u} {β : α → Type v} :

has_emptyc (finmap β)

The empty map.

Equations

finmap.has_emptyc = {emptyc := {entries := 0, nodupkeys := _}}

source

@[protected, instance]

def finmap.inhabited {α : Type u} {β : α → Type v} :

inhabited (finmap β)

Equations

finmap.inhabited = {default := ∅}

source

@[simp]

theorem finmap.empty_to_finmap {α : Type u} {β : α → Type v} :

∅.to_finmap = ∅

source

@[simp]

theorem finmap.to_finmap_nil {α : Type u} {β : α → Type v} [decidable_eq α] :

list.nil.to_finmap = ∅

source

theorem finmap.not_mem_empty {α : Type u} {β : α → Type v} {a : α} :

a ∉ ∅

source

@[simp]

theorem finmap.keys_empty {α : Type u} {β : α → Type v} :

∅.keys = ∅

source

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

finmap β

The singleton map.

Equations

finmap.singleton a b = (alist.singleton a b).to_finmap

source

@[simp]

theorem finmap.keys_singleton {α : Type u} {β : α → Type v} (a : α) (b : β a) :

(finmap.singleton a b).keys = {a}

source

@[simp]

theorem finmap.mem_singleton {α : Type u} {β : α → Type v} (x y : α) (b : β y) :

x ∈ finmap.singleton y b ↔ x = y

source

@[protected, instance]

def finmap.has_decidable_eq {α : Type u} {β : α → Type v} [decidable_eq α] [Π (a : α), decidable_eq (β a)] :

decidable_eq (finmap β)

Equations

finmap.has_decidable_eq s₁ s₂ = decidable_of_iff (s₁.entries = s₂.entries) finmap.ext_iff

source

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

finmap.lookup a s = s.lift_on (alist.lookup a) _

source

@[simp]

theorem finmap.lookup_to_finmap {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : alist β) :

finmap.lookup a s.to_finmap = alist.lookup a s

source

@[simp]

theorem finmap.lookup_list_to_finmap {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : list (sigma β)) :

finmap.lookup a s.to_finmap = list.lookup a s

source

@[simp]

theorem finmap.lookup_empty {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :

finmap.lookup a ∅ = option.none

source

theorem finmap.lookup_is_some {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : finmap β} :

↥((finmap.lookup a s).is_some) ↔ a ∈ s

source

theorem finmap.lookup_eq_none {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : finmap β} :

finmap.lookup a s = option.none ↔ a ∉ s

source

theorem finmap.mem_lookup_iff {α : Type u} {β : α → Type v} [decidable_eq α] {f : finmap β} {a : α} {b : β a} :

b ∈ finmap.lookup a f ↔ ⟨a, b⟩ ∈ f.entries

source

theorem finmap.lookup_eq_some_iff {α : Type u} {β : α → Type v} [decidable_eq α] {f : finmap β} {a : α} {b : β a} :

finmap.lookup a f = option.some b ↔ ⟨a, b⟩ ∈ f.entries

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

source

@[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 := _}

source

@[simp]

theorem finmap.lookup_singleton_eq {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} :

finmap.lookup a (finmap.singleton a b) = option.some b

source

@[protected, instance]

def finmap.has_mem.mem.decidable {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : finmap β) :

decidable (a ∈ s)

Equations

finmap.has_mem.mem.decidable a s = decidable_of_iff ↥((finmap.lookup a s).is_some) _

source

theorem finmap.mem_iff {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : finmap β} :

a ∈ s ↔ ∃ (b : β a), finmap.lookup a s = option.some b

source

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

source

theorem finmap.ext_lookup {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ : finmap β} :

(∀ (x : α), finmap.lookup x s₁ = finmap.lookup x s₂) → s₁ = s₂

source

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

finmap.keys_lookup_equiv = {to_fun := λ (f : finmap β), ⟨(f.keys, λ (i : α), finmap.lookup i f), _⟩, inv_fun := λ (f : {f // ∀ (i : α), ↥((f.snd i).is_some) ↔ i ∈ f.fst}), {entries := (f.val.fst.sigma (λ (i : α), (f.val.snd i).to_finset)).val, nodupkeys := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem finmap.keys_lookup_equiv_apply_coe_fst {α : Type u} {β : α → Type v} [decidable_eq α] (f : finmap β) :

↑(⇑finmap.keys_lookup_equiv f).fst = f.keys

source

@[simp]

theorem finmap.keys_lookup_equiv_apply_coe_snd {α : Type u} {β : α → Type v} [decidable_eq α] (f : finmap β) (i : α) :

↑(⇑finmap.keys_lookup_equiv f).snd i = finmap.lookup i f

source

@[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}) :

(⇑(finmap.keys_lookup_equiv.symm) f).keys = ↑f.fst

source

@[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 : α) :

finmap.lookup a (⇑(finmap.keys_lookup_equiv.symm) f) = ↑f.snd a

source

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

finmap β

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

Equations

finmap.replace a b s = s.lift_on (λ (t : alist β), (alist.replace a b t).to_finmap) _

source

@[simp]

theorem finmap.replace_to_finmap {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (s : alist β) :

finmap.replace a b s.to_finmap = (alist.replace a b s).to_finmap

source

@[simp]

theorem finmap.keys_replace {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (s : finmap β) :

(finmap.replace a b s).keys = s.keys

source

@[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

source

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

finmap.foldl f H d m = multiset.foldl (λ (d : δ) (s : sigma β), f d s.fst s.snd) _ d m.entries

source

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

bool

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

Equations

finmap.any f s = finmap.foldl (λ (x : bool) (y : α) (z : β y), x || f y z) _ bool.ff s

source

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

bool

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

Equations

finmap.all f s = finmap.foldl (λ (x : bool) (y : α) (z : β y), x && f y z) _ bool.tt s

source

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

finmap β

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

Equations

finmap.erase a s = s.lift_on (λ (t : alist β), (alist.erase a t).to_finmap) _

source

@[simp]

theorem finmap.erase_to_finmap {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : alist β) :

finmap.erase a s.to_finmap = (alist.erase a s).to_finmap

source

@[simp]

theorem finmap.keys_erase_to_finset {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : alist β) :

(alist.erase a s).to_finmap.keys = s.to_finmap.keys.erase a

source

@[simp]

theorem finmap.keys_erase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : finmap β) :

(finmap.erase a s).keys = s.keys.erase a

source

@[simp]

theorem finmap.mem_erase {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {s : finmap β} :

a' ∈ finmap.erase a s ↔ a' ≠ a ∧ a' ∈ s

source

theorem finmap.not_mem_erase_self {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : finmap β} :

a ∉ finmap.erase a s

source

@[simp]

theorem finmap.lookup_erase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : finmap β) :

finmap.lookup a (finmap.erase a s) = option.none

source

@[simp]

theorem finmap.lookup_erase_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {s : finmap β} (h : a ≠ a') :

finmap.lookup a (finmap.erase a' s) = finmap.lookup a s

source

theorem finmap.erase_erase {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {s : finmap β} :

finmap.erase a (finmap.erase a' s) = finmap.erase a' (finmap.erase a s)

source

def finmap.sdiff {α : Type u} {β : α → Type v} [decidable_eq α] (s s' : finmap β) :

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

s.sdiff s' = finmap.foldl (λ (s : finmap β) (x : α) (_x : β x), finmap.erase x s) finmap.sdiff._proof_1 s s'

source

@[protected, instance]

def finmap.has_sdiff {α : Type u} {β : α → Type v} [decidable_eq α] :

has_sdiff (finmap β)

Equations

finmap.has_sdiff = {sdiff := finmap.sdiff (λ (a b : α), _inst_1 a b)}

source

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

finmap β

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

Equations

finmap.insert a b s = s.lift_on (λ (t : alist β), (alist.insert a b t).to_finmap) _

source

@[simp]

theorem finmap.insert_to_finmap {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (s : alist β) :

finmap.insert a b s.to_finmap = (alist.insert a b s).to_finmap

source

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

source

@[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

source

@[simp]

theorem finmap.lookup_insert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} (s : finmap β) :

finmap.lookup a (finmap.insert a b s) = option.some b

source

@[simp]

theorem finmap.lookup_insert_of_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b : β a} (s : finmap β) (h : a' ≠ a) :

finmap.lookup a' (finmap.insert a b s) = finmap.lookup a' s

source

@[simp]

theorem finmap.insert_insert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b b' : β a} (s : finmap β) :

finmap.insert a b' (finmap.insert a b s) = finmap.insert a b' s

source

theorem finmap.insert_insert_of_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b : β a} {b' : β a'} (s : finmap β) (h : a ≠ a') :

finmap.insert a' b' (finmap.insert a b s) = finmap.insert a b (finmap.insert a' b' s)

source

theorem finmap.to_finmap_cons {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (xs : list (sigma β)) :

(⟨a, b⟩ :: xs).to_finmap = finmap.insert a b xs.to_finmap

source

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

source

@[simp]

theorem finmap.insert_singleton_eq {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b b' : β a} :

finmap.insert a b (finmap.singleton a b') = finmap.singleton a b

source

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

finmap.extract a s = s.lift_on (λ (t : alist β), prod.map id alist.to_finmap (alist.extract a t)) _

source

@[simp]

theorem finmap.extract_eq_lookup_erase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : finmap β) :

finmap.extract a s = (finmap.lookup a s, finmap.erase a s)

source

def finmap.union {α : Type u} {β : α → Type v} [decidable_eq α] (s₁ s₂ : finmap β) :

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

s₁.union s₂ = s₁.lift_on₂ s₂ (λ (s₁ s₂ : alist β), (s₁ ∪ s₂).to_finmap) finmap.union._proof_1

source

@[protected, instance]

def finmap.has_union {α : Type u} {β : α → Type v} [decidable_eq α] :

has_union (finmap β)

Equations

finmap.has_union = {union := finmap.union (λ (a b : α), _inst_1 a b)}

source

@[simp]

theorem finmap.mem_union {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s₁ s₂ : finmap β} :

a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

source

@[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

source

theorem finmap.keys_union {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ : finmap β} :

(s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys

source

@[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₁

source

@[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₂

source

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₁

source

@[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₂

source

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₃)

source

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₂

source

theorem finmap.union_assoc {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ s₃ : finmap β} :

s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

source

@[simp]

theorem finmap.empty_union {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ : finmap β} :

∅ ∪ s₁ = s₁

source

@[simp]

theorem finmap.union_empty {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ : finmap β} :

s₁ ∪ ∅ = s₁

source

theorem finmap.erase_union_singleton {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (s : finmap β) (h : finmap.lookup a s = option.some b) :

finmap.erase a s ∪ finmap.singleton a b = s

source