1. Introduction

1.1. Getting Started

1.2. Overview

1.2.1. Types

  • Lean is a formal language uses dependent type theory.

  • Every expression has a type

    • use #check to print it.

    • use #eval to do the calculation.

Some typical types:

  • Prop: propositions, e.g. def, example, ... = ..., regardless of the correctness.

  • A proof (theorem) is of the type of its own proposition.

    • In Lean, proof checking = type checking.

  • Type / Type u: user-defined data structures, u is the level.

#check 2 + 2

#eval 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
-- conceptually, you can replace ``FermatLastTheorem`` using the definition above,
-- i.e. unfold ``FermatLastTheorem``'s definition.
  sorry

#check hard

1.2.2. Common Keywords to Define Types

  • def: Define a semi-reducible data / functions / propositions, executable named value.

    • By default, Lean will unfold def whenever you use it; except for expensive tactics like simp.

    • @[irreducible] to force fold

Syntax:

def [name] ([arg₁] : [Type₁]) ([arg₂] : [Type₂]) : [ReturnType] :=
  [definition_body]

Examples:

def Sum' := Nat.add     -- semireducible
@[irreducible] def Tally := Nat.add

example (x y : Nat) : Sum' x y = x + y := by  -- semireducible unfolds by defeq
  rfl                                         -- OK via definitional equality

-- But irreducible will *not* unfold def:
-- example (x y : Nat) : Tally x y = x + y := by rfl  -- fails

example (x y : Nat) : Tally x y = x + y := by
  -- Explicitly ask to unfold:
  simp [Tally]  -- works

  • theorem / lemma: Define named propositions and proofs; Syntactic sugar for a non-computable def whose type is a Prop, provided with a proof.

    • Lean tags proofs irreducible so proofs are fold.

Syntax:

theorem [name]
([arg₁] : [Type₁]) ([arg₂] : [Type₂])
([hyp₁] : [Proposition₁]) ([hyp₂] : [Proposition₂]) : [conclusion] := by
  [tactic-style proof steps]

  • example: unnamed functions or values for tutorial / exercises.

  • instance: declare that a particular type implements a typeclass, e.g., an instance of a data structure.

1.2.3. Proofs

Example: a proof of the fact that if n is even then so is m * n.

Tactic-style proof:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Say `m` and `n` are natural numbers, and assume `n = 2 * k`.
  rintro m n ⟨k, hk⟩
  -- We need to prove `m * n` is twice a natural number. Let's show it's twice `m * k`.
  use m * k
  -- Substitute for `n`,
  rw [hk]
  -- and now it's obvious.
  ring

Term-style proof:

example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  -- ⟨ ⟩ unpack the existential statement
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩ -- "show Goal from Proof"
  -- "_" will be automatically inferred by Lean as "m * k"