Zulip Chat Archive

Stream: new members

Topic: Use of implicit arguments


view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 24 2020 at 07:39):

thanks for providing an #mwe

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 24 2020 at 07:42):

so maybe this time it isn't minimal?

view this post on Zulip Patrick Stevens (May 24 2020 at 07:46):

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

view this post on Zulip Patrick Stevens (May 24 2020 at 07:46):

because that definitely does work

view this post on Zulip Reid Barton (May 24 2020 at 10:39):

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

view this post on Zulip 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