Tactic wishlist: Omega

Stream: metaprogramming / tactics

[Sam Ezeh]

The tactic wishlist has an entry that says "boost omega into a full decision procedure for Presburger arithmetic". What's the difference between what omega does now and what we want it to do?

My current understanding is that omega works in the quantifier free fragment of presburger arithmetic so can't deal with statements with arbitrary quantifiers and the task is now to add quantifier-elimination to omega using, for example, Cooper's algorithm? Is this correct?

Is anybody working on this? This is something I'd like to help out with if it's something that needs doing.

[Kim Morrison]

We're hoping to replace omega's implementation over the next 6-12 months or so with something tightly integrated with a new automation framework in Lean. No details yet, but I'd suggest this isn't the best thing to work on right now unless there is an urgent need for some project.