Zulip Chat Archive

Stream: new members

Topic: unexpected lambda


Szymon Kitowski (Dec 02 2020 at 18:19):

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 (Dec 02 2020 at 18:28):

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 (Dec 02 2020 at 18:30):

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

Kevin Lacker (Dec 02 2020 at 18:30):

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

Yakov Pechersky (Dec 02 2020 at 18:39):

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 (Dec 02 2020 at 18:47):

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 (Dec 02 2020 at 18:53):

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 (Dec 02 2020 at 18:56):

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 (Dec 02 2020 at 18:57):

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 (Dec 02 2020 at 19:03):

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 (Dec 02 2020 at 19:06):

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 (Dec 02 2020 at 19:06):

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

Reid Barton (Dec 02 2020 at 19:12):

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 (Dec 02 2020 at 19:14):

Thanks. I get it now. :tada:


Last updated: Dec 20 2023 at 11:08 UTC