2. Basics

This chapter is designed to introduce you to the nuts and bolts of mathematical reasoning in Lean: calculating, applying lemmas and theorems, and reasoning about generic structures.

2.1. Calculating Proof Steps via Rewriting

2.1.1. Proof State

Lean reports on the current proof state in the Lean Infoview window (click ∀ button on the top-right of VS Code, then “Toggle InfoView”).
Move cursor to see state at each proof step.

1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4

⊢: current proof goal to be proved.
Lines before ⊢: all current context, including objects (x, y), assumptions/hypotheses (h₁, h₂, h₃). Everything in the context is labelled with an identifier.
- Type subscripted labels as h\1, h\2, h\3.

2.1.2. Scope via `section ... end`

We can declare variables once within a scope defined in a section ... end block.

section
variable (a b c : ℝ)

#check a
#check a + b
#check (a : ℝ)
#check mul_comm a b
#check (mul_comm a b : a * b = b * a)
#check mul_assoc c a b
#check mul_comm a
#check mul_comm

end

2.1.3. rw [`thm` arg₁ arg₂]

Use the left-hand side of thm’s identity to match patterns in your current proof goal, and replace matched patterns with the right-hand side of thm.
You can use a left arrow (\l) to reverse an identity (i.e. go from right to left in the thm provided).
- For example, rw [← mul_assoc a b c] replaces a * (b * c) by a * b * c in the current goal.

example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [mul_comm a b]  -- ``mul_comm a b`` implies ``a * b = b * a``
  rw [mul_assoc b a c]  -- ``mul_assoc a b c`` implies ``a * b * c = a * (b * c)``

example (a b c : ℝ) : c * b * a = b * (a * c) := by
  rw [mul_comm c b]
  rw [mul_assoc b c a]
  rw [mul_comm a c]
  -- sorry

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry

If you just use rw [thm] without providing arguments arg₁ arg₂, rw will try to match its left-hand side with the first pattern it can match in the goal.

example (a b c : ℝ) : a * b * c = b * c * a := by
  rw [mul_assoc]
  rw [mul_comm]

You can also provide partial arguments. For example, mul_comm a matches any pattern of the form a * ? and rewrites it to ? * a.

example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
  -- sorry  -- without providing any arguments at all
  rw [mul_comm]
  rw [mul_assoc]


example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry  -- with only one argument

rw can also take facts from the local context.

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h']
  rw [← mul_assoc]
  rw [h]
  rw [mul_assoc]

Multiple rewrite commands can be chained and carried out in a single command, by listing identities separated by commas.

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

Rewrite in a specific assumption via rw [thm arg] at hyp.

example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp'] at hyp
  rw [mul_comm d a] at hyp
  rw [← two_mul (a * d)] at hyp
  rw [← mul_assoc 2 a d] at hyp
  exact hyp  -- ``hyp`` matches the goal exactly

nth_rw : replace only particular instances of an expression in the goal. Possible matches are enumerated starting with 1.

example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
  nth_rw 2 [h]  -- replaces the second occurrence of ``a + b`` with ``c``
  rw [add_mul]

2.1.4. calc (Proof Term)

Chained rw could make the proof progress hard to read:

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  rw [mul_add, add_mul, add_mul]  -- distributivity of multiplication over addition
  rw [← add_assoc, add_assoc (a * a)]  -- associativity of addition
  rw [mul_comm b a, ← two_mul]  -- ``2 * a = a + a``

Lean provides a more structured way of writing proofs using the calc proof term.
calc is not a tactic: no need by after :=.
Lean uses indentation to determine the begin and end of a block (tactics, calc, etc.).

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      rw [mul_add, add_mul, add_mul]
    _ = a * a + (b * a + a * b) + b * b := by  -- _ is a placehold for the RHS in previous step
      rw [← add_assoc, add_assoc (a * a)]
    _ = a * a + 2 * (a * b) + b * b := by
      rw [mul_comm b a, ← two_mul]

calc helps first outline with sorry, then justify individual steps using tactics.

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      sorry
    _ = a * a + (b * a + a * b) + b * b := by
      sorry
    _ = a * a + 2 * (a * b) + b * b := by
      sorry

2.2. Proving Basic Identities in Ring Algebraic Structure

2.2.1. Namespace

When a definition or theorem foo is introduced in a namespace bar, its full name is bar.foo.
open bar later opens the namespace and allows us to use the shorter name foo.

namespace MyRing
variable {R : Type*} [Ring R]

theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]

theorem add_neg_cancel (a : R) : a + -a = 0 := by rw [add_comm, neg_add_cancel]

#check MyRing.add_zero
#check add_zero

end MyRing

