Ordered association lists

OrderedAssocList is a wrapper around AssocList, with the additional invariant that the keys are in strictly increasing order.

As a consequence, an OrderedAssocList is determined by the lookup function l[x]?, that is (∀ a, l₁[a]? = l₂[a]?) → l₁ = l₂ and this makes proving identities between operations much easier than with AssocList.

As the operations on OrderedAssocList are defined in terms of AssocList, they evaluate in the kernel, but inherit the O(n) time complexity (i.e. are not suitable for large data). Their advantage relative to an ordered map is the simple extensionality property above.

We will later add another wrapper requiring that a "default" value does not appear, so e.g. finitely supported functions can be uniquely represented.

The main operations defined are:

• l[x]?, which linearly searches the list, stopping if the keys get too large.
• insert, which inserts a new key-value pair, maintaining the order invariant.
• filterMapVal f, for f : α → β → Option γ, which applies a function to values, dropping some values.
• merge f for f : α → Option β → Option γ → Option δ which merges two lists, dropping some values. It runs in time O(l₁.length + l₂.length).

We first define some predicates and operations in the AssocList namespace.

• KeysOrdered cmp l asserts that the keys of an l : AssocList are strictly increasing with respect to a comparator cmp.
• LTHeadKey cmp a l asserts that a is less than (according to cmp) the first key of l, or that l is empty.

def Batteries.AssocList.headKey? {α : Type u_1} {β : Type u_2} (l : AssocList α β) : Option α

The head key of an AssocList, or none if the list is empty.

Equations

• Batteries.AssocList.nil.headKey? = none
• (Batteries.AssocList.cons a value tail).headKey? = some a

@[simp]

theorem Batteries.AssocList.headKey?_nil {α : Type u_1} {β : Type u_2} : nil.headKey? = none

@[simp]

theorem Batteries.AssocList.headKey?_cons {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} : (cons a b t).headKey? = some a

theorem Batteries.AssocList.headKey?_eq_head? {α : Type u_1} {β : Type u_2} (l : AssocList α β) : l.headKey? = Option.map Prod.fst l.toList.head?

@[reducible, inline]

