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

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

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?

Clone this wiki locally