#check add_zero

2.2.2. Implicit and Explicit Arguments

“Parentheses” (R : Type*) — explicit parameter; you must supply R when you use the enclosing definition.

def idR (R : Type*) (x : R) : R := x
#check idR Nat 3                   -- R given positionally
#check idR (List String) ["hi"]    -- R given positionally
#check idR (R := Nat) 3            -- R given by name (same effect)

“Curly Braces” {R : Type*} — implicit parameter; Lean will try to infer it from later arguments.

def dup {R : Type*} (x : R) : R × R := (x, x)

#check dup 5                       -- infers R = Nat
#check dup (R := String) "hi"      -- give the implicit explicitly

“Square brackets” [Ring R] — instance-implicit; Lean must find via type-class search.

-- needs +, *, 0, 1, etc., so we ask for a (semi)ring instance
def square {R : Type*} [Semiring R] (x : R) : R := x * x

#check square 5                    -- R = Nat; uses the built-in Semiring Nat
#check square (R := Int) 7         -- pick the type; instance found automatically

-- If Lean can't find an instance, provide one locally:
section
  structure Weird where n : Nat
  instance : Semiring Weird := by
    sorry
  #check square (R := Weird) ⟨3⟩
end

2.2.3. Ring and ring

Ring consists of: a collection of objects \(R\), operations \(+\) \(\times\), constants \(0\) \(1\), and the negation operation \(x \mapsto -x\) such that:

\(R\) with \(+\) is an abelian group, with \(0\) as the additive identity and negation as inverse.
Multiplication is associative with identity \(1\), and multiplication distributes over addition.

If we define a collection of objects of a type R and a generic ring structure on R, the ring axioms are as follows:

variable (R : Type*) [Ring R]

#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (neg_add_cancel : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)

Any theorem about rings can be applied to concrete rings (e.g. integers, ℤ, rational numbers, ℚ, complex numbers ℂ), and any instance of an abstract structure that extends rings (e.g. any ordered ring or any field).

ring tactic proves equivalence b/w LHS and RHS by operations supported by Ring.
- The ring tactic is imported indirectly when we import Mathlib.Data.Real.Basic. It can be imported explicitly with the command import Mathlib.Tactic.

If we further declare R to be a commutative ring via CommRing, then we can support commutative multiplication on ℝ:

variable (R : Type*) [CommRing R]
variable (a b c d : R)

example : c * b * a = b * (a * c) := by ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring

Here is a useful theorem:

theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by
  rw [← add_assoc, neg_add_cancel, zero_add]

Prove the companion version:

theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
  sorry

Use these to prove the following:

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
  sorry

theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
  sorry

2.2.4. have

have introduce a new (intermediate, auxiliary) hypothesis h during the proof
- After we prove this intermediate hypothesis, we can feel free to use it for further proofs

let us show that a * 0 = 0 follows from the ring axioms.

theorem mul_zero (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by  -- ``have`` introduce a new (intermediate) hypothesis h
    rw [← mul_add, add_zero, add_zero]  -- indentation: sub-proof for the new goal.
  -- we now feel free to use h
  rw [add_left_cancel h]  -- ``apply add_left_cancel h`` or ``exact add_left_cancel h`` also works

theorem zero_mul (a : R) : 0 * a = 0 := by  -- multiplication is not assumed to be commutative
  sorry

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  sorry

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
  sorry

theorem neg_zero : (-0 : R) = 0 := by  -- have to distinguish -0 in the arg by specifying its type
  apply neg_eq_of_add_eq_zero
  rw [add_zero]

theorem neg_neg (a : R) : - -a = a := by
  sorry

2.2.5. rfl

In Lean, subtraction in a ring is provably equal to addition of the additive inverse.

example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b

On the real numbers, it is defined that way:

example (a b : ℝ) : a - b = a + -b := by
  rfl

The proof term rfl is short for “reflexivity”. The rfl tactic forces Lean to unfold the definition and recognize both sides as being the same, i.e. definitional equality.

2.3. Using Theorems and Lemmas

2.3.1. apply

Consider the library theorems le_refl and le_trans:

#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)  -- should be interpreted as ``a ≤ b → (b ≤ c → a ≤ c)``
-- P → Q → R means P → (Q → R), i.e., a function taking a proof of P and returning a function that,
-- given a proof of Q, produces a proof of R

The apply tactic: 1) takes a statement as the argument; 2) tries to match the statement’s conclusion with your current goal; 3) leaves the hypotheses, if any, as new goals.
If the given proof matches the goal exactly (modulo definitional equality), you can use the exact tactic instead of apply.

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans  -- leaves two goals
  -- · “start to focus on a new tactic block for the next goal”
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans h₀
  apply h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

