Requiring LawfulHashable for HashMap

Stream: batteries

[Johannes Tantow]

Hi,

currently in Batteries the HashMaps only require BEq and Hashable. I think it would be useful to also require LawfulHashable for the type. Otherwise there can be elements that are equal according to BEq, but are in different buckets. The currently stated proof goal in HashMap.Lemmas does not work if the Hash is not lawful. Nonetheless, I think that this is a desired specification to have and is what I would expect.

LawfulHashable is used in the specification of the well-formedness of the HashMap, but the hashMap below appears to be still well-formed.

proof_wanted insert_find? [BEq α] [Hashable α] (m : HashMap α β) (a a' : α) (b : β) :
    (m.insert a b).find? a' = if a' == a then some b else m.find? a'

See counterexample:

import Batteries.Data.HashMap

namespace Batteries

inductive testType
| firstElement: testType
| secondElement: testType

def hashtestType (t: testType): UInt64 :=
  match t with
  | testType.firstElement => UInt64.ofNat 1
  | testType.secondElement => UInt64.ofNat 2

instance: Hashable testType where hash:=hashtestType

def compTestType (_ _: testType): Bool := True

instance: BEq testType where beq:=compTestType

#eval ((HashMap.ofList [(testType.firstElement, 0)]).insert testType.secondElement 2).find? testType.firstElement

#eval if testType.firstElement == testType.secondElement then some 2 else (HashMap.ofList [(testType.firstElement, 0)]).find? testType.firstElement

[Markus Himmel]

You're right that the given lemma is not provable if the hash is not lawful. It's good that the HashMap type itself does not require LawfulHashable, so that you can use the hashmap if you're in a situation where you're just programming and don't care about proofs. The corresponding lemma in the hashmap implementation that will soon be part of Lean core requires that the hash is lawful and also that the BEq instance is an equivalence relation.

[Johannes Tantow]

From this point of view it makes sense. I didn't think of the purely programming side.

Is there a roadmap or channel for your project ? I have worked a bit on proving lemmas about the current hash map implementation, but I didn't manage to prove all of the requirements I need yet.

[François G. Dorais]

@Markus Himmel EquivBEq has been wanted for a while... I almost submitted it to Batteries last week but other priorities got in the way. Anyway, please consider incremental submissions to lean core if possible!

[Markus Himmel]

It should land in core soon and will likely be part of the 4.10 release. (Update: nope, missed the 4.10 rc, 4.11 it is)