Issue with tutorial code

Stream: new members

[Oliver D]

Hello folks!

I think I'm having trouble with my lean4 environment in Visual Studio Code.

The following code-snippet from this tutorial is given me errors:

https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html#getting-started

Here's the Snippet:

example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦

  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]

  show ∃ l, m * n = l + l from ⟨_, hmn⟩

Here are the errors:

function expected at Even
term has type
?m.9

function expected at
Even
term has type
?m.9

Here's my setup information:

Operating system: Windows_NT (release: 10.0.22631)
CPU architecture: x64
CPU model: 16 x 11th Gen Intel(R) Core(TM) i9-11900K @ 3.50GHz
Available RAM: 34.24 GB

Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.1.0-rc1)
Project: No open project

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable
leanprover/lean4:v4.1.0-rc1 (default)


active toolchain
----------------

leanprover/lean4:v4.1.0-rc1 (default)

Lean (version 4.1.0-rc1, commit 339615042d90, Release)

Are these errors sensible? or is there something wrong with my Lean setup?

Any help would be appreciated.

[Ralf Stephan]

Cannot be answered unless you include your import headers, see #mwe.

[llllvvuu]

I assume the issue here is that MIL snippets themselves are not runnable. It looks like they recommend running the MIL repo which probably comes with an environment

EDIT: indeed here it is: https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C01_Introduction/S02_Overview.lean

there is import MIL.Common

That file contains:

import Mathlib.Tactic
import Mathlib.Util.Delaborators

set_option warningAsError false

but I would recommend just running it their way

[Oliver D]

Thanks for the replies!

I had zero imports above the code snippet - I didn't think to include any in my scratchpad, apologies for the stupid question.

Does Visual Studio Code / Lean4 / elan not have support for detecting if an import is missing for a piece of code, or perhaps a primitive object?

[Mark Fischer]

Something that might be a bit confusing when you first start in lean is that if you use an undeclared identifier, Lean may assume that it must be a term and elaborate with an anonymous type.

For example:

def Bar : p → q := sorry
#check Bar -- Bar.{u_1, u_2} {p : Sort u_1} {q : Sort u_2} : p → q

Instead of saying "I don't know what p or q are in this context," leans just says "Cool, these must be terms in some universe of types." and doesn't throw an error.

Which is nice in some cases: for example in the follow the conjunction ∧, it's easy to infer that p and q must be Propositions (terms in Prop) and we can drop the boilerplate.

def Bar : p ∧ q := sorry
#check Bar -- Bar {p q : Prop} : p ∧ q

The issue is that Even has a type like: Nat → Prop, which is not something the elaborator will do for you. You could, for example, get a different error if you include a type for Even

example {Even : Nat → Prop} : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩

but really, you need the definition for Even, which requires the import as you've seen.

---

I suspect in future, the language server may see such errors and be able to suggest possible imports that would fix it. As far as I know, that's not currently a thing.

[Oliver D]

Understood - thanks!

I'm currently in that stage where I'm so new, it's a little harder to distinguish between a setup issue, or a syntax / code issue - I don't have confidence in the installation just yet it seems.

Indeed my problem seemed to have been an import issue - I included the following import:

import Mathlib

It seemed to load the entirety of that package (which took, expectedly, a whole hour or so), and the errors disappeared - I imagine I could have just included the import specific to even and this would have finished MUCH faster.

[Kevin Buzzard]

I would not expect anything to take an hour. If you have a fully compiled mathlib (and you can download compiled binaries using lake exe cache get) then it should just take a few seconds to run import Mathlib.