unexpected lambda

Stream: new members

[Szymon Kitowski]

Hi, I am trying to use Lean for verification of software for electrical transmission optimization that uses Mixed Integer Linear Programming. Therefore I have to deal with many finite sums. I get stuck with a trivial lemma trying to apply finset.sum_nonneg. Why did the lambda expression appear? How to get rid of it to proceed further with the proof?

import data.real.basic
import data.finset
import algebra.big_operators.basic
import algebra.big_operators.order
open_locale big_operators

lemma something {α : Type} (S : finset α) (f : α → ℝ) (H : ∀ (k : α), k ∈ S → 0 <= f(k)) :
(∑ (k : α) in S, f(k) <= 0) ↔ (∀ (k : α), k ∈ S → f(k) = 0) :=
begin
  have r := finset.sum_nonneg H, -- r : 0 ≤ ∑ (x : α) in S, (λ (k : α), f k) x <<-- WHY LAMBDA?!?
  sorry, -- what to do next?
end

[Kevin Lacker]

lean just isn't automatically simplifying that expression for you. throw in a simp at r to simplify r and it'll be simpler

[Kevin Lacker]

personally, i would use a bunch of tactics to break up the lemma into smaller bits before trying to proveit

[Kevin Lacker]

this cheat sheet is handy: https://leanprover-community.github.io//img/lean-tactics.pdf

[Yakov Pechersky]

import data.real.basic
import data.finset
import algebra.big_operators.basic
import algebra.big_operators.order
open_locale big_operators

lemma something {α : Type} (S : finset α) (f : α → ℝ) (H : ∀ (k : α), k ∈ S → 0 <= f(k)) :
(∑ (k : α) in S, f(k) <= 0) ↔ (∀ (k : α), k ∈ S → f(k) = 0) :=
begin
  rw ←finset.sum_eq_zero_iff_of_nonneg H,
  split,
  { intro h,
    exact le_antisymm h (finset.sum_nonneg H) },
  { intro h,
    rw h },
end

not the neatest proof, some golfing possible

[Szymon Kitowski]

Thank you all. This was super fast. @Yakov Pechersky I am trying to figure out the role of le_antisymm. How did it help with simplifying finset.sum_nonneg?

[Yakov Pechersky]

le_antisymm says that if you have an x such that x <= 0 and 0 <= x then x = 0. By spliting, we turn the iff into two implications we have to prove. The forward implication gives us the hypothesis that the sum is <= 0. Your H hypothesis can be used in finset.sum_nonneg to give the 0 <= _ hypothesis.

[Reid Barton]

It's generally not a great idea to write a term and have Lean guess what it is a proof of, like in have r := finset.sum_nonneg H.

[Reid Barton]

Better to use tactics which operate on the goal (which Lean already knows) like rw or exact, or use have with an explicit type: have r : ... := ...

[Szymon Kitowski]

Thanks.
@Yakov Pechersky I just wonder why le_antisymm worked with ∑ (k : α) in S, f k ≤ 0 and 0 ≤ ∑ (x : α) in S, (λ (k : α), f k) x. Is it like that Lean can somehow perform implicit beta reduction so he knows that both sigma sums are the same?
@Reid Barton I understand that this is because type interference can get me something strange, right?

[Reid Barton]

Lean has to solve a higher-order unification to figure out what f is in finset.sum_nonneg, because f only ever appears applied to an argument. In this case it probably doesn't really make a difference whether Lean knows the expected type too.

[Reid Barton]

It decided that f was your \lam k, f k, but that's fine because of beta reduction like you said.

[Reid Barton]

More precisely, (λ (k : α), f k) x is definitionally equal to f x and so le_antisymm h (finset.sum_nonneg H) will type check even though the types look a bit different.

[Szymon Kitowski]

Thanks. I get it now. :tada: