Why does omega fail on this simple lemma?

Stream: new members

[Dylan Ede]

import Mathlib

-- this works fine
lemma foo (a b : ℕ) (h : 0 < a) : a * b = a * b - b + b := by
  rw [Nat.sub_add_cancel]
  apply Nat.le_mul_of_pos_left
  exact h

-- this does not
lemma foo' (a b : ℕ) (h : 0 < a) : a * b = a * b - b + b := by
  omega

-- nor does this
lemma foo'' (a b : ℕ) (h : 0 < a) : a * b = a * b - b + b := by
  linarith

[Luigi Massacci]

That goal is arguably out of scope for linarith (it is not really about linear arithmetic, and the naturals are already borderline for linarith).

[Bjørn Kjos-Hanssen]

ring helps a bit:

import Mathlib

lemma foo' (a b : ℕ) (h : 0 < a) : a * b = a * b - b + b := by
  cases a <;> (ring_nf;omega) -- works

[Dylan Ede]

@Bjørn Kjos-Hanssen thanks. What's interesting is that that technique fails on an ever so slightly more complicated version and instead ring! does the trick:

import Mathlib

-- this works fine
lemma bar (a b : ℕ) (h : 0 < a) : a * b = (a - 1) * b + b := by
  rw [Nat.sub_one_mul, Nat.sub_add_cancel]
  apply Nat.le_mul_of_pos_left
  exact h

-- this does not
lemma bar' (a b : ℕ) (h : 0 < a) : a * b = (a - 1) * b + b := by
  cases a
  . contradiction
  . ring_nf
    omega -- FAILED

-- but this does
lemma bar'' (a b : ℕ) (h : 0 < a) : a * b = (a - 1) * b + b := by
  cases a
  . contradiction
  . ring!

But ring! doesn't work on the original example.

[Kenny Lau]

The theory of (N, +, -, *) would seem to me to be completely equivalent to the usual theory of (N, +, *) (which I assume omega is based on), but maybe nobody has actually studied the decision algorithms for the first one yet? Especially since it's not a very "standard" system

[Kenny Lau]

I would assume that b + c = a -> a - b = c and a - b = 0 iff exists c, a + c = b would be the translations... oh but now it would increase the arithmetic complexity of the formula...

[Kenny Lau]

ok maybe they're not completely equivalent once you bring arithmetic complexity into the picture

[Kenny Lau]

maybe someone who knows more about proof theory can offer some pointers

[Bjørn Kjos-Hanssen]

That quantifier over c is bounded though (c is at most b), so it shouldn't really increase the complexity.

[Robin Arnez]

omega treats natural number subtraction like

b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

so basically ↑(a - b) = if b ≤ a then ↑a - ↑b else 0
(for reference: docs#Lean.Omega.Int.ofNat_sub_dichotomy).
grind does almost literally this, it uses:

if ↑b + (-1) * ↑x ≤ 0 then
  ↑x + (-1) * ↑y
else
  0

(docs#Int.Linear.natCast_sub)

[Robin Arnez]

so... case split

[Kenny Lau]

@Robin Arnez if omega has a correct translation of -, then why would it fail?

[Markus Himmel]

omega is a decision procedure for linear arithmetic, i.e., it can only reason about multiplication by constants.

[Robin Arnez]

Yes, it's not quite right to say omega supports +, - and * and it's better to say it supports +, - and * (constant)

[Kenny Lau]

I see, now I understand

[Dylan Ede]

Is this kind of problem within scope for grind?

[Robin Arnez]

No, as far as I know, grind only supports +, - and * (constant) (like omega) fully. Solving equations with variable by variable multiplication is a much harder problem

[Robin Arnez]

To be fair though, grind does support basic simplification similar to ring (in commutative rings, not e.g. Nat) like (a + b) ^ 2 = a^2 + 2*a*b + b^2