How does RCLike.toDecidableEq work?

Stream: new members

[Lawrence Wu (llllvvuu)]

How does docs#RCLike.toDecidableEq work? I thought RCLike fields would be very not DecidableEq

[Aaron Liu]

the instances for Real and Complex use the classical decidability

[Kevin Buzzard]

The fact that this instance is here at all is an indication to me that something is surely wrong, but it's been there for ages and I don't hear the analysts complaining about it so if they're happy then that's great

[Kevin Buzzard]

Could it be because some order theory (maybe LinearOrder) has some decidable stuff in it still, so lean doesn't go nuts when you do a case split on x<= y or x>y? And then you have to deal with the fact that you can't always use the classical instance because what if the base is the rationals, so you have to use the instance that typeclass inference finds.

[Eric Wieser]

This is by design, we deliberately add non-computable instances for things we know can never be computable

[Eric Wieser]

Otherwise users reach for open scoped Classical which will shoot them in the foot at the same time, add a Decidable hypothesis which can never be satisfied, and/or complain on Zulip about how annoying decidable is.

[Eric Wieser]

I don't think there are any downsides to having the RCLike / Real / Complex instances, though I guess those aren't immune to Zulip complaints either :)

[Kevin Buzzard]

Yeah I guess this sounds like a good compromise.

[Kevin Buzzard]

I suppose the philosophy is that because lean/mathlib attempts to offer a computable functionality for computable types, this computable stuff becomes embedded in our system. So every concrete type should have exactly one instance of decidable equality, decidable LE if there's an LE etc, otherwise it won't be usable. So presumably the p-adic numbers should have a non-computable DecidableEQ instance for the same reason.