Chris Hughes (Apr 18 2019 at 13:20):
Is this the correct use of
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?
Chris Hughes (Apr 18 2019 at 14:31):
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
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