linarith failed to find a contradiction

Stream: new members

[Vasily Ilin]

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]

linarith doesn't know about multiplication.

[Yaël Dillies]

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

[Vasily Ilin]

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

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Yaël Dillies]

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]

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

[Vasily Ilin]

Oh. My. God. Okay... Thanks

[Yaël Dillies]

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

[Yaël Dillies]

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

[Vasily Ilin]

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

[Alex J. Best]

Are you using vscode?

[Yaël Dillies]

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

[Vasily Ilin]

Yes

[Vasily Ilin]

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

[Yaël Dillies]

This is how it looks like. image.png

[Alex J. Best]

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

[Vasily Ilin]

Ohhh, very cool! I did not know about this functionality. Thank you!

[Yaël Dillies]

This is THE functionality :wink:

[Yaël Dillies]

where interactive theorem proving comes true.

[Shange Tang]

Hi, I have a trivial question. I am writing the following lean code, which seems can be solved easily by linarith. However linarith failed to find a contradiction. I am wondering why? And how to fix it?

import Mathlib
import Aesop
set_option maxHeartbeats 0

open BigOperators Real Nat



theorem problem1_step3 (n : ℕ) (a : ℕ → ℝ) (h₀ : ∀ k < n, |a k| < 1) (h₁ : ∑ k ∈ Finset.range n, |a k| = 19 + |∑ k ∈ Finset.range n, a k|) (t_ge_19 : ∑ k ∈ Finset.range n, |a k| ≥ 19) (t_lt_n : ∑ k ∈ Finset.range n, |a k| < ↑n) : 19 < n := by
  linarith [t_ge_19, t_lt_n]

[Shange Tang]

For your information, I receive the following message.
Screenshot 2024-10-27 at 8.55.33 AM.png

[Ruben Van de Velde]

Probably it's not dealing with the coercions between naturals and reals

[Ruben Van de Velde]

Though that doesn't help:

import Mathlib
import Aesop
set_option maxHeartbeats 0

open BigOperators Real Nat



theorem problem1_step3 (n : ℕ) (a : ℕ → ℝ) (h₀ : ∀ k < n, |a k| < 1) (h₁ : ∑ k ∈ Finset.range n, |a k| = 19 + |∑ k ∈ Finset.range n, a k|) (t_ge_19 : ∑ k ∈ Finset.range n, |a k| ≥ 19) (t_lt_n : ∑ k ∈ Finset.range n, |a k| < ↑n) : 19 < n := by
  rw [← Nat.ofNat_lt_cast (α := ℝ)]
  rw [ge_iff_le] at t_ge_19
  fail_if_success linarith [t_ge_19, t_lt_n]
  exact t_ge_19.trans_lt t_lt_n

[Shange Tang]

Thank you very much! It seems that even after dealing with the coercions, linarith still can not close the goal.

[Daniel Weber]

Fwiw

theorem problem1_step3 (n : ℕ) (a : ℕ → ℝ) (h₀ : ∀ k < n, |a k| < 1) (h₁ : ∑ k ∈ Finset.range n, |a k| = 19 + |∑ k ∈ Finset.range n, a k|) (t_ge_19 : ∑ k ∈ Finset.range n, |a k| ≥ 19) (t_lt_n : ∑ k ∈ Finset.range n, |a k| < ↑n) : 19 < n := by
  rify at *
  linarith

works

[Ruben Van de Velde]

:exploding_head: