Organize some directories separated by definitions and theorems about mathlib HOT 3 CLOSED

I don't know if this applies in such low-level files, but abstractly in mathematics it's not uncommon to see a definition which relies on a theorem (if X is a perfectoid distrib then maybe there's a theorem that says there's exactly one function from X to X with some property, and then the definition of this fundamental function is that it's the unique function which the theorem says exists). I completely agree that multiset.lean is a monster, however it is laid out in a pretty logical way. Once you get going, each definition is preceded by a comment saying what we're about to and then a bunch of theorems, some end-user-friendly and some technical intermediate stuff. In this instance you might just be suggesting that these little sections all become separate files in a multiset directory. I guess this might make human-search easier (you would have multiset/powerset.lean, multiset/countp.lean, multiset/count.lean and so on.

I am not sure anyone has any feeling about the amount of work which will need to be refactored anyway when Lean 4 hits. I also have no understanding (as an "end user" of theorems) how much the packaging of them matters, but let me make the slightly superficial remark that initially I found the length of multiset.lean quite scary.

from mathlib.

@kbuzzard:

it's not uncommon to see a definition which relies on a theorem

Sure, that's in mathlib. I think it will depend on the particular example as to what is done with it. That is, it will probably be a judgment call. For example, the definitions of both multiset and finset involve theorems, but they also form the center of their own topics, with a collection of associated definitions and theorems. In other cases, there may be smaller associated collections that don't deserve forming entire hierarchies. This should fall under the Exceptions heading of the proposal.

I completely agree that multiset.lean is a monster, however it is laid out in a pretty logical way.

Sure, no argument about the arrangement.

In this instance you might just be suggesting that these little sections all become separate files in a multiset directory. I guess this might make human-search easier (you would have multiset/powerset.lean, multiset/countp.lean, multiset/count.lean and so on.

Actually, I'm not suggesting that here. I would consider that as a follow-on proposal. I have tried to frame this proposal as a small step with a noticeable improvement so that (a) it doesn't get mixed up with other possibilities and (b) it's easier to implement. Even if all of the little sections do not become separate files, I still think it's better to extract the definitions, so I see these as independent issues.

I am not sure anyone has any feeling about the amount of work which will need to be refactored anyway when Lean 4 hits.

I'm not sure of the relevance of Lean 4 here. We could be eternally waiting for something to happen without knowing what that thing is, and this would certainly slow down development. Since we don't know what to expect, I don't think waiting will do any good. And since mathlib development has continued apace, I think other people agree.

Besides, one object of this proposal is to figure out (a small part of) what makes for good Lean code organization. I don't think Lean 4 is going to change that.

from mathlib.

I think at this stage we've decided to mostly not do this, except where it resolves dependency problems. #499 above broke apart data/list/basic.lean, so that the tactics files could depend on the definitions, and then the theorems about lists could use the tactics. If we have further instances of this problem, let's continue breaking apart files as needed.

from mathlib.