Contract for equality and Hashable?

Stream: lean4

[David Thrane Christiansen]

In Java, there's an expectation that every implementation of hashCode will generate identical codes for values that are equal.

What is the contract that relates BEq α, {x y : α} : Decidable (x = y), and Hashable α? My guess, based on reading various Lean code, is that all of the following should hold:

• beq should always return true when two values are propositionally equal (that is, for an inhabited type, it shouldn't be fun x y => false)
• beq should always return false when two values are propositionally inequal (that is, it shouldn't do more quotienting than the type's notion of propositional equality)
• x == y = true → hashCode x = hashCode y should be true

Is this a correct understanding? I'm not saying that users should have to prove all of these, merely that it's a bug if they don't all hold. The last point is a consequence of beq reflecting propositional equality in the sense of the first two points, but it seems useful to state in case that is a misunderstanding.

Thanks!

[Henrik Böving]

We have LawfulBEq already but I'm not aware of a LawfulHashable, although that might be a nice addition for std4? CC @Mario Carneiro

[Matthew Ballard]

https://github.com/leanprover/std4/blob/a7237a4a4a7dd520ba1425295306bc1b4f754577/Std/Data/HashMap/Basic.lean#L13

[Henrik Böving]

Hurray

[David Thrane Christiansen]

Hmm, LawfulBEq seems to admit fun x y => true as lawful...

Sorry, it's late here :-)

[Sebastian Ullrich]

David Thrane Christiansen said:

beq should always return false when two values are propositionally inequal (that is, it shouldn't do more quotienting than the type's notion of propositional equality)

Violating this one is not considered a bug (or else we would just use Decidable (x = y) instead of BEq, like we did in Lean 3). BEq Expr for example works modulo binder annotations. BEq Float arguably violates it as well, even though here we can't prove propositional inequality.

[Wojciech Nawrocki]

or else we would just use Decidable (x = y) instead of BEq

Interesting, I thought the point of BEq was more that you don't actually have to prove x = y rather than allowing for quotients.

[Wojciech Nawrocki]

Also, that does mean BEq Expr is not a LawfulBEq right?

[James Gallicchio]

(deleted)

[Mario Carneiro]

Now that the core invariant proofs of HashMap are done, I am fairly confident in the necessity of each of the properties used in the definition of HashMap:

• a == b -> hash a = hash b
• a == b -> b == a (I tried getting around this by permuting the equality checks but it really does need both directions)
• a == b -> b == c -> a == c

The first one is LawfulHashable and the last two are PartialEquivBEq. Perhaps surprisingly, we don't need to require a == a (which would make it a total equivalence relation instead of a partial equivalence relation) for the core invariants, although you will need this to prove that (m.insert k v).find? k = some v.

[Tom]

I don't want to derail this topic too much but it has now been several times that I've seen this recently. I asked not that long ago about some guidance for BEq and DecidableEq; specifically about when one should prefer one over the other in the context of e.g. deriving for structures etc.

From some of the recent discussions (including the above), I am inferring that the consensus is moving toward always using BEq (==) (instead of =, at least for programming) for equalities; and the difference will be that if LawfulBEq class exists, it will also be useful for doing proofs? (such as e.g. matching/ifs for things like "List is not empty" when using List.head)

If the answer is too long/complicated, I can start a separate topic, please just LMK.

[David Thrane Christiansen]

Thanks!

I think requiring BEq to give an equivalence relation makes a lot of sense, and I also get the practical reasons for coarsening it WRT decidable equality. Does this imply that LawfulBEq is improperly named?