ExtTreeMap - Filter / MergeWith

Stream: mathlib4

[František Silváši 🦉]

Can anyone please recommend an approach to proving properties about Std.ExtTreeMap.filter and Std.ExtTreeMap.mergeWith - the proofs that already exist regarding Std.ExtTreeMap use some exceedingly convoluted custom machinery.

For example, something as simple as the analogue of Std.ExtHashMap.getElem?_filter.

I am happy to do the legwork, but I would appreciate some general guidance.

In a broader context, we are reasonably close to finishing 'some' version of computable polynomials in Lean - in particular, we have an equivalence between an ExtTreeMap-based polynomial with computable operations and Mathlib.MvPolynomial and we are midway towards a full RingEquiv.

Please note that this is all very much WIP and in no way polished for any 'public' consumption.

[Johannes Tantow]

It seems that noone has proved anything about filter for treemaps yet, so you will have to do this from the basics. The general process for HashMaps is described here: https://github.com/leanprover/lean4/blob/0071bea64eb57afff8339f22ec71944080246e7b/src/Std/Data/DHashMap/Internal/Defs.lean and TreeMaps are kind of similar. So you would prove something on the list model (which might already exists since the list model is the same for Hash and tree maps and filter is verified for hashmaps). Afterwards you use the simp_to_model tactic with your list lemma. The last steps are usually just copying the name of the lemma and the statement to the next level of the hierarchy.

[Johannes Tantow]

This is the filter PR for Hashmaps https://github.com/leanprover/lean4/pull/7400

[František Silváši 🦉]

Thank you kindly for the pointers.

[Johannes Tantow]

Are treemaps critical for your application? With Hashmaps you would already have the filter operation verified and union should be easy to verify as well, since it is based on fold and insert which are already verified. You wouldnt need the framework then.

[František Silváši 🦉]

Well, ExtTreeMap had mergeWith and keys whereas ExtHashMap didn't (IIRC), so in general the reasoning didn't go beyond: the former has all the operations I needed, and I sort of... assumed? that it would have some statements pertaining thereto.

The order is not critical at all, as a matter of fact, I think performance-wise, I'd rather have the constant amortised access, they won't see many inserts regardless.

The broader context is computable polynomials, the even broader context is finite field decision procedure bridge to CVC5.

This is an interesting direction to explore - the keys might be slightly annoying because (obviously) hash maps are unordered, but I technically don't care because the sums in polynomials commute. I'll investigate this, I think it should be reasonably straightforward to port to ExtHashMap modulo not sure how annoying the keys will be.

[František Silváši 🦉]

Thank you for your valuable insights! :)

[Johannes Tantow]

keys wont be possible for ExtHashMap as this not the same list for equivalent hashmaps. The stuff about union I said above is also not completely correct, as foldl is for the same reason only available on hashmap and not exthashmap

[Markus Himmel]

FWIW, here is the proof of one of the lemmas you requested in the original message, just to demonstrate the principle that Johannes described:

import Std.Data.ExtTreeMap.Lemmas

variable {α : Type u} {β : Type v}

namespace Std

attribute [local instance low] beqOfOrd

theorem DTreeMap.Internal.Impl.Const.get?_filter [Ord α] [TransOrd α]
    (m : DTreeMap.Internal.Impl α (fun _ => β)) (h : m.WF) (f : α → β → Bool) (k : α) :
    Const.get? (m.filter f h.balanced).1 k = (Const.get? m k).pfilter (fun v h' => f (m.getKey k ((contains_eq_isSome_get? h).trans (Option.isSome_of_eq_some h'))) v) := by
  -- This manual proof is usually done by the `simp_to_model` tactic
  simp only [Const.get?_eq_getValue? h.filter.ordered, toListModel_filter,
    Const.get?_eq_getValue? h.ordered, getKey_eq_getKey h.ordered]
  apply Std.Internal.List.Const.getValue?_filter
  apply h.ordered.distinctKeys

theorem DTreeMap.get?_filter {cmp : α → α → Ordering} [TransCmp cmp]
    (m : DTreeMap α (fun _ => β) cmp) (f : α → β → Bool) (k : α) :
    Const.get? (m.filter f) k = (Const.get? m k).pfilter (fun v h' => f (m.getKey k (Const.contains_eq_isSome_get?.trans (Option.isSome_of_eq_some h'))) v) :=
  letI : Ord α := ⟨cmp⟩
  DTreeMap.Internal.Impl.Const.get?_filter m.inner m.wf _ _

theorem ExtDTreeMap.get?_filter {cmp : α → α → Ordering} [TransCmp cmp]
    (m : ExtDTreeMap α (fun _ => β) cmp) (f : α → β → Bool) (k : α) :
    Const.get? (m.filter f) k = (Const.get? m k).pfilter (fun v h' => f (m.getKey k (Const.contains_eq_isSome_get?.trans (Option.isSome_of_eq_some h'))) v) :=
  m.inductionOn fun _ => DTreeMap.get?_filter _ _ _

theorem ExtTreeMap.getElem?_filter {cmp : α → α → Ordering} [TransCmp cmp]
    (m : ExtTreeMap α β cmp) (f : α → β → Bool) (k : α) :
    (m.filter f)[k]? = m[k]?.pfilter (fun v h' => f (m.getKey k (contains_eq_isSome_getElem?.trans (Option.isSome_of_eq_some h'))) v) :=
  ExtDTreeMap.get?_filter m.inner f k

end Std

[František Silváši 🦉]

Well ok this is far beyond 'enough' for me to do the rest; I appreciate this and will make sure to PR all the other ones to ExtTreeMap.

[František Silváši 🦉]

Especially the simp_to_model sugar seemed a little too arcane, but this is perfectly reasonable now :).

[Markus Himmel]

I'll concede that the machinery is somewhat elaborate, but as there are literally thousands of lemmas that we have proved and many more that still have to be proved, it makes sense to optimize the process.

[František Silváši 🦉]

Oh that's prefectly understandable, I am all for abusing any and all automation - it miiight be missing a docstring if only to appear less daunting, because honestly I had no idea what kind of rabbit hole I would be getting myself into if I had decided to take an in-depth look.

[Markus Himmel]

By the way, you might want to talk to @Kim Morrison, who is working on something similar at https://github.com/kim-em/sparse-polynomial

[Kim Morrison]

Happy to be made redundant on that front, although I do like the fact that my development starts to provide an implementation of finitely supported functions along the way.

[František Silváši 🦉]

@Markus Himmel MergeWith lemmas are now proven pending some cleanups, props to @Vladislav Isenbaev and apparently some AI???? :) I think they have a report on this coming up in a week or two.

I'll make some time next week to make this Batteries-worthy. The computable polynomial is finished as well.

[Robin Arnez]

FYI, we have lemmas for filter, map and filterMap in latest nightly now; mergeWith still need verification though