Proving `LawfulBEq` for `Std.HashSet` with Batter

Stream: new members

[Vadim Zaliva]

I'm trying to prove a LawfulBEq instance for Std.HashSet using the BEq instance defined in Batteries.Lean.HashSet:

instance : BEq (HashSet α) where
  beq s t := s.all (t.contains ·) && t.all (s.contains ·)

This checks element-wise equality. For LawfulBEq, I need to prove reflexivity and soundness. I've managed to prove reflexivity:

theorem LocSet.beq_refl (ls : LocSet) : BEq.beq ls ls = true

However, I'm stuck on soundness:

theorem sound (a b : Std.HashSet α) : (a == b) = true → a = b

The BEq definition establishes that a and b contain the same elements, but I cannot find a lemma in Std.Data.HashSet.Lemmas that would let me conclude propositional equality from this.

I need a set of natural numbers that I can use both in executable code and in proofs. I tried Finset but its noncomputability was propagating up to main, making it difficult to prove things about executable code in the IO monad. I also tried Std.ExtHashSet but it is missing operations I need (e.g., fold, toList).

Questions:

1. Is this provable at all? I suspect two HashSets with the same elements might have different internal representations (e.g., different bucket structures), which propositional equality would distinguish.
2. If not, is the Batteries BEq instance intended to be used with LawfulBEq, or should I define a different BEq based on structural equality?
3. Is there another set implementation I could use that supports both executable operations (fold, toList, etc.) and has LawfulBEq/DecidableEq?

I'm using Lean 4.25.2.

[Aaron Liu]

I don't think it is lawfulbeq

[Aaron Liu]

@loogle "hashset", "equiv"

[loogle]

:search: Std.HashSet.Equiv, Std.HashSet.Equiv.inner, and 73 more

[Aaron Liu]

Vadim Zaliva said:

I also tried Std.ExtHashSet but it is missing operations I need (e.g., fold, toList).

How do you expect to get a list out if the elements inside are unordered

[Markus Himmel]

Regarding your questions:

1. It's not provable, for the reasons you suspect.
2. Ideally you should wait until Lean 4.27.0-rc1 is released early next week. In this version, core itself adds a BEq instance for hash sets and tree sets which is more efficient than the one in batteries (it only iterates once instead of twice) and comes with LawfulBEq (ExtHashSet _) and LawfulBEq (ExtTreeSet _) out of the box.
3. Yes, docs#Std.ExtTreeSet sounds like what you want. It has docs#Std.ExtTreeSet.foldl and docs#Std.ExtTreeSet.toList. If you really prefer to use a hash set, then your best shot would be to use docs#Std.HashSet and reason about docs#Std.HashSet.Equiv instead of propositional equality.