Zulip Chat Archive

I would like to use the lemma continuous_linear_map.has_fderiv_within_at (docs), which takes 5 implicit arguments, 5 type annotations, and one explicit argument. I would also like to explicitly provide one of the implicit arguments (x in the docs).

I gather that @ is used to make implicit arguments explicit, although I am not familiar with the syntax. Is there a way of using it which makes explicit only the one implicit argument I need, and not all the others?

Kevin Buzzard (Jun 19 2020 at 19:21):

nope...

Kevin Buzzard (Jun 19 2020 at 19:22):

There's @@ which does something I've forgotten (but it will say in TPIL). It's vanishingly unlikely that it will solve your problem. I've heard that in other languages you can do things like @@@f {thing_i_want_to_specify := this} ... but not in Lean

Sebastien Gouezel (Jun 19 2020 at 19:23):

Not in Lean 3, but in Lean 4 yes I believe.

Heather Macbeth (Jun 19 2020 at 19:23):

OK, so it will be messy. What is the syntax exactly? I cannot see how to provide the type annotations.

Heather Macbeth (Jun 19 2020 at 19:24):

Sebastien, you wrote this lemma :slight_smile: Is it easy to explain why x is implicit?

Yakov Pechersky (Jun 19 2020 at 19:26):

Just underscores everywhere, and it will infer the types and instances from the linear_map you gave it

Sebastien Gouezel (Jun 19 2020 at 19:28):

That's the standard style in the topology/analysis part of the library, initiated by Johannes Hölzl. The idea is that you will use it as

example : has_fderiv_at_within_at (complicated expression) (complicated expression again) x :=
thing built using the lemmas, where x can be inferred from the goal

95% of the time, it is super-efficient. 5% of the time, you need the @-version and underscores.

Heather Macbeth (Jun 19 2020 at 19:30):

@Yakov Pechersky thank you, that's much better than I feared!

Heather Macbeth (Jun 19 2020 at 19:32):

@Sebastien Gouezel I think I understand, the point is that only the definitions (eg has_fderiv_within_at), not the lemmas, include x explicitly?

Sebastien Gouezel (Jun 19 2020 at 19:39):

Yes, precisely.

Kevin Buzzard (Jun 19 2020 at 19:44):

Oh sorry Heather! Yes, it's just lots of underscores. I thought you were asking if they could be avoided. Search mathlib for _ _ _ _ to see plenty of examples of this :-) I think the last time I looked the record was about 8

Reid Barton (Jun 19 2020 at 19:49):

somehow this reminds me of https://github.com/torvalds/linux/blob/v5.4/include/linux/rcupdate.h#L310

Sebastien Gouezel (Jun 19 2020 at 19:53):

Kevin Buzzard said:

Oh sorry Heather! Yes, it's just lots of underscores. I thought you were asking if they could be avoided. Search mathlib for _ _ _ _ to see plenty of examples of this :-) I think the last time I looked the record was about 8

No, 11 :)

lemma is_add_group_hom_map
  {f : α → β} [is_add_group_hom f] (hf : continuous f) : is_add_group_hom (completion.map f) :=
@is_add_group_hom_extension _ _ _ _ _ _ _ _ _ _ _ (is_add_group_hom.comp _ _)
  ((continuous_coe _).comp hf)

Kevin Buzzard (Jun 19 2020 at 19:54):

woohoo -- we beat Linux!

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib