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