Zulip Chat Archive

Stream: general

Topic: omega


view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 18 2019 at 13:31):

well you just broke logic :P

view this post on Zulip Chris Hughes (Apr 18 2019 at 13:32):

I get the error here as well

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

view this post on Zulip Seul Baek (Apr 18 2019 at 14:27):

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

view this post on Zulip 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.

view this post on Zulip Seul Baek (Apr 18 2019 at 14:30):

Does it work on the unmodified branch?

view this post on Zulip Chris Hughes (Apr 18 2019 at 14:31):

Yes.

view this post on Zulip 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...

view this post on Zulip Chris Hughes (Apr 18 2019 at 14:33):

I'm not editing lean source code.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 18 2019 at 15:06):

you have piqued the computer scientists' interest!

view this post on Zulip Kevin Buzzard (Apr 18 2019 at 15:07):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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