List.Sigma definitions for mapping keys and values

Stream: mathlib4

[Chris Henson]

There are a few theorems in List.Sigma about mapping keys and values (docs#List.dlookup_map, docs#List.dlookup_map₁, and docs#List.dlookup_map₂), but not any API around this idea. Would adding definitions like these make sense?

import Mathlib

variable {α : Type u} {α' : Type u'} [DecidableEq α] [DecidableEq α']

namespace List

@[grind =]
def map₁₂ (f : α → α') (g : (a : α) → β a → β' (f a))
    (l : List (Sigma β)) : List (Sigma β') :=
  l.map (fun ⟨a, b⟩ => ⟨f a, g a b⟩)

@[grind =]
def map₁ (f : α → α') (l : List (Σ _ : α, β)) : List (Σ _ : α', β) :=
  l.map (fun ⟨a, b⟩ => ⟨f a, b⟩)

@[grind =]
def map₂ {β β' : α → Type*} (f : (a : α) → β a → β' a) (l : List (Σ a, β a)) :
    List (Σ a, β' a) :=
  l.map (fun ⟨a, b⟩ => ⟨a, f a b⟩)

theorem dlookup_map₁₂ {β : α → Type v} {β' : α' → Type v'} (l : List (Sigma β)) {f : α → α'}
    (hf : Function.Injective f) (g : ∀ a, β a → β' (f a)) (a : α) :
    (l.map₁₂ f g).dlookup (f a) = (l.dlookup a).map (g a) := dlookup_map l hf g a

theorem dlookup_map₁' {β : Type v} (l : List (Σ _ : α, β))
    {f : α → α'} (hf : Function.Injective f) (a : α) :
    (l.map₁ f).dlookup (f a) = l.dlookup a := dlookup_map₁ l hf a

theorem dlookup_map₂' {γ δ : α → Type*} {l : List (Σ a, γ a)} {f : ∀ a, γ a → δ a} (a : α) :
    (l.map₂ f).dlookup a = (l.dlookup a).map (f a) := dlookup_map₂ a

-- I don't think this is in Mathlib?
theorem NodupKeys_map₁ (f : α → α') (hf : Function.Injective f) {l : List (Σ _ : α, β)}
    (nd : l.NodupKeys) : (l.map₁ f).NodupKeys := by
  induction l with
  | nil => grind [nodupKeys_nil]
  | cons hd tl =>
    have := dlookup_map₁ tl hf hd.fst
    grind [dlookup_isSome, → notMem_keys_of_nodupKeys_cons, nodupKeys_of_nodupKeys_cons,
      nodupKeys_cons]

omit [DecidableEq α] in
theorem map₂_keys {β β' : α → Type*} (f : (a : α) → β a → β' a) (l : List (Σ a, β a)) :
    (l.map₂ f).keys = l.keys := by
  induction l <;> grind [keys_nil, keys_cons]

omit [DecidableEq α] in
theorem NodupKeys_map₂ {β β' : α → Type*} (f : (a : α) → β a → β' a) (l : List (Σ a, β a))
    (nd : l.NodupKeys) : (l.map₂ f).NodupKeys :=
  by simp_all only [NodupKeys, map₂_keys]

I wasn't sure about the naming so I just mirrored those theorems, but I also considered map_key_val, map_key, and map_val

[Kenny Lau]

more api is better

[Aaron Liu]

what about docs#List.TProd I wanna see it get more love

[Aaron Liu]

since I'm using it

[Aaron Liu]

especially for when the list doesn't not have duplicates

[Christian Merten]

The first three are l.map (Sigma.map f g), l.map (Sigma.map f fun _ ↦ id) and l.map (Sigma.map id f) respectively. I don't think we need separate definitions for these.

[Chris Henson]

Christian Merten said:

The first three are l.map (Sigma.map f g), l.map (Sigma.map f fun _ ↦ id) and l.map (Sigma.map id f) respectively. I don't think we need separate definitions for these.

Hmm, this seems mostly fine. Should these be the spellings that these theorems all use? My only hesitation is the second is slightly awkward to write as it seems you have to give type annotations, e.g.

import Mathlib

variable {α : Type u} {α' : Type u'} [DecidableEq α] [DecidableEq α']

theorem List.dlookup_map₁' {β : Type v} (l : List (Σ _ : α, β))
    {f : α → α'} (hf : Function.Injective f) (a : α) :
    (l.map (.map f fun _ => id) : List (Σ _ : α', β)).dlookup (f a) = l.dlookup a :=
  dlookup_map₁ l hf a

is there a way to avoid that?

[Chris Henson]

Given the advice (that I think I agree with) to not add those additional definitions, I have gone ahead and pushed the remaining theorems to my existing PR: #30313