More complete omega

Stream: general

[Huỳnh Trần Khanh]

Is there demand for a more complete omega tactic, similar to the lia tactic in Coq? I myself need it. omega as it currently stands is incomplete, which makes it hard to predict when omega can clear the goal. In contrast, in Coq I can have a rough idea of whether lia can or cannot clear the goal.

[Huỳnh Trần Khanh]

An example is decomposing a nonnegative integer into its constituent digits. For 3 digit numbers you can make omega prove n = 100 * (n / 100) + 10 * (n / 10 % 10) + n % 10. But for 5 digit numbers omega completely fails.

[Kyle Miller]

Yes there is, and that tactic is under development (grind) :-)

There's a recent discussion (yesterday?) where Kim Morrison is explaining its capabilities.

[Kyle Miller]

I do not know its relationship to lia.

[Jihoon Hyun]

Is it for compatibility that the tactic is not being replaced but is newly created?

[Johan Commelin]

No, grind does a lot more than omega.