@[reducible, inline]

abbrev Data.Set' (k : Type u) [Ord k] : Type u

An ordered finite set of elements of type k, backed by a red-black tree. $$\text{Set'}(k) \cong \text{RBMap}(k, \text{Unit}, \text{compare})$$ Provides $O(\log n)$ membership, insert, and delete. Named Set' to avoid clashing with Lean's Set (α → Prop).

Equations

• Data.Set' k = Lean.RBMap k Unit compare

@[inline]

def Data.Set'.empty {k : Type u} [Ord k] : Set' k

The empty set. $$\text{empty} = \emptyset$$

Equations

• Data.Set'.empty = Lean.RBMap.empty

@[inline]

def Data.Set'.singleton {k : Type u} [Ord k] (x : k) : Set' k

A set with a single element. $$\text{singleton}(x) = \{x\}$$

Equations

• Data.Set'.singleton x = Lean.RBMap.empty.insert x ()

def Data.Set'.fromList {k : Type u} [Ord k] (l : List k) : Set' k

Build a set from a list of elements. $$\text{fromList}([x_1, \ldots, x_n]) = \{x_1, \ldots, x_n\}$$

Equations

• Data.Set'.fromList l = List.foldl (fun (s : Data.Set' k) (x : k) => Lean.RBMap.insert s x ()) Lean.RBMap.empty l

@[inline]

def Data.Set'.member {k : Type u} [Ord k] (x : k) (s : Set' k) : Bool

Test membership. $$\text{member}(x, s) \iff x \in s$$

Equations

• Data.Set'.member x s = Lean.RBMap.contains s x

@[inline]

def Data.Set'.null {k : Type u} [Ord k] (s : Set' k) : Bool

Is the set empty? $$\text{null}(s) \iff s = \emptyset$$

Equations

• s.null = Lean.RBMap.isEmpty s

@[inline]

def Data.Set'.size' {k : Type u} [Ord k] (s : Set' k) : Nat

The number of elements. $$\text{size}(s) = |s|$$

Equations

• s.size' = Lean.RBMap.size s

@[inline]

def Data.Set'.insert' {k : Type u} [Ord k] (x : k) (s : Set' k) : Set' k

Insert an element. $$\text{insert}(x, s) = s \cup \{x\}$$

Equations

• Data.Set'.insert' x s = Lean.RBMap.insert s x ()

@[inline]

def Data.Set'.delete {k : Type u} [Ord k] (x : k) (s : Set' k) : Set' k

Delete an element. $$\text{delete}(x, s) = s \setminus \{x\}$$

Equations

• Data.Set'.delete x s = Lean.RBMap.erase s x

def Data.Set'.union {k : Type u} [Ord k] (s1 s2 : Set' k) : Set' k

Union of two sets. $$\text{union}(s_1, s_2) = s_1 \cup s_2$$

Equations

• s1.union s2 = Lean.RBMap.mergeBy (fun (x : k) (x_1 x_2 : Unit) => ()) s1 s2

def Data.Set'.intersection {k : Type u} [Ord k] (s1 s2 : Set' k) : Set' k

Intersection of two sets. $$\text{intersection}(s_1, s_2) = s_1 \cap s_2$$

Equations

• s1.intersection s2 = Lean.RBMap.intersectBy (fun (x : k) (x_1 x_2 : Unit) => ()) s1 s2

def Data.Set'.difference {k : Type u} [Ord k] (s1 s2 : Set' k) : Set' k

Difference of two sets. $$\text{difference}(s_1, s_2) = s_1 \setminus s_2$$

Equations

• s1.difference s2 = Lean.RBMap.filter (fun (key : k) (x : Unit) => !Lean.RBMap.contains s2 key) s1

def Data.Set'.isSubsetOf {k : Type u} [Ord k] (s1 s2 : Set' k) : Bool

Is s1 a subset of s2? $$\text{isSubsetOf}(s_1, s_2) \iff s_1 \subseteq s_2$$

Equations

• s1.isSubsetOf s2 = Lean.RBMap.all s1 fun (key : k) (x : Unit) => Lean.RBMap.contains s2 key

def Data.Set'.mapSet {k : Type u} [Ord k] {k₂ : Type u_1} [Ord k₂] (f : k → k₂) (s : Set' k) : Set' k₂

Map a function over all elements. The result may be smaller if f maps distinct elements to the same value. $$\text{map}(f, s) = \{f(x) \mid x \in s\}$$

