# Finite maps over Multiset#

### Multisets of sigma types #

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

Multiset of keys of an association multiset.

Equations
Instances For
@[simp]
theorem Multiset.coe_keys {α : Type u} {β : αType v} {l : List ()} :
(l).keys = l.keys
def Multiset.NodupKeys {α : Type u} {β : αType v} (s : Multiset ()) :

NodupKeys s means that s has no duplicate keys.

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

Alias of the reverse direction of Multiset.nodup_keys.

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

### 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
theorem Finmap.nodupKeys {α : Type u} {β : αType v} (self : ) :
self.entries.NodupKeys

There are no duplicate keys in entries

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

The quotient map from AList to Finmap.

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

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

Equations
• s.toFinmap = s.toAList.toFinmap
Instances For
theorem Finmap.nodup_entries {α : Type u} {β : αType v} (f : ) :
f.entries.Nodup

### Lifting from AList #

def Finmap.liftOn {α : Type u} {β : αType v} {γ : Type u_1} (s : ) (f : γ) (H : ∀ (a b : ), 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.
Instances For
@[simp]
theorem Finmap.liftOn_toFinmap {α : Type u} {β : αType v} {γ : Type u_1} (s : ) (f : γ) (H : ∀ (a b : ), 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₂ : ) (f : γ) (H : ∀ (a₁ b₁ a₂ b₂ : ), 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
• s₁.liftOn₂ s₂ f H = s₁.liftOn (fun (l₁ : ) => s₂.liftOn (f l₁) )
Instances For
@[simp]
theorem Finmap.liftOn₂_toFinmap {α : Type u} {β : αType v} {γ : Type u_1} (s₁ : ) (s₂ : ) (f : γ) (H : ∀ (a₁ b₁ a₂ b₂ : ), 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 : Prop} (s : ) (H : ∀ (a : ), C a.toFinmap) :
C s
theorem Finmap.induction_on₂ {α : Type u} {β : αType v} {C : Prop} (s₁ : ) (s₂ : ) (H : ∀ (a₁ a₂ : ), C a₁.toFinmap a₂.toFinmap) :
C s₁ s₂
theorem Finmap.induction_on₃ {α : Type u} {β : αType v} {C : Prop} (s₁ : ) (s₂ : ) (s₃ : ) (H : ∀ (a₁ a₂ a₃ : ), C a₁.toFinmap a₂.toFinmap a₃.toFinmap) :
C s₁ s₂ s₃

### extensionality #

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

### mem #

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

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

Equations
• Finmap.instMembership = { mem := fun (a : α) (s : ) => a s.entries.keys }
theorem Finmap.mem_def {α : Type u} {β : αType v} {a : α} {s : } :
a s a s.entries.keys
@[simp]
theorem Finmap.mem_toFinmap {α : Type u} {β : αType v} {a : α} {s : } :
a s.toFinmap a s

### keys #

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

The set of keys of a finite map.

Equations
• s.keys = { val := s.entries.keys, nodup := }
Instances For
@[simp]
theorem Finmap.keys_val {α : Type u} {β : αType v} (s : ) :
s.toFinmap.keys.val = s.keys
@[simp]
theorem Finmap.keys_ext {α : Type u} {β : αType v} {s₁ : } {s₂ : } :
s₁.toFinmap.keys = s₂.toFinmap.keys s₁.keys.Perm s₂.keys
theorem Finmap.mem_keys {α : Type u} {β : αType v} {a : α} {s : } :
a s.keys a s

### empty #

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

The empty map.

Equations
• Finmap.instEmptyCollection = { emptyCollection := { entries := 0, nodupKeys := } }
instance Finmap.instInhabited {α : Type u} {β : αType v} :
Equations
• Finmap.instInhabited = { default := }
@[simp]
theorem Finmap.empty_toFinmap {α : Type u} {β : αType v} :
.toFinmap =
@[simp]
theorem Finmap.toFinmap_nil {α : Type u} {β : αType v} [] :
[].toFinmap =
theorem Finmap.not_mem_empty {α : Type u} {β : αType v} {a : α} :
a
@[simp]
theorem Finmap.keys_empty {α : Type u} {β : αType v} :
.keys =

### singleton #

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

The singleton map.

Equations
• = ().toFinmap
Instances For
@[simp]
theorem Finmap.keys_singleton {α : Type u} {β : αType v} (a : α) (b : β a) :
().keys = {a}
@[simp]
theorem Finmap.mem_singleton {α : Type u} {β : αType v} (x : α) (y : α) (b : β y) :
x x = y
instance Finmap.decidableEq {α : Type u} {β : αType v} [] [(a : α) → DecidableEq (β a)] :
Equations
• x✝.decidableEq x = match x✝, x with | x, x_1 => decidable_of_iff (x.entries = x_1.entries)

### lookup #

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

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

Equations
• = s.liftOn ()
Instances For
@[simp]
theorem Finmap.lookup_toFinmap {α : Type u} {β : αType v} [] (a : α) (s : ) :
Finmap.lookup a s.toFinmap =
@[simp]
theorem Finmap.dlookup_list_toFinmap {α : Type u} {β : αType v} [] (a : α) (s : List ()) :
Finmap.lookup a s.toFinmap =
@[simp]
theorem Finmap.lookup_empty {α : Type u} {β : αType v} [] (a : α) :
= none
theorem Finmap.lookup_isSome {α : Type u} {β : αType v} [] {a : α} {s : } :
().isSome = true a s
theorem Finmap.lookup_eq_none {α : Type u} {β : αType v} [] {a : α} {s : } :
= none as
theorem Finmap.mem_lookup_iff {α : Type u} {β : αType v} [] {s : } {a : α} {b : β a} :
b a, b s.entries
theorem Finmap.lookup_eq_some_iff {α : Type u} {β : αType v} [] {s : } {a : α} {b : β a} :
= some b a, b s.entries
@[simp]
theorem Finmap.sigma_keys_lookup {α : Type u} {β : αType v} [] (s : ) :
(s.keys.sigma fun (i : α) => ().toFinset) = { val := s.entries, nodup := }
@[simp]
theorem Finmap.lookup_singleton_eq {α : Type u} {β : αType v} [] {a : α} {b : β a} :
= some b
instance Finmap.instDecidableMem {α : Type u} {β : αType v} [] (a : α) (s : ) :
Equations
theorem Finmap.mem_iff {α : Type u} {β : αType v} [] {a : α} {s : } :
a s ∃ (b : β a), = some b
theorem Finmap.mem_of_lookup_eq_some {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } (h : = some b) :
a s
theorem Finmap.ext_lookup {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } :
(∀ (x : α), = )s₁ = s₂
@[simp]
theorem Finmap.keysLookupEquiv_apply_coe_fst {α : Type u} {β : αType v} [] (s : ) :
((Finmap.keysLookupEquiv s)).1 = s.keys
@[simp]
theorem Finmap.keysLookupEquiv_apply_coe_snd {α : Type u} {β : αType v} [] (s : ) (i : α) :
((Finmap.keysLookupEquiv s)).2 i =
def Finmap.keysLookupEquiv {α : Type u} {β : αType v} [] :
{ f : × ((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.
Instances For
@[simp]
theorem Finmap.keysLookupEquiv_symm_apply_keys {α : Type u} {β : αType v} [] (f : { f : × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true i f.1 }) :
(Finmap.keysLookupEquiv.symm f).keys = (f).1
@[simp]
theorem Finmap.keysLookupEquiv_symm_apply_lookup {α : Type u} {β : αType v} [] (f : { f : × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true i f.1 }) (a : α) :
Finmap.lookup a (Finmap.keysLookupEquiv.symm f) = (f).2 a

### replace #

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

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

Equations
• = s.liftOn (fun (t : ) => ().toFinmap)
Instances For
@[simp]
theorem Finmap.replace_toFinmap {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :
Finmap.replace a b s.toFinmap = ().toFinmap
@[simp]
theorem Finmap.keys_replace {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :
().keys = s.keys
@[simp]
theorem Finmap.mem_replace {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} {s : } :
a' 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 : ) :
δ

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

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

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

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

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

Equations
Instances For

### erase #

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

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

Equations
• = s.liftOn (fun (t : ) => ().toFinmap)
Instances For
@[simp]
theorem Finmap.erase_toFinmap {α : Type u} {β : αType v} [] (a : α) (s : ) :
Finmap.erase a s.toFinmap = ().toFinmap
@[simp]
theorem Finmap.keys_erase_toFinset {α : Type u} {β : αType v} [] (a : α) (s : ) :
().toFinmap.keys = s.toFinmap.keys.erase a
@[simp]
theorem Finmap.keys_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
().keys = s.keys.erase a
@[simp]
theorem Finmap.mem_erase {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } :
a' a' a a' s
theorem Finmap.not_mem_erase_self {α : Type u} {β : αType v} [] {a : α} {s : } :
a
@[simp]
theorem Finmap.lookup_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
Finmap.lookup a () = none
@[simp]
theorem Finmap.lookup_erase_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } (h : a a') :
theorem Finmap.erase_erase {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } :

### sdiff #

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

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 (fun (s : ) (x : α) (x_1 : β x) => ) s s'
Instances For
instance Finmap.instSDiff {α : Type u} {β : αType v} [] :
Equations
• Finmap.instSDiff = { sdiff := Finmap.sdiff }

### insert #

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

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

Equations
Instances For
@[simp]
theorem Finmap.insert_toFinmap {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :
Finmap.insert a b s.toFinmap = (AList.insert a b s).toFinmap
theorem Finmap.insert_entries_of_neg {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } :
as().entries = a, b ::ₘ s.entries
@[simp]
theorem Finmap.mem_insert {α : Type u} {β : αType v} [] {a : α} {a' : α} {b' : β a'} {s : } :
a Finmap.insert a' b' s a = a' a s
@[simp]
theorem Finmap.lookup_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} (s : ) :
@[simp]
theorem Finmap.lookup_insert_of_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} (s : ) (h : a' a) :
@[simp]
theorem Finmap.insert_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} {b' : β a} (s : ) :
theorem Finmap.insert_insert_of_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} {b' : β a'} (s : ) (h : a a') :
theorem Finmap.toFinmap_cons {α : Type u} {β : αType v} [] (a : α) (b : β a) (xs : List ()) :
(a, b :: xs).toFinmap = Finmap.insert a b xs.toFinmap
theorem Finmap.mem_list_toFinmap {α : Type u} {β : αType v} [] (a : α) (xs : List ()) :
a xs.toFinmap ∃ (b : β a), a, b xs
@[simp]
theorem Finmap.insert_singleton_eq {α : Type u} {β : αType v} [] {a : α} {b : β a} {b' : β a} :

### extract #

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

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

Equations
• = s.liftOn (fun (t : ) => Prod.map id AList.toFinmap ())
Instances For
@[simp]
theorem Finmap.extract_eq_lookup_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
= (, )

### union #

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

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₁.liftOn₂ s₂ (fun (s₁ s₂ : ) => (s₁ s₂).toFinmap)
Instances For
instance Finmap.instUnion {α : Type u} {β : αType v} [] :
Equations
• Finmap.instUnion = { union := Finmap.union }
@[simp]
theorem Finmap.mem_union {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
a s₁ s₂ a s₁ a s₂
@[simp]
theorem Finmap.union_toFinmap {α : Type u} {β : αType v} [] (s₁ : ) (s₂ : ) :
s₁.toFinmap s₂.toFinmap = (s₁ s₂).toFinmap
theorem Finmap.keys_union {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } :
(s₁ s₂).keys = s₁.keys s₂.keys
@[simp]
theorem Finmap.lookup_union_left {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
a s₁Finmap.lookup a (s₁ s₂) =
@[simp]
theorem Finmap.lookup_union_right {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
as₁Finmap.lookup a (s₁ s₂) =
theorem Finmap.lookup_union_left_of_not_in {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } (h : as₂) :
Finmap.lookup a (s₁ s₂) =
theorem Finmap.mem_lookup_union {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
b Finmap.lookup a (s₁ s₂) b as₁ b
theorem Finmap.mem_lookup_union_middle {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } {s₃ : } :
b Finmap.lookup a (s₁ s₃)as₂b Finmap.lookup a (s₁ s₂ s₃)
theorem Finmap.insert_union {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
Finmap.insert a b (s₁ s₂) = Finmap.insert a b s₁ s₂
theorem Finmap.union_assoc {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } {s₃ : } :
s₁ s₂ s₃ = s₁ (s₂ s₃)
@[simp]
theorem Finmap.empty_union {α : Type u} {β : αType v} [] {s₁ : } :
s₁ = s₁
@[simp]
theorem Finmap.union_empty {α : Type u} {β : αType v} [] {s₁ : } :
s₁ = s₁
theorem Finmap.erase_union_singleton {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) (h : = some b) :
= s

### Disjoint #

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

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

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