Complex.ext

Stream: mathlib4

[Yaël Dillies]

How do people feel about removing the @[ext] from docs#Complex.ext? It's annoying that I must manually stop ext before it duplicates every goal whenever I deal with complex-valued functions.

[Pedro Sánchez Terraf]

Out of curiosity: Is there a way to override that locally?

[Yaël Dillies]

Last time I tried, you couldn't but it seems now you can!

[Johan Commelin]

I think Complex.ext should be locally turned into an ext-lemma when setting up the API for complex numbers. But when that's done, it probably shouldn't be an ext-lemma by default.

[Yaël Dillies]

Yeah that's exactly my thought.

[Kevin Buzzard]

That was also my conclusion when I made the complex number game. It was super-useful to have it as an ext lemma when making the API and then annoying afterwards.

[Heather Macbeth]

Yaël Dillies said:

Last time I tried, you couldn't but it seems now you can!

@Yaël Dillies Which version of Std are/were you on? I added the ability to locally remove ext attributes in https://github.com/leanprover/std4/pull/235

[Yaël Dillies]

The first time I tried was beginning of July. Now I've just synced my project with mathlib. Are you telling me you can now globally erase @[ext]? I thought we could only locally erase attributes now.

[Scott Morrison]

I think it would be great if you could PR a change so that @[ext] is only ever add locally to Complex.ext.

[Jireh Loreaux]

I'm implementing this now because I just realized no one ever did it (no blame here!). Should it be a local attribute or a scoped attribute (in the Complex namespace). I was thinking local, and I think that's what people were suggesting above, but I wanted to be sure.

[Kyle Miller]

That appears to agree with Johan's suggestion. It makes sense to me too, since you should have to do more than open Complex to cause Complex.ext to be an @[ext] lemma.

[Frédéric Dupuis]

I definitely think it should be local and not scoped; this is not something we want by default when working with complex numbers.

[Jireh Loreaux]

Hmmm... I wonder if it's worth extending the syntax for ext so that it can accept a list of identifiers to use as ext lemmas. Probably not.

[Frédéric Dupuis]

At that point it's probably easier to use the lemma you want manually with refine.

[Jireh Loreaux]

yes, unless it's being applied as part of a larger seequence of ext lemmas and you don't want to call them all manually. But you're right I think. I expect that to be a pretty niche use case.

[Kyle Miller]

In the spirit of composable interfaces, I'd say the current syntax is

section
attribute [local ext] thm1 ... thmn

theorem ... := by
   ...
   ext
   ...

end

It's not very precise, but it's probably sufficient in most cases.

[Jireh Loreaux]

Yeah, I'm at 3978/4012 and I only had this issue come up once.

[Jireh Loreaux]

#9010