Basic import issues + advice

Stream: new members

[Bernardo Anibal Subercaseaux Roa]

Hi everyone! I've tried Lean on and off and something that has bugged me several times is the import system. Here's the case I just ran into today. My goal is to receive feedback/ideas on how a noobie like me should be thinking about imports.

1) I created a new project following https://leanprover-community.github.io/install/project.html#creating-a-lean-project, after updating everything.

2) The tutorial shows as an example to test that the following works:

// Test.lean
import Mathlib.Topology.Basic

#check TopologicalSpace

and indeed that works for me.
3) Now I wanted to do a small example of my own:

// Test.lean
def foo (x: ℤ) : ℤ := 3*x^2 + 7

example : ∀ x : ℤ, foo x ≥ 7 := by
  sorry

but this fails with failed to synthesize HMul Nat ℤ ?m.99, which I take as roughly: I need to import the basic integer things. I try adding as first line
import Mathlib.Data.Int.Basic but that fails with

stderr:
✖ [2/3] Running Mathlib.Data.Int.Basic
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Data/Int/Basic.lean
✖ [3/3] Running imports (/Users/bsuberca/School/mylean/mylearning/Mylearning/Test.lean)
error: /Users/bsuberca/School/mylean/mylearning/Mylearning/Test.lean: bad import 'Mathlib.Data.Int.Basic'
Some required builds logged failures:
- Mathlib.Data.Int.Basic
- imports (/Users/bsuberca/School/mylean/mylearning/Mylearning/Test.lean)
error: build failed

even though it seems to be an actual file in Mathlib (https://github.com/leanprover/lean4/blob/master/src/Init/Data/Int/Basic.lean) and I should have an up to date version of Mathlib by having followed the tutorial.

Using VS Code autocomplete (not the LLM based, just the deterministic list), I see that import Mathlib.Data.Int.Defs exists, and importing that makes the code run.
At this point I have no idea if that is actually what I should be importing or not… But I keep going…

4) I try to write the trivial proof

example : ∀ x : ℤ, foo x ≥ 7 := by
  intro x
  simp [foo] // after this the goal is 7 ≤ 3 * x ^ 2 + 7
  apply Int.le_add_of_nonneg_left // 0 ≤ 3 * x ^ 2
  apply Int.mul_nonneg // 0 ≤ 3  and then 0 ≤  x ^ 2
  simp

at which point my goal is

x : ℤ
⊢ 0 ≤ x ^ 2

I look up the lemma guessing its name and I see that sq_nonneg exists in Mathlib/Algebra/GroupPower/Order.lean. So I try adding import Mathlib.Algebra.GroupPower.Order, which also fails with the same error: no such file or directory (error code: 2). Based on VS Code I try import Mathlib.Algebra.Algebra.Basic, but now there’s an error on the line apply Int.le_add_of_nonneg_left; this import has changed the goal after line simp [foo] to just 0 ≤ 3 * x ^ 2. So I delete the apply Int.le_add_of_nonneg_left line, and now see that sq_nonneg doesn’t seem to be imported through import Mathlib.Algebra.Algebra.Basic anyway. Following another VSCode suggestion, I use import Mathlib.Algebra.Order.Algebra. Now actually the state after simp [foo] is directly 0 ≤ x ^ 2, so I have to remove another line, and now finally sq_nonneg works :smile:

How can I do better at imports? Is there a way see what particular things are being done by simp (or other tactics) based on my imports? How awful is it if I just start doing import Mathlib for my projects? Is there some reasonable middle ground?

[Ruben Van de Velde]

Please fix your backticks :)

[Ruben Van de Velde]

It's an option to use import Mathlib, and then if you like you can use #min_imports at the end of your file to reduce back to what you need

[Ruben Van de Velde]

(Looks like Mathlib.Data.Int.Basic existed but was removed in #11924)

[Bernardo Anibal Subercaseaux Roa]

Thanks! #min_imports looks great! :) it also outputs what the import is, which is very helpful!

[Bernardo Anibal Subercaseaux Roa]

Unfortunately, it doesn't seem to be true that the output of #min_imports gives back something sufficient. In this case it just gives me back import Mathlib.Algebra.Group.Int.Defs, which is not enough for the sq_nonneg to work. At the end I found that import Mathlib.Algebra.Order.Algebra is enough to make things work...

[Ruben Van de Velde]

It's not entirely accurate, unfortunately. If you share the exact code where it has trouble, someone could check if it's a known issue. (Not me though, at least today)