Proving equality of Std.DHashMap

Stream: general

[Michael Sammler]

Hi, I am struggling to prove some trivial equalities on Std.DHashMap like the following:

import Std

example n (x : Std.DHashMap Nat (λ _ => Nat)) :
  (x.insert n 10).insert n 11 = x.insert n 11 := by
    sorry

Is there a way to prove this equality?

[Henrik Böving]

I think while there is indeed a way to prove this equality this is not publicly exposed in the API and you probably want to stick to extensional hashmaps

[Kim Morrison]

While agreeing with that advice, the closest trueprovable thing is

example n (x : Std.DHashMap Nat (λ _ => Nat)) :
  (x.insert n 10).insert n 11 ~m x.insert n 11 := by
    refine Equiv.of_forall_get?_eq ?_
    intro k
    rw [DHashMap.get?_insert]
    split <;> rename_i h
    · simp at h
      simp [h]
    · simp at h
      rw [DHashMap.get?_insert, DHashMap.get?_insert]
      simp [h]

Moreover, we probably should just make an insert_insert_self lemma available.

[Michael Sammler]

Thanks both of you for the quick answers! I did not know about ~m. I will look into that and extensional hashmaps.

[Markus Himmel]

To expand a bit on Henrik's message: Lean 4.20 introduces docs#Std.ExtDHashMap which has lemmas like docs#Std.ExtDHashMap.ext_get? which makes something like this easy to prove:

import Std

example n (x : Std.ExtDHashMap Nat (λ _ => Nat)) :
    (x.insert n 10).insert n 11 = x.insert n 11 := by
  refine Std.ExtDHashMap.ext_get? (fun k => ?_)
  by_cases h : k = n <;> simp_all [Std.ExtDHashMap.get?_insert]

At the moment there aren't many lemmas specific to extensional hash maps. These (including a simp lemma like insert_insert_self) will be added in future releases.