Filter keys of a Finmap?

Stream: general

[Qiancheng Fu]

Using Mathlib4, is there a good way to filter the entries of Finmap? I also want to prove that the result of the filtered map is equal to another maps under certain choice of predicate....

Basically something like the following:

M : Finmap fun (x : Nat) -> Nat

M.filter (fun x => 0 <= x) = M

I tried getting the underlying list of map M, performing the filter then turning it back into a finmap. However, I don't know how to prove anything after doing so......

[Kenny Lau]

@Qiancheng Fu I tried to make it but there's a sorry that I'm stuck on, but this should be what you need:

import Mathlib

set_option diagnostics true
def Finmap.filter {α : Type*} {β : α → Type*} (f : Finmap β)
    (p : α → Prop) [DecidablePred p] : Finmap β where
  entries := f.entries.filter (fun xy => p xy.1)
  nodupKeys := sorry

theorem foo (M : Finmap fun (x : Nat) ↦ Nat) : M.filter (fun x => 0 ≤ x) = M := by
  apply Finmap.ext
  rw [Finmap.filter, Multiset.filter_eq_self]
  · intros; exact Nat.zero_le _

[Qiancheng Fu]

Thanks! Unfortunately, the real thing that I want to be able to prove is a bit more complicated....

def Finmap.filter {α : Type*} {β : α → Type*} (f : Finmap β)
    (p : Sigma β → Prop) [DecidablePred p] : Finmap β where
  entries := f.entries.filter p
  nodupKeys := sorry

def Finmap.lookup_filter {α : Type*} {β : α → Type*}  [DecidableEq α]
    (f : Finmap β) (p : Sigma β → Prop) [DecidablePred p] {l b}  :
    f.lookup l = some b -> p ⟨l, b⟩ -> (Finmap.filter f p).lookup l = b := by
  sorry

Basically I want to say that if some entry exists that satisfies a predicate p, then this entry is still present after filtering using p.

The quotient around the underlying lists is frying my brain.....

[Kenny Lau]

@Qiancheng Fu there's no need to use underlying quotients (or underlying anything) if you have what we call an "API"

import Mathlib

def Finmap.filter {α : Type*} {β : α → Type*} (f : Finmap β)
    (p : Sigma β → Prop) [DecidablePred p] : Finmap β where
  entries := f.entries.filter p
  nodupKeys := sorry

def Finmap.lookup_filter {α : Type*} {β : α → Type*}  [DecidableEq α]
    (f : Finmap β) (p : Sigma β → Prop) [DecidablePred p] {l : α} {b : β l}
    (h1 : f.lookup l = some b) (h2 : p ⟨l, b⟩) : (Finmap.filter f p).lookup l = b :=
  lookup_eq_some_iff.2 <| Multiset.mem_filter_of_mem (lookup_eq_some_iff.1 h1) h2

[Kenny Lau]

the philosophy here is that the "API" is the set of defining and characteristic properties where everything else can be derived from

[Qiancheng Fu]

Thank you so much! I'm gonna try to digest your answer. I find it quite hard to prove stuff when there's things that the api doesnt expose directly (i.e. filter).

[Kenny Lau]

@Qiancheng Fu this is the API of Multiset.filter: @loogle Multiset.filter

[loogle]

:search: Multiset.filter, Multiset.Nodup.filter, and 76 more

[Robin Arnez]

Just going to note that Std.ExtDHashMap is a good alternative that has filter:

example {α : Type*} {β : α → Type*} [DecidableEq α] [Hashable α]
    (f : Std.ExtDHashMap α β) (p : (a : α) → β a → Bool) {l : α} {b : β l}
    (h1 : f.get? l = some b) (h2 : p l b) : (f.filter p).get? l = some b := by
  simp_all

[Robin Arnez]

Oh and

example (M : Std.ExtHashMap Nat Nat) : M.filter (fun x _ => 0 <= x) = M := by
  ext; simp [Std.ExtHashMap.getElem?_filter]

[Qiancheng Fu]

@Robin Arnez That’s pretty slick. Exactly what I was looking for in a finite map data structure.