Lemmas about HashSets

Stream: Is there code for X?

[Johannes Tantow]

Are there any lemmas about HashSets ? I wrote some verified algorithm using Finsets in Lean and managed to show its correctness. Unfortunately, this is really slow so I replaced it with the HashSets defined in Lean, which helps a lot, but now the proof no longer works.

I tried proving it myself but it seems difficult. Did anyone ever work on this before ? I am mainly interested in the correctness of the insertion under LawfulBEq so something like:

∀ (b': B), ((S.insert b).contains b' ↔ S.contains b' ∨ b == b')

[Kim Morrison]

There is a second implementation of HashSet/HashMap in Std, which has quite a few proofs. The HashSet in the Lean repository is mainly intended for implementation of the compiler, and has little proved about it.

[Johannes Tantow]

I guess I best define then a hashSet as abbrev HashSet (A: Type) := Std.HashMap A Unit and try from there. Thank you.

[Kim Morrison]

(deleted)

[Kim Morrison]

Depending on how your verified algorithm works, note that HashMap (either Std's or Lean's) is (edit:) not suitable for kernel computation. If you need that, then you want RBMap or AssocList instead.

[Johannes Tantow]

Sorry, but I don't know what you mean by kernel computation. I mainly want a faster variant compared to Finsets, which HashSets fulfilled and replace the lemmas about insertion to Finset by lemmas for my new data structure.The requirements are rather simple: I traverse something and insert into the set where I already way.

[Gareth Ma]

Scott Morrison said:

Depending on how your verified algorithm works, note that HashMap (either Std's or Lean's) is suitable for kernel computation. If you need that, then you want RBMap or AssocList instead.

Are you missing a "not" somewhere, or am I misreading haha

[Kim Morrison]

@Johannes Tantow, where will you be running your code? Unfortunately "faster" depends on whether it is running in native code (i.e. under reduceBool), interpreted code (i.e. most tactics), or in the kernel (if you are asking the kernel to give you a rfl proof that f x = y).

[Johannes Tantow]

I want to use it in an compiled program by lake. I guess that is native code ?