Skip to content

Lean 4 survival guide for Lean 3 users

Jump to bottom
Floris van Doorn edited this page May 25, 2023 · 50 revisions

Links

  • [manual] The most important differences with Lean 3 are documented in the Lean 4 manual.

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

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

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

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.

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?

Clone this wiki locally