inductive Std.AssocList (α : Type u) (β : Type v) : Type (max u v)

AssocList α β is "the same as" List (α × β), but flattening the structure leads to one fewer pointer indirection (in the current code generator). It is mainly intended as a component of HashMap, but it can also be used as a plain key-value map.

• nil: {α : Type u} → {β : Type v} → Std.AssocList α β

  An empty list

• cons: {α : Type u} → {β : Type v} → α → β → Std.AssocList α β → Std.AssocList α β

  Add a key, value pair to the list

instance Std.instInhabitedAssocList : {a : Type u_1} → {a_1 : Type u_2} → Inhabited (Std.AssocList a a_1)

Equations

• Std.instInhabitedAssocList = { default := Std.AssocList.nil }

def Std.AssocList.toList {α : Type u_1} {β : Type u_2} : Std.AssocList α β → List (α × β)

O(n). Convert an AssocList α β into the equivalent List (α × β). This is used to give specifications for all the AssocList functions in terms of corresponding list functions.

Equations

• Std.AssocList.toList Std.AssocList.nil = []
• Std.AssocList.toList (Std.AssocList.cons a b es) = (a, b) :: Std.AssocList.toList es

instance Std.AssocList.instEmptyCollectionAssocList {α : Type u_1} {β : Type u_2} : EmptyCollection (Std.AssocList α β)

Equations

• Std.AssocList.instEmptyCollectionAssocList = { emptyCollection := Std.AssocList.nil }

@[simp]

theorem Std.AssocList.empty_eq {α : Type u_1} {β : Type u_2} : ∅ = Std.AssocList.nil

def Std.AssocList.isEmpty {α : Type u_1} {β : Type u_2} : Std.AssocList α β → Bool

O(1). Is the list empty?

Equations

• Std.AssocList.isEmpty x = match x with | Std.AssocList.nil => true | x => false

@[simp]

theorem Std.AssocList.isEmpty_eq {α : Type u_1} {β : Type u_2} (l : Std.AssocList α β) : Std.AssocList.isEmpty l = List.isEmpty (Std.AssocList.toList l)

def Std.AssocList.length {α : Type u_1} {β : Type u_2} (L : Std.AssocList α β) : Nat

The number of entries in an AssocList.

Equations

• Std.AssocList.length Std.AssocList.nil = 0
• Std.AssocList.length (Std.AssocList.cons a b es) = Std.AssocList.length es + 1

@[simp]

theorem Std.AssocList.length_nil {α : Type u_1} {β : Type u_2} : Std.AssocList.length Std.AssocList.nil = 0

@[simp]

theorem Std.AssocList.length_cons : ∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β} {t : Std.AssocList α β}, Std.AssocList.length (Std.AssocList.cons a b t) = Std.AssocList.length t + 1

theorem Std.AssocList.length_toList {α : Type u_1} {β : Type u_2} (l : Std.AssocList α β) : List.length (Std.AssocList.toList l) = Std.AssocList.length l

