Lean 4 survival guide for Lean 3 users

Links

• [manual] The most important differences with Lean 3 are documented in the Lean 4 manual.
• The porting wiki has various tips

Syntax changes

• Function notation changed from λ x, f x to fun x => f x or λ x => f x or fun x ↦ f x or λ x ↦ f x.
• Π x : A, P x is not legal anymore. Use ∀ x : A, P x or (x : A) → P x
• For structures, { field1 := value1, field2 := value2, ..parent1, ..parent2 } is now entered as

{ parent1,
  parent2 with 
  field1 := value1
  field2 := value2 }

If you have no additional fields, this becomes { parent1, parent2 with }.

• Pattern matching notation is different, you can use the following examples. Note the use of => instead of := (you cannot use ↦ here) and that there is no end ending a match.

def Option.str1 : Option Nat → String
  | some a => "some " ++ toString a
  | none   => "none"

def Option.str2 (x : Option Nat) : String :=
  match x with
  | some a => "some " ++ toString a
  | none   => "none"

def Option.str3 : Option Nat → String :=
  fun
    | some a => "some " ++ toString a
    | none   => "none"

• For infix notation like + you cannot use (+) or (+ n) anymore, instead use (· + ·) or (· + n). The · (entered with \., not \cdot) is an implicit lambda expression. The lambda expression will be inserted at the nearest enclosing parentheses (see [manual]).
• f $ x has a new notation f <| x (although the old notation still works).
• Lean is whitespace sensitive. This generally means that you end a multi-line command (like by, do, match, the tactic mode ·, ...) by unindenting the first line after the command.

example : (True → p) → q → p ∧ q := by
  intros hp hq
  constructor
  · apply hp
    trivial
  exact hq

In the above example the last line is not in scope of the · anymore, since it is indented less than the line above it. This tactic block would raise an error if you add two additional spaces in front of the last line.

• The new calc-block notation is

calc
  A = B := proof1
  _ = C := proof2

Note that this is whitespace-sensitive!

• To define a term my_term of a structure Struc that expands other structures, say preStruct_1, preStruct_2 and preStruct_3 each with the corresponding constructors preStruct_i.mk, VSCode still proposes to build a skeleton of the structure under consideration. This gets totally unfolded, so if preStruc_1 was itself extending several other structures, each with constructors mk_11, mk_12, ... mk_13, all the fields mk_1i appear and need to be filled. In order to directly pass a term of type preStruct_1, the new equivalent of the old syntax {Struct:= _, ..preStruct_1} is now

my_term : Struct A where
   preStruct_2.mk := proof1
   preStruct_3.mk := proof2
   __ : preStruct_1 := proof3

The final line starts with two underscores (and no space between them) and if the type preStruct_1 can be inferred by proof3, then the type-specification can be omitted.

Tactic changes

Tactic block changes

• Enter tactic mode by using by and then a newline, and indenting the tactics. Example:

example : True := by
  trivial

• Don't place comma's after tactics, you can go to the next tactic if you write it on a new line (in the same column)
• If you have multiple goals, you can work on the first goal using · <tactics> instead of {<tactics>}. Note that · is \., not \cdot.

example : (True → p) → q → p ∧ q := by
  intros hp hq
  constructor
  · apply hp
    trivial
  · exact hq

• If you want multiple tactics on the same line, you can use tac1; tac2 (which corresponds to tac1, tac2 in Lean 3) or tac1 <;> tac2 (which corresponds to tac1; tac2 in Lean 3)
• Certain new Lean 4 tactics (like refine and calc) treat _ and ?_ differently. _ should be used for implicit arguments that can be figured out by the elaborator. ?_ should be used for underscores that produce a new subgoal. You can name these subgoals using ?myName instead of ?_.

Specific tactic changes

Here is a list of tactic translations from Lean 3 to Lean 4.

• Lean 3's refine is Lean 4's refine'.
• Lean 3's cases is Lean 4's cases'.
• Lean 3's induction is Lean 4's induction'.
• The square brackets in rw [h] are mandatory.
• split has been removed. Use constructor.

Misc changes

• @[simp, priority 100] is replaced by @[simp 100]. Note: you can also do @[simp low] or @[simp high].
• open_locale foo is (roughly) replaced by open scoped Foo

Naming Conventions

(This list is taken from the porting wiki. The instructions there might be more up to date in certain edge cases. There are also some examples on that page.)

1. Terms of Props (e.g. proofs, theorem names) are in snake_case.
2. Props and Types (or Sort) (inductive types, structures, classes) are in UpperCamelCase.
3. Functions are named the same way as their return values (e.g. a function of type A → B → C is named as though it is a term of type C).
4. All other terms of Types (basically anything else) are in lowerCamelCase.
5. When something named with UpperCamelCase is part of something named with snake_case, it is referenced in lowerCamelCase.
6. Acronyms like LE are written upper-/lowercase as a group, depending on what the first character would be.
7. Rules 1-6 apply to fields of a structure or constructors of an inductive type in the same way.

There are some rare counter-exceptions to preserve local naming symmetry: e.g., we use Ne rather than NE to follow the example of Eq; outParam has a Sort output but is not UpperCamelCase; etc. Any such counter-exceptions should be discussed on Zulip.

Pitfalls

• If you write a name in the type of a declaration that does not mean anything (is not a declaration name or a variable), then it is assumed to be a fresh variable of unknown type, and added as argument to the declaration. In the next example a is interpreted as a variable of type Nat.

example : a + 3 = 3 + a := by rw [Nat.add_comm]

This can be a problem if you make a mistake in a name, now it is interpreted as a fresh variable. Remark: A variable like this will be colored differently than a declaration, but you might need a high-contrast color scheme to see the difference. You can disable this behavior using set_option autoImplicit false.

• In Lean 4 all variables are included in the context for a declaration (including named instances - which were not automatically included in Lean 3). This means that the commands include and omit are also removed. After elaborating the declaration, Lean checks which variables are actually used, and only turns the variables that are actually used into arguments. This can cause a few issues:
  • the goal state might be cluttered by variables that are not actually arguments of the current declaration
  • the induction tactic generalizes all variables in the local context. This means that all the variables will therefore occur in the proof term, even though they are not actually used in the declaration. You can work around this by using clear on all variables that you don't want before the induction tactic.

New features

• Named implicit arguments, like f (x := 3) a. This can be used instead of something like @f _ _ _ 3 _ _ _ a (see [manual])
• f .. for multiple unnamed arguments (see [manual])
• #align is a command to connect Lean 3 names to Lean 4 names, used by mathport. They will be deleted from mathlib at some point after the port is finished.
• You can generally hover over more declarations/commands/... to get a pop-up with information. You can also jump to more definitions and notation (using F12). Note that when right-clicking on a declaration you can both "go to definition" and "go to declaration".

How do I do X?

• Metaprogramming works completely differently in Lean 4, see the Lean 4 Metaprogramming book, Functional Programming in Lean and meta4dummies.
• How to declare notation? [todo]

Cache

• What used to be called leanproject get-cache is now lake exe cache get. This downloads as many ready-made "olean" files as possible from the so-called "cache" on Github. This makes building on your own computer go much faster.
• If you think something might have gone wrong while downloading the cache (for example if things are suddenly very slow), try running lake exe cache get!. The exclamation mark forces Lean to (re)download the entire cache.