private imports / private section

Stream: lean4

[Jan-Mirko Otter]

Hello everybody,

my first project grows a little larger and I'd like to refactor it.

For example, I have some very important types and theorems about them. Those theorems should be enough to reason about those types, there is no need to know the implementation details.

In fact, those implementation details are likely to change, and I do not want users to use them directly.

For example, consider a theory about real numbers. There are several constructions available (cauchy sequences, dedekind cuts, probably others)

For the end user, I want to expose some type Real with the corresponding axioms for the real numbers. Any theorem that requires details about the explicit construction is probably not a theorem about real numbers, otherwise the axioms should be enough.

Currently, I mark my internal constructions as private, and this works fine. However, as my project grows, there are some problems:

• I have to work in a single file, otherwise I have no access to the private definitions
• Private definitions are automatically protected, so I lose syntax sugar like dot notation
• I have to add private to basically every definition (a private section would be nice)

What I'd really like is some kind of "private import": In a certain file / folder, I develop all my internal constructions. I can even use syntactic sugar like dot syntax inside those files.
When they are imported with a private import, all theorems / definitions from this import are becoming private theorems.

Is something like this already available, or is something like this planned? Maybe my use case is stupid but I think that there are cases where hiding implementation details may be a good idea. In my case, the explicit constructions are rather ugly while the resulting a theorems are quite nice.

[Henrik Böving]

What you could do right now is instead of talking about concrete types use some sort of proof carrying type class IsReal (a : Type u) : Prop which contains proofs of the axioms. This would force you to write your theorems as [Real R] (a b c : R) (f : R -> R) ... instead of just using real numbers directly though.