linarith power

Stream: maths

[Kevin Buzzard]

linarith is doing far more than I would have given it credit for:

import tactic

example (n : ℕ) : (n - 2 : ℤ) ^ 2 = (n - 4) ^ 2 → n = 3 :=
begin
  intro h,
  linarith,
end

We suffer from not having a Groebner basis tactic, but linarith is an extremely useful subtitute. It is only recently that it has dawned on me that linarith doesn't just prove inequalities.

[Heather Macbeth]

@Kevin Buzzard nlinarith is even better! In the construction of the stereographic projection, there are several things like (from docs#stereo_left_inv):

import data.real.basic

example (a b : ℝ) (h : 1 = a ^ 2 + b ^ 2) :
  (1 - a) ^ 2 * 4 * 2 = (2 ^ 2 * b ^ 2 + 4 * (1 - a) ^ 2) * (1 - a) :=
by nlinarith

[Rob Lewis]

Actually, linarith does just prove inequalities, but an equality is the same two inequalities. Your example should take ~twice as long as showing n ≤ 3

[Rob Lewis]

You can imagine any input getting ring-normalized. So (n - 2 : ℤ) ^ 2 = (n - 4) ^ 2 gets expanded and the squares get canceled so it's really a linear equation.

[Kevin Buzzard]

I don't really know what ring-normalisation is, I only ever use the tactic to close goals. When I was writing this proof I expanded everything out and cancelled the n^2 terms before hopefully trying linarith (expecting it to fail because of the coercion)

[Kevin Buzzard]

I then got optimistic

[Marc Masdeu]

On the other hand, why does it fail to prove directly this one?

import tactic
open nat

lemma nhalves {n m r : ℕ} :  n / 2 + m < n + m + r + 1 := by linarith -- fails

lemma nhalves {n m r : ℕ} :  n / 2 + m < n + m + r + 1 :=
begin
  have h : n < 2*(n+1), by linarith,
  linarith [nat.div_lt_of_lt_mul h],
end

[Kevin Buzzard]

I know that linarith is not a big fan of natural number subtraction so by the same argument I'm guessing it's not a fan of natural number division.

[Marc Masdeu]

Oh but this fails as well:

example {n m r : ℤ} {hn : 0 ≤ n} {hm : 0 ≤ m} {hr : 0 ≤ r} : n / 2 + m < n + m + r + 1 := by linarith

[Kevin Buzzard]

That's because integer division is also a pathological operation. It works for rationals.

[Kevin Buzzard]

example (n : ℤ) (hn : 0 ≤ n) : n / 2 ≤ n := by linarith -- fails

This is probably one of those situations where one could pester the author of linarith to extend the domain of the tactic to make it work. But as a mathematician I would instead say -- why are you using integer division at all? It is not a natural operation for mathematicians. If you want to divide, you should be using rationals.

[Kevin Buzzard]

import tactic

example {n m r : ℤ} {hn : 0 ≤ n} {hm : 0 ≤ m} {hr : 0 ≤ r} : n / 2 + m < n + m + r + 1 :=
begin
  have hn2 : n / 2 ≤ n, sorry, -- the missing part of the story
  linarith, -- works
end