data.real.basic

Stream: mathlib4

[Heather Macbeth]

I started a project of removing module and finset from the imports of data.real.basic. #17758, #17760, #17761 are the first steps.

[Ruben Van de Velde]

Heh, I had #17761 just about ready as well. Pushed my final fixes to your branch

[Ruben Van de Velde]

I also pushed #17764, but now I'm off :)

[Heather Macbeth]

Can anyone suggest how to fix the broken test in #17760? The task is

filter.map g (map f A) ≤ filter.map g B,

the timing-out proof is by library_search!, and I can't see how this would be affected by splitting char_zero into two files.

(I tried adding back in both post-split files, in case it was a missing import, but the timeout remains.)

[Junyan Xu]

Maybe use docs#tactic.interactive.try_for

[Heather Macbeth]

Heather Macbeth said:

I started a project of removing module and finset from the imports of data.real.basic. #17758, #17760, #17761 are the first steps.

#17768 and #17772 are also in pursuit of this goal.

[Heather Macbeth]

The number of lines to reach data.real.basic dropped from 120,374 yesterday to 92,135
today! This is thanks to the elimination of finset from its imports with #17791, #17768 and #17792 landing (as well as a series of previous PRs by myself and @Ruben Van de Velde, which reduced the finset imports to those three paths).

The submonoid object disappeared the day before that, thanks to @Eric Wieser in #17786. The module import will be gone after #17804. There's more that could be done, but I'm going to stop here.

[Eric Wieser]

What's the motivation for pulling algebra.module.basicout of the import path? Are there heavy imports there that perhaps suggest algebra.module.basic should be split instead?

[Eric Wieser]

module doesn't strike me as a particularly complex thing to depend on, especially from the perspective that many mul lemmas can be stated as special cases of a smul lemma.

[Yaël Dillies]

In general, I'm afraid that the file atomisation taking place currently will work towards rebuilding more things from scratch rather than using general theory (because the general theory requires more imports).

[Heather Macbeth]

@Eric Wieser @Yaël Dillies Perhaps you don't realise that removing module from the import path of data/real/basic did not actually require changing any proofs. The chain of declarations leading to this file was already independent of module, it just happened that some of these declarations lived in the same files as declarations depending on module.

[Heather Macbeth]

Personally, I would also be happy to change a few proofs in order to eliminate an import (for example, one or two proofs of the kind conjectured by Eric:
Eric Wieser said:

many mul lemmas can be stated as special cases of a smul lemma.

) if the duplication is not too egregious. We already are effectively doing that by constructing real using the special-purpose docs#cau_seq rather than by using docs#uniform_space.completion. But I agree that such changes are more controversial.