feat(data/set/basic): decidable_mem

src/data/equiv/encodable/basic.lean

@@ -142,7 +142,7 @@ theorem encodek₂ [encodable α] (a : α) : decode₂ α (encode a) = some a :=
 mem_decode₂.2 rfl
 
 /-- The encoding function has decidable range. -/
-def decidable_range_encode (α : Type*) [encodable α] : decidable_pred (∈ set.range (@encode α _)) :=
+def decidable_range_encode (α : Type*) [encodable α] : decidable_mem (set.range (@encode α _)) :=
 λ x, decidable_of_iff (option.is_some (decode₂ α x))
   ⟨λ h, ⟨option.get h, by rw [← decode₂_is_partial_inv (option.get h), option.some_get]⟩,
   λ ⟨n, hn⟩, by rw [← hn, encodek₂]; exact rfl⟩

src/data/equiv/set.lean

@@ -196,76 +196,76 @@ protected def of_eq {α : Type u} {s t : set α} (h : s = t) : s ≃ t :=
   right_inv := λ _, subtype.eq rfl }
 
 /-- If `a ∉ s`, then `insert a s` is equivalent to `s ⊕ punit`. -/
-protected def insert {α} {s : set.{u} α} [decidable_pred (∈ s)] {a : α} (H : a ∉ s) :
+protected def insert {α} {s : set.{u} α} [decidable_mem s] {a : α} (H : a ∉ s) :
   (insert a s : set α) ≃ s ⊕ punit.{u+1} :=
 calc (insert a s : set α) ≃ ↥(s ∪ {a}) : equiv.set.of_eq (by simp)
 ... ≃ s ⊕ ({a} : set α) : equiv.set.union (by finish [set.subset_def])
 ... ≃ s ⊕ punit.{u+1} : sum_congr (equiv.refl _) (equiv.set.singleton _)
 
-@[simp] lemma insert_symm_apply_inl {α} {s : set.{u} α} [decidable_pred (∈ s)] {a : α} (H : a ∉ s)
+@[simp] lemma insert_symm_apply_inl {α} {s : set.{u} α} [decidable_mem s] {a : α} (H : a ∉ s)
   (b : s) : (equiv.set.insert H).symm (sum.inl b) = ⟨b, or.inr b.2⟩ :=
 rfl
 
-@[simp] lemma insert_symm_apply_inr {α} {s : set.{u} α} [decidable_pred (∈ s)] {a : α} (H : a ∉ s)
+@[simp] lemma insert_symm_apply_inr {α} {s : set.{u} α} [decidable_mem s] {a : α} (H : a ∉ s)
   (b : punit.{u+1}) : (equiv.set.insert H).symm (sum.inr b) = ⟨a, or.inl rfl⟩ :=
 rfl
 
-@[simp] lemma insert_apply_left {α} {s : set.{u} α} [decidable_pred (∈ s)] {a : α} (H : a ∉ s) :
+@[simp] lemma insert_apply_left {α} {s : set.{u} α} [decidable_mem s] {a : α} (H : a ∉ s) :
   equiv.set.insert H ⟨a, or.inl rfl⟩ = sum.inr punit.star :=
 (equiv.set.insert H).apply_eq_iff_eq_symm_apply.2 rfl
 
-@[simp] lemma insert_apply_right {α} {s : set.{u} α} [decidable_pred (∈ s)] {a : α} (H : a ∉ s)
+@[simp] lemma insert_apply_right {α} {s : set.{u} α} [decidable_mem s] {a : α} (H : a ∉ s)
   (b : s) : equiv.set.insert H ⟨b, or.inr b.2⟩ = sum.inl b :=
 (equiv.set.insert H).apply_eq_iff_eq_symm_apply.2 rfl
 
 /-- If `s : set α` is a set with decidable membership, then `s ⊕ sᶜ` is equivalent to `α`. -/
