# 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 `split`

ing, 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: May 08 2021 at 10:12 UTC