decidable_eq for finsupp

Stream: general

[Bolton Bailey]

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]

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

[Eric Wieser]

Which dec_trivial can't use

[Bolton Bailey]

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]

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]

Meanwhile, docs#dfinsupp still has the decidability assumption present