Here are a few more library theorems:

#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)

Use them together with apply and exact to prove the following:

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  sorry

2.3.2. linarith

linarith can prove the problem above automatically using equations and inequalities in the context by linear arithmetic:

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  linarith

example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by
  linarith

linarith can also use additional inequalities passed as arguments (see the example below).

2.3.3. Bi-Implication

example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
  -- exp_le_exp: rexp x ≤ rexp y ↔ x ≤ y
  linarith [exp_le_exp.mpr h']  -- .mpr (“modus ponens reverse”) is a function derived

Some theorems like exp_le_exp, exp_lt_exp use a bi-implication, implying “if and only if” (\lr or \iff).
h.mp establishes the forward direction, A → B, and h.mpr establishes the reverse direction, B → A.
- mp stands for “modus ponens” and mpr stands for “modus ponens reverse.”
- You can also use h.1 and h.2 for h.mp and h.mpr.

example (h : a ≤ b) : exp a ≤ exp b := by
  rw [exp_le_exp]
  exact h

Here are some more theorems in the library that can be used to establish inequalities on the real numbers.

#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → a ≤ b → log a ≤ log b)
-- #check (log_lt_log : 0 < a → a < b → log a < log b)
-- #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
-- #check (add_le_add_right : a ≤ b → ∀ c, a + c ≤ b + c)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d)
-- #check (add_lt_add_left : a < b → ∀ c, c + a < c + b)
-- #check (add_lt_add_right : a < b → ∀ c, a + c < b + c)
-- #check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
-- #check (add_pos : 0 < a → 0 < b → 0 < a + b)
-- #check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
-- #check add_le_add_left

Thus the following proof works:

example (h₀ : a ≤ b) (h₁ : c < d) : a + exp c + e < b + exp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
    apply exp_lt_exp.mpr h₁
  apply le_refl

2.3.4. norm_num

norm_num tactic can be used to solve concrete numeric goals.

example : (0 : ℝ) < 1 := by norm_num  -- ``norm_num`` tactic can solve concrete numeric goals

2.3.5. Search Mathlib Statements

example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry

example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
  have h₀ : 0 < 1 + exp a := by sorry
  apply log_le_log h₀
  sorry

As you meet more complex problems, you will find it necessary to search library theorems instead of always memorizing them. There are a number of strategies you can use:

Search box on Mathlib documentation web pages.
Loogle and Lean Finder to search Lean and Mathlib definitions and theorems by patterns.
You can use the apply? tactic, which tries to find the relevant theorem in the library.

example : 0 ≤ a ^ 2 := by
  -- apply?
  exact sq_nonneg a

To try out apply? in this example, delete the exact command and uncomment the previous line. Using these tricks, see if you can find what you need to do the next example:

example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  refine tsub_le_tsub ?_ ?_
  -- sorry

2.4. min, max, ∣, .gcd, .lcm

2.4.1. min, max

The min function on the real numbers is uniquely characterized by the following three facts:

#check (min_le_left a b : min a b ≤ a)
#check (min_le_right a b : min a b ≤ b)
#check (le_min : c ≤ a → c ≤ b → c ≤ min a b)

min is a function of type ℝ → ℝ → ℝ and is interpreted as ℝ → (ℝ → ℝ).
- min a has type ℝ → ℝ and min a b has type ℝ
- Function application binds tighter than infix operations: min a b + c is interpreted as (min a b) + c.

example : min a b = min b a := by
  apply le_antisymm  --  two real numbers are equal if each is less than or equal to the other
  · show min a b ≤ min b a  -- ``show`` t finds the first goal whose target unifies with t, such that to indicate what is being proved in each block
    apply le_min
    · apply min_le_right
    apply min_le_left
  · show min b a ≤ min a b
    apply le_min
    · apply min_le_right
    apply min_le_left

2.4.2. Divisibility ∣

a ∣ b (typed as |) “a divides b” means that there exists some c such that b = a * c

example (h₀ : x ∣ y) (h₁ : y ∣ z) : x ∣ z :=
  dvd_trans h₀ h₁

example : x ∣ y * x * z := by
  apply dvd_mul_of_dvd_left
  apply dvd_mul_left

2.4.3. .gcd, .lcm

With respect to divisibility, the greatest common divisor, gcd, and least common multiple, lcm, are analogous to min and max. Since every number divides 0, 0 is really the greatest element with respect to divisibility:

variable (m n : ℕ)

#check (Nat.gcd_zero_right n : Nat.gcd n 0 = n)
#check (Nat.gcd_zero_left n : Nat.gcd 0 n = n)
#check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0)
#check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0)