List.pmap analogue for Std.HashMap

Stream: Is there code for X?

[Christian Merten]

Is there an analogue of docs#List.pmap for docs#Std.HashMap ?
(Related question: Why does List.pmap take (f : ∀ a, P a → β) (H : ∀ a ∈ l, P a) instead of (f : ∀ a, a ∈ l → β)?)

[Edward van de Meent]

answering your related question: i think that's because functions tend to be written with specific predicates in mind. Suppose we have the following context:

variable {A B C: Type*} (f : A -> List (Option B)) (some_lemma : ∀ a, ∀ b ∈ f a, P b)
  (foo : (b : Option B) -> P b -> C)

If you wanted to apply a map over this, you'd either write (f a).pmap foo (some_lemma a) (which is what you'd currently do), or you'd write (f a).pmap (fun b hb => foo b (some_lemma a b hb) (if it had the alternative signature you're asking about). I for one certainly prefer the first option here, and i suspect i'm not the onely one.
If you really want, you can recover the alternative version by specifying P := fun a => a ∈ l and H := id.

[Christian Merten]

I am aware of the workaround, my point is that I mostly run into the second case and having to specify P and H manually is annoying. List.pmap in the current version combines two unrelated operations in one function, while my proposed version does precisely one thing. So I would prefer to see (f a).pmap (fun b hb => foo b (some_lemma a b hb) although it is longer.

[Robin Arnez]

I honestly don't like that though because then you get stuff like:

α : Type u_1
l : List (Option α)
h : ∀ x ∈ l, x ≠ none
⊢ List.pmap (fun x h' => x.get ⋯) l ⋯ = List.pmap (fun x h' => x.get ⋯) l ⋯

which can't be solved by rfl.

[Robin Arnez]

For reference:

example (l : List (Option α)) (h : ∀ x ∈ l, x ≠ none) :
    l.pmap (fun x h' => x.get (Option.isSome_iff_ne_none.mpr h')) (fun a => h a) =
      l.pmap (fun x h' => x.get (Option.isSome_iff_ne_none.mpr (h _ h'))) (fun _ h => h) := by
  rfl