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


Alex J. Best (Sep 14 2021 at 19:59):

The difference being the brackets, 1/2 * 1 / n is treated as (1/2 * 1) / n and not (1/2)*(1/n).

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

Oh. My. God. Okay... Thanks

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

The Infoview is your friend! Click on the operators and see what gets selected.

Yaël Dillies (Sep 14 2021 at 20:00):

Clicking on the second / in 1/2 * 1/(n+1 : ℝ) selects everything. That's how I spotted it.

Vasily Ilin (Sep 14 2021 at 20:00):

What do you mean @Yaël Dillies ? Click on *? Nothing happens for me.

Alex J. Best (Sep 14 2021 at 20:01):

Are you using vscode?

Yaël Dillies (Sep 14 2021 at 20:01):

in the Infoview, I mean. Are you not using VScode?

Yes

Vasily Ilin (Sep 14 2021 at 20:01):

No, I use VScode. I just don't know what is infoview

Yaël Dillies (Sep 14 2021 at 20:01):

This is how it looks like. image.png

Alex J. Best (Sep 14 2021 at 20:02):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Christopher.20Hoskin/near/220710143