omega

Stream: general

[Chris Hughes]

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]

well you just broke logic :P

[Chris Hughes]

I get the error here as well

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

[Seul Baek]

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

[Chris Hughes]

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

[Seul Baek]

Does it work on the unmodified branch?

[Chris Hughes]

Yes.

[Rob Lewis]

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

[Chris Hughes]

I'm not editing lean source code.

[Rob Lewis]

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]

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]

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

[Kevin Buzzard]

you have piqued the computer scientists' interest!

[Kevin Buzzard]

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

[Chris Hughes]

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

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

[Seul Baek]

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]

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

[Kevin Buzzard]

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]

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]

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]

@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]

@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]

I think this will be addressed by #1748.