@[specialize #[]]

def Std.AssocList.foldlM {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δ → α → β → m δ) (init : δ) : Std.AssocList α β → m δ

O(n). Fold a monadic function over the list, from head to tail.

Equations

• Std.AssocList.foldlM f x Std.AssocList.nil = pure x
• Std.AssocList.foldlM f x (Std.AssocList.cons a b es) = do let __do_lift ← f x a b Std.AssocList.foldlM f __do_lift es

@[simp]

theorem Std.AssocList.foldlM_eq {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δ → α → β → m δ) (init : δ) (l : Std.AssocList α β) : Std.AssocList.foldlM f init l = List.foldlM (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init (Std.AssocList.toList l)

@[inline]

def Std.AssocList.foldl {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (as : Std.AssocList α β) : δ

O(n). Fold a function over the list, from head to tail.

Equations

• Std.AssocList.foldl f init as = Id.run (Std.AssocList.foldlM f init as)

@[simp]

theorem Std.AssocList.foldl_eq {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (l : Std.AssocList α β) : Std.AssocList.foldl f init l = List.foldl (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init (Std.AssocList.toList l)

def Std.AssocList.toListTR {α : Type u_1} {β : Type u_2} (as : Std.AssocList α β) : List (α × β)

Optimized version of toList.

Equations

• Std.AssocList.toListTR as = Array.toList (Std.AssocList.foldl (fun (r : Array (α × β)) (a : α) (b : β) => Array.push r (a, b)) #[] as)

@[csimp]

theorem Std.AssocList.toList_eq_toListTR : @Std.AssocList.toList = @Std.AssocList.toListTR

@[specialize #[]]

def Std.AssocList.forM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : α → β → m PUnit) : Std.AssocList α β → m PUnit

O(n). Run monadic function f on all elements in the list, from head to tail.

Equations

• Std.AssocList.forM f Std.AssocList.nil = pure PUnit.unit
• Std.AssocList.forM f (Std.AssocList.cons a b es) = do f a b Std.AssocList.forM f es

@[simp]

theorem Std.AssocList.forM_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : α → β → m PUnit) (l : Std.AssocList α β) : Std.AssocList.forM f l = List.forM (Std.AssocList.toList l) fun (x : α × β) => match x with | (a, b) => f a b

def Std.AssocList.mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) : Std.AssocList α β → Std.AssocList δ β

O(n). Map a function f over the keys of the list.

Equations

• Std.AssocList.mapKey f Std.AssocList.nil = Std.AssocList.nil
• Std.AssocList.mapKey f (Std.AssocList.cons a b es) = Std.AssocList.cons (f a) b (Std.AssocList.mapKey f es)

@[simp]

theorem Std.AssocList.toList_mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) (l : Std.AssocList α β) : Std.AssocList.toList (Std.AssocList.mapKey f l) = List.map (fun (x : α × β) => match x with | (a, b) => (f a, b)) (Std.AssocList.toList l)

@[simp]

theorem Std.AssocList.length_mapKey : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {β : Type u_3} {l : Std.AssocList α β}, Std.AssocList.length (Std.AssocList.mapKey f l) = Std.AssocList.length l

def Std.AssocList.mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) : Std.AssocList α β → Std.AssocList α δ

O(n). Map a function f over the values of the list.

Equations

• Std.AssocList.mapVal f Std.AssocList.nil = Std.AssocList.nil
• Std.AssocList.mapVal f (Std.AssocList.cons a b es) = Std.AssocList.cons a (f a b) (Std.AssocList.mapVal f es)

@[simp]

theorem Std.AssocList.toList_mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) (l : Std.AssocList α β) : Std.AssocList.toList (Std.AssocList.mapVal f l) = List.map (fun (x : α × β) => match x with | (a, b) => (a, f a b)) (Std.AssocList.toList l)

@[simp]

theorem Std.AssocList.length_mapVal : ∀ {α : Type u_1} {β : Type u_2} {β_1 : Type u_3} {f : α → β → β_1} {l : Std.AssocList α β}, Std.AssocList.length (Std.AssocList.mapVal f l) = Std.AssocList.length l

@[specialize #[]]

def Std.AssocList.findEntryP? {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : Std.AssocList α β → Option (α × β)

O(n). Returns the first entry in the list whose entry satisfies p.

Equations

• Std.AssocList.findEntryP? p Std.AssocList.nil = none
• Std.AssocList.findEntryP? p (Std.AssocList.cons a b es) = bif p a b then some (a, b) else Std.AssocList.findEntryP? p es

@[simp]

theorem Std.AssocList.findEntryP?_eq {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Std.AssocList α β) : Std.AssocList.findEntryP? p l = List.find? (fun (x : α × β) => match x with | (a, b) => p a b) (Std.AssocList.toList l)

@[inline]

def Std.AssocList.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Option (α × β)

O(n). Returns the first entry in the list whose key is equal to a.

Equations

• Std.AssocList.findEntry? a l = Std.AssocList.findEntryP? (fun (k : α) (x : β) => k == a) l

@[simp]

theorem Std.AssocList.findEntry?_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Std.AssocList.findEntry? a l = List.find? (fun (x : α × β) => x.fst == a) (Std.AssocList.toList l)

def Std.AssocList.find? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) : Std.AssocList α β → Option β

O(n). Returns the first value in the list whose key is equal to a.

Equations

• Std.AssocList.find? a Std.AssocList.nil = none
• Std.AssocList.find? a (Std.AssocList.cons a_1 b es) = match a_1 == a with | true => some b | false => Std.AssocList.find? a es

theorem Std.AssocList.find?_eq_findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Std.AssocList.find? a l = Option.map (fun (x : α × β) => x.snd) (Std.AssocList.findEntry? a l)

@[simp]

theorem Std.AssocList.find?_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Std.AssocList.find? a l = Option.map (fun (x : α × β) => x.snd) (List.find? (fun (x : α × β) => x.fst == a) (Std.AssocList.toList l))

@[specialize #[]]

def Std.AssocList.any {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : Std.AssocList α β → Bool

O(n). Returns true if any entry in the list satisfies p.

Equations

• Std.AssocList.any p Std.AssocList.nil = false
• Std.AssocList.any p (Std.AssocList.cons a b es) = (p a b || Std.AssocList.any p es)

@[simp]

theorem Std.AssocList.any_eq {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Std.AssocList α β) : Std.AssocList.any p l = List.any (Std.AssocList.toList l) fun (x : α × β) => match x with | (a, b) => p a b

@[specialize #[]]

def Std.AssocList.all {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : Std.AssocList α β → Bool

O(n). Returns true if every entry in the list satisfies p.

Equations

• Std.AssocList.all p Std.AssocList.nil = true
• Std.AssocList.all p (Std.AssocList.cons a b es) = (p a b && Std.AssocList.all p es)

@[simp]

theorem Std.AssocList.all_eq {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Std.AssocList α β) : Std.AssocList.all p l = List.all (Std.AssocList.toList l) fun (x : α × β) => match x with | (a, b) => p a b

def Std.AssocList.All {α : Type u_1} {β : Type u_2} (p : α → β → Prop) (l : Std.AssocList α β) : Prop

Returns true if every entry in the list satisfies p.

Equations

• Std.AssocList.All p l = ∀ (a : α × β), a ∈ Std.AssocList.toList l → p a.fst a.snd

@[inline]

def Std.AssocList.contains {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Bool

O(n). Returns true if there is an element in the list whose key is equal to a.

Equations

• Std.AssocList.contains a l = Std.AssocList.any (fun (k : α) (x : β) => k == a) l

@[simp]

theorem Std.AssocList.contains_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Std.AssocList.contains a l = List.any (Std.AssocList.toList l) fun (x : α × β) => x.fst == a

def Std.AssocList.replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) : Std.AssocList α β → Std.AssocList α β

O(n). Replace the first entry in the list with key equal to a to have key a and value b.

Equations

• Std.AssocList.replace a b Std.AssocList.nil = Std.AssocList.nil
• Std.AssocList.replace a b (Std.AssocList.cons a_1 b_1 es) = match a_1 == a with | true => Std.AssocList.cons a b es | false => Std.AssocList.cons a_1 b_1 (Std.AssocList.replace a b es)

@[simp]

theorem Std.AssocList.toList_replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) (l : Std.AssocList α β) : Std.AssocList.toList (Std.AssocList.replace a b l) = List.replaceF (fun (x : α × β) => bif x.fst == a then some (a, b) else none) (Std.AssocList.toList l)

@[simp]

theorem Std.AssocList.length_replace {α : Type u_1} : ∀ {β : Type u_2} {b : β} {l : Std.AssocList α β} [inst : BEq α] {a : α}, Std.AssocList.length (Std.AssocList.replace a b l) = Std.AssocList.length l

@[specialize #[]]

def Std.AssocList.eraseP {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : Std.AssocList α β → Std.AssocList α β

O(n). Remove the first entry in the list with key equal to a.

Equations

• Std.AssocList.eraseP p Std.AssocList.nil = Std.AssocList.nil
• Std.AssocList.eraseP p (Std.AssocList.cons a b es) = bif p a b then es else Std.AssocList.cons a b (Std.AssocList.eraseP p es)

@[simp]

theorem Std.AssocList.toList_eraseP {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Std.AssocList α β) : Std.AssocList.toList (Std.AssocList.eraseP p l) = List.eraseP (fun (x : α × β) => match x with | (a, b) => p a b) (Std.AssocList.toList l)

@[inline]

def Std.AssocList.erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Std.AssocList α β

O(n). Remove the first entry in the list with key equal to a.

Equations

• Std.AssocList.erase a l = Std.AssocList.eraseP (fun (k : α) (x : β) => k == a) l

@[simp]

theorem Std.AssocList.toList_erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Std.AssocList α β) : Std.AssocList.toList (Std.AssocList.erase a l) = List.eraseP (fun (x : α × β) => x.fst == a) (Std.AssocList.toList l)

def Std.AssocList.modify {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (f : α → β → β) : Std.AssocList α β → Std.AssocList α β

O(n). Replace the first entry a', b in the list with key equal to a to have key a and value f a' b.

Equations

• Std.AssocList.modify a f Std.AssocList.nil = Std.AssocList.nil
• Std.AssocList.modify a f (Std.AssocList.cons a_1 b es) = match a_1 == a with | true => Std.AssocList.cons a (f a_1 b) es | false => Std.AssocList.cons a_1 b (Std.AssocList.modify a f es)

@[simp]

theorem Std.AssocList.toList_modify {α : Type u_1} {β : Type u_2} {f : α → β → β} [BEq α] (a : α) (l : Std.AssocList α β) : Std.AssocList.toList (Std.AssocList.modify a f l) = List.replaceF (fun (x : α × β) => match x with | (k, v) => bif k == a then some (a, f k v) else none) (Std.AssocList.toList l)

@[simp]

theorem Std.AssocList.length_modify {α : Type u_1} : ∀ {β : Type u_2} {f : α → β → β} {l : Std.AssocList α β} [inst : BEq α] {a : α}, Std.AssocList.length (Std.AssocList.modify a f l) = Std.AssocList.length l

@[specialize #[]]

def Std.AssocList.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [Monad m] (as : Std.AssocList α β) (init : δ) (f : α × β → δ → m (ForInStep δ)) : m δ

The implementation of ForIn, which enables for (k, v) in aList do ... notation.

Equations

• One or more equations did not get rendered due to their size.
• Std.AssocList.forIn Std.AssocList.nil init f = pure init

instance Std.AssocList.instForInAssocListProd {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} : ForIn m (Std.AssocList α β) (α × β)

Equations

• Std.AssocList.instForInAssocListProd = { forIn := fun {β_1 : Type u_1} [Monad m] => Std.AssocList.forIn }

@[simp]

theorem Std.AssocList.forIn_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [Monad m] (l : Std.AssocList α β) (init : δ) (f : α × β → δ → m (ForInStep δ)) : forIn l init f = forIn (Std.AssocList.toList l) init f

def Std.AssocList.pop? {α : Type u_1} {β : Type u_2} : Std.AssocList α β → Option ((α × β) × Std.AssocList α β)

Split the list into head and tail, if possible.

Equations

• Std.AssocList.pop? x = match x with | Std.AssocList.nil => none | Std.AssocList.cons a b l => some ((a, b), l)

instance Std.AssocList.instToStreamAssocList {α : Type u_1} {β : Type u_2} : ToStream (Std.AssocList α β) (Std.AssocList α β)

Equations

• Std.AssocList.instToStreamAssocList = { toStream := fun (x : Std.AssocList α β) => x }

instance Std.AssocList.instStreamAssocListProd {α : Type u_1} {β : Type u_2} : Stream (Std.AssocList α β) (α × β)

Equations

• Std.AssocList.instStreamAssocListProd = { next? := Std.AssocList.pop? }

def List.toAssocList {α : Type u_1} {β : Type u_2} : List (α × β) → Std.AssocList α β

Converts a list into an AssocList. This is the inverse function to AssocList.toList.

Equations

• List.toAssocList [] = Std.AssocList.nil
• List.toAssocList ((a, b) :: es) = Std.AssocList.cons a b (List.toAssocList es)

@[simp]

theorem List.toList_toAssocList {α : Type u_1} {β : Type u_2} (l : List (α × β)) : Std.AssocList.toList (List.toAssocList l) = l

@[simp]

theorem Std.AssocList.toList_toAssocList {α : Type u_1} {β : Type u_2} (l : Std.AssocList α β) : List.toAssocList (Std.AssocList.toList l) = l

@[simp]

theorem List.length_toAssocList {α : Type u_1} {β : Type u_2} (l : List (α × β)) : Std.AssocList.length (List.toAssocList l) = List.length l

def Std.AssocList.beq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : Std.AssocList α β → Std.AssocList α β → Bool

Implementation of == on AssocList.

Equations

• Std.AssocList.beq Std.AssocList.nil Std.AssocList.nil = true
• Std.AssocList.beq (Std.AssocList.cons key value tail) Std.AssocList.nil = false
• Std.AssocList.beq Std.AssocList.nil (Std.AssocList.cons key value tail) = false
• Std.AssocList.beq (Std.AssocList.cons a b t) (Std.AssocList.cons a' b' t') = (a == a' && b == b' && Std.AssocList.beq t t')

instance Std.AssocList.instBEqAssocList {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : BEq (Std.AssocList α β)

Boolean equality for AssocList. (This relation cares about the ordering of the key-value pairs.)

Equations

• Std.AssocList.instBEqAssocList = { beq := Std.AssocList.beq }

@[simp]

theorem Std.AssocList.beq_nil₂ {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : (Std.AssocList.nil == Std.AssocList.nil) = true

@[simp]

theorem Std.AssocList.beq_nil_cons {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Std.AssocList α β} [BEq α] [BEq β] : (Std.AssocList.nil == Std.AssocList.cons a b t) = false

@[simp]

theorem Std.AssocList.beq_cons_nil {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Std.AssocList α β} [BEq α] [BEq β] : (Std.AssocList.cons a b t == Std.AssocList.nil) = false

@[simp]

theorem Std.AssocList.beq_cons₂ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Std.AssocList α β} {a' : α} {b' : β} {t' : Std.AssocList α β} [BEq α] [BEq β] : (Std.AssocList.cons a b t == Std.AssocList.cons a' b' t') = (a == a' && b == b' && t == t')

instance Std.AssocList.instLawfulBEqAssocListInstBEqAssocList {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] : LawfulBEq (Std.AssocList α β)

Equations

• (_ : LawfulBEq (Std.AssocList α β)) = (_ : LawfulBEq (Std.AssocList α β))

theorem Std.AssocList.beq_eq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] {l : Std.AssocList α β} {m : Std.AssocList α β} : (l == m) = (Std.AssocList.toList l == Std.AssocList.toList m)