feat: OrderedAssocList

[kim-em]

Ordered wrapper around AssocList, and basic functions find?, insert?, filterMapVal, and merge. An extensionality lemma (∀ a, l₁.find? a = l₂.find? a) → l₁ = l₂.

I will later use this to implement sparse coefficients in omega.

[joehendrix]

I'm assuming this is useful for kernel execution efficiency. Is that the case? Could you test performance against RBMap?

[kim-em]

I'm assuming this is useful for kernel execution efficiency. Is that the case? Could you test performance against RBMap?

No, actually, there's no need to run any of this in the kernel. I want this because I think it will be easier to write the theorems about algebraic operations on finitely supported functions Nat \to Int that I need in this representation than in RBMap.

[digama0]

In that case I'm a bit dubious of adding a new data structure like this to std, since it has neither good kernel performance nor good runtime performance, and we already have other ways to write finitely supported functions for proving purposes.

[kim-em]

Hmm, okay. I will see how proofs go on top of RBMap + a wrapper asserting there are no zero values.

[kim-em]

Currently RBMap.mergeWith is O(n₂ * log (n₁ + n₂)), whereas the merge here is O(n₁ + n₂). (I hope. :-)

[digama0]

Hmm, okay. I will see how proofs go on top of RBMap + a wrapper asserting there are no zero values.

What are you trying to do more specifically? Why do you need proofs in this case? If this is an omega data structure I would expect proofs to not be necessary.

Currently RBMap.mergeWith is O(n₂ * log (n₁ + n₂)), whereas the merge here is O(n₁ + n₂). (I hope. :-)

Wikipedia describes a better algorithm for RBMap merge with complexity O(n₂ * log (n₁ / n₂ + 1)), which is strictly better than O(n₁ + n₂) (it wins mainly in the unbalanced case). The implementation here is a bit lazy, but with some proof work I think it wouldn't be too bad to implement the more efficient algorithm.

[kim-em]

Hmm, okay. I will see how proofs go on top of RBMap + a wrapper asserting there are no zero values.

What are you trying to do more specifically? Why do you need proofs in this case? If this is an omega data structure I would expect proofs to not be necessary.

This is very slightly inaccurate (because of subsequent laziness taking some shortcuts), but the functions and theorems I need on the representation of coefficients are given in https://github.com/leanprover/std4/blob/main/Std/Tactic/Omega/Coeffs/IntList.lean

Currently all these functions are implemented on List Int, i.e. a dense representation of coefficients, only trimming trailing zeros as needed to make the theorems true!

As you can see the intention is that I should be able to swap out any representation satisfying that API.

This is not particularly urgent, as right now now one is actually calling omega with more than ~10 variables... But Leo assures me that that someone will want to eventually.

[digama0]

So why not just use AssocList there? Or Array (Nat x Int) for that matter.

[kim-em]

So why not just use AssocList there? Or Array (Nat x Int) for that matter.

Because then the merge operation (which is actually run, not just proved about) is O(n1 * n2), and I wanted to avoid that.

[digama0]

So why not just use AssocList there? Or Array (Nat x Int) for that matter.

Because then the merge operation (which is actually run, not just proved about) is O(n1 * n2), and I wanted to avoid that.

I mean, you can still implement a O(n1 + n2) merge operation on AssocList which works provided the inputs are sorted. That is, you are working with ordered AssocLists, just not as a distinct type.

[kim-em]

So why not just use AssocList there? Or Array (Nat x Int) for that matter.

Because then the merge operation (which is actually run, not just proved about) is O(n1 * n2), and I wanted to avoid that.

I mean, you can still implement a O(n1 + n2) merge operation on AssocList which works provided the inputs are sorted. That is, you are working with ordered AssocLists, just not as a distinct type.

That's what this PR does! AssocList.orderedMerge. It seems really cumbersome to then state all the theorems about it (e.g. how it relates to find?, associativity, etc) if you forbid yourself from mentioning the bundled type that wraps up the witness of ordered-ness.

[digama0]

Is it? I would expect it to just be a simple predicate, e.g.

theorem orderedMerge_ordered : Ordered l1 -> Ordered l2 -> Ordered (l1.orderedMerge l2) := ...

Actually it might not even be Ordered, it could be Pairwise R or something, at least for the low level primitive. You can therefore manipulate the ordered-ness independently of the list itself, and this features quite prominently in sorting functions for lists, for example, so I don't think it's a particularly bad design.

[kim-em]

Is it?

I've started refactoring, and agree this is better. Thanks for talking me around. :-)

[fgdorais]

I think all my concerns have been addressed. Just one additional remark: the design of AssocList so far is that defs are specced using toList, correctness and other lemmas are then proved using the toList translation and the List library. I think this makes good sense and should be considered in the revisions.

[kim-em]

the design of AssocList so far is that defs are specced using toList, correctness and other lemmas are then proved using the toList translation and the List library.

This is still WIP, I will probably eventually remove the bundled OrderedAssocList entirely when I get back to this PR.

However, I am not intending to use toList for specification: the great property of an ordered assoc list is that find? suffices for specifications, and this is intentionally different from what we have to do for AssocList.