Canonical list-based sets

This file defines a simple set data type, backed by a sorted duplicate-free list. Functions on sets assume but don't require their inputs to be well-formed (sorted and duplicate-free). Separate theorems show that these functions produce well-formed outputs when given well-formed inputs.

Use Set.make to construct well-formed sets from lists.

inductive Cedar.Data.Set (α : Type u) : Type u

• mk {α : Type u} (l : List α) : Set α

def Cedar.Data.instReprSet.repr {α✝ : Type u_1} [Repr α✝] : Set α✝ → Nat → Std.Format

Equations

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

instance Cedar.Data.instReprSet {α✝ : Type u_1} [Repr α✝] : Repr (Set α✝)

Equations

• Cedar.Data.instReprSet = { reprPrec := Cedar.Data.instReprSet.repr }

def Cedar.Data.instDecidableEqSet.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Set α✝) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Data.instDecidableEqSet.decEq (Cedar.Data.Set.mk a) (Cedar.Data.Set.mk b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Data.instDecidableEqSet {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Set α✝)

Equations

• Cedar.Data.instDecidableEqSet = Cedar.Data.instDecidableEqSet.decEq

def Cedar.Data.instInhabitedSet.default {a✝ : Type u_1} : Set a✝

Equations

• Cedar.Data.instInhabitedSet.default = Cedar.Data.Set.mk default

instance Cedar.Data.instInhabitedSet {a✝ : Type u_1} : Inhabited (Set a✝)

Equations

• Cedar.Data.instInhabitedSet = { default := Cedar.Data.instInhabitedSet.default }

instance Cedar.Data.instToJsonSet {α✝ : Type u_1} [Lean.ToJson α✝] : Lean.ToJson (Set α✝)

Equations

• Cedar.Data.instToJsonSet = { toJson := Cedar.Data.instToJsonSet.toJson }

def Cedar.Data.instToJsonSet.toJson {α✝ : Type u_1} [Lean.ToJson α✝] : Set α✝ → Lean.Json

Equations

• Cedar.Data.instToJsonSet.toJson (Cedar.Data.Set.mk a) = Lean.Json.mkObj [("mk", Lean.Json.mkObj [("l", Lean.toJson a)])]

@[reducible, inline]

abbrev Cedar.Data.Set.elts {α : Type u} (s : Set α) : List α

Equations

• s.elts = s.1

def Cedar.Data.Set.toList {α : Type u} (s : Set α) : List α

Creates an ordered/duplicate free list from a set provided the underlying set is well formed.

Equations

• s.toList = s.elts

def Cedar.Data.Set.make {α : Type u_1} [LT α] [DecidableLT α] (elts : List α) : Set α

Creates a well-formed set from the given list.

Equations

• Cedar.Data.Set.make elts = Cedar.Data.Set.mk (List.canonicalize (fun (x : α) => x) elts)

def Cedar.Data.Set.empty {α : Type u_1} : Set α

Empty set ∅

Equations

• Cedar.Data.Set.empty = Cedar.Data.Set.mk []

def Cedar.Data.Set.isEmpty {α : Type u_1} [DecidableEq α] (s : Set α) : Bool

s == ∅

Equations

• s.isEmpty = (s == Cedar.Data.Set.empty)

def Cedar.Data.Set.contains {α : Type u_1} [DecidableEq α] (s : Set α) (elt : α) : Bool

elt ∈ s

Equations

• s.contains elt = List.elem elt s.elts

def Cedar.Data.Set.subset {α : Type u_1} [DecidableEq α] (s₁ s₂ : Set α) : Bool

s₁ ⊆ s₂

Equations

• s₁.subset s₂ = s₁.elts.all s₂.contains

def Cedar.Data.Set.intersects {α : Type u_1} [DecidableEq α] (s₁ s₂ : Set α) : Bool

s₁ ∩ s₂ ≠ ∅

Equations

• s₁.intersects s₂ = s₁.elts.any s₂.contains

def Cedar.Data.Set.intersect {α : Type u_1} [DecidableEq α] (s₁ s₂ : Set α) : Set α

s₁ ∩ s₂

Equations

• s₁.intersect s₂ = Cedar.Data.Set.mk (s₁.elts.inter s₂.elts)

def Cedar.Data.Set.union {α : Type u_1} [LT α] [DecidableLT α] (s₁ s₂ : Set α) : Set α

s₁ ∪ s₂

Equations

• s₁.union s₂ = Cedar.Data.Set.make (s₁.elts ++ s₂.elts)

instance Cedar.Data.Set.instHAppendOfDecidableLT {α : Type u_1} [LT α] [DecidableLT α] : HAppend (Set α) (Set α) (Set α)

Equations

• Cedar.Data.Set.instHAppendOfDecidableLT = { hAppend := Cedar.Data.Set.union }

def Cedar.Data.Set.filter {α : Type u_1} (f : α → Bool) (s : Set α) : Set α

Filters s using f.

Equations

• Cedar.Data.Set.filter f s = Cedar.Data.Set.mk (List.filter f s.elts)

def Cedar.Data.Set.difference {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] (s₁ s₂ : Set α) : Set α

s₁ \ s₂.

Equations

• s₁.difference s₂ = Cedar.Data.Set.filter (fun (x : α) => !s₂.contains x) s₁

def Cedar.Data.Set.map {α : Type u_1} {β : Type u_2} [LT β] [DecidableLT β] (f : α → β) (s : Set α) : Set β

Maps f to s.

Equations

• Cedar.Data.Set.map f s = Cedar.Data.Set.make (List.map f s.elts)

def Cedar.Data.Set.mapOrErr {α : Type u_1} {β : Type u_2} {ε : Type u_3} [DecidableEq β] [LT β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : α → Except ε β) (s : Set α) (err : ε) : Except ε (Set β)

Maps f to s and returns the result of err if any error is encountered.

Equations

• Cedar.Data.Set.mapOrErr f s err = match List.mapM f s.elts with | Except.ok elts => Except.ok (Cedar.Data.Set.make elts) | Except.error a => Except.error err

def Cedar.Data.Set.all {α : Type u_1} (f : α → Bool) (s : Set α) : Bool

Returns true if all elements of s satisfy f.

Equations

• Cedar.Data.Set.all f s = s.elts.all f

def Cedar.Data.Set.any {α : Type u_1} (f : α → Bool) (s : Set α) : Bool

Returns true if some element of s satisfies f.

Equations

• Cedar.Data.Set.any f s = s.elts.any f

def Cedar.Data.Set.size {α : Type u_1} (s : Set α) : Nat

Equations

• s.size = s.elts.length

def Cedar.Data.Set.singleton {α : Type u_1} (a : α) : Set α

Equations

• Cedar.Data.Set.singleton a = Cedar.Data.Set.mk [a]

def Cedar.Data.Set.wellFormed {α : Type u_1} [LT α] [DecidableLT α] (s : Set α) : Bool

Checks if a set if well-formed

Equations

• s.wellFormed = s.elts.isSorted

def Cedar.Data.Set.singleton? {α : Type u_1} [Inhabited α] (s : Set α) : Option α

If s is a singleton set, returns the single element

Equations

• s.singleton? = match s.elts with | [] => none | [x] => some x | x => none

def Cedar.Data.Set.foldl {α : Type u_1} {β : Type u_2} (f : α → β → α) (init : α) (s : Set β) : α

Equations

• Cedar.Data.Set.foldl f init s = List.foldl f init s.elts

instance Cedar.Data.Set.instLT {α : Type u_1} [LT α] : LT (Set α)

Equations

• Cedar.Data.Set.instLT = { lt := fun (a b : Cedar.Data.Set α) => a.elts < b.elts }

instance Cedar.Data.Set.decLt {α : Type u_1} [LT α] [DecidableEq α] [DecidableLT α] (n m : Set α) : Decidable (n < m)

Equations

• (Cedar.Data.Set.mk nelts).decLt (Cedar.Data.Set.mk melts) = nelts.decidableLT melts

instance Cedar.Data.Set.instEmptyCollection {α : Type u_1} : EmptyCollection (Set α)

Equations

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

instance Cedar.Data.Set.instMembership {α : Type u_1} : Membership α (Set α)

Equations

• Cedar.Data.Set.instMembership = { mem := fun (s : Cedar.Data.Set α) (v : α) => v ∈ s.elts }

instance Cedar.Data.Set.instHasSubsetOfDecidableEq {α : Type u_1} [DecidableEq α] : HasSubset (Set α)

Equations

• Cedar.Data.Set.instHasSubsetOfDecidableEq = { Subset := fun (s₁ s₂ : Cedar.Data.Set α) => s₁.subset s₂ = true }

instance Cedar.Data.Set.instInterOfDecidableEq {α : Type u_1} [DecidableEq α] : Inter (Set α)

Equations

• Cedar.Data.Set.instInterOfDecidableEq = { inter := Cedar.Data.Set.intersect }

instance Cedar.Data.Set.instUnionOfDecidableLT {α : Type u_1} [LT α] [DecidableLT α] : Union (Set α)

Equations

• Cedar.Data.Set.instUnionOfDecidableLT = { union := Cedar.Data.Set.union }

def Cedar.Data.Set.map₁ {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (s : Set α) (f : { a : α // a ∈ s } → β) : Set β

Equations

• s.map₁ f = Cedar.Data.Set.make (List.map f s.elts.attach)

def Cedar.Data.Set.all₁ {α : Type u_1} (s : Set α) (f : { a : α // a ∈ s } → Bool) : Bool

Equations

• s.all₁ f = s.elts.attach.all f

def Cedar.Data.Set.any₁ {α : Type u_1} (s : Set α) (f : { a : α // a ∈ s } → Bool) : Bool

Equations

• s.any₁ f = s.elts.attach.any f