# Zulip Chat Archive

## 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