# Zulip Chat Archive

## Stream: new members

### Topic: Use of implicit arguments

#### Patrick Stevens (May 24 2020 at 07:38):

Something I'm finding slightly annoying is the fact that mathlib makes arguments "as implicit as possible", so when I am applying a lemma I very often have to `@`

the function just so that I can tell Lean what I'm trying to prove. Sometimes it ends up that I can remove the `@`

again when I've constructed a call, but often I have an inline `by linarith`

or similar as an argument, and when I remove the `@`

Lean stops being able to infer the types correctly.

The example I'm looking at right now is `finset.single_le_sum`

, which has an argument "for all x, `f x`

is positive"; and Lean can't infer `f`

. (Lean can infer the `finset.range (n + 1)`

in my real example because it's sufficiently constrained by the thing I've replaced with `by sorry`

; but it can't infer the function `choose (2 * n + 1)`

.)

```
import algebra.commute
import tactic.linarith
open nat
open_locale big_operators
lemma choose_middle_le_pow (n : ℕ) : choose (2 * n + 1) n ≤ 4 ^ n :=
begin
have t : choose (2 * n + 1) n ≤ ∑ i in finset.range (n + 1), choose (2 * n + 1) i :=
@finset.single_le_sum _ _ (finset.range (n + 1)) (choose (2 * n + 1)) _ (λ x _, by linarith) n (by sorry),
sorry,
end
```

Do people usually just extract the `(λ x _, by linarith)`

into its own term with a specific named type? That gives Lean enough to infer the function, but it's kind of verbose.

Agda makes this a non-issue by allowing you to specify just a named subset of the implicit arguments, rather than underscoring them all out; but a mathlib-level solution would be to make the argument `f`

explicit, so that a consumer who had a term in hand could just underscore it out at the cost of two characters, while a consumer who wanted to construct it by tactic would be able to supply it at a saving of a full line.

#### Kenny Lau (May 24 2020 at 07:39):

thanks for providing an #mwe

#### Kenny Lau (May 24 2020 at 07:42):

but this works in both tactic and term mode:

```
import algebra.commute
import tactic.linarith
open nat
open_locale big_operators
lemma choose_middle_le_pow (n : ℕ) : choose (2 * n + 1) n ≤ 4 ^ n :=
have t : choose (2 * n + 1) n ≤ ∑ i in finset.range (n + 1), choose (2 * n + 1) i :=
finset.single_le_sum (λ x _, by linarith) (finset.mem_range.2 $ n.lt_succ_self),
begin
have t : choose (2 * n + 1) n ≤ ∑ i in finset.range (n + 1), choose (2 * n + 1) i :=
finset.single_le_sum (λ x _, by linarith) (finset.mem_range.2 $ n.lt_succ_self),
sorry,
end
```

#### Kenny Lau (May 24 2020 at 07:42):

so maybe this time it isn't minimal?

#### Patrick Stevens (May 24 2020 at 07:46):

I'm so confused - I must have done something stupid

#### Patrick Stevens (May 24 2020 at 07:46):

because that definitely does work

#### Reid Barton (May 24 2020 at 10:39):

maybe it *is* minimal, but not an example :upside_down:

#### Chris Hughes (May 24 2020 at 20:09):

I do find myself being annoyed by this sometimes. There are no hard and fast rules, I think sometimes we could do with a few more explicit arguments. I don't think there's much wrong with a show or a have though either.

Last updated: May 16 2021 at 05:21 UTC