Zulip Chat Archive

Stream: lean4

Topic: Lean.Name DecidableEq


view this post on Zulip Scott Viteri (Apr 14 2021 at 21:10):

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

view this post on Zulip Sebastian Ullrich (Apr 14 2021 at 21:29):

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

view this post on Zulip Scott Viteri (Apr 14 2021 at 21:32):

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

view this post on Zulip Daniel Selsam (Apr 14 2021 at 22:02):

@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.

view this post on Zulip Scott Viteri (Apr 14 2021 at 22:20):

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

view this post on Zulip Mario Carneiro (Apr 15 2021 at 01:19):

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.

view this post on Zulip Scott Viteri (Apr 15 2021 at 01:50):

Hmm

grep -r "LawfulBEq" ./

Coming up empty in lean3 and lean4 for me.

view this post on Zulip Scott Viteri (Apr 15 2021 at 01:53):

Oh, could exist nm

view this post on Zulip François G. Dorais (Apr 15 2021 at 06:51):

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.

view this post on Zulip Mario Carneiro (Apr 15 2021 at 20:27):

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

view this post on Zulip Mario Carneiro (Apr 15 2021 at 20:28):

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

view this post on Zulip Mario Carneiro (Apr 15 2021 at 20:29):

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

view this post on Zulip François G. Dorais (Apr 15 2021 at 20:57):

It's the right equality for Float

view this post on Zulip François G. Dorais (Apr 15 2021 at 20:58):

(that one is also not lawful).

view this post on Zulip Jakob von Raumer (Apr 16 2021 at 12:07):

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 :-/


Last updated: May 07 2021 at 12:15 UTC