Lean 4 survival guide for Lean 3 users

Links

• Lean 4 cheatsheet: https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf
• Differences with Lean 3 from the official Lean 4 manual: https://leanprover.github.io/lean4/doc/lean3changes.html

Syntax changes

• Function notation changed from λ x, f x to fun x => f x or λ x => f x. If you import (almost) any file from mathlib, you can also use 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 }.

• For infix notation like + you cannot use (+) or (+ n) anymore, instead use (· + ·) or (· + n). The · (entered with \., not \cdot) is an anonymous lambda expression. The lambda expression will be inserted at the nearest enclosing parentheses (see linked manual page).
• f $ x has a new notation f <| x (although the old notation still works)

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) 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

• 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.

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.

New features

• Named implicit arguments, like f (x := 3) (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.

How do I do X?

• Metaprogramming works completely differently in Lean 4, see the Lean 4 Metaprogramming book and Functional Programming in Lean.