RBSet functions

Stream: std4

[Scott Morrison]

Could we also have

/-- `s.filter p` returns the subset of the set `s` satisfying the predicate `p`. -/
def filter (self : RBSet α cmp) (p : α → Bool) : RBSet α cmp := ...

/-- `sdiff s t` returns the set of elements that are in `s` but not in `t`. -/
def sdiff (s t : RBSet α cmp) : RBSet α cmp := ...

in Std?

[Scott Morrison]

And a few more requests:

namespace Std.RBMap

def keys (m : RBMap α β cmp) : List α :=
m.foldr (fun k _ ks => k :: ks) []

def values (m : RBMap α β cmp) : List β :=
m.foldr (fun _ v vs => v :: vs) []

def mergeWith (f : α → β → β → β) (self other : RBMap α β cmp) : RBMap α β cmp :=
  sorry

def mapVal (self : RBMap α β cmp) (f : β → γ) : RBMap α γ cmp :=
  sorry

instance [DecidableEq β] : DecidableEq (RBMap α β cmp) := sorry

[Mario Carneiro]

That DecidableEq instance does not say what you want it to

[Mario Carneiro]

We could have a BEq instance but it definitely won't be lawful

[Scott Morrison]

Let me #xy regarding the DecidableEq!

In mathlib3's linarith, we define monom := rb_map ℕ ℕ and then sum := rb_map monom ℤ.

I want to replace these with Monom := RBMap ℕ ℕ Ord.compare and Sum := RBMap Monom ℤ Ord.compare, but for this to work I need an instance of Ord (RBMap ℕ ℕ Ord.compare).

[Mario Carneiro]

what does Ord mean there?

[Mario Carneiro]

@Scott Morrison Okay, I implemented everything on the list, except for the DecidableEq instance (I implemented a BEq instance instead)

[Scott Morrison]

Ord

[Scott Morrison]

I just need the function RBMap ℕ ℕ cmp → RBMap ℕ ℕ cmp → Ordering (where cmp : ℕ → ℕ → Ordering is the obvious one).

[Scott Morrison]

The keys and values implementations are nice!

[Scott Morrison]

Could we also have

namespace Std.HashMap

variable [BEq α] [Hashable α]

def keys (m : HashMap α β) : List α :=
m.fold (fun ks k _ => k :: ks) []

def values (m : HashMap α β) : List β :=
m.fold (fun vs _ v => v :: vs) []

def consVal (self : HashMap α (List β)) (a : α) (b : β) :=
match self.find? a with
| none => self.insert a [b]
| some L => self.insert a (b::L)

end Std.HashMap

I'm happy to do consVal locally if you don't want it. Lean3 core had rb_lmap with a bit of API around this.

[Mario Carneiro]

Oh, RBMap should totally be using Ord instead of having a cmp in the type as it is currently. I don't think we want to encourage nonstandard Ord implementations, at least outside the implementation itself - people should typedef either the key type or the map type to supply a nonstandard Ord implementation

[Mario Carneiro]

I'll take a look at consVal tomorrow. For multimaps, it's a tough call whether it is better to use List or Array in the values. @Leonardo de Moura made some observations yesterday about how it's a performance pitfall to use HashMap K (Array V) because you have to be careful to use the thing linearly, but maybe it's fine if we make an API around this? Assuming we do ensure linear usage, is it a performance issue to be making arrays of size ~8 all the time if the median number of uses is 1 or 2? Just spitballing based on my guesses about typical multimap usage patterns.

[Tomas Skrivan]

Speaking of Ord. Is there Lawful version of Ord in std or in main Lean? I could not find it.

[Mario Carneiro]

What does lawful mean though? For RBSet, we need the comparator function to be lawful in the sense of docs4#TransCmp, which would be spelled TransCmp compare if used as a prop mixin on Ord

[Tomas Skrivan]

Lawful Ord for linear ordering would mean that it can decide Eq and LT.