abbrev Batteries.AssocList.LTHeadKey {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (a : α) (t : AssocList α β) : Prop

The condition that an element is less than the first key of an AssocList, or that list is empty.

Equations

• Batteries.AssocList.LTHeadKey cmp a t = match t.headKey? with | none => True | some x => cmp a x = Ordering.lt

@[simp]

theorem Batteries.AssocList.ltHeadKey_nil {α : Type u_1} {a : α} {β : Type u_2} {cmp : α → α → Ordering} : LTHeadKey cmp a nil = True

@[simp]

theorem Batteries.AssocList.ltHeadKey_cons {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a x : α✝} {β✝ : Type u_2} {y : β✝} {t : AssocList α✝ β✝} : LTHeadKey cmp a (cons x y t) = (cmp a x = Ordering.lt)

theorem Batteries.AssocList.ltHeadKey_iff {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {a : α} {l : AssocList α β} : LTHeadKey cmp a l ↔ ∀ (p : α × β), p ∈ l.toList.head? → cmp a p.fst = Ordering.lt

def Batteries.AssocList.KeysOrdered {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) : AssocList α β → Prop

The predicate that the keys of an AssocList are in strictly increasing order according to the comparator cmp.

Equations

• Batteries.AssocList.KeysOrdered cmp Batteries.AssocList.nil = True
• Batteries.AssocList.KeysOrdered cmp (Batteries.AssocList.cons a value tail) = (Batteries.AssocList.LTHeadKey cmp a tail ∧ Batteries.AssocList.KeysOrdered cmp tail)

@[simp]

theorem Batteries.AssocList.keysOrdered_cons_nil {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {b : β✝} : KeysOrdered cmp (cons a b nil)

theorem Batteries.AssocList.keysOrdered_iff_pairwise {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : AssocList α β} : KeysOrdered cmp l ↔ List.Pairwise (fun (p q : α × β) => cmp p.fst q.fst = Ordering.lt) l.toList

theorem Batteries.AssocList.KeysOrdered.tail {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} (h : KeysOrdered cmp (AssocList.cons a b t)) : KeysOrdered cmp t

theorem Batteries.AssocList.KeysOrdered.lt_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {x : α} {y : β} {t : AssocList α β} (h : KeysOrdered cmp (AssocList.cons x y t)) {p : α × β} (hp : p ∈ t.toList) : cmp x p.fst = Ordering.lt

theorem Batteries.AssocList.KeysOrdered.ltHeadKey {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} (w : KeysOrdered cmp (AssocList.cons a b t)) : LTHeadKey cmp a t

theorem Batteries.AssocList.ltHeadKey_of_cons {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a x : α✝} {β✝ : Type u_2} {y : β✝} {t : AssocList α✝ β✝} [Std.TransCmp cmp] (w : LTHeadKey cmp a (cons x y t)) (h : KeysOrdered cmp (cons x y t)) : LTHeadKey cmp a t

theorem Batteries.AssocList.ltHeadKey_of_le {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {x a : α✝} {β✝ : Type u_2} {t : AssocList α✝ β✝} [Std.TransCmp cmp] (h : cmp x a ≠ Ordering.gt) (w : LTHeadKey cmp a t) : LTHeadKey cmp x t

@[reducible, inline]

abbrev Batteries.AssocList.LEHeadKey {α : Type u_1} {β : Type u_2} {γ : Type u_3} (cmp : α → α → Ordering) (s : AssocList α β) (t : AssocList α γ) : Prop

A relation on two AssocLists, asserting that the head key of the first list is at most the head key of the second list, or that the second list is empty.

Equations

• Batteries.AssocList.LEHeadKey cmp s t = match s.headKey?, t.headKey? with | some a₁, some a₂ => cmp a₁ a₂ ≠ Ordering.gt | none, some val => False | x, none => True

@[simp]

theorem Batteries.AssocList.leHeadKey_cons_cons {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} {x : α✝} {β✝¹ : Type u_3} {y : β✝¹} {s : AssocList α✝ β✝¹} : LEHeadKey cmp (cons a b t) (cons x y s) = (cmp a x ≠ Ordering.gt)

theorem Batteries.AssocList.leHeadKey_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : α → α → Ordering} {s : AssocList α β} {t : AssocList α γ} : LEHeadKey cmp s t ↔ ∀ (q : α × γ), q ∈ t.toList.head? → ∃ (p : α × β), p ∈ s.toList.head? ∧ cmp p.fst q.fst ≠ Ordering.gt

theorem Batteries.AssocList.ltHeadKey_of_leHeadKey {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {s : AssocList α✝ β✝} {β✝¹ : Type u_3} {t : AssocList α✝ β✝¹} [Std.TransCmp cmp] (w : LTHeadKey cmp a s) (h : LEHeadKey cmp s t) : LTHeadKey cmp a t

theorem Batteries.AssocList.leHeadKey_cons {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {x : α✝} {β✝ : Type u_2} {y : β✝} {t : AssocList α✝ β✝} {β✝¹ : Type u_3} {s : AssocList α✝ β✝¹} [Std.TransCmp cmp] (h : KeysOrdered cmp (cons x y t)) (w : LEHeadKey cmp t s) : LEHeadKey cmp (cons x y t) s

theorem Batteries.AssocList.KeysOrdered.cons {α : Type u_1} {a : α} {β✝ : Type u_2} {t : AssocList α β✝} {b : β✝} {cmp : α → α → Ordering} (w : LTHeadKey cmp a t) (h : KeysOrdered cmp t) : KeysOrdered cmp (AssocList.cons a b t)

theorem Batteries.AssocList.find?_eq_none_of_ltHeadKey {α : Type u_1} {a : α} {β✝ : Type u_2} {l : AssocList α β✝} {cmp : α → α → Ordering} [Std.TransCmp cmp] [BEq α] [LawfulBEq α] (w : LTHeadKey cmp a l) (h : KeysOrdered cmp l) : find? a l = none

Ordered-respecting operations on AssocList

We now define orderedInsert, and orderedMerge, which will later be wrapped as OrderedAssocList.insert and OrderedAssocList.merge.

We prove that with KeysOrdered input these functions produce KeysOrdered outputs. We prove the same about AssocList.filterMapVal.

def Batteries.AssocList.orderedInsert {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (l : AssocList α β) (a : α) (b : β) : AssocList α β

Insert a key-value pair into an AssocList, in such a way that if the original list has keys in increasing order, so does the result. (Otherwise, it is inserted before the first key the new key is smaller than, or replaces the first key the new key is equal to.)

We later wrap this as OrderedAssocList.insert.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.AssocList.orderedInsert cmp Batteries.AssocList.nil a b = Batteries.AssocList.cons a b Batteries.AssocList.nil

@[simp]

theorem Batteries.AssocList.orderedInsert_nil {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {a : α} {b : β} : orderedInsert cmp nil a b = cons a b nil

@[simp]

theorem Batteries.AssocList.orderedInsert_cons {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {x : α✝} {β✝ : Type u_2} {y : β✝} {t : AssocList α✝ β✝} {a : α✝} {b : β✝} : orderedInsert cmp (cons x y t) a b = match _w : cmp a x with | Ordering.lt => cons a b (cons x y t) | Ordering.eq => cons a b t | Ordering.gt => cons x y (orderedInsert cmp t a b)

theorem Batteries.AssocList.headKey?_orderedInsert {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {a : α} {b : β} {l : AssocList α β} : (orderedInsert cmp l a b).headKey? = match l.headKey? with | none => some a | some x => match cmp a x with | Ordering.lt => some a | Ordering.eq => some a | Ordering.gt => some x

theorem Batteries.AssocList.headKey?_orderedInsert_or {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (l : AssocList α β) (a : α) (b : β) : (orderedInsert cmp l a b).headKey? = some a ∨ (orderedInsert cmp l a b).headKey? = l.headKey?

theorem Batteries.AssocList.KeysOrdered.orderedInsert_aux {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {b : β✝} [Std.LawfulEqCmp cmp] [Std.OrientedCmp cmp] {x : α✝} {y : β✝} {t : AssocList α✝ β✝} (h : KeysOrdered cmp (AssocList.cons x y t)) (w : cmp a x = Ordering.gt) : KeysOrdered cmp (AssocList.cons x y (AssocList.orderedInsert cmp t a b))

theorem Batteries.AssocList.KeysOrdered.orderedInsert {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {β✝ : Type u_2} {l : AssocList α✝ β✝} {a : α✝} {b : β✝} [Std.LawfulEqCmp cmp] [Std.OrientedCmp cmp] (h : KeysOrdered cmp l) : KeysOrdered cmp (AssocList.orderedInsert cmp l a b)

theorem Batteries.AssocList.toList_orderedInsert {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {l : AssocList α β} (h : KeysOrdered cmp l) (a : α) (b : β) : (orderedInsert cmp l a b).toList = List.filter (fun (p : α × β) => cmp a p.fst == Ordering.gt) l.toList ++ (a, b) :: List.filter (fun (p : α × β) => cmp a p.fst == Ordering.lt) l.toList

theorem Batteries.AssocList.leHeadKey_filterMapVal {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {β✝ : Type u_2} {l : AssocList α✝ β✝} {α✝¹ : Type u_3} {f : α✝ → β✝ → Option α✝¹} [Std.TransCmp cmp] (h : KeysOrdered cmp l) : LEHeadKey cmp l (filterMapVal f l)

theorem Batteries.AssocList.KeysOrdered.filterMapVal {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {β✝ : Type u_2} {l : AssocList α✝ β✝} {α✝¹ : Type u_3} {f : α✝ → β✝ → Option α✝¹} [Std.TransCmp cmp] (h : KeysOrdered cmp l) : KeysOrdered cmp (AssocList.filterMapVal f l)

@[irreducible]

def Batteries.AssocList.orderedMerge {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (cmp : α → α → Ordering) (f : α → Option β → Option γ → Option δ) : AssocList α β → AssocList α γ → AssocList α δ

Merge two AssocLists, at each stage taking the first key-value pair from whichever list has a smaller first key. If both inputs have keys in strictly increasing order, so does the result. (We later wrap this as OrderedAssocList.merge.)

We combine values using a function f : α → Option β → Option γ → Option δ which we call as f a (some b) none when encountering a key present only in the first list (with value b), f a none (some g) when encountering a key present only in the second list (with value g), and f a (some b) (some g) when encountering a key present in both lists. (Note the value of f a none none is never used.)

Equations

• One or more equations did not get rendered due to their size.
• Batteries.AssocList.orderedMerge cmp f Batteries.AssocList.nil Batteries.AssocList.nil = Batteries.AssocList.nil

theorem Batteries.AssocList.ltHeadKey_orderedMerge {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {l₁ : AssocList α✝ β✝} {β✝¹ : Type u_3} {l₂ : AssocList α✝ β✝¹} {α✝¹ : Type u_4} {f : α✝ → Option β✝ → Option β✝¹ → Option α✝¹} [Std.TransCmp cmp] (h₁ : LTHeadKey cmp a l₁) (h₂ : LTHeadKey cmp a l₂) (w₁ : KeysOrdered cmp l₁) (w₂ : KeysOrdered cmp l₂) : LTHeadKey cmp a (orderedMerge cmp f l₁ l₂)

theorem Batteries.AssocList.KeysOrdered.orderedMerge {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {β✝ : Type u_2} {l₁ : AssocList α✝ β✝} {β✝¹ : Type u_3} {l₂ : AssocList α✝ β✝¹} {α✝¹ : Type u_4} {f : α✝ → Option β✝ → Option β✝¹ → Option α✝¹} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] (h₁ : KeysOrdered cmp l₁) (h₂ : KeysOrdered cmp l₂) : KeysOrdered cmp (AssocList.orderedMerge cmp f l₁ l₂)

def Batteries.AssocList.orderedFind? {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (l : AssocList α β) (x : α) : Option β

Find the value associated to a key by traversing left to right, short-circuiting once we are considering larger keys.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.AssocList.orderedFind? cmp Batteries.AssocList.nil x = none

@[simp]

theorem Batteries.AssocList.orderedFind?_nil {α : Type u_1} {β : Type u_2} {x : α} {cmp : α → α → Ordering} : orderedFind? cmp nil x = none

theorem Batteries.AssocList.orderedFind?_eq_find? {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [BEq α] [LawfulBEq α] (l : AssocList α β) (h : KeysOrdered cmp l) (x : α) : orderedFind? cmp l x = find? x l

theorem Batteries.AssocList.orderedFind?_eq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [BEq α] [LawfulBEq α] (l : AssocList α β) (h : KeysOrdered cmp l) (x : α) : orderedFind? cmp l x = Option.map (fun (x : α × β) => x.snd) (List.find? (fun (x_1 : α × β) => x_1.fst == x) l.toList)

theorem Batteries.AssocList.orderedFind?_eq_none_of_ltHeadKey {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} (l : AssocList α β) (w : LTHeadKey cmp x l) : orderedFind? cmp l x = none

theorem Batteries.AssocList.orderedFind?_cons {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} {x : α✝} [Std.TransCmp cmp] (h : KeysOrdered cmp (cons a b t)) : orderedFind? cmp (cons a b t) x = if cmp x a = Ordering.eq then some b else orderedFind? cmp t x

@[simp]

theorem Batteries.AssocList.orderedFind?_cons_self {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} [Std.OrientedCmp cmp] : orderedFind? cmp (cons a b t) a = some b

theorem Batteries.AssocList.orderedFind?_orderedInsert {α : Type u_1} {β : Type u_2} {x : α} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] (l : AssocList α β) (h : KeysOrdered cmp l) (a : α) (b : β) : orderedFind? cmp (orderedInsert cmp l a b) x = if cmp x a = Ordering.eq then some b else orderedFind? cmp l x

theorem Batteries.AssocList.orderedFind?_orderedInsert_self {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] (l : AssocList α β) (h : KeysOrdered cmp l) (a : α) (b : β) : orderedFind? cmp (orderedInsert cmp l a b) a = some b

theorem Batteries.AssocList.ext_orderedFind? {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {l₁ l₂ : AssocList α β} (h₁ : KeysOrdered cmp l₁) (h₂ : KeysOrdered cmp l₂) (w : ∀ (a : α), orderedFind? cmp l₁ a = orderedFind? cmp l₂ a) : l₁ = l₂

If two AssocLists have ordered keys we can check whether they are equal by checking if their orderedFind? functions are equal.

@[simp]

theorem Batteries.AssocList.orderedFind?_filterMapVal {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → Option α✝} {a : α} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {l : AssocList α β} (h : KeysOrdered cmp l) : orderedFind? cmp (filterMapVal f l) a = (orderedFind? cmp l a).bind fun (b : β) => f a b

theorem Batteries.AssocList.filterMapVal_filterMapVal {α : Type u_1} {γ : Type u_2} {δ : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} {l : AssocList α β} (h : KeysOrdered cmp l) : filterMapVal f (filterMapVal g l) = filterMapVal (fun (a : α) (b : β) => (g a b).bind fun (c : γ) => f a c) l

structure Batteries.OrderedAssocList {α : Type u} (cmp : α → α → Ordering) (β : Type v) : Type (max u v)

An OrderedAssocList is an AssocList with the additional invariant that the keys are in strictly increasing order according to some specified comparator function.

• toAssocList : AssocList α β

  The underlying AssocList of an OrderedAssocList.

• keysOrdered : AssocList.KeysOrdered cmp self.toAssocList

  The invariant that the keys are in strictly increasing order according to cmp.

def Batteries.OrderedAssocList.nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} : OrderedAssocList cmp β

The empty OrderedAssocList.

Equations

• Batteries.OrderedAssocList.nil = { toAssocList := Batteries.AssocList.nil, keysOrdered := trivial }

@[simp]

theorem Batteries.OrderedAssocList.toAssocList_nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} : nil.toAssocList = AssocList.nil

def Batteries.OrderedAssocList.length {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (l : OrderedAssocList cmp β) : Nat

The length of an OrderedAssocList.

Equations

• l.length = l.toAssocList.length

@[simp]

theorem Batteries.OrderedAssocList.length_nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} : nil.length = 0

@[simp]

theorem Batteries.OrderedAssocList.length_mk_cons {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} {cmp✝ : α✝ → α✝ → Ordering} {h : AssocList.KeysOrdered cmp✝ (AssocList.cons a b t)} : { toAssocList := AssocList.cons a b t, keysOrdered := h }.length = { toAssocList := t, keysOrdered := ⋯ }.length + 1

def Batteries.OrderedAssocList.head? {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (l : OrderedAssocList cmp β) : Option (α × β)

The first key-value pair in an OrderedAssocList.

Equations

• { toAssocList := Batteries.AssocList.nil, keysOrdered := keysOrdered }.head? = none
• { toAssocList := Batteries.AssocList.cons a b tail, keysOrdered := keysOrdered }.head? = some (a, b)

theorem Batteries.OrderedAssocList.head?_eq_head? {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (l : OrderedAssocList cmp β) : l.head? = l.toAssocList.toList.head?

def Batteries.OrderedAssocList.tail {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (l : OrderedAssocList cmp β) : OrderedAssocList cmp β

The tail of an OrderedAssocList.

Equations

• { toAssocList := Batteries.AssocList.nil, keysOrdered := keysOrdered }.tail = { toAssocList := Batteries.AssocList.nil, keysOrdered := keysOrdered }
• { toAssocList := Batteries.AssocList.cons a b tail, keysOrdered := keysOrdered }.tail = { toAssocList := tail, keysOrdered := ⋯ }

@[simp]

theorem Batteries.OrderedAssocList.toAssocList_tail_mk_nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {h : AssocList.KeysOrdered cmp AssocList.nil} : { toAssocList := AssocList.nil, keysOrdered := h }.tail.toAssocList = AssocList.nil

@[simp]

theorem Batteries.OrderedAssocList.toAssocList_tail_mk_cons {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {a : α} {b : β} {t : AssocList α β} {h : AssocList.KeysOrdered cmp (AssocList.cons a b t)} : { toAssocList := AssocList.cons a b t, keysOrdered := h }.tail.toAssocList = t

@[simp]

theorem Batteries.OrderedAssocList.length_tail {α✝ : Type u_1} {cmp✝ : α✝ → α✝ → Ordering} {β✝ : Type u_2} {l : OrderedAssocList cmp✝ β✝} : l.tail.length = l.length - 1

def Batteries.OrderedAssocList.find? {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (l : OrderedAssocList cmp β) (x : α) : Option β

Find the value associated to a key by traversing left to right, short-circuiting once we are considering larger keys.

This is the internal implementation of l[x]?, which should be preferred.

Equations

• l.find? x = Batteries.AssocList.orderedFind? cmp l.toAssocList x

def Batteries.OrderedAssocList.contains {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (l : OrderedAssocList cmp β) (x : α) : Bool

Check if an OrderedAssocList contains a specific key.

Equations

• l.contains x = (l.find? x).isSome

@[instance_reducible]

instance Batteries.OrderedAssocList.instGetElem?EqBoolContainsTrue {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} : GetElem? (OrderedAssocList cmp β) α β fun (l : OrderedAssocList cmp β) (a : α) => l.contains a = true

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Batteries.OrderedAssocList.getElem?_nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {x : α} : nil[x]? = none

@[simp]

theorem Batteries.OrderedAssocList.getElem?_mk_nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {h : AssocList.KeysOrdered cmp AssocList.nil} {x : α} : { toAssocList := AssocList.nil, keysOrdered := h }[x]? = none

theorem Batteries.OrderedAssocList.contains_eq_isSome_getElem? {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {a : α} {l : OrderedAssocList cmp β} : l.contains a = l[a]?.isSome

def Batteries.OrderedAssocList.headKey? {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (l : OrderedAssocList cmp β) : Option α

The first key in an OrderedAssocList, or none if the list is empty.

Equations

• l.headKey? = l.toAssocList.headKey?

@[simp]

theorem Batteries.OrderedAssocList.headKey?_nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} : nil.headKey? = none

@[simp]

theorem Batteries.OrderedAssocList.headKey?_mk_cons {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {b : β✝} {t : AssocList α✝ β✝} {cmp✝ : α✝ → α✝ → Ordering} {h : AssocList.KeysOrdered cmp✝ (AssocList.cons a b t)} : { toAssocList := AssocList.cons a b t, keysOrdered := h }.headKey? = some a

def Batteries.OrderedAssocList.LTHeadKey {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (a : α) (l : OrderedAssocList cmp β) : Prop

Either a is less than the first key of l, or l is empty.

Equations

• Batteries.OrderedAssocList.LTHeadKey a l = Batteries.AssocList.LTHeadKey cmp a l.toAssocList

theorem Batteries.OrderedAssocList.ltHeadKey_tail {α : Type u} {cmp : α → α → Ordering} {a : α} {β✝ : Type u_1} {b : β✝} {t : AssocList α β✝} (h : AssocList.KeysOrdered cmp (AssocList.cons a b t)) : LTHeadKey a { toAssocList := t, keysOrdered := ⋯ }

The head key of a tail is either none, or greater than the original head key.

theorem Batteries.OrderedAssocList.getElem?_eq_none_of_ltHeadKey {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {x : α} (l : OrderedAssocList cmp β) (w : LTHeadKey x l) : l[x]? = none

theorem Batteries.OrderedAssocList.getElem?_mk_cons {α : Type u} {cmp : α → α → Ordering} {a : α} {β✝ : Type u_1} {b : β✝} {t : AssocList α β✝} {x : α} [Std.TransCmp cmp] {h : AssocList.KeysOrdered cmp (AssocList.cons a b t)} : { toAssocList := AssocList.cons a b t, keysOrdered := h }[x]? = if cmp x a = Ordering.eq then some b else { toAssocList := t, keysOrdered := ⋯ }[x]?

@[simp]

theorem Batteries.OrderedAssocList.getElem?_mk_cons_self {α : Type u} {cmp : α → α → Ordering} {a : α} {β✝ : Type u_1} {b : β✝} {t : AssocList α β✝} [Std.OrientedCmp cmp] {h : AssocList.KeysOrdered cmp (AssocList.cons a b t)} : { toAssocList := AssocList.cons a b t, keysOrdered := h }[a]? = some b

theorem Batteries.OrderedAssocList.ext_toAssocList {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {l₁ l₂ : OrderedAssocList cmp β} (w : l₁.toAssocList = l₂.toAssocList) : l₁ = l₂

theorem Batteries.OrderedAssocList.ext {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} (w : ∀ (a : α), l₁[a]? = l₂[a]?) : l₁ = l₂

theorem Batteries.OrderedAssocList.ext_iff {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {l₁ l₂ : OrderedAssocList cmp β} : l₁ = l₂ ↔ ∀ (a : α), l₁[a]? = l₂[a]?

@[simp]

theorem Batteries.OrderedAssocList.contains_nil {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {x : α} : nil.contains x = false

@[simp]

theorem Batteries.OrderedAssocList.contains_mk_cons_self {α : Type u} {cmp : α → α → Ordering} {a : α} {β✝ : Type u_1} {b : β✝} {t : AssocList α β✝} [Std.OrientedCmp cmp] {h : AssocList.KeysOrdered cmp (AssocList.cons a b t)} : { toAssocList := AssocList.cons a b t, keysOrdered := h }.contains a = true

def Batteries.OrderedAssocList.cons {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} (a : α) (b : β) (l : OrderedAssocList cmp β) (w : LTHeadKey a l) : OrderedAssocList cmp β

Prepend a key-value pair, requiring a proof that the key is smaller than the existing smallest key.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Batteries.OrderedAssocList.toAssocList_cons {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {b : β✝} {cmp✝ : α✝ → α✝ → Ordering} {l : OrderedAssocList cmp✝ β✝} {w : LTHeadKey a l} : (cons a b l w).toAssocList = AssocList.cons a b l.toAssocList

@[simp]

theorem Batteries.OrderedAssocList.getElem?_cons {α : Type u} {cmp : α → α → Ordering} {β : Type u_1} {a : α} {b : β} {x : α} [Std.TransCmp cmp] {l : OrderedAssocList cmp β} {w : LTHeadKey a l} : (cons a b l w)[x]? = if cmp x a = Ordering.eq then some b else l[x]?

@[simp]

theorem Batteries.OrderedAssocList.headKey?_cons {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {b : β✝} {cmp✝ : α✝ → α✝ → Ordering} {l : OrderedAssocList cmp✝ β✝} {w : LTHeadKey a l} : (cons a b l w).headKey? = some a

def Batteries.OrderedAssocList.insert {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.OrientedCmp cmp] {β : Type u_1} (l : OrderedAssocList cmp β) (a : α) (b : β) : OrderedAssocList cmp β

Insert a key-value pair into an OrderedAssocList. This replaces the current value if the key is already present, and otherwise inserts it before the first key which is greater than the inserted key.

Equations

• l.insert a b = { toAssocList := Batteries.AssocList.orderedInsert cmp l.toAssocList a b, keysOrdered := ⋯ }

@[simp]

theorem Batteries.OrderedAssocList.toAssocList_insert {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.OrientedCmp cmp] {β : Type u_1} (l : OrderedAssocList cmp β) (a : α) (b : β) : (l.insert a b).toAssocList = AssocList.orderedInsert cmp l.toAssocList a b

@[simp]

theorem Batteries.OrderedAssocList.insert_mk_nil {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.OrientedCmp cmp] {β : Type u_1} {h : AssocList.KeysOrdered cmp AssocList.nil} {a : α} {b : β} : { toAssocList := AssocList.nil, keysOrdered := h }.insert a b = { toAssocList := AssocList.cons a b AssocList.nil, keysOrdered := ⋯ }

@[simp]

theorem Batteries.OrderedAssocList.insert_mk_cons {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.OrientedCmp cmp] {β : Type u_1} {x : α} {y : β} {t : AssocList α β} {h : AssocList.KeysOrdered cmp (AssocList.cons x y t)} {a : α} {b : β} : { toAssocList := AssocList.cons x y t, keysOrdered := h }.insert a b = match _w : cmp a x with | Ordering.lt => { toAssocList := AssocList.cons a b (AssocList.cons x y t), keysOrdered := ⋯ } | Ordering.eq => { toAssocList := AssocList.cons a b t, keysOrdered := ⋯ } | Ordering.gt => { toAssocList := AssocList.cons x y (AssocList.orderedInsert cmp t a b), keysOrdered := ⋯ }

theorem Batteries.OrderedAssocList.length_insert_ne_zero {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.OrientedCmp cmp] {β : Type u_1} {a : α} {b : β} {l : OrderedAssocList cmp β} : (l.insert a b).length ≠ 0

theorem Batteries.OrderedAssocList.getElem?_insert {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {x : α} (l : OrderedAssocList cmp β) (a : α) (b : β) : (l.insert a b)[x]? = if cmp x a = Ordering.eq then some b else l[x]?

theorem Batteries.OrderedAssocList.getElem?_insert_self {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} (l : OrderedAssocList cmp β) (a : α) (b : β) : (l.insert a b)[a]? = some b

theorem Batteries.OrderedAssocList.contains_insert {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {x : α} (l : OrderedAssocList cmp β) (a : α) (b : β) : (l.insert a b).contains x = (decide (cmp x a = Ordering.eq) || l.contains x)

theorem Batteries.OrderedAssocList.contains_insert_self {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} (l : OrderedAssocList cmp β) (a : α) (b : β) : (l.insert a b).contains a = true

def Batteries.OrderedAssocList.filterMapVal {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type u_1} {δ : Type u_2} (f : α → β → Option δ) (l : OrderedAssocList cmp β) : OrderedAssocList cmp δ

Apply a function to each key-value pair, either replacing the value or dropping it if the function returns none.

Equations

• Batteries.OrderedAssocList.filterMapVal f l = { toAssocList := Batteries.AssocList.filterMapVal f l.toAssocList, keysOrdered := ⋯ }

@[simp]

theorem Batteries.OrderedAssocList.toAssocList_filterMapVal {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type u_1} {δ : Type u_2} (f : α → β → Option δ) (l : OrderedAssocList cmp β) : (filterMapVal f l).toAssocList = AssocList.filterMapVal f l.toAssocList

@[simp]

theorem Batteries.OrderedAssocList.getElem?_filterMapVal {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type u_1} {α✝ : Type u_2} {f : α → β → Option α✝} {a : α} [Std.LawfulEqCmp cmp] (l : OrderedAssocList cmp β) : (filterMapVal f l)[a]? = l[a]?.bind fun (b : β) => f a b

theorem Batteries.OrderedAssocList.filterMapVal_filterMapVal {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {γ : Type u_1} {δ : Type u_2} {β : Type u_3} [Std.LawfulEqCmp cmp] {f : α → γ → Option δ} {g : α → β → Option γ} {l : OrderedAssocList cmp β} : filterMapVal f (filterMapVal g l) = filterMapVal (fun (a : α) (b : β) => (g a b).bind fun (c : γ) => f a c) l

def Batteries.OrderedAssocList.merge {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α → Option β → Option γ → Option δ) (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp γ) : OrderedAssocList cmp δ

Merge two OrderedAssocLists using a function α → Option β → Option γ → Option δ, dropping values where the function returns none.

Equations

• Batteries.OrderedAssocList.merge f l₁ l₂ = { toAssocList := Batteries.AssocList.orderedMerge cmp f l₁.toAssocList l₂.toAssocList, keysOrdered := ⋯ }

@[simp]

theorem Batteries.OrderedAssocList.toAssocList_merge {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {α✝ : Type u_2} {α✝¹ : Type u_3} {f : α → Option β → Option α✝ → Option α✝¹} {l₂ : OrderedAssocList cmp α✝} {l₁ : OrderedAssocList cmp β} : (merge f l₁ l₂).toAssocList = AssocList.orderedMerge cmp f l₁.toAssocList l₂.toAssocList

@[simp]

theorem Batteries.OrderedAssocList.merge_nil_nil {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {f : α → Option β → Option γ → Option δ} : merge f nil nil = nil

@[simp]

theorem Batteries.OrderedAssocList.merge_mk_nil_mk_cons {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {h : AssocList.KeysOrdered cmp AssocList.nil} {x' : α} {y' : γ} {t' : AssocList α γ} {h' : AssocList.KeysOrdered cmp (AssocList.cons x' y' t')} {f : α → Option β → Option γ → Option δ} : merge f { toAssocList := AssocList.nil, keysOrdered := h } { toAssocList := AssocList.cons x' y' t', keysOrdered := h' } = filterMapVal (fun (a : α) (g : γ) => f a none (some g)) { toAssocList := AssocList.cons x' y' t', keysOrdered := h' }

@[simp]

theorem Batteries.OrderedAssocList.merge_mk_cons_mk_nil {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {x : α} {y : β} {t : AssocList α β} {h : AssocList.KeysOrdered cmp (AssocList.cons x y t)} {h' : AssocList.KeysOrdered cmp AssocList.nil} {f : α → Option β → Option γ → Option δ} : merge f { toAssocList := AssocList.cons x y t, keysOrdered := h } { toAssocList := AssocList.nil, keysOrdered := h' } = filterMapVal (fun (a : α) (b : β) => f a (some b) none) { toAssocList := AssocList.cons x y t, keysOrdered := h }

@[simp]

theorem Batteries.OrderedAssocList.getElem?_merge {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {a : α} {f : α → Option β → Option γ → Option δ} (hf : f a none none = none) {l₁ : OrderedAssocList cmp β} {l₂ : OrderedAssocList cmp γ} : (merge f l₁ l₂)[a]? = f a l₁[a]? l₂[a]?

theorem Batteries.OrderedAssocList.merge_comm {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α → Option β → Option γ → Option δ) (g : α → Option γ → Option β → Option δ) (hg : ∀ (a : α), g a none none = none) (w : ∀ (a : α) (x : Option β) (y : Option γ), f a x y = g a y x) (l₁ : OrderedAssocList cmp β) (l₂ : OrderedAssocList cmp γ) : merge f l₁ l₂ = merge g l₂ l₁

theorem Batteries.OrderedAssocList.merge_assoc {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β₁ : Type u_1} {β₂ : Type u_2} {γ₁ : Type u_3} {β₃ : Type u_4} {ε : Type u_5} {γ₂ : Type u_6} (f₁ : α → Option β₁ → Option β₂ → Option γ₁) (f₂ : α → Option γ₁ → Option β₃ → Option ε) (g₁ : α → Option β₂ → Option β₃ → Option γ₂) (g₂ : α → Option β₁ → Option γ₂ → Option ε) (hf₁ : ∀ (a : α), f₁ a none none = none) (hf₂ : ∀ (a : α), f₂ a none none = none) (hg₁ : ∀ (a : α), g₁ a none none = none) (hg₂ : ∀ (a : α), g₂ a none none = none) (w : ∀ (a : α) (x : Option β₁) (y : Option β₂) (z : Option β₃), f₂ a (f₁ a x y) z = g₂ a x (g₁ a y z)) (l₁ : OrderedAssocList cmp β₁) (l₂ : OrderedAssocList cmp β₂) (l₃ : OrderedAssocList cmp β₃) : merge f₂ (merge f₁ l₁ l₂) l₃ = merge g₂ l₁ (merge g₁ l₂ l₃)

def Batteries.OrderedAssocList.add {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} [Add β] (l₁ l₂ : OrderedAssocList cmp β) : OrderedAssocList cmp β

Add two OrderedAssocLists, taking the value from one list if the other value is missing. (That is, treating missing values as 0.)

Equations

• l₁.add l₂ = Batteries.OrderedAssocList.merge (fun (x : α) => Batteries.OrderedAssocList.add.addOption) l₁ l₂

def Batteries.OrderedAssocList.add.addOption {β : Type u_1} [Add β] : Option β → Option β → Option β

Add two values, treating missing values as 0.

Equations

• Batteries.OrderedAssocList.add.addOption (some x_2) (some y) = some (x_2 + y)
• Batteries.OrderedAssocList.add.addOption (some x_2) none = some x_2
• Batteries.OrderedAssocList.add.addOption none (some y) = some y
• Batteries.OrderedAssocList.add.addOption none none = none

@[simp]

theorem Batteries.OrderedAssocList.getElem?_add {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {l₂ : OrderedAssocList cmp β} [Add β] {l₁ : OrderedAssocList cmp β} {a : α} : (l₁.add l₂)[a]? = match l₁[a]?, l₂[a]? with | some x, some y => some (x + y) | some x, none => some x | none, some y => some y | none, none => none

def Batteries.OrderedAssocList.mul {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} [Mul β] (l₁ l₂ : OrderedAssocList cmp β) : OrderedAssocList cmp β

Multiply two OrderedAssocLists, dropping any values where the corresponding value in the other list is missing. (That is, treating missing values as 0.)

Equations

• l₁.mul l₂ = Batteries.OrderedAssocList.merge (fun (x : α) => Batteries.OrderedAssocList.mul.mulOption) l₁ l₂

def Batteries.OrderedAssocList.mul.mulOption {β : Type u_1} [Mul β] : Option β → Option β → Option β

Multiply two values, treating missing values as 0.

Equations

• Batteries.OrderedAssocList.mul.mulOption (some x_2) (some y) = some (x_2 * y)
• Batteries.OrderedAssocList.mul.mulOption (some x_2) none = none
• Batteries.OrderedAssocList.mul.mulOption none (some y) = none
• Batteries.OrderedAssocList.mul.mulOption none none = none

@[simp]

theorem Batteries.OrderedAssocList.getElem?_mul {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {β : Type u_1} {l₂ : OrderedAssocList cmp β} [Mul β] {l₁ : OrderedAssocList cmp β} {a : α} : (l₁.mul l₂)[a]? = match l₁[a]?, l₂[a]? with | some x, some y => some (x * y) | some val, none => none | none, some val => none | none, none => none