feat(finset): add has_sep instance (#1477)

src/data/finset.lean

@@ -659,6 +659,28 @@ begin
   { intro x, simp, intros hx hx₂, refine ⟨or.resolve_left (h hx) hx₂, hx₂⟩ }
 end
 
+/- We can simplify an application of filter where the decidability is inferred in "the wrong way" -/
+@[simp] lemma filter_congr_decidable {α} (s : finset α) (p : α → Prop) (h : decidable_pred p)
+  [decidable_pred p] : @filter α p h s = s.filter p :=
+by congr
+
+section classical
+open_locale classical
+/-- The following instance allows us to write `{ x ∈ s | p x }` for `finset.filter s p`.
+  Since the former notation requires us to define this for all propositions `p`, and `finset.filter`
+  only works for decidable propositions, the notation `{ x ∈ s | p x }` is only compatible with
+  classical logic because it uses `classical.prop_decidable`.
+  We don't want to redo all lemmas of `finset.filter` for `has_sep.sep`, so we make sure that `simp`
+  unfolds the notation `{ x ∈ s | p x }` to `finset.filter s p`. If `p` happens to be decidable, the
+  simp-lemma `filter_congr_decidable` will make sure that `finset.filter` uses the right instance
+  for decidability.
+-/
+noncomputable instance {α : Type*} : has_sep α (finset α) := ⟨λ p x, x.filter p⟩
+
+@[simp] lemma sep_def {α : Type*} (s : finset α) (p : α → Prop) : {x ∈ s | p x} = s.filter p := rfl
+
+end classical
+
 -- This is not a good simp lemma, as it would prevent `finset.mem_filter` from firing
 -- on, e.g. `x ∈ s.filter(eq b)`.
 lemma filter_eq [decidable_eq β] (s : finset β) (b : β) :

test/examples.lean

@@ -177,3 +177,25 @@ meta structure meta_struct (α : Type u) : Type u :=
   (z : list α)
   (k : list (list α))
   (w : expr)
+
+/- tests of has_sep on finset -/
+
+
+example {α} (s : finset α) (p : α → Prop) [decidable_pred p] : {x ∈ s | p x} = s.filter p :=
+by simp
+
+example {α} (s : finset α) (p : α → Prop) [decidable_pred p] :
+  {x ∈ s | p x} = @finset.filter α p (λ _, classical.prop_decidable _) s :=
+by simp
+
+section
+open_locale classical
+
+example {α} (s : finset α) (p : α → Prop) : {x ∈ s | p x} = s.filter p :=
+by simp
+
+example (n m k : ℕ) : {x ∈ finset.range n | x < m ∨ x < k } =
+  {x ∈ finset.range n | x < m } ∪ {x ∈ finset.range n | x < k } :=
+by simp [finset.filter_or]
+
+end