capabilities of nlinarith

Stream: general

[Julian Külshammer]

For my understanding, why does nlinarithnot work on the following lemma? Is it just a matter of complexity? I had the impression it was able to solve similar looking goals with similar hypotheses that I tried before? Is there any other tactic that I should have tried? I was able to do it by hand, by preprocessing to the step where hrs and huv had already been used.

import data.int.basic
import tactic.linarith

  lemma helper (r1 r2 s1 s2 u1 u2 v1 v2 : ℤ) (hrs : r1 * s2 = s1 * r2) (huv : u1 * v2 = v1 * u2) :
  (r1 * u2 + r2 * u1) * (s2 * v2) = (s1 * v2 + s2 * v1) * (r2 * u2) :=
  begin
    sorry
  end

[Mario Carneiro]

this isn't linear arithmetic at all. nlinarith only does some basic preprocessing before going to the linear arithmetic solver

[Mario Carneiro]

you should be using ring or linear_combination to solve this

[Mario Carneiro]

keep in mind that nonlinear arithmetic is undecidable so you are bound to be disappointed by things that are nominally in its domain

[Mario Carneiro]

lemma helper (r1 r2 s1 s2 u1 u2 v1 v2 : ℤ) (hrs : r1 * s2 = s1 * r2) (huv : u1 * v2 = v1 * u2) :
  (r1 * u2 + r2 * u1) * (s2 * v2) = (s1 * v2 + s2 * v1) * (r2 * u2) :=
by linear_combination u2*v2*hrs + s2*r2*huv

[Julian Külshammer]

Thanks a lot for the explanation and the right way to do it.