Zulip Chat Archive

This problem feels simple, but it's giving me a headache. I am trying to erase an element from a finset. This behaves fine when I am working with finsets of natural numbers. However, when I work with finsets of an arbitrary Type α, I have problems. Here are two silly examples to illustrate:

import data.set.finite
import data.finset.basic

example {b : ℕ} (S : finset ℕ) (hb : b ∈ S) :
    1 + 1 = 2 :=
begin
    let not_b : finset ℕ := finset.erase S b,
    exact rfl,
end

example {α : Type} {b : α} (S : finset α) (hb : b ∈ S) :
    1 + 1 = 2 :=
begin
    let not_b : finset α := finset.erase S b,
    sorry,
end

The first one works; the second one tells me "failed to synthesize Type class instance." What's going on here? Is there a general lesson here to help me feel better about asking this question in the first place?

Heather Macbeth (Dec 22 2020 at 18:38):

Try

example {α : Type} [decidable_eq α] {b : α} (S : finset α) (hb : b ∈ S) :
    1 + 1 = 2 :=

Heather Macbeth (Dec 22 2020 at 18:41):

I think it also works to open_locale classical pre-emptively (and then the decidable_eq isn't needed) whenever you are dealing with finsets :)

Heather Macbeth (Dec 22 2020 at 18:42):

One way to figure out what was missing would be to check docs#finset.erase, where you can see that [decidable_eq α] is one of the arguments needed.

Heather Macbeth (Dec 22 2020 at 18:47):

Another way is to use @ to make all arguments explicit. Then you can feed finset.erase explicitly the things you had hoped it would figure out automatically, and in failing it will give you a more useful message. So here,

    let not_b : finset α := @finset.erase α _ S b,

gives a more useful error message,

failed to synthesize type class instance for
α : Type,
b : α,
S : finset α,
hb : b ∈ S
⊢ decidable_eq α

Andrew Souther (Dec 22 2020 at 18:55):

Ahhh I see, the docs do make that very clear, thank you.
I was looking at the source code for erase inside of data.finset.basic.... I didn't see variables [decidable_eq α] 300 lines above. Also, good to know about @ as a troubleshooting tool.

Eric Wieser (Dec 22 2020 at 19:34):

The error message will have told you exactly which typeclass instance couldn't be synthesized, I think

Andrew Souther (Dec 22 2020 at 20:08):

Oof, you're right. I never really learned (or got in the habit of) reading these error messages properly, but I see what's going on. Thanks.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib