A simple result that `omega` fails to prove

Stream: metaprogramming / tactics

[Geoffrey Irving]

import Mathlib.Data.Nat.Order.Basic

-- A true lemma
lemma right {t i : ℕ} (t0 : t ≠ 0) (h : i < 64) : i + t - 64 < t := by
  simp only [add_comm _ t, ←tsub_tsub_eq_add_tsub_of_le h.le, imp_false, not_le]
  apply Nat.sub_lt (Nat.pos_of_ne_zero t0) (Nat.sub_pos_of_lt h)

-- `omega` fails to prove it
lemma wrong {t i : ℕ} (t0 : t ≠ 0) (h : i < 64) : i + t - 64 < t := by omega

Result:

omega did not find a contradiction:
[1, 0, 0] ∈ (-∞, 63]
[1] ∈ [0, 63]

This happened to be the first thing I tried omega on. :)

[Geoffrey Irving]

Is omega missing that 0 < t?

[Geoffrey Irving]

Ah, possibly it thinks it can cancel the ts from both sides, which doesn't work since the subtraction saturates at 0.

[Geoffrey Irving]

I should say, I've since tried on a lot of other cases, and it's extremely useful! :heart:

[Kevin Buzzard]

What happens if you explicitly add 0 < t to the local context?

[Geoffrey Irving]

^ Then it works.

[Kevin Buzzard]

Maybe open an issue then? I think Scott is on holiday for a while.

[Geoffrey Irving]

https://github.com/leanprover/std4/issues/482

[Mirek Olšák]

Ideally, one would expect a tactic that can deal with non-equalities / proving equality. So for example it could prove

example (a : ℤ) : 3*a > 4 → 3*a ≤ 11 → a ≠ 2 → a = 3

only that it goes beyond simple linear programming, rather something on top of that to case split a ≠ 2 as a < 2 ∨ a > 2 which goes towards SMT-solving (extension of SAT solving). It should be doable but it is not trivial.

[Damiano Testa]

This is not related to the issue just mentioned, but it seems that omega may not be ignoring mdata correctly:

import Mathlib.Tactic

example : 0 = 0 := by
  have : 0 = 0 := by omega -- works
  omega -- fails

[Eric Rodriguez]

is there any way to clear all mdata in the context? I've had many, many omega failures and maybe this is the root issue

[Damiano Testa]

It should be easy to write a clear_mdata tactic, but I think that it would be somewhat a hack, since mdata stores information that is actually useful for something.

[Eric Rodriguez]

it'd be useful for debugging at least!

[Mario Carneiro]

Eric Rodriguez said:

is there any way to clear all mdata in the context? I've had many, many omega failures and maybe this is the root issue

Please report these as issues so we can track and fix them

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/.60omega.60.20did.20not.20find.20a.20contradiction/near/410345497

my whinging is here, will open the Std issues in a sec

[Mirek Olšák]

Oh, I realized that omega can deal with (a < 2 or a > 2), so the only trick is to replace non-equality with disjunction of two strict inequalities, I guess

[Mario Carneiro]

Since Scott wrote most of the code, it would be best to whinge while he's not on holiday :)

[Eric Rodriguez]

std4#499, std4#500 - some nice presents for when they're back :)

[Mirek Olšák]

Ok, I will wait with my question about a counterexample too. Now, to my understanding, the issues here are more about user experience that any algorithmic difficulty. For example, the power question is about general coefficient evaluation.

[Eric Rodriguez]

I do think there's other stuff going on:

import Std.Tactic.Omega

example (x : Nat) (h : x ^ 2 = 4) : x = 2 := by
  change 1 * x * x = 4 at h -- this line doesn't matter
  omega

[Mirek Olšák]

But what does this has anything to do with linear inequalities? It feels a bit like complaining that omega doesn't know that (sin x)^2 is the same as 1-(cos x)^2

[Mirek Olšák]

If we had a tactic that could deal with non-linear (in)equalities, like SMT-NIA, then understanding constant powers should be expected. On the other hand, non-linear problems are algorithmically much harder.

[Eric Rodriguez]

ah, my apologies! I thought that omega was a full decision procedure, not a linear one

[Eric Rodriguez]

(now that I think about it, a non-linear decision procedure is provably impossible...)

[Yaël Dillies]

I thought omega was supposed to be complete?

[Mirek Olšák]

It is complete within the realm of linear inequalities over integers (which is an NP-complete problem afaik)

[Mirek Olšák]

non-linear problems (Diophantine equations) are generally undecidable

[Alex J. Best]

Omega is a decision procedure for Presburger arithmetic, which means in a complete implementation it can decide any first order sentence using addition on the naturals, this means that you can't deal with things like n^2 only things like 4*n + 5*m for fixed constants (as these can be expressed via a longer formula using only addition), hence the linear part.

[Mario Carneiro]

over real closed fields it is decidable again, but with double-exponential performance

