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