omega, romega, lia: pick one

[maximedenes]

The redundancy between these three tactics is putting some burden on maintainers of the system. For example, #186 is much more costly to implement than it should be. I believe the situation is also confusing newcomers. I would like to understand what is the plan to resolve this redundancy, and help implement it.

Here's my understanding of the situation:

• The implementation of romega was started 17 years ago (according to its header). It is meant as a reflection-based replacement of omega but hasn't reached full compatibility. I don't know if it is the sign of serious difficulty in resolving the incompatibilities.
• romega is undocumented
• when in the compatible fragment, romega should always be preferred to omega (reflection should bring some performance improvements).
• lia has incomparable power (sometimes it can do more than (r)omega, sometimes less (that's what I thought, although the manual seems to say that it is strictly more powerful).
• the three tactics are basically not maintained externally

I believe our manpower is way too limited (compared to the size of the code base) to afford maintaining the three. Note however that lia is part of the larger micromega, for which I don't think there exists a general replacement. Not maintaing two of them doesn't necessarily mean making them disappear, but rather moving them out of the Coq repo and calling for external maintainers.

So I believe the first question that needs to be evaluated is: can lia be used as a replacement for (r)omega in practice today? I believe @RalfJung experimented it recently, maybe he can give some feedback.

If the answer is no, then maybe we should favor romega, starting with writing down all known incompatibilties that have been resisting for all those years.

@ppedrot do you know if it would be hard to rebind (r)omega to lia, so that we could see what it gives on our CI?

[Zimmi48]

I think @letouzey probably has some experience to share on this question.

[RalfJung]

I believe @RalfJung experimented it recently, maybe he can give some feedback.

You must be confusing me with someone... I don't remember ever doing experiments like that.^^

However, what I can say is that in Iris, was prefer to use lia because it is much faster than omega. I did not know about romega.

EDIT: I just replaced all sues of omega by lia in Iris itself, and everything still works.

[maximedenes]

@Zimmi48 I don't know how I forgot to cite Pierre's nickname, he's clearly the one who can answer some of the questions above. Thanks!

@RalfJung Really? I remember a discussion on gitter where somebody was impressed by the performance of lia and started using it in a development as a replacement for omega. I thought it was you in Iris. If not, maybe @Zimmi48 remembers, I believe he was part of the discussion too. But maybe that also never happened :)

[RalfJung]

I remember a discussion on gitter where somebody was impressed by the performance of lia and started using it in a development as a replacement for omega.

Well yeah Robbert told me about that when he re-wrote Iris 3 or 4 years ago. I'm using lia ever since. That was way before I joined Gitter.^^

[maximedenes]

Well yeah Robbert told me about that when he re-wrote Iris 3 or 4 years ago. I'm using lia ever since. That was way before I joined Gitter.^^

Ok, then I'm definitely confusing you with someone else, sorry about the noise! Anyway, it was useful to learn that for Iris, lia worked fine as a replacement for omega.

[Zimmi48]

Yeah the discussion on Gitter definitely happened but I don't know who took part.

[SkySkimmer]

Around https://gitter.im/coq/coq?at=5a87038e76ced47639eee0f4

Joachim Breitner @nomeata

Feb 16 17:17 My module went down from 140s to 10s. And colleagues here have been staring at even longer Qeds… Maybe omega could print a warning when it takes too long, suggesting to use lio :-)

[maximedenes]

I just discovered that some proofs in plugins/micromega/ZMicromega.v rely on omega through hints...

[JasonGross]

I recently found a case where lia is slower than omega (maybe 2s instead of 1s, though I didn't time it). I can try to recreate the case and minimize it, if that's useful?

[JasonGross]

More generally, I've yet to encounter a case in fiat-crypto where lia is less powerful than omega, but that might just be because I try omega and then lia ( and then nia and then nsatz.)

[letouzey]

Killing the legacy code of omega is indeed one of my own goals. It is indeed a burden to maintain, and you can expect major speedups and proof-term shrinks on large problems (either via romega or lia). Honestly, I've never been far in my attempts at actually doing the replacement many years ago, ending with incompatibilities and bugs of romega. So that lead me to a first step : debugging and improving romega. I was still on it last year, but I consider it done now :smiley:. I still have to document romega, but that won't take long (@maximedenes point 2). Agreed, the question of compatibility (@maximedenes point 1) is not fully solved by romega. But that's in large part because omega is quite funky in many aspects, while romega has been designed from day 1 to not mimic these funky aspects. For instance, omega is hard-wired with support for nat (and even mixed Z/nat goals), courtesy of a direct-style implementation. Meanwhile, romega is dedicated to Z, since reification of many domains is a serious pain. That's where the zify tactic comes handy to migrate your goal to Z. But I'm pretty sure there are silly corner-cases where omega works and not romega with * (shortcut for zify;omega), eg. due to the way the propositional parts are handled. I consider we should dodge the bullet here, drop 100% compatibiliy over omega, consider something like zify;romega (or zify;lia) to be the new reference, and go fixing little glitches in real proofs. Or maybe provide a better wrapper around romega or lia if we find too much practical shortcomings to address.

Now, should we go for lia or romega ? I admit lia seems more powerful, and probably slightly more efficient (I've got some benchmarks donated by Chantal Keller years ago, I will put them somewhere). But sadly it's still a black box for me (even worse, it's part of a larger set of black boxes named micromega). Ok, that's largely due to my lack of efforts in grasping this code, and moreover I'm pretty sure Frederic Besson can help understanding it. On the other hand, romega is clearly less ambitious, and share its core solver with omega. But at least I can now say I master this code pretty well, I've mostly two files to show you to describe its behavior, and I've even left quite some comments in them.

So for now I'd vote for romega, even if the actual winner will probably be the one able to replace omega without too much drama.

PS: I'm also slightly worried by the dependency order : is it that simple to build lia early, before the first omega usages ?

[eponier]

Here is one example that omega can solve, but not lia.

Require Import Psatz.
Require Import Omega.

Lemma test : forall n0 x (l:x < S n0) (H : l = l), x < S (S n0).
Proof.
  intros.
  Fail lia.
  omega.
  (* clear H. lia. works *)

I am not sure if this is a good example, since lia seems to be confused mostly by the use of a dependent type.

[maximedenes]

@eponier Indeed, this is probably the same as #7886.

[olaure01]

In the situations where I am using them, I find usually omega faster than lia but lia required in presence of max so I often use try omega ; try lia.

[eponier]

@maximedenes You're right. And I had just looked at https://github.com/coq/coq/issues/7886 when I wrote my post... At least, my example is a little simpler.

[pi8027]

omega and romega have been removed in favor of lia. Let's close.