[Yaël Dillies]

Uh, I thought Presburger arithmetic included multiplication. But of course that's bogus.

[Mario Carneiro]

I've long wanted to get an implementation of CAD in lean, but last I checked it was waiting on a bunch of results on permanents needed for a computable algebraic numbers implementation

[Eric Rodriguez]

and $\mathbb{C}$ is undecidable again because we get $e^{2\pi it}$ which can let us emulate integers

[Mario Carneiro]

Do we have algebraic numbers in mathlib yet? Surely we do

[Eric Rodriguez]

docs#IsAlgebraic

[Mario Carneiro]

I see that but it's a proposition

[Kevin Buzzard]

Yaël Dillies said:

Uh, I thought Presburger arithmetic included multiplication. But of course that's bogus.

Multiplication by constants but not by variables.

[Mirek Olšák]

Eric Rodriguez said:

and $\mathbb{C}$ is undecidable again because we get $e^{2\pi it}$ which can let us emulate integers

Algebraically closed fields are decidable too, I believe the complexity should be the same as with real (sure not harder)

[Eric Rodriguez]

docs#Algebraic.cardinal_mk_of_infinite uses the subtype so I don't think there's anything else

[Mario Carneiro]

is there a type of algebraic numbers over $\mathbb{Q}$ or as elements of $\mathbb{C}$

[Yaël Dillies]

Eric Rodriguez said:

and $ℂ$ is undecidable again because we get $e^{2π it}$ which can let us emulate integers

But only integers with addition, right? You don't get multiplication because that would correspond to exponentiation.

[Mario Carneiro]

AlgebraicCard.lean's module doc references Liouville.is_transcendental but I don't think docs#Liouville.is_transcendental exists

[Yaël Dillies]

docs#Liouville.transcendental it seems

[Mario Carneiro]

and I see it uses Transcendental ℤ (x : ℝ) in the statement, which is ¬IsAlgebraic ℤ (x : ℝ), so I guess that's all there is

[Mario Carneiro]

Do we know the algebraic numbers are closed under addition and such?

[Mario Carneiro]

there are some basic results in the Algebraic file but not addition or ringness

[Yaël Dillies]

docs#IsAlgebraic.add is not there, it seems

[Mario Carneiro]

Eric Rodriguez said:

and $\mathbb{C}$ is undecidable again because we get $e^{2\pi it}$ which can let us emulate integers

This by the way is the proof that although you can decide polynomial equations and inequalities using $\mathbb{R}$ and $\mathbb{C}$, once you add exponentials or trig functions it becomes undecidable.

[Damiano Testa]

Eric Rodriguez said:

it'd be useful for debugging at least!

Here is a very simple-minded implementation of clear_mdata:

import Mathlib.Lean.Meta
import Std.Tactic.Omega

open Lean.Elab.Tactic in
/-- removes the first layer of `mdata` from the main goal. -/
elab (name := tacClearMData) "clear_mdata" : tactic => do
  let goal ← getMainGoal
  replaceMainGoal [← goal.change (← goal.getType'')]

example : 0 = 0 := by
  have : 0 = 0 := by omega -- works
  --omega  -- fails
  clear_mdata
  omega -- works

[Geoffrey Irving]

Is this the mdata thing again, or something else?

import Std.Tactic.Omega
import Mathlib.Data.Nat.Basic

theorem good {n : ℕ} (h : n ≤ 62) : 64 - (62 - n) = n + 2 := by
  omega

lemma bad {X : Type} {x : X} {f : X → ℕ} : 64 - (62 - f x) = f x + 2 := by
  replace h : f x ≤ 62 := sorry
  -- Works
  --   `exact good h`
  -- Fails with
  --   `omega did not find a contradiction:`
  --   `[1] ∈ [0, 62]`
  omega

[Damiano Testa]

Likely: using clear_mdata before the failing omega, makes the omega call work.

[Geoffrey Irving]

Is there a bug already filed about the mdata issue? I don't see one: https://github.com/leanprover/std4/issues?q=is%3Aissue+omega+mdata

[Damiano Testa]

I didn't file any bug. If someone did, it might be @Eric Rodriguez , but I do not know if he got around to it.

[Geoffrey Irving]

mdata bug: https://github.com/leanprover/std4/issues/509

[Eric Rodriguez]

I didn't file one for mdata, just for powers and for constants on the right

[Damiano Testa]

Btw, the mdata issue is very simple: if, inside a proof, you use a have or let, this changes the goal to a DefEq expression that begins with a "metadata" field. If a tactic like omega does some matching on the goal and does not "see through" mdata, it will fail to identify what the target really is.

[Damiano Testa]

The solution is typically to add a ← whnf or a consumeMData or something similar. I just do not have the time to figure out where it should go...

[Kim Morrison]

Fixed in std4#510.

[Geoffrey Irving]

Thank you!