## Stream: maths

### Topic: linarith power

#### Kevin Buzzard (Mar 23 2021 at 16:11):

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 (Mar 23 2021 at 17:15):

@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 (Mar 23 2021 at 17:53):

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 (Mar 23 2021 at 17:54):

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 (Mar 23 2021 at 18:00):

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 (Mar 23 2021 at 18:00):

I then got optimistic

#### Marc Masdeu (Mar 26 2021 at 11:22):

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 (Mar 26 2021 at 12:55):

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 (Mar 31 2021 at 09:41):

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 (Mar 31 2021 at 10:06):

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

#### Kevin Buzzard (Mar 31 2021 at 10:07):

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 (Mar 31 2021 at 10:09):

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


Last updated: May 10 2021 at 06:13 UTC