chore(library/init/data/set): drop set.sUnion (#675)

Moving to `mathlib`

library/init/data/set.lean

@@ -8,88 +8,33 @@ import init.meta.interactive
 import init.control.lawful
 
 universes u v
+
+/-- A set of elements of type `α`; implemented as a predicate `α → Prop`. -/
 def set (α : Type u) := α → Prop
 
-def set_of {α : Type u} (p : α → Prop) : set α :=
-p
+/-- The set `{x | p x}` of elements satisfying the predicate `p`. -/
+def set_of {α : Type u} (p : α → Prop) : set α := p
 
 namespace set
-variables {α : Type u} {β : Type v}
-
-protected def mem (a : α) (s : set α) :=
-s a
-
-instance : has_mem α (set α) :=
-⟨set.mem⟩
-
-protected def subset (s₁ s₂ : set α) :=
-∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂
-
-instance : has_subset (set α) :=
-⟨set.subset⟩
 
-protected def sep (p : α → Prop) (s : set α) : set α :=
-{a | a ∈ s ∧ p a}
+variables {α : Type u}
 
-instance : has_sep α (set α) :=
-⟨set.sep⟩
+instance has_mem : has_mem α (set α) := ⟨λ x s, s x⟩
 
-instance : has_emptyc (set α) :=
-⟨λ a, false⟩
+@[simp] lemma mem_set_of_eq {x : α} {p : α → Prop} : x ∈ {y | p y} = p x := rfl
 
-def univ : set α :=
-λ a, true
+instance : has_emptyc (set α) := ⟨{x | false}⟩
 
-protected def insert (a : α) (s : set α) : set α :=
-{b | b = a ∨ b ∈ s}
+/-- The set that contains all elements of a type. -/
+def univ : set α := {x | true}
 
-instance : has_insert α (set α) :=
-⟨set.insert⟩
+instance : has_insert α (set α) := ⟨λ a s, {b | b = a ∨ b ∈ s}⟩
 
 instance : has_singleton α (set α) := ⟨λ a, {b | b = a}⟩
 
+instance : has_sep α (set α) := ⟨λ p s, {x | x ∈ s ∧ p x}⟩
+
 instance : is_lawful_singleton α (set α) :=
 ⟨λ a, funext $ λ b, propext $ or_false _⟩
 
-protected def union (s₁ s₂ : set α) : set α :=
-{a | a ∈ s₁ ∨ a ∈ s₂}
-
-instance : has_union (set α) :=
-⟨set.union⟩
-
-protected def inter (s₁ s₂ : set α) : set α :=
-{a | a ∈ s₁ ∧ a ∈ s₂}
-
-instance : has_inter (set α) :=
-⟨set.inter⟩
-
-def compl (s : set α) : set α :=
-{a | a ∉ s}
-
-protected def diff (s t : set α) : set α :=
-{a ∈ s | a ∉ t}
-
-instance : has_sdiff (set α) :=
-⟨set.diff⟩
-
-def powerset (s : set α) : set (set α) :=
-{t | t ⊆ s}
-prefix `𝒫`:100 := powerset
-
-@[reducible]
-def sUnion (s : set (set α)) : set α := {t | ∃ a ∈ s, t ∈ a}
-prefix `⋃₀`:110 := sUnion
-
-def image (f : α → β) (s : set α) : set β :=
-{b | ∃ a, a ∈ s ∧ f a = b}
-
-instance : functor set :=
-{ map := @set.image }
-
-instance : is_lawful_functor set :=
-{ id_map := λ _ s, funext $ λ b, propext ⟨λ ⟨_, sb, rfl⟩, sb, λ sb, ⟨_, sb, rfl⟩⟩,
-  comp_map := λ _ _ _ g h s, funext $ λ c, propext
-    ⟨λ ⟨a, ⟨h₁, h₂⟩⟩, ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩,
-     λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, by dsimp; cc⟩⟩⟩ }
-
 end set

tests/lean/run/cc_ac4.lean

@@ -1,6 +1,8 @@
 --import data.set.basic
 open tactic
 
+instance {α} : has_union (set α) := ⟨λ s t, {a | a ∈ s ∨ a ∈ t}⟩
+
 constant union_is_assoc {α} : is_associative (set α) (∪)
 constant union_is_comm {α} : is_commutative (set α) (∪)
 attribute [instance] union_is_assoc union_is_comm

tests/lean/run/empty_set_inside_quotations.lean

@@ -1,3 +1,4 @@
+instance {α} : has_union (set α) := ⟨λ s t, {a | a ∈ s ∨ a ∈ t}⟩
 constant union_is_assoc {α} : is_associative (set α) (∪)
 attribute [instance] union_is_assoc
 

tests/lean/run/set1.lean

@@ -1,5 +1,7 @@
 variables A : Type
 
+instance : has_subset (set A) := ⟨λ s t, ∀ ⦃x⦄, x ∈ s → x ∈ t⟩
+
 example (s₁ s₂ s₃ : set A) : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ :=
 assume h₁ h₂ a ains₁,
 h₂ (h₁ ains₁)