BEq DecidableEq Diamond

Stream: mathlib4

[Chris Hughes]

import Data.List.Basic

example {α : Type _} [DecidableEq α] : @instBEq (List α) instDecidableEqList= instBEqList := rfl --fails

Having both BEq and DecidableEq doing the exact same thing seems like a recipe for disaster to me

[Johan Commelin]

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instBEqNat.20.3D.20instBEq.20.3A.3D.20rfl.20--fails/near/320613655 for that Nat version.

[Yaël Dillies]

This is going to be a headache. I want to use docs4#List.erase_sublist, but this lemma is miswritten as it requires DecidableEq α instead of the mere BEq α from List.erase. And now I am trying to prove the correct List.erase_sublist but I notice that I can't use List.erase_eq_eraseP because eraseP requires DecidablePred and adding DecidableEq α to the proof context results in docs4#instBEq being inferred (also, that's a terrible instance name).

[Yaël Dillies]

Ah! In fact that means erase_eq_eraseP is miswritten because the LHS should refer to any BEq α instance (instead of instBEq) and the RHS to a DecidableEq α one.

[Yaël Dillies]

This seems like the decidability conundrum got worse as we now have two typeclasses to annoy us rather than just one.

[Yaël Dillies]

Oh god, we don't even have Subsingleton (BEq α)

[Eric Rodriguez]

(what's the new syntax for docs4#HEq now that docs4#BEq steals ==?)

[Yaël Dillies]

===

[Mario Carneiro]

there isn't one

[Mario Carneiro]

this is deliberate since we want you to feel bad for using it

[Yaël Dillies]

Oh really? I am misremembering.

[Yaël Dillies]

But it's very useful for sigma types. I think removing the notation is a bit too strong of a warning.

[Mario Carneiro]

you can still use it, HEq is not that hard to write

[Eric Rodriguez]

It's definitely very useful in some circumstances

[Mario Carneiro]

but being useful doesn't mean it has to have notation

[Eric Rodriguez]

It's quite hard to read equivalence relations without some infix notation, in my experience

[Thomas Murrills]

Compromise: an infix notation that’s terrible to look at

[Thomas Murrills]

E.g. a ≡≡ b

[Thomas Murrills]

(fwiw if I were suggesting a notation we were meant to like, I’d suggest ⚍, a “broken” equality)

[Eric Wieser]

a =💥= b

[Yury G. Kudryashov]

BTW, should we simplify decide (a = b) to a == b?

[Yury G. Kudryashov]

(or should I move this question to a new thread?)