-protected def sum_compl {α} (s : set α) [decidable_pred (∈ s)] : s ⊕ (sᶜ : set α) ≃ α :=
+protected def sum_compl {α} (s : set α) [decidable_mem s] : s ⊕ (sᶜ : set α) ≃ α :=
 calc s ⊕ (sᶜ : set α) ≃ ↥(s ∪ sᶜ) : (equiv.set.union (by simp [set.ext_iff])).symm
 ... ≃ @univ α : equiv.set.of_eq (by simp)
 ... ≃ α : equiv.set.univ _
 
-@[simp] lemma sum_compl_apply_inl {α : Type u} (s : set α) [decidable_pred (∈ s)] (x : s) :
+@[simp] lemma sum_compl_apply_inl {α : Type u} (s : set α) [decidable_mem s] (x : s) :
   equiv.set.sum_compl s (sum.inl x) = x := rfl
 
-@[simp] lemma sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred (∈ s)] (x : sᶜ) :
+@[simp] lemma sum_compl_apply_inr {α : Type u} (s : set α) [decidable_mem s] (x : sᶜ) :
   equiv.set.sum_compl s (sum.inr x) = x := rfl
 
-lemma sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_pred (∈ s)] {x : α}
+lemma sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_mem s] {x : α}
   (hx : x ∈ s) : (equiv.set.sum_compl s).symm x = sum.inl ⟨x, hx⟩ :=
 have ↑(⟨x, or.inl hx⟩ : (s ∪ sᶜ : set α)) ∈ s, from hx,
 by { rw [equiv.set.sum_compl], simpa using set.union_apply_left _ this }
 
-lemma sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred (∈ s)] {x : α}
+lemma sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_mem s] {x : α}
   (hx : x ∉ s) : (equiv.set.sum_compl s).symm x = sum.inr ⟨x, hx⟩ :=
 have ↑(⟨x, or.inr hx⟩ : (s ∪ sᶜ : set α)) ∈ sᶜ, from hx,
 by { rw [equiv.set.sum_compl], simpa using set.union_apply_right _ this }
 
-@[simp] lemma sum_compl_symm_apply {α : Type*} {s : set α} [decidable_pred (∈ s)] {x : s} :
+@[simp] lemma sum_compl_symm_apply {α : Type*} {s : set α} [decidable_mem s] {x : s} :
   (equiv.set.sum_compl s).symm x = sum.inl x :=
 by cases x with x hx; exact set.sum_compl_symm_apply_of_mem hx
 
 @[simp] lemma sum_compl_symm_apply_compl {α : Type*} {s : set α}
-  [decidable_pred (∈ s)] {x : sᶜ} : (equiv.set.sum_compl s).symm x = sum.inr x :=
+  [decidable_mem s] {x : sᶜ} : (equiv.set.sum_compl s).symm x = sum.inr x :=
 by cases x with x hx; exact set.sum_compl_symm_apply_of_not_mem hx
 
 /-- `sum_diff_subset s t` is the natural equivalence between
 `s ⊕ (t \ s)` and `t`, where `s` and `t` are two sets. -/
-protected def sum_diff_subset {α} {s t : set α} (h : s ⊆ t) [decidable_pred (∈ s)] :
+protected def sum_diff_subset {α} {s t : set α} (h : s ⊆ t) [decidable_mem s] :
   s ⊕ (t \ s : set α) ≃ t :=
 calc s ⊕ (t \ s : set α) ≃ (s ∪ (t \ s) : set α) :
   (equiv.set.union (by simp [inter_diff_self])).symm
 ... ≃ t : equiv.set.of_eq (by { simp [union_diff_self, union_eq_self_of_subset_left h] })
 
 @[simp] lemma sum_diff_subset_apply_inl
-  {α} {s t : set α} (h : s ⊆ t) [decidable_pred (∈ s)] (x : s) :
+  {α} {s t : set α} (h : s ⊆ t) [decidable_mem s] (x : s) :
   equiv.set.sum_diff_subset h (sum.inl x) = inclusion h x := rfl
 
 @[simp] lemma sum_diff_subset_apply_inr
