# Zulip Chat Archive

## Stream: general

### Topic: decidable_eq for finsupp

#### Bolton Bailey (Feb 13 2021 at 02:26):

Hey, I'm wondering about the following

```
import data.finsupp.basic
section
universe u
@[derive decidable_eq]
inductive vars : Type
| X : vars
| Y : vars
| Z : vars
lemma foo : ¬(finsupp.single vars.Y 4) = (finsupp.single vars.X 3) :=
begin
-- rw finsupp.single_eq_single_iff,
exact dec_trivial,
end
end
```

If I uncomment the `single_eq_single_iff`

, then it works fine. But `finsupp.decidable_eq`

should be derivable, since both `vars`

and `nat`

have `decidable_eq`

. So how do I get the above to work without using `single_eq_single_iff`

?

#### Eric Wieser (Feb 13 2021 at 02:29):

docs#finsupp.single uses classical decidability on its domain (vars),

#### Eric Wieser (Feb 13 2021 at 02:29):

Which dec_trivial can't use

#### Bolton Bailey (Feb 13 2021 at 03:19):

Ok, then is it ever possible to use decidability to prove equivalence of two `finsupps`

? Can I define my own single for decidable domain types for which the above lemma will work? Is there some way of telling the existing `single`

to avoid using classical decidability and just use the decidability instance that is derived?

It seems to me it shouldn't matter how `single`

is defined - it returns a finsupp with decidable domain and decidable range so it should be decidable to determine if two of them are equal.

#### Mario Carneiro (Feb 13 2021 at 07:13):

This used to be the design, but it requires a `[decidable_eq]`

argument in the definition of `single`

and many other operations on finsupp, and these arguments can get in the way when you are doing proofs, so now finsupps are entirely classical. You can of course implement your own version of `single`

that is decidable - you can even just copy-paste the definition and insert the requisite `[decidable_eq]`

typeclass argument, and then the above calculation will work

#### Eric Wieser (Feb 13 2021 at 09:41):

Meanwhile, docs#dfinsupp still has the decidability assumption present

Last updated: May 14 2021 at 05:20 UTC