Set properties

This file proves useful properties of canonical list-based sets defined in Cedar.Data.Set.

Well-formed sets

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

Equations

• s.WellFormed = (s = Cedar.Data.Set.make s.toList)

theorem Cedar.Data.Set.if_wellformed_then_exists_make {α : Type u_1} [LT α] [DecidableLT α] (s : Set α) : s.WellFormed → ∃ (list : List α), s = make list

theorem Cedar.Data.Set.wf_iff_sorted {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (s : Set α) : s.WellFormed ↔ s.elts.Sorted

theorem Cedar.Data.Set.mapOrErr_eq_match {α : Type u_1} {β : Type u_2} {ε : Type u_3} [DecidableEq β] [LT β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (f : α → Except ε β) (s : Set α) (err : ε) : mapOrErr f s err = match List.mapM f s.elts with | Except.ok elts => Except.ok (make elts) | Except.error a => Except.error err

Equation lemma for Set.mapOrErr, for clients that cannot unfold it.

contains and mem

@[simp]

theorem Cedar.Data.Set.contains_prop_bool_equiv {α : Type u_1} [DecidableEq α] {v : α} {s : Set α} : s.contains v = true ↔ v ∈ s

@[simp]

theorem Cedar.Data.Set.not_contains_prop_bool_equiv {α : Type u_1} [DecidableEq α] {v : α} {s : Set α} : s.contains v = false ↔ ¬v ∈ s

theorem Cedar.Data.Set.mem_elts_iff_mem_set {α : Type u} (v : α) (s : Set α) : v ∈ s.elts ↔ v ∈ s

theorem Cedar.Data.Set.mem_set_iff_mem_mk {α : Type u} (v : α) (xs : List α) : v ∈ xs ↔ v ∈ mk xs

theorem Cedar.Data.Set.mem_mk_hd {α : Type u} (hd : α) (tl : List α) : hd ∈ mk (hd :: tl)

theorem Cedar.Data.Set.mem_mk_tl {α : Type u} (a hd : α) (tl : List α) : a ∈ mk tl → a ∈ mk (hd :: tl)

@[simp]

theorem Cedar.Data.Set.mem_cons {α : Type u_1} {a hd : α} {tl : List α} : a ∈ mk (hd :: tl) ↔ a = hd ∨ a ∈ tl

theorem Cedar.Data.Set.mem_set_implies_elts_non_empty {α : Type u} (v : α) (s : Set α) : v ∈ s → ¬s.elts = []

empty

theorem Cedar.Data.Set.empty_eq_mk_nil {α : Type u_1} : empty = mk []

@[simp]

theorem Cedar.Data.Set.elts_empty {α : Type u_1} : empty.elts = []

theorem Cedar.Data.Set.not_mem_empty {α : Type u} (v : α) : ¬v ∈ empty

Like List.not_mem_nil, lifted to Sets

theorem Cedar.Data.Set.empty_wf {α : Type u} [LT α] [DecidableLT α] : empty.WellFormed

@[simp]

theorem Cedar.Data.Set.map_empty {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) : map f empty = empty

@[simp]

theorem Cedar.Data.Set.all_empty {α : Type u_1} (f : α → Bool) : all f empty = true

@[simp]

theorem Cedar.Data.Set.any_empty {α : Type u_1} (f : α → Bool) : any f empty = false

isEmpty

@[simp]

theorem Cedar.Data.Set.isEmpty_empty {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] : empty.isEmpty = true

theorem Cedar.Data.Set.isEmpty_iff_eq_empty {α : Type u_1} [DecidableEq α] {s : Set α} : s.isEmpty = true ↔ s = empty

@[simp]

theorem Cedar.Data.Set.isEmpty_make {α : Type u_1} [DecidableEq α] [LT α] [DecidableLT α] {xs : List α} : (make xs).isEmpty = true ↔ xs = []

@[simp]

theorem Cedar.Data.Set.isEmpty_make_eq_false {α : Type u_1} [DecidableEq α] [LT α] [DecidableLT α] (xs : List α) : (make xs).isEmpty = false ↔ xs ≠ []

theorem Cedar.Data.Set.non_empty_iff_exists {α : Type u_1} [DecidableEq α] (s : Set α) : ¬s.isEmpty = true ↔ ∃ (a : α), a ∈ s

theorem Cedar.Data.Set.empty_iff_not_exists {α : Type u_1} [DecidableEq α] (s : Set α) : s.isEmpty = true ↔ ¬∃ (a : α), a ∈ s

Corollary of non_empty_iff_exists

singleton

theorem Cedar.Data.Set.singleton_wf {α : Type u_1} [DecidableEq α] [LT α] [DecidableLT α] (a : α) : (singleton a).WellFormed

@[simp]

theorem Cedar.Data.Set.mem_singleton {α : Type u_1} [DecidableEq α] (a b : α) : a ∈ singleton b ↔ a = b

theorem Cedar.Data.Set.mem_singleton_self {α : Type u_1} [DecidableEq α] (a : α) : a ∈ singleton a

make

theorem Cedar.Data.Set.make_wf {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (xs : List α) : (make xs).WellFormed

theorem Cedar.Data.Set.make_elts {α : Type u_1} [LT α] [DecidableLT α] {s : Set α} : s.WellFormed → make s.elts = s

theorem Cedar.Data.Set.make_sorted {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {xs : List α} : xs.Sorted → make xs = mk xs

@[simp]

theorem Cedar.Data.Set.mem_make {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (x : α) (xs : List α) : x ∈ make xs ↔ x ∈ xs

theorem Cedar.Data.Set.make_mk_eqv {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {xs ys : List α} : make xs = mk ys → xs ≡ ys

theorem Cedar.Data.Set.make_make_eqv {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {xs ys : List α} : make xs = make ys ↔ xs ≡ ys

theorem Cedar.Data.Set.elts_make_eqv {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {xs : List α} : (make xs).elts ≡ xs

@[simp]

theorem Cedar.Data.Set.make_nil {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] : make [] = empty

@[simp]

theorem Cedar.Data.Set.make_eq_empty {α : Type u_1} [LT α] [DecidableLT α] [DecidableEq α] {xs : List α} : make xs = empty ↔ xs = []

theorem Cedar.Data.Set.make_singleton_nonempty {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] (a : α) : make [a] ≠ empty

theorem Cedar.Data.Set.eq_means_eqv {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {s₁ s₂ : Set α} : s₁.WellFormed → s₂.WellFormed → (s₁ = s₂ ↔ s₁.elts ≡ s₂.elts)

@[simp]

theorem Cedar.Data.Set.any_make {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (f : α → Bool) (xs : List α) : any f (make xs) = xs.any f

@[simp]

theorem Cedar.Data.Set.make_elts_make {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (xs : List α) : make (make xs).elts = make xs

theorem Cedar.Data.Set.elts_make_implies_equiv {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {xs ys : List α} : (make xs).elts = ys → ys ≡ xs

theorem Cedar.Data.Set.make_cons {α : Type u_1} [LT α] [DecidableLT α] {xs ys : List α} {a : α} : make xs = make ys → make (a :: xs) = make (a :: ys)

Note that the converse of this is not true: counterexample xs = [1], ys = [], a = 1.

inter and union

theorem Cedar.Data.Set.inter_def {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {s₁ s₂ : Set α} : s₁ ∩ s₂ = s₁.intersect s₂

@[simp]

theorem Cedar.Data.Set.mem_inter_iff {α : Type u_1} [DecidableEq α] {x : α} {s₁ s₂ : Set α} : x ∈ s₁ ∩ s₂ ↔ x ∈ s₁ ∧ x ∈ s₂

theorem Cedar.Data.Set.inter_wf {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {s₁ s₂ : Set α} (h₁ : s₁.WellFormed) : (s₁ ∩ s₂).WellFormed

@[simp]

theorem Cedar.Data.Set.inter_empty_left {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] (s : Set α) : empty ∩ s = empty

@[simp]

theorem Cedar.Data.Set.inter_empty_right {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] (s : Set α) : s ∩ empty = empty

@[simp]

theorem Cedar.Data.Set.inter_self {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] (s : Set α) : s ∩ s = s

theorem Cedar.Data.Set.intersects_def {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {s₁ s₂ : Set α} : (s₁.intersects s₂ = true) = ¬(s₁ ∩ s₂).isEmpty = true

theorem Cedar.Data.Set.intersects_iff_exists {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {s₁ s₂ : Set α} : s₁.intersects s₂ = true ↔ ∃ (a : α), a ∈ s₁ ∧ a ∈ s₂

theorem Cedar.Data.Set.union_wf {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {s₁ s₂ : Set α} : s₁.WellFormed → s₂.WellFormed → (s₁ ∪ s₂).WellFormed

theorem Cedar.Data.Set.make_cons_eq_singleton_union {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (a : α) (xs : List α) : make (a :: xs) = singleton a ∪ make xs

@[simp]

theorem Cedar.Data.Set.append_eq_union {α : Type u_1} [LT α] [DecidableLT α] (s₁ s₂ : Set α) : s₁ ++ s₂ = s₁ ∪ s₂

The ++ notation on sets is definitionally ∪.

@[simp]

theorem Cedar.Data.Set.mem_union {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (s₁ s₂ : Set α) (a : α) : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

theorem Cedar.Data.Set.prop_union_iff_prop_and {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (p : α → Prop) (s₁ s₂ : Set α) : ((∀ (a : α), a ∈ s₁ → p a) ∧ ∀ (a : α), a ∈ s₂ → p a) ↔ ∀ (a : α), a ∈ s₁ ∪ s₂ → p a

theorem Cedar.Data.Set.union_comm {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (s₁ s₂ : Set α) : s₁ ∪ s₂ = s₂ ∪ s₁

Union is commutative even if its operands are not well-formed.

theorem Cedar.Data.Set.union_assoc {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (s₁ s₂ s₃ : Set α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

Union is associative even if its operands are not well-formed.

theorem Cedar.Data.Set.union_empty_right {α : Type u_1} [LT α] [DecidableLT α] {s : Set α} : s ∪ empty = s

Union with the empty set does not require well-formedness.

theorem Cedar.Data.Set.union_empty_left {α : Type u_1} [LT α] [DecidableLT α] {s : Set α} : empty ∪ s = s

Union with the empty set does not require well-formedness.

theorem Cedar.Data.Set.union_idempotent {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] {s : Set α} : s ∪ s = s

Union with itself does not require well-formedness.

subset

theorem Cedar.Data.Set.elts_subset_then_subset {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {xs ys : List α} : xs ⊆ ys → make xs ⊆ make ys

theorem Cedar.Data.Set.subset_def {α : Type u_1} [DecidableEq α] {s₁ s₂ : Set α} : s₁ ⊆ s₂ ↔ ∀ (a : α), a ∈ s₁ → a ∈ s₂

Like List.subset_def, but lifted to Sets

@[simp]

theorem Cedar.Data.Set.subset_empty {α : Type u_1} [DecidableEq α] {s : Set α} : empty ⊆ s

theorem Cedar.Data.Set.superset_empty_subset_empty {α : Type u_1} [DecidableEq α] {s₁ s₂ : Set α} : s₁ ⊆ s₂ → s₂.isEmpty = true → s₁.isEmpty = true

theorem Cedar.Data.Set.subset_iff_subset_elts {α : Type u_1} [DecidableEq α] {s₁ s₂ : Set α} : s₁ ⊆ s₂ ↔ s₁.elts ⊆ s₂.elts

theorem Cedar.Data.Set.subset_iff_eq {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {s₁ s₂ : Set α} : s₁.WellFormed → s₂.WellFormed → (s₁ ⊆ s₂ ∧ s₂ ⊆ s₁ ↔ s₁ = s₂)

theorem Cedar.Data.Set.subset_trans {α : Type u_1} [DecidableEq α] {s₁ s₂ s₃ : Set α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃

theorem Cedar.Data.Set.subset_refl {α : Type u_1} [DecidableEq α] {s : Set α} : s ⊆ s

theorem Cedar.Data.Set.mem_subset_mem {α : Type u_1} [DecidableEq α] {a : α} {s₁ s₂ : Set α} : a ∈ s₁ → s₁ ⊆ s₂ → a ∈ s₂

theorem Cedar.Data.Set.subset_union {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] (s₁ s₂ : Set α) : s₁ ⊆ s₁ ∪ s₂

theorem Cedar.Data.Set.union_subset {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {s₁ s₂ s₃ : Set α} : s₁ ∪ s₂ ⊆ s₃ ↔ s₁ ⊆ s₃ ∧ s₂ ⊆ s₃

theorem Cedar.Data.Set.union_subset_eq {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {s₁ s₂ : Set α} : s₁.WellFormed → s₂.WellFormed → s₁ ⊆ s₂ → s₁ ∪ s₂ = s₂

theorem Cedar.Data.Set.wellFormed_correct {α : Type u_1} [LT α] [StrictLT α] [DecidableLT α] {s : Set α} : s.wellFormed = true ↔ s.WellFormed

map

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

theorem Cedar.Data.Set.map_id {α : Type u_1} [LT α] [DecidableLT α] (s : Set α) : s.WellFormed → map id s = s

@[simp]

theorem Cedar.Data.Set.mem_map {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] [StrictLT β] {b : β} {f : α → β} {s : Set α} : b ∈ map f s ↔ ∃ (a : α), a ∈ s ∧ f a = b

Analogue of List.mem_map but for sets

theorem Cedar.Data.Set.map_congr {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] {f g : α → β} {s : Set α} : (∀ (a : α), a ∈ s → f a = g a) → map f s = map g s

Analogue of List.map_congr, but for sets

@[simp]

theorem Cedar.Data.Set.isEmpty_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [LT β] [DecidableLT β] [DecidableEq β] {f : α → β} {s : Set α} : (map f s).isEmpty = s.isEmpty

@[simp]

theorem Cedar.Data.Set.map_make {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [LT β] [DecidableLT β] [StrictLT β] {f : α → β} {xs : List α} : map f (make xs) = make (List.map f xs)

theorem Cedar.Data.Set.map_def {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) (s : Set α) : map f s = make (List.map f s.elts)

theorem Cedar.Data.Set.map_union {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [StrictLT α] [LT β] [DecidableLT β] [StrictLT β] (f : α → β) (s₁ s₂ : Set α) : map f (s₁ ∪ s₂) = map f s₁ ∪ map f s₂

Set.map distributes over ∪.

filter and differences

theorem Cedar.Data.Set.filter_wf {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (p : α → Bool) (s : Set α) : s.WellFormed → (filter p s).WellFormed

@[simp]

theorem Cedar.Data.Set.mem_filter {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] (p : α → Bool) (s : Set α) (e : α) : e ∈ filter p s ↔ e ∈ s ∧ p e = true

theorem Cedar.Data.Set.difference_wf {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] (s₁ s₂ : Set α) : s₁.WellFormed → (s₁.difference s₂).WellFormed

@[simp]

theorem Cedar.Data.Set.mem_difference {α : Type u_1} [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] (s₁ s₂ : Set α) (e : α) : e ∈ s₁.difference s₂ ↔ e ∈ s₁ ∧ ¬e ∈ s₂

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

all and any

@[simp]

theorem Cedar.Data.Set.all_eq_true {α : Type u_1} {f : α → Bool} {s : Set α} : all f s = true ↔ ∀ (x : α), x ∈ s → f x = true

Like List.all_eq_true, but for Set.all

@[simp]

theorem Cedar.Data.Set.all_eq_false {α : Type u_1} {f : α → Bool} {s : Set α} : all f s = false ↔ ∃ (x : α), x ∈ s ∧ ¬f x = true

Like List.all_eq_false, but for Set.all

@[simp]

theorem Cedar.Data.Set.any_eq_true {α : Type u_1} {f : α → Bool} {s : Set α} : any f s = true ↔ ∃ (x : α), x ∈ s ∧ f x = true

Like List.any_eq_true, but for Set.any

@[simp]

theorem Cedar.Data.Set.any_eq_false {α : Type u_1} {f : α → Bool} {s : Set α} : any f s = false ↔ ∀ (x : α), x ∈ s → ¬f x = true

Like List.any_eq_false, but for Set.any

map₁, all₁, and any₁

@[simp]

theorem Cedar.Data.Set.map₁_eq_map {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [LT β] [DecidableLT β] (f : α → β) (s : Set α) : (s.map₁ fun (x : { a : α // a ∈ s }) => match x with | ⟨elt, property⟩ => f elt) = map f s

@[simp]

theorem Cedar.Data.Set.all₁_eq_all {α : Type u_1} {s : Set α} {f : α → Bool} : (s.all₁ fun (x : { a : α // a ∈ s }) => match x with | ⟨elt, property⟩ => f elt) = all f s

@[simp]

theorem Cedar.Data.Set.any₁_eq_any {α : Type u_1} {s : Set α} {f : α → Bool} : (s.any₁ fun (x : { a : α // a ∈ s }) => match x with | ⟨elt, property⟩ => f elt) = any f s

product

@[simp]

theorem Cedar.Data.Set.mem_product {α : Type u_1} {β : Type u_2} {a : α} {b : β} {s₁ : Set α} {s₂ : Set β} : (a, b) ∈ s₁.product s₂ ↔ a ∈ s₁ ∧ b ∈ s₂

An element is in s₁.product s₂ iff its components are in s₁ and s₂.

@[simp]

theorem Cedar.Data.Set.product_empty {α : Type u_1} {β : Type u_2} (s : Set α) : s.product empty = empty

@[simp]

theorem Cedar.Data.Set.empty_product {α : Type u_1} {β : Type u_2} (s : Set β) : empty.product s = empty