-  {α} {s t : set α} (h : s ⊆ t) [decidable_pred (∈ s)] (x : t \ s) :
+  {α} {s t : set α} (h : s ⊆ t) [decidable_mem s] (x : t \ s) :
   equiv.set.sum_diff_subset h (sum.inr x) = inclusion (diff_subset t s) x := rfl
 
 lemma sum_diff_subset_symm_apply_of_mem
-  {α} {s t : set α} (h : s ⊆ t) [decidable_pred (∈ s)] {x : t} (hx : x.1 ∈ s) :
+  {α} {s t : set α} (h : s ⊆ t) [decidable_mem s] {x : t} (hx : x.1 ∈ s) :
   (equiv.set.sum_diff_subset h).symm x = sum.inl ⟨x, hx⟩ :=
 begin
   apply (equiv.set.sum_diff_subset h).injective,
@@ -274,7 +274,7 @@ begin
 end
 
 lemma sum_diff_subset_symm_apply_of_not_mem
-  {α} {s t : set α} (h : s ⊆ t) [decidable_pred (∈ s)] {x : t} (hx : x.1 ∉ s) :
+  {α} {s t : set α} (h : s ⊆ t) [decidable_mem s] {x : t} (hx : x.1 ∉ s) :
   (equiv.set.sum_diff_subset h).symm x = sum.inr ⟨x, ⟨x.2, hx⟩⟩  :=
 begin
   apply (equiv.set.sum_diff_subset h).injective,
@@ -284,7 +284,7 @@ end
 
 /-- If `s` is a set with decidable membership, then the sum of `s ∪ t` and `s ∩ t` is equivalent
 to `s ⊕ t`. -/
-protected def union_sum_inter {α : Type u} (s t : set α) [decidable_pred (∈ s)] :
+protected def union_sum_inter {α : Type u} (s t : set α) [decidable_mem s] :
   (s ∪ t : set α) ⊕ (s ∩ t : set α) ≃ s ⊕ t :=
 calc  (s ∪ t : set α) ⊕ (s ∩ t : set α)
     ≃ (s ∪ t \ s : set α) ⊕ (s ∩ t : set α) : by rw [union_diff_self]
@@ -300,8 +300,8 @@ calc  (s ∪ t : set α) ⊕ (s ∩ t : set α)
 /-- Given an equivalence `e₀` between sets `s : set α` and `t : set β`, the set of equivalences
 `e : α ≃ β` such that `e ↑x = ↑(e₀ x)` for each `x : s` is equivalent to the set of equivalences
 between `sᶜ` and `tᶜ`. -/
