Showing `((m : Std.HashMap).map f).keys = m.keys`

Stream: Is there code for X?

[Dillon Shaffer]

I'm sorry if this is a dumb question but I'm fairly sure that it's a missing theorem in the standard library. I feel like it should be fairly simple but I'm not adept with solving techniques yet and haven't been able to crack it myself.

[Eric Wieser]

Is docs#Std.HashMap.keys defined such that the equality is actually true?

[Eric Wieser]

It looks like your equation could in principle have the LHS as a permutation of the RHS, rather than as an equality

[Dillon Shaffer]

Ha, no the equality is not defined as true but I do want it to be. A permutation would definitely work, then I would only have to figure out how to do transitive membership between an original and updated map.

[Dillon Shaffer]

If I understand, the proposition m.keys = (m.map f).keys could be the empty proposition (in which it is untrue) and to enforce truthiness I would need to write (m.keys = (m.map f).keys) = true?

apparently not xd. Now I'm assuming that the empty proposition is a bottom value that can't exist.

[Markus Himmel]

There are currently no lemmas for docs#Std.HashMap.map, but there is work in progress on this and full lemma coverage for map, filterMap and filter will (most likely) be part of Lean 4.20.0.

As Eric points out, the two lists will only be equal up to permutation:

import Std

#eval (Std.HashMap.ofList [(0, 0), (16, 0)]).keys -- [16, 0]
#eval ((Std.HashMap.ofList [(0, 0), (16, 0)]).map (fun _ v => v + 1)).keys -- [0, 16]

[Johannes Tantow]

The lemma got now merged into the master. In at most a day there should be a nightly available with the results if you need them now. Keep in mind that this nightly version might not be as stable as a release.