Equations

• Data.Set'.mapSet f s = Lean.RBMap.fold (fun (acc : Data.Set' k₂) (key : k) (x : Unit) => Lean.RBMap.insert acc (f key) ()) Lean.RBMap.empty s

def Data.Set'.filter {k : Type u} [Ord k] (p : k → Bool) (s : Set' k) : Set' k

Filter elements satisfying a predicate. $$\text{filter}(p, s) = \{x \in s \mid p(x)\}$$

Equations

• Data.Set'.filter p s = Lean.RBMap.filter (fun (key : k) (x : Unit) => p key) s

@[inline]

def Data.Set'.foldl {k : Type u} [Ord k] {α : Type u_1} (f : α → k → α) (init : α) (s : Set' k) : α

Left fold over elements in ascending order. $$\text{foldl}(f, z, s) = f(\ldots f(f(z, x_1), x_2) \ldots, x_n)$$

Equations

• Data.Set'.foldl f init s = Lean.RBMap.fold (fun (acc : α) (key : k) (x : Unit) => f acc key) init s

@[inline]

def Data.Set'.foldr {k : Type u} [Ord k] {α : Type u_1} (f : k → α → α) (init : α) (s : Set' k) : α

Right fold over elements in ascending order. $$\text{foldr}(f, z, s) = f(x_1, f(x_2, \ldots f(x_n, z)))$$

Equations

• Data.Set'.foldr f init s = Lean.RBMap.revFold (fun (acc : α) (key : k) (x : Unit) => f key acc) init s

def Data.Set'.toList' {k : Type u} [Ord k] (s : Set' k) : List k

Convert the set to a list in ascending order. $$\text{toList}(s) = [x_1, \ldots, x_n]$$ where $x_1 < \cdots < x_n$.

Equations

• s.toList' = Lean.RBMap.fold (fun (acc : List k) (key : k) (x : Unit) => acc ++ [key]) [] s

@[inline]

def Data.Set'.toAscList {k : Type u} [Ord k] (s : Set' k) : List k

Convert the set to an ascending list (same as toList' for an ordered set). $$\text{toAscList} = \text{toList'}$$

Equations

• s.toAscList = s.toList'

def Data.Set'.findMin {k : Type u} [Ord k] (s : Set' k) : Option k

The smallest element, or none if the set is empty. $$\text{findMin}(s) = \min(s)$$

Equations

• s.findMin = Option.map (fun (x : (_ : k) × Unit) => match x with | ⟨key, snd⟩ => key) s.val.min

def Data.Set'.findMax {k : Type u} [Ord k] (s : Set' k) : Option k

The largest element, or none if the set is empty. $$\text{findMax}(s) = \max(s)$$

Equations

• s.findMax = Option.map (fun (x : (_ : k) × Unit) => match x with | ⟨key, snd⟩ => key) s.val.max

@[implicit_reducible]

instance Data.Set'.instEmptyCollection {k : Type u} [Ord k] : EmptyCollection (Set' k)

Equations

• Data.Set'.instEmptyCollection = { emptyCollection := Data.Set'.empty }

@[implicit_reducible]

instance Data.Set'.instInhabited {k : Type u} [Ord k] : Inhabited (Set' k)

Equations

• Data.Set'.instInhabited = { default := Data.Set'.empty }

@[implicit_reducible]

instance Data.Set'.instRepr {k : Type u} [Ord k] [Repr k] : Repr (Set' k)

Equations

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

@[implicit_reducible]

instance Data.Set'.instBEq {k : Type u} [Ord k] [BEq k] : BEq (Set' k)

Equations

• Data.Set'.instBEq = { beq := fun (s1 s2 : Data.Set' k) => s1.toList' == s2.toList' }

theorem Data.Set'.null_empty {k : Type u} [Ord k] : empty.null = true

The empty set has no elements. $$\text{null}(\emptyset) = \text{true}$$

theorem Data.Set'.member_empty {k : Type u} [Ord k] (x : k) : member x empty = false

Membership in the empty set is always false. $$\text{member}(x, \emptyset) = \text{false}$$

theorem Data.Set'.size_empty {k : Type u} [Ord k] : empty.size' = 0

The empty set has size zero. $$\text{size'}(\emptyset) = 0$$

theorem Data.Set'.null_singleton {k : Type u} [Ord k] (x : k) : (singleton x).null = false

A singleton set is not null. $$\text{null}(\text{singleton}(x)) = \text{false}$$