-protected def compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decidable_pred (∈ s)]
-  [decidable_pred (∈ t)] (e₀ : s ≃ t) :
+protected def compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decidable_mem s]
+  [decidable_mem t] (e₀ : s ≃ t) :
   {e : α ≃ β // ∀ x : s, e x = e₀ x} ≃ ((sᶜ : set α) ≃ (tᶜ : set β)) :=
 { to_fun := λ e, subtype_equiv e
     (λ a, not_congr $ iff.symm $ maps_to.mem_iff

src/data/fintype/basic.lean

@@ -204,7 +204,7 @@ instance decidable_exists_fintype {p : α → Prop} [decidable_pred p] [fintype
 decidable_of_iff (∃ a ∈ @univ α _, p a) (by simp)
 
 instance decidable_mem_range_fintype [fintype α] [decidable_eq β] (f : α → β) :
-  decidable_pred (∈ set.range f) :=
+  decidable_mem (set.range f) :=
 λ x, fintype.decidable_exists_fintype
 
 section bundled_homs
@@ -1054,7 +1054,7 @@ instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fin
 fintype.subtype (univ.filter p) (by simp)
 
 /-- A set on a fintype, when coerced to a type, is a fintype. -/
-def set_fintype {α} [fintype α] (s : set α) [decidable_pred (∈ s)] : fintype s :=
+def set_fintype {α} [fintype α] (s : set α) [decidable_mem s] : fintype s :=
 subtype.fintype (λ x, x ∈ s)
 
 lemma set_fintype_card_le_univ {α : Type*} [fintype α] (s : set α) [fintype ↥s] :

src/data/int/order.lean

@@ -49,7 +49,7 @@ instance : conditionally_complete_linear_order ℤ :=
 
 namespace int
 
-lemma cSup_eq_greatest_of_bdd {s : set ℤ} [decidable_pred (∈ s)]
+lemma cSup_eq_greatest_of_bdd {s : set ℤ} [decidable_mem s]
   (b : ℤ) (Hb : ∀ z ∈ s, z ≤ b) (Hinh : ∃ z : ℤ, z ∈ s) :
   Sup s = greatest_of_bdd b Hb Hinh :=
 begin
@@ -63,7 +63,7 @@ lemma cSup_empty : Sup (∅ : set ℤ) = 0 := dif_neg (by simp)
 
 lemma cSup_of_not_bdd_above {s : set ℤ} (h : ¬ bdd_above s) : Sup s = 0 := dif_neg (by simp [h])
 
-lemma cInf_eq_least_of_bdd {s : set ℤ} [decidable_pred (∈ s)]
+lemma cInf_eq_least_of_bdd {s : set ℤ} [decidable_mem s]
   (b : ℤ) (Hb : ∀ z ∈ s, b ≤ z) (Hinh : ∃ z : ℤ, z ∈ s) :
   Inf s = least_of_bdd b Hb Hinh :=
 begin

src/data/nat/basic.lean

@@ -101,7 +101,7 @@ instance : canonically_linear_ordered_add_monoid ℕ :=
 { .. (infer_instance : canonically_ordered_add_monoid ℕ),
   .. nat.linear_order }
 
-instance nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_pred (∈ s)] [h : nonempty s] :
+instance nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_mem s] [h : nonempty s] :
   semilattice_sup_bot s :=
 { bot := ⟨nat.find (nonempty_subtype.1 h), nat.find_spec (nonempty_subtype.1 h)⟩,
   bot_le := λ x, nat.find_min' _ x.2,

src/data/set/basic.lean

@@ -35,6 +35,8 @@ Notation used here:
 
 Definitions in the file:
 
+* `decidable_mem s` for `decidable_pred (∈ s)`.
+
 * `strict_subset s₁ s₂ : Prop` : the predicate `s₁ ⊆ s₂` but `s₁ ≠ s₂`.
 
 * `nonempty s : Prop` : the predicate `s ≠ ∅`. Note that this is the preferred way to express the
@@ -211,7 +213,14 @@ lemma set_of_app_iff {p : α → Prop} {x : α} : { x | p x } x ↔ p x := iff.r
 
 theorem mem_def {a : α} {s : set α} : a ∈ s ↔ s a := iff.rfl
 
-instance decidable_set_of (p : α → Prop) [H : decidable_pred p] : decidable_pred (∈ {a | p a}) := H
+/-- A decidable set is one whose membership predicate is decidable.
+This is short for `decidable_pred (∈ s)`. -/
+/- TODO: maybe move to core since it's not set-specific? -/
+@[reducible]
+def decidable_mem {α : Type u} {β : Type v} [has_mem α β] (s : β) :=
+decidable_pred (∈ s)
+
+instance decidable_mem_of (p : α → Prop) [H : decidable_pred p] : decidable_mem {a | p a} := H
 
 @[simp] theorem set_of_subset_set_of {p q : α → Prop} :
   {a | p a} ⊆ {a | q a} ↔ (∀a, p a → q a) := iff.rfl
@@ -437,7 +446,7 @@ eq_univ_of_univ_subset $ hs ▸ h
 lemma exists_mem_of_nonempty (α) : ∀ [nonempty α], ∃x:α, x ∈ (univ : set α)
 | ⟨x⟩ := ⟨x, trivial⟩
 
-instance univ_decidable : decidable_pred (∈ @set.univ α) :=
+instance univ_decidable : decidable_mem (@set.univ α) :=
 λ x, is_true trivial
 
 lemma ne_univ_iff_exists_not_mem {α : Type*} (s : set α) : s ≠ univ ↔ ∃ a, a ∉ s :=
@@ -2323,19 +2332,19 @@ by { ext z, simp [hy] }
   prod.mk x ⁻¹' s.prod t = ∅ :=
 by { ext z, simp [hx] }
 
-lemma mk_preimage_prod_left_eq_if {y : β} [decidable_pred (∈ t)] :
+lemma mk_preimage_prod_left_eq_if {y : β} [decidable_mem t] :
   (λ x, (x, y)) ⁻¹' s.prod t = if y ∈ t then s else ∅ :=
 by { split_ifs; simp [h] }
 
-lemma mk_preimage_prod_right_eq_if {x : α} [decidable_pred (∈ s)] :
+lemma mk_preimage_prod_right_eq_if {x : α} [decidable_mem s] :
   prod.mk x ⁻¹' s.prod t = if x ∈ s then t else ∅ :=
 by { split_ifs; simp [h] }
 
-lemma mk_preimage_prod_left_fn_eq_if {y : β} [decidable_pred (∈ t)] (f : γ → α) :
+lemma mk_preimage_prod_left_fn_eq_if {y : β} [decidable_mem t] (f : γ → α) :
   (λ x, (f x, y)) ⁻¹' s.prod t = if y ∈ t then f ⁻¹' s else ∅ :=
 by rw [← mk_preimage_prod_left_eq_if, prod_preimage_left, preimage_preimage]
 
-lemma mk_preimage_prod_right_fn_eq_if {x : α} [decidable_pred (∈ s)] (g : δ → β) :
+lemma mk_preimage_prod_right_fn_eq_if {x : α} [decidable_mem s] (g : δ → β) :
   (λ y, (x, g y)) ⁻¹' s.prod t = if x ∈ s then g ⁻¹' t else ∅ :=
 by rw [← mk_preimage_prod_right_eq_if, prod_preimage_right, preimage_preimage]
 

src/data/set/finite.lean

@@ -289,11 +289,11 @@ instance fintype_sep (s : set α) (p : α → Prop) [fintype s] [decidable_pred
   fintype ({a ∈ s | p a} : set α) :=
 fintype.of_finset (s.to_finset.filter p) $ by simp
 
-instance fintype_inter (s t : set α) [fintype s] [decidable_pred (∈ t)] : fintype (s ∩ t : set α) :=
+instance fintype_inter (s t : set α) [fintype s] [decidable_mem t] : fintype (s ∩ t : set α) :=
 set.fintype_sep s t
 
 /-- A `fintype` structure on a set defines a `fintype` structure on its subset. -/
-def fintype_subset (s : set α) {t : set α} [fintype s] [decidable_pred (∈ t)] (h : t ⊆ s) :
+def fintype_subset (s : set α) {t : set α} [fintype s] [decidable_mem t] (h : t ⊆ s) :
   fintype t :=
 by rw ← inter_eq_self_of_subset_right h; apply_instance
 

src/data/sym/sym2.lean

@@ -292,8 +292,8 @@ lemma mem_from_rel_irrefl_other_ne {sym : symmetric r} (irrefl : irreflexive r)
   {a : α} {z : sym2 α} (hz : z ∈ from_rel sym) (h : a ∈ z) : h.other ≠ a :=
 mem_other_ne (from_rel_irreflexive.mp irrefl hz) h
 
-instance from_rel.decidable_pred (sym : symmetric r) [h : decidable_rel r] :
-  decidable_pred (∈ sym2.from_rel sym) :=
+instance from_rel.decidable_mem (sym : symmetric r) [h : decidable_rel r] :
+  decidable_mem (sym2.from_rel sym) :=
 λ z, quotient.rec_on_subsingleton z (λ x, h _ _)
 
 end relations