import specific lemma from mathlib

Stream: general

[ZHAO Jinxiang]

import tactic.suggest
import data.nat.basic -- I only want to import `nat.pos_iff_ne_zero`
open nat (add_zero add_succ succ_ne_zero add_one succ_eq_add_one)

// invalid definition, a declaration named 'zero_add' has already been declaredLean
lemma zero_add : ∀ n : ℕ,  0 + n = n := sorry

I want to define my own zero_add,succ_add, add_comm, add_assoc and so on.

Can I import only nat.pos_iff_ne_zero in data.nat.basic?

In JavaScript I can

import { pos_iff_ne_zero as pos_iff_ne_0, add_zero } from './data/nat/basic.js';

And it will not import other useless variables.

[Jannis Limperg]

I asked a similar question recently and the answer is no, you unfortunately can't. Possible workaround: define your lemmas in a separate namespace.

[ZHAO Jinxiang]

Will lean 4 support this?
This is really helpful for users.

[ZHAO Jinxiang]

Importing Files

Importing is transitive. In other words, if you import foo and foo imports bar, then you also have access to the contents of bar, and do not need to import it explicitly.

This approach ignores encapsulation of module.

---

If library provider import some library like tactic.suggest, it will cause users also import this by accident.

Moreover, if library import other library include some lemma which has the same name with user's lemma, it will cause error.

[Eric Wieser]

I don't think this is all that different to how things work in C - you can define your own printf in main.c, but doing so is a really bad idea, as you'll get linker errors as soon as you pull in any code that uses the real printf.

In my mind the problem is either;

• Mathlib is putting things in the global namespace that it should be putting in a subnamespace (ie, the C++ model)
• Your code is working in the global namespace but should be working in a subnamespace (ie, the java model)

[Kevin Lacker]

c imports are not a great import system, though. more modern programming languages generally do not use the c style import mechanism

[Simon Hudon]

The comparison to the C import model is superficial at best. I think comparing to C#, Haskell or Coq might be more interesting

[Kevin Lacker]

it does work like C though right now, in that when you import something you get a bunch of stuff added to the global namespace

[Kevin Lacker]

the C# model is better - when you do using System; in a C# library it doesn't make the system libraries visible at the top level for libraries that import your library

[Simon Hudon]

The same holds for open in Lean. You open a namespace and its names become available in the enclosing section or namespace. The effect does not extend beyond the current file

[Bryan Gin-ge Chen]

There was a brief discussion about plans for a module system in Lean 4 here.

[Kyle Miller]

@Kevin Lacker Maybe you're saying the .NET approach is better, where almost nothing is put in the global namespace except for some builtins, if I remember correctly. Other than that, I think namespace and open work similarily to namespace and using in C#.

[Kevin Lacker]

I guess the difference is that in c# you can just use using. but in Lean you can't really only use open, in practice there are many files that only work with import. or can you get by with only using open?

[Kyle Miller]

Although, C# doesn't do imports, right? It's up to the "Solution" to link everything together?

[Kevin Lacker]

using in C# is essentially an import

[Eric Wieser]

I think actually C++ is the isomorphic comparison - import is #include, and open is using namespace.

[Kevin Lacker]

yeah I agree - C++ and C have the same #include style

[Kevin Lacker]

but, it does cause problems once codebases get large, which is why C# was basically like "#include is no longer allowed"

[Kyle Miller]

C#'s system allows cyclic dependencies between files, right? The Lean way helps guarantee that doesn't happen, where you curate the list of imports, which is the list of file dependencies for what is being constructed in the given file.

[Kyle Miller]

The Lean module system is very similar to Common Lisp, where there's a mechanism to ensure you've loaded a file, but there is also a cross-cutting mechanism for putting symbols in different "packages" (namespaces).

[Kevin Lacker]

I don't think C# allows circular dependencies but I am not that much of a C# expert

[Simon Hudon]

I believe dafny has a similar approach to import as C# except that it does internally check that definitions do not have cyclical dependencies or, if they do, that they can be treated as a valid mutually recursive definition

[Simon Hudon]

I don't think cyclical definitions in C# are a problem at all unless you have struct mutually reference each other. That's because struct defines value types and those values are not represented as pointers to a chunk of memory that contains values but as the values themselves

[Reid Barton]

Ultimately the issue here is that Lean assumes that every top-level definition has a unique name within a global namespace, and every .lean file can add names arbitrarily to this namespace. In this respect it indeed resembles C, but the ABI more so than the #include mechanism.

[Reid Barton]

Even if there was a way to selectively import dense from order.lean and not topology.lean, say, having both definitions would run afoul of this assumption, which is baked into the way name and environments work.

[Reid Barton]

Other languages have per-module (i.e., file) namespaces, for example, Haskell "foldr in the Data.List module of version 3.4 of the base package", or no global namespace at all (Javascript?)

[Reid Barton]

Separate to this global namespace issue there is the question of manipulating the "identifier environment", i.e., which name a given identifier in a source file will resolve to. For this Lean has the usual open, hiding, renaming etc.

[Reid Barton]

In principle I see no reason why Lean couldn't use a system like Haskell's, with corresponding changes to name. It would certainly make the semantics of name more involved though.

[Yury G. Kudryashov]

I love the fact that we can add lemmas to ring_hom namespace in any file, and access them using dot notation later.

[ZHAO Jinxiang]

TypeScript can add variables to specific namespace in any file using Module Augmentation. And TypeScript is also using per-file module namespace like JavaScript.