kuniga.me > Docs > Lean Cheatsheet

Lean Cheatsheet

NOTE: This refers to the community fork of Lean (test with v3.42).

Index

  1. Setup
  2. Syntax
    1. Inductive Type
    2. Function
  3. Inference
  4. Symbols
    1. Subscripts
    2. Arrows
    3. Operators
  5. Tactics
    1. apply
    2. assumption
    3. cases
    4. have
    5. intro
    6. revert
    7. rewrite (rw)
  6. split
  7. Tactic Combinators
    1. repeat
  8. How To?
    1. Assume the left-hand side of an implication in the goal
    2. Bind a value to ∀ in the goal
    3. Bind a value to ∃ in the goal
    4. Bind a value to ∀ in a hypothesis
    5. Bind a value to ∃ in a hypothesis
    6. Split a hypothesis in the form H1 ∧ H2 into two hypothesis
    7. Introduce new hypothesis within a proof
  9. References

Setup

If you already have an existing folder, run this inside the folder.

leanproject new

Syntax

Inductive Type

inductive Nat
| zero : Nat
| succ (n : Nat) : Nat

Function

def inc (x: nat): nat := x + 1

Alternative: pattern matching.

def add : nat → nat → nat
| m 0 := m
| m (succ n) := succ (add m n)

Function Composition.

def inc (x: nat): nat := x + 1
def dbl (x: nat): nat := 2 * x
def f := dbl ∘ inc
#eval f 3 -- prints 8

Inference

Typing an underscore in an expression asks Lean to infer a suitable value for the expression and fill it in automatically.

Symbols

For copy and pasting:

Subscripts

₀ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉

Arrows

←

Operators

∧ -- and

Tactics

apply

Given goal b and hypothesis h: a -> b, apply h turns goal b into a.

assumption

The assumption tactic looks through the assumptions in context of the current goal, and if there is one matching the conclusion, it applies it.

variables x y z w : ℕ

example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w :=
begin
  apply eq.trans h₁, -- y = w
  apply eq.trans h₂, -- z = w
  assumption         -- applied h₃
end

cases

Split a hyposesis of the form a ^ b into two hypothesis a and b.

have

have q := f p, https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=6&level=7

intro

If the current goal is a → b, intro h assumes a is true (adding as hypothesis h) and the goal becomes b.

revert

If there’s a hypothesis h: a → b and the current goal is b, revert h, turns the goal into a → b.

rewrite (rw)

Syntax:

axiom foo : a = b
...
rw foo -- replaces a with b

Example:

axiom add_succ (m n: nat) : m + nat.succ n = nat.succ (m + n)

lemma my_add_assoc (a b c : nat) : (a + b) + c = a + (b + c) :=
begin
  induction c with d hd,
  -- ⊢ a + b + 0 = a + (b + 0)
  rw add_zero,
  -- ⊢ a + b = a + (b + 0)
  rw add_zero,
  -- ⊢ a + b = a + b
  -- ...

end

reversed rewrite.

Replace expr2 with expr1 instead:

Syntax:

axiom foo : a = b
...
rw ←foo -- replaces b with a

rewrite only the n-th match.

Syntax:

nth_rewrite 0 H1,

rewrite multiple hypothesis

Syntax:

rewrite 0 [H1, H2, H1, H3],

split

If the current goal is a ∧ b, split generates 2 goals a and b. (Same as apply and.intro)

Tactic Combinators

repeat

Executes a tactic while it’s applicable. Example:

repeat {rw h}

How To?

Assume the left-hand side of an implication in the goal

If the goal is of the form ⊢ x → y we add x to our hypothesis and prove y:

-- ⊢ x → y
intro h
-- h: x
-- ⊢ y

Bind a value to ∀ in the goal

If the goal is of the form ⊢ ∀ x, f(x) we can bind x to some specific variable y and prove the goal for it:

-- ⊢ ∀ x, f(x)
intro y
-- y
-- ⊢ f(y)

Bind a value to ∃ in the goal

If the goal is of the form ⊢ ∃ x, f(x) we can replace with a specific instance via existsi:

-- ⊢ ∃ x, f(x)
existsi y
-- ⊢ y, f(y)

Bind a value to ∀ in a hypothesis

If we have a hypothesis H: ∀ x, f(x), we can create a new hypothesis binding x with some instance via have Hy := H y:

-- : H: ∀ x, f(x)
have H2 := H y
-- Hy: y, f(y)

Bind a value to ∃ in a hypothesis

If we have a hypothesis H: ∃ x, f(x), we can introduce some y and create a new hypothesis that is H applied to y:

-- : H: ∃ x, f(x)
cases H with y Hy,
-- Hy: y, f(y)
-- y

Split a hypothesis in the form H1 ∧ H2 into two hypothesis

If we have a hypothesis H: H1 ∧ H2, we can get two hypothesis H1 and H2:

-- : H: H1 ∧ H2
cases H with H1 H2,
-- H1
-- H2

Introduce new hypothesis within a proof

We can choose to prove an intermediate result within a proof for better readability/organization.

let H: <Prop>

This adds a new hypothesis H and a new goal to prove that hypothesis. If this proof is long, it might be worth to define an actual lemma.

References