Importing mathlib conventions?

Stream: new members

[Baran Zadeoglu]

I am a bit confused by naming theorems as I import them. The following seem to work. I am confused on multiple points.

import Mathlib.Algebra.Star.Unitary
import Mathlib.Data.Real.Basic

#check unitary.mem_iff
#check Real.cauchy_one
#check lt_of_le_of_lt

1)Why the prefix for unitary is not capitalized?
2)Why are we using 'Real' as a prefix? I assume the file 'basic' is special (like default). What are the other special file names?
3) Why the third check works? I did not import Mathlib.Order.Defs ?
4)It seems also that the following does not work. Is there a way to make it work?

import Mathlib.Algebra.Star.Unitary
#check Mathlib.Algebra.Star.Unitary.mem_iff

import Mathlib.Algebra
#check Algebra.Star.Unitary.mem_iff

Thanks.

[Damiano Testa]

From your post it seems that you expect that the name of the file that you are importing has a consequence on the namespaces of the declarations that it contains. This is not the case: the declarations in a file can have names that are completely unrelated to the path of the file.

[Damiano Testa]

However, since the paths of the files are meant to help humans understand what is going on, it is common for the path to share some namespaces with the declarations that it contains.

[Damiano Testa]

Finally, imports are transitive: it is hard not to import Mathlib.Order.Defs transitively. I.e., every file that you import, typically starts itself with import X import Y .... This means that X and Y are also imported in your environment, and so on recursively.

[Luigi Massacci]

1) unitary the mathematical object should be lowercase according to mathlib’s #naming conventions (it should fall under case 4) of General Conventions). unitary the namespace I would assume has been put lowercase for consistency with dot notation with the mathematical structure, but it’s the first time I see a lowercase namespace. This does raise an interesting point, the conventions are surprisingly silent about namespaces.
2) Again there Real refers to the namespace, which is a convenient way to distinguish things to which we would like to give the same name, compare docs#Real.exp and docs#Complex.exp
There’s nothing special about Real.Basic, except that it’s meant to signify that it sets up the basic theory of real numbers (in particular, their definition)
3) Like in most programming languages, importing is transitive (i.e. if you import A, and A imports B, you also get B). There’s a lake command to view the import graph if I remember correctly.
4) You are confusing namespaces with filenames. lean is more like C/C++ and less like python, in that the file name is pretty much completely irrelevant as far as the software is concerned

[Niels Voss]

If you are curious as to why namespaces have nothing to do with the directory structure, one of the many reasons is that Lean cannot handle circular imports (since that would let you use mutual recursion and create proofs of False). So if we tied namespaces to the directory structure, then everything in the Nat namespace would have to be declared in one file, early in the inheritance hierarchy. Then we couldn't have things like Nat.nth, because that depends on something in Mathlib.Data.Finset.Sort, which in turn depends on the file in which Nat is declared. Basically, the way it is set up right now allows you to add to the Nat namespace later.

Importing has to be transitive because if B depends on A, then B might use a type or declaration in A, and if you were writing file C and were able to import B but not A, then those definitions from B might not make any sense.