Map typeclasses outside of mathlib

Stream: Is there code for X?

[Markus de Medeiros]

Apologies if this has been answered but I couldn't find it. Are there any typeclasses for things which behave like maps outside of mathlib? I want some way to specify that a type with eg. an Insert instance (like in Init/Core.lean) is well-behaved--I could write it myself, but I'm wondering if somebody already has.

[Aaron Liu]

What do you mean "behave like map"?

[Markus de Medeiros]

Like, it should have a typeclass for an insert and get operation, and if I insert and then get at a key it will give me the same value

[Markus de Medeiros]

There are a few ways I could think to specify this, but it just seems like the kind of thing someone might have already done.

[Kenny Lau]

but you can't do that for multisets, sets, or finsets

[Kenny Lau]

basically only works for List

[Markus de Medeiros]

To be clear, I meant "map" as in "key value store". Sorry, I was unclear with my terminology.

[Robin Arnez]

do you mean HashMap, TreeMap, RBMap, etc.? In that case, why do you want to a type class and not just use a specific type?

[Markus de Medeiros]

Because I'm writing a library with proofs that apply to all three of those (and more)

[Robin Arnez]

In that case, yeah you'd probably need to write something yourself (I'm not even certain this is in mathlib in any form)

[Robin Arnez]

Although maybe some of the lemmas are worth upstreaming to core?

[Robin Arnez]

Something like this?

class MapLike (α : Type u) (β : outParam (Type v)) (γ : outParam (β → Type w)) extends EmptyCollection α, Insert ((a : β) × γ a) α where
  get? : α → (a : β) → Option (γ a)
  get?_empty (a : β) : get? ∅ a = none
  get?_insert_self (as : α) (k : β) (v : γ k) : get? (insert ⟨k, v⟩ as) k = v
  get?_insert_of_ne (as : α) (k k' : β) (v : γ k) (h : k ≠ k') : get? (insert ⟨k, v⟩ as) k' = get? as k'

[Yaël Dillies]

You might be interested in LeanColls