Lean.Name DecidableEq

Stream: lean4

[Scott Viteri]

Hello,
I am finding that Lean.Name implements BEq, but not DecidableEq.
Is there a lemma somewhere that says everything with BEq is DecidableEq?

[Sebastian Ullrich]

No, because it is not true. For example, BEq Expr is defined modulo alpha equivalence.

[Scott Viteri]

My understanding of why we differentiate between BEq and Eq in the first place is that we can return a boolean if the function in question is decidable

[Daniel Selsam]

@Scott Viteri Sebastian's point is that one could define BEq arbitrarily, and so in general it might not actually be a decision procedure for equality. So the lemma you ask for cannot exist. As for Name, it does support DecidableEq and AFAICT BEq decides it, but the DecidableEq Name instance just hasn't been implemented yet.

[Scott Viteri]

I see, BEq could be any function at all from a to a to bool.

[Mario Carneiro]

So the lemma you ask for cannot exist.

Well it could exist, it would be a LawfulBEq typeclass like we currently have for monads. Although if BEq implementations which do not coincide with equality are normal and common, then maybe this typeclass should only include equivalence relation axioms to turn it into a setoid. You can already use x = y if you want something that is unambiguously an equality decision procedure.

[Scott Viteri]

Hmm

grep -r "LawfulBEq" ./

Coming up empty in lean3 and lean4 for me.

[Scott Viteri]

Oh, could exist nm

[François G. Dorais]

I like Mario's idea of LawfulBEq. I ran into this issue last week. I had been occasionally using the lemma

theorem decide_Eq {α} [DecidableEq α] (x y : α) : decide (x = y) = (x == y) := rfl

until it broke on Bool × Bool because that type's BEq is derived using instBEqProd instead of through instDecidableEqProd. I then realized this kind of lemma was basically hopeless. I'm glad I caught that early! A LawfulBEq class would help so would LawfulOrd.

[Mario Carneiro]

Why would you ever use BEq? What are the current use cases?

[Mario Carneiro]

I would be fine for reserving the use of BEq to the cases where it's not just Eq

[Mario Carneiro]

(or I guess if you are in programming context and don't want to prove anything)

[François G. Dorais]

It's the right equality for Float

[François G. Dorais]

(that one is also not lawful).

[Jakob von Raumer]

It's also used in Init.Data.List, in functions like erase and replace, which is why we even have to refer to BEq in teaching :-/