## Stream: general

### Topic: omega

#### Chris Hughes (Apr 18 2019 at 13:20):

Is this the correct use of omega?

import tactic.omega

example : ∀ (a b : ℕ), a + b = 1 → (a = 0 ∧ b = 1) ∨ (a = 1 ∧ b = 0) :=
by omega -- 'unreachable' code was reached


#### Kenny Lau (Apr 18 2019 at 13:31):

well you just broke logic :P

#### Chris Hughes (Apr 18 2019 at 13:32):

I get the error here as well

example : ∀ (a : ℕ), a = a :=
by omega


#### Seul Baek (Apr 18 2019 at 14:27):

Probably some error in equality elimination. I'll look into it.

#### Chris Hughes (Apr 18 2019 at 14:29):

It's a problem on my end. I'm on a branch of mathlib which I modified.

#### Seul Baek (Apr 18 2019 at 14:30):

Does it work on the unmodified branch?

Yes.

#### Rob Lewis (Apr 18 2019 at 14:32):

"unreachable code was reached" is a bad sign no matter what, unless you're modifying Lean source code...

#### Chris Hughes (Apr 18 2019 at 14:33):

I'm not editing lean source code.

#### Rob Lewis (Apr 18 2019 at 14:37):

If you feel like digging deep, you could compile Lean in debug mode and see if there's an assertion violation that leads to this.

#### Seul Baek (Apr 18 2019 at 14:40):

Not quite sure what could be causing this; I've never encountered this error when using omega. But both examples are definitely correct usage

#### Chris Hughes (Apr 18 2019 at 14:41):

Okay, I restarted Lean, and it all works on my modified branch. Probably no need to worry.

#### Kevin Buzzard (Apr 18 2019 at 15:06):

you have piqued the computer scientists' interest!

#### Kevin Buzzard (Apr 18 2019 at 15:07):

Can you please try very hard to reproduce so they can debug properly? :-)

#### Chris Hughes (Apr 18 2019 at 15:08):

Is this a Presburger formula? omega doesn't solve it

example : ∃ (a : ℕ), a = 0 := by omega -- failed


#### Seul Baek (Apr 18 2019 at 15:19):

The formula is in Presburger arithmetic, but not in the quantifier-free (i.e., purely universally quantified) fragment of Presburger arithmetic, which is what omegaworks with

#### Seul Baek (Apr 18 2019 at 15:22):

cooper would solve it since it handles quantifiers in any combination, but would be much slower overall

#### Kevin Buzzard (Apr 18 2019 at 16:05):

Out of interest, where are the limitations here? example : ∃ (a b c : ℕ), a ^ 3 = b ^ 3 + c ^ 3 + 42 is presumably not within the realm of cooper -- it is an open question in pure mathematics in fact, although it is believed that such integers exist.

#### Kevin Buzzard (Apr 18 2019 at 16:18):

Oh -- I remember now -- Presburger arithmetic can't do squaring or cubing of variables can it. It can only do multiplication by a numerical constant (and that's by cheating -- repeated addition)

#### Mario Carneiro (Apr 18 2019 at 17:36):

that's the intuitive justification, but most algorithms I know for presburger explicitly represent multiplication by constants (and divisibility by constants in the case of cooper)

#### Jasmin Blanchette (Feb 19 2020 at 12:30):

@Seul Baek , all -- I have encountered a strange bug with omega. I'm showing one successful example below and one where I get some low-level error message about s. Observe that the second example is an instance of the first example.

example (n m n₀ m₀ : ℕ) (hnm : m + n = n₀ + m₀)
(hn : ¬ n = 0) :
m + (1 + (n - 1)) = m + n :=
by omega  -- succeeds

example (n₀ m₀ : ℕ) (s : string → ℕ) (hnm : s "m" + s "n" = n₀ + m₀)
(hn : ¬ s "n" = 0) :
s "m" + (1 + (s "n" - 1)) = s "m" + s "n" :=
by omega  -- fails


It's a pity, because it prevents me from using "omega" in my MSc-level course.

#### Johan Commelin (Feb 19 2020 at 14:51):

@Jasmin Blanchette I think there has been some effort to get omega into a usable state in mathlib. But it seems to be a non-trivial effort.

#### Floris van Doorn (Feb 19 2020 at 17:09):

I think this will be addressed by #1748.

Last updated: May 06 2021 at 21:09 UTC