Zulip Chat Archive

Stream: maths

Topic: linarith power


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 18:00):

I then got optimistic

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 31 2021 at 10:06):

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

view this post on Zulip 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.

view this post on Zulip 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