Zulip Chat Archive

Stream: new members

Topic: linarith failed to find a contradiction

Vasily Ilin (Sep 14 2021 at 19:50):

In the following script I get the error "linarith failed to find a contradiction" even though k1 asserts that the same thing times 2 is positive. I don't understand what is going on.

import data.real.basic

example {n : ℕ} : 0 < 1/(n+1 : ℝ) :=
begin
  have k1 : 1/(n+1 : ℝ) > 0,
    exact nat.one_div_pos_of_nat,
  have k2 : 1/2 * 1/(n+1 : ℝ) > 0,
    linarith,
end

Yaël Dillies (Sep 14 2021 at 19:52):

linarith doesn't know about multiplication.

Yaël Dillies (Sep 14 2021 at 19:53):

I would have expected nlinarith to solve this, but it doesn't :thinking:. Just apply mul_pos, I guess.

Vasily Ilin (Sep 14 2021 at 19:54):

But this works just fine. So linarith must know about multiplication.

example {ε : ℝ} (h : ε > 0) : 1/2 * ε > 0 :=
begin
  linarith,
end

Yaël Dillies (Sep 14 2021 at 19:56):

Actually, you didn't really write what you meant.

Yaël Dillies (Sep 14 2021 at 19:57):

linarith does know about multiplication, but only handles constants well.

Yaël Dillies (Sep 14 2021 at 19:57):

This works.

import data.real.basic

example {n : ℕ} : 0 < 1/(n+1 : ℝ) :=
begin
  have k1 : 0 < 1/(n+1 : ℝ),
    exact nat.one_div_pos_of_nat,
  have k2 : 0 < 1/2 * (1/(n+1 : ℝ)),
    linarith,
end