Use of implicit arguments

Stream: new members

[Patrick Stevens]

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]

thanks for providing an #mwe

[Kenny Lau]

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]

so maybe this time it isn't minimal?

[Patrick Stevens]

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

[Patrick Stevens]

because that definitely does work

[Reid Barton]

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

[Chris Hughes]

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.