Lemmas for Std.HashMap.filter and Std.HashSet.filter?

Stream: new members

[aron]

There don't seem to be any lemmas about Std.HashMap.filter and Std.HashSet.filter in the stdlib. And when I try to repeatedly simp on their definitions like:

simp [HashSet.filter, HashMap.filter, DHashMap.filter, DHashMap.Internal.Raw₀.filter] at h

things get really messy and I end up with something like:

  {
    inner :=
      {
        inner :=
          ⟨{
              size :=
                (DHashMap.Internal.toListModel
                    (Array.map (DHashMap.Internal.AssocList.filter fun a x => b.contains a)
                      a.inner.inner.1.buckets)).length,
              buckets :=
                Array.map (DHashMap.Internal.AssocList.filter fun a x => b.contains a) a.inner.inner.1.buckets },
            ⋯⟩ } }

which I don't know what to do with :/

Is there a way for me to write my own lemmas about these types' filter functions in a way that's accessible to a beginner like myself?

---

For context here's the kind of thing I'd like to be able to do:

def Std.HashSet.intersection {k : Type u} [BEq k] [Hashable k] (a : HashSet k) (b : HashSet k) : HashSet k :=
  a.filter b.contains

def Std.HashSet.intersection_mem_both {k : Type u} [BEq k] [Hashable k] (a : HashSet k) (b : HashSet k) : ∀ v ∈ (a.intersection b), v ∈ a ∧ v ∈ b :=
  by sorry

[Markus Himmel]

Unfortunately, there are no lemmas for filter, filterMap and map yet (but this is on the Lean FRO's TODO list. Contributions are welcome!). For the time being, you can implement intersection using fold, for which lemmas are available:

import Std.Data.HashSet.Lemmas

import Std

def Std.HashSet.intersection {k : Type u} [BEq k] [Hashable k] (a : HashSet k) (b : HashSet k) : HashSet k :=
  a.fold (init := ∅) fun s x => if x ∈ b then s.insert x else s

theorem Std.HashSet.intersection_mem_both {k : Type u} [BEq k] [Hashable k] [EquivBEq k] [LawfulHashable k] (a : HashSet k) (b : HashSet k) : ∀ v ∈ (a.intersection b), v ∈ a ∧ v ∈ b := by
  rw [intersection]
  suffices ∀ a : List k, ∀ q : HashSet k, ∀ (v : k), v ∈ List.foldl (fun s x => if x ∈ b then s.insert x else s) q a → v ∈ q ∨ a.contains v ∧ v ∈ b by
    simpa [HashSet.fold_eq_foldl_toList] using this a.toList ∅
  intro a q
  induction a generalizing q with
  | nil => simp
  | cons hd tl ih =>
    simp
    intro v hv
    obtain (h|h) := ih _ _ hv
    · split at h
      · next ht =>
        rw [HashSet.mem_insert] at h
        obtain (h|h) := h
        · refine Or.inr ⟨Or.inl (BEq.symm h), ?_⟩
          rwa [← HashSet.mem_congr h]
        · exact Or.inl h
      · exact Or.inl h
    · exact Or.inr ⟨Or.inr h.1, h.2⟩

[Robin Arnez]

aron schrieb:

Is there a way for me to write my own lemmas about these types' filter functions in a way that's accessible to a beginner like myself?

As Markus said, lemmas currently don't exist and there is no easy way to write them without knowing the internals, however I'm planning on adding some along with developments towards extensional hash maps (hash maps with lemmas like (∀ k, m₁[k]? = m₂[k]?) → m₁ = m₂)

[aron]

@Markus Himmel thanks so much, that looks exactly like what I need! I actually initially tried to define it using fold but couldn't figure out how to prove things with that either.

Btw I can see that your code snippet works when using latest mathlib but not when using mathlib stable. I've just updated my local project to use mathlib 4.17 but it seems to be missing the Std.HashSet.fold_eq_foldl_toList lemma because I'm getting an unknown constant error. Do you by any chance know when that lemma will be included in mathlib stable?

[Markus Himmel]

The missing lemmas will be part of Lean 4.18.0, which will be released in early April. The corresponding stable version of mathlib usually appears on the same day as the Lean release.

[aron]

I've decided to install the v4.18 release candidate which does indeed have these theorems – thanks! :tada: