Analysis.NormedSpace.Basic !4#3280

Stream: mathlib4

[Jeremy Tan]

!4#3280 5 errors remain in this file:

• 2 continuity failures
• 2 instance failures
• 1 deterministic timeout

Would really appreciate continuing the work on this file!

[Matthew Ballard]

It looks like the continuity failures are (partially) due to order of attribute application. Eg

@[to_additive (attr := continuity) something]

look like we get the additive version in the rules set for continuity
vs

@[continuity, to_additive something]

where we do not. For example continuous_norm is not currently in the rules set. This goes beyond this particular example and should probably be taken care of globally before continuing with this PR. Assuming my understanding of the situation is correct.

[Matthew Ballard]

The other fixes should be incoming momentarily.

[Frédéric Dupuis]

I suspect it's easier to just add missing continuity tags whenever we find them instead of trying to fix it all at once.

[Matthew Ballard]

Can’t we do a global search and replace taking the latter to former? My awk-foo is non-existent (or is it sed)?

[Matthew Ballard]

Matthew Ballard said:

The other fixes should be incoming momentarily.

Hmm. One will be. The instance failures are the same and are being more annoying.

[Eric Wieser]

We should definitely do a standalone first pass at catching all the obviously missing continuity lemmas before continuing with this porting PR

[Matthew Ballard]

Ah. I see some confusion. They are not “missing” in that they are missing the tag altogether. They are “missing” in that the tag is out of order. We don’t need to find anything that doesn’t already start with @[continuity, to_additive…]

[Matthew Ballard]

(There are some other things that need to be tagged that are not but those I agree should be added case by case)

[Eric Wieser]

I think probably every to_additive not immediately following a @[ is probably a mistake

[Eric Wieser]

The only possible exception I can think of is reducible after seeing some weirdness there with @Jeremy Tan; there we found that @[reducible, to_additive (attr := reducible)] seemed to behave differently to all the other options.

[Eric Wieser]

(cc @Floris van Doorn)

[Matthew Ballard]

Oh wait. There might be only two instances of this. There were next to each in the file I jumped into so I assumed it was more prevalent

[Matthew Ballard]

Grepping only gives continuous_norm’ and continuous_nnnorm’

[Matthew Ballard]

I flush regex from my mind after each use so I didn’t do the more general pattern @Eric Wieser suggests

[Frédéric Dupuis]

Hmm, I just realized that the continuity tag doesn't show up in the mathlib4 docs like it did for mathlib3. I see your point now.

[Frédéric Dupuis]

I searched for continuous_norm in the docs and was under the impression that the tag was missing altogether.

[Jeremy Tan]

@Matthew Ballard

Continuity is a still a little fiddly. Further diagnostics are a good idea before merging

How are we going to collect diagnostics?

[Matthew Ballard]

There are two issues that I noticed:

• editor misbehaves around continuity (eg hangs)
• since everything is currently marked a safe rule in aesop it gets itself into some pickles. For example, npowRec gets exposed when proving f^2 is continuous or Inv.inv when f^-1. The first can be handled by give a normalisation rule. The latter is more problematic. These examples stem from safe applications of comp which gets applied before the more appropriate rules. I tried to make it unsafe but that broke a good deal more.

I've made continuity work as much as possible with quick fixes and included the tactic terms that close the goals as comments.

[Matthew Ballard]

I am guessing these problems will persist later in analysis (though people more intimately familiar with the library would know better) so getting good continuity behavior will save time in the long run

[Moritz Doll]

Fixing issues with continuity is not hard, but fixing continuity is more involved and I don't think that it is just a matter of finding the right aesop rules for various lemmas, but it will probably need some support from aesop itself.

[Moritz Doll]

I'll try to see whether adding a penalty to Continuous.comp' fixes some of the issues

[Scott Morrison]

Maybe I'll try a clean implementation of continuity not using aesop at some point...? It feels like the sort of thing that solve_by_elim with its new flow-control handles should be able to manage fine.

[Moritz Doll]

One of the big advantages of aesop is that it makes it very easy to create more tactics that are very similar in spirit. When proving the Taylor theorem I was very annoyed by the fact that there was no continuity for continuous_on and the lack of a smoothness tactic has been discussed here as well.

[Moritz Doll]

Matthew Ballard said:

There are two issues that I noticed:

• editor misbehaves around continuity (eg hangs)
• since everything is currently marked a safe rule in aesop it gets itself into some pickles. For example, npowRec gets exposed when proving f^2 is continuous or Inv.inv when f^-1. The first can be handled by give a normalisation rule. The latter is more problematic. These examples stem from safe applications of comp which gets applied before the more appropriate rules. I tried to make it unsafe but that broke a good deal more.

I've made continuity work as much as possible with quick fixes and included the tactic terms that close the goals as comments.

Was your 'the editor misbehaves' problem that the linter was saying that tactics were never executed? that was what I was seeing when playing around with in the file and the answer was that continuity was proving the continuity of the inverse without any help.

[Matthew Ballard]

Moritz Doll said:

continuity was proving the continuity of the inverse without any help.

I still get an error from aesop here. Manually putting in continuous_invFun := by continuity also does not work. Odd.

[Matthew Ballard]

Mostly my editor failed to update reliably and showed old state.

[Moritz Doll]

I am quite confused, I was getting no errors in VSCode, but the CI run failed.

[Moritz Doll]

(I am at the moment compiling some modifications of continuity, maybe that magically solves the issue :pray: )

[Scott Morrison]

Moritz Doll said:

One of the big advantages of aesop is that it makes it very easy to create more tactics that are very similar in spirit. When proving the Taylor theorem I was very annoyed by the fact that there was no continuity for continuous_on and the lack of a smoothness tactic has been discussed here as well.

I don't think this need be an obstacle. Heather Macbeth has written several nice frontends for solve_by_elim as teaching tactics, and we should be able to make a "generic" version of continuity that is customisable for different goals.