Zulip Chat Archive

Stream: mathlib4

Topic: BEq DecidableEq Diamond


Chris Hughes (Jan 11 2023 at 14:51):

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 (Jan 11 2023 at 15:32):

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 (Jan 15 2023 at 00:19):

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 (Jan 15 2023 at 00:21):

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 (Jan 15 2023 at 00:21):

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

Yaël Dillies (Jan 15 2023 at 00:26):

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

Eric Rodriguez (Jan 15 2023 at 00:45):

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

Yaël Dillies (Jan 15 2023 at 01:41):

===

Mario Carneiro (Jan 15 2023 at 01:41):

there isn't one

Mario Carneiro (Jan 15 2023 at 01:41):

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

Yaël Dillies (Jan 15 2023 at 01:42):

Oh really? I am misremembering.

Yaël Dillies (Jan 15 2023 at 01:42):

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

Mario Carneiro (Jan 15 2023 at 01:43):

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

Eric Rodriguez (Jan 15 2023 at 01:43):

It's definitely very useful in some circumstances

Mario Carneiro (Jan 15 2023 at 01:43):

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

Eric Rodriguez (Jan 15 2023 at 01:51):

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

Thomas Murrills (Jan 15 2023 at 01:52):

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

Thomas Murrills (Jan 15 2023 at 01:55):

E.g. a ≡≡ b

Thomas Murrills (Jan 15 2023 at 01:58):

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

Eric Wieser (Jan 15 2023 at 02:06):

a =💥= b

Yury G. Kudryashov (Jan 15 2023 at 06:37):

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

Yury G. Kudryashov (Jan 15 2023 at 06:37):

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


Last updated: Dec 20 2023 at 11:08 UTC