Module 6 · Lesson 1

calc — Calculational Proofs

calc enables step-by-step proofs that chain equalities and relations, making complex proofs readable and natural.

Basic Equality Chains

calc chains a sequence of equalities. Each step transforms the expression, and Lean verifies that the steps are valid. The result is a proof that reads like a mathematical calculation on paper.

lean

1example (a b c : Nat) : (a + b) + c = (c + b) + a := calc
2  (a + b) + c = (b + a) + c := by rw [Nat.add_comm a b]
3  _ = c + (b + a) := by rw [Nat.add_comm]
4  _ = c + (a + b) := by rw [Nat.add_comm a b]
5  _ = (c + a) + b := by rw [Nat.add_assoc]
6  _ = (a + c) + b := by rw [Nat.add_comm c a]
7  _ = a + (c + b) := by rw [Nat.add_assoc]
8  _ = a + (b + c) := by rw [Nat.add_comm c b]
9  _ = (b + c) + a := by rw [Nat.add_comm]
10  _ = (c + b) + a := by rw [Nat.add_comm b c]

Each _ refers to the previous line's right-hand side. This makes chains easy to write: each step picks up where the last left off.

Key Takeaway

calc makes proofs look like paper calculations. Each step justifies one transformation, and the chain combines them.

Using Automation

You can use any tactic to justify a calc step. Use ringfor polynomial identities, omega for integer arithmetic, and simp for definitional simplifications.

lean

1-- calc with ring, omega, simp
2example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := calc
3  (a + b)^2 = (a + b) * (a + b) := by ring
4  _ = a*a + a*b + b*a + b*b := by ring
5  _ = a^2 + 2*a*b + b^2 := by ring
6
7-- Or just one step with ring
8example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring
9
10-- calc is for when you want to show the reasoning
11example (n : Nat) (h : n > 5) : n + 10 > 15 := calc
12  n + 10 > 5 + 10 := by omega
13  _ = 15 := by rfl
14  _ ≥ 15 := by omega

Mixed Relations

calc can chain different relations as long as they're transitive together:

lean

1-- Mix = with ≤ and <
2example (a b c d : Nat) (h1 : a = b) (h2 : b < c) (h3 : c ≤ d) 
3    : a < d := calc
4  a = b := h1
5  _ < c := h2
6  _ ≤ d := h3
7
8-- The chain uses transitivity: a = b < c ≤ d implies a < d
9
10-- Mix = with ≠
11example (a b : Nat) (h : a = b + 1) : a ≠ b := calc
12  a = b + 1 := h
13  _ ≠ b := by omega

Justifications

lean

1-- Various ways to justify steps
2example (a b c : Nat) (h : a = b) : a + c = b + c := calc
3  a + c = b + c := by rw [h]
4
5example (a b c : Nat) (h : a = b) : a + c = b + c := calc
6  a + c = b + c := congrArg (· + c) h
7
8-- Direct application of lemmas
9example (a b : Nat) : a + b = b + a := calc
10  a + b = b + a := Nat.add_comm a b

Deep Dive: How calc Works

calc is syntax sugar that builds a chain of transitivity proofs:

lean

1-- This calc:
2example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := calc
3  a = b := h1
4  _ = c := h2
5
6-- Is equivalent to:
7example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c :=
8  Eq.trans h1 h2
9
10-- For inequalities, it uses the appropriate transitivity lemma

calc in Tactic Mode

lean

1-- calc can appear inside by blocks
2example (a b c : Nat) (h1 : a < b) (h2 : b ≤ c) : a < c := by
3  calc a < b := h1
4       _ ≤ c := h2
5
6-- Or as part of a larger proof
7example (n : Nat) (h : n > 0) : 2 * n > 0 := by
8  have step1 : 2 * n ≥ 2 * 1 := by omega
9  calc 2 * n ≥ 2 * 1 := step1
10       _ = 2 := by ring
11       _ > 0 := by omega

Readable Proof Style

lean

1-- calc for readable proofs
2theorem sum_first_n (n : Nat) : 2 * (Finset.range (n + 1)).sum id = n * (n + 1) := by
3  induction n with
4  | zero => simp
5  | succ k ih =>
6    calc 2 * (Finset.range (k + 2)).sum id 
7        = 2 * ((Finset.range (k + 1)).sum id + (k + 1)) := by simp [Finset.sum_range_succ]
8      _ = 2 * (Finset.range (k + 1)).sum id + 2 * (k + 1) := by ring
9      _ = k * (k + 1) + 2 * (k + 1) := by rw [ih]
10      _ = (k + 1) * (k + 2) := by ring

ℹ

calc shines in mathematical proofs where showing your work matters. It's self-documenting—each step explains itself.

Examples

Arithmetic Simplification

lean

1example (x : Int) : (x + 1) * (x - 1) = x^2 - 1 := calc
2  (x + 1) * (x - 1) = x*x - x + x - 1 := by ring
3  _ = x*x - 1 := by ring
4  _ = x^2 - 1 := by ring

Inequality Chain

lean

1example (a b c : Nat) (h1 : a ≤ 2*b) (h2 : b ≤ c + 1) (h3 : c ≤ 5) 
2    : a ≤ 12 := calc
3  a ≤ 2*b := h1
4  _ ≤ 2*(c + 1) := by omega
5  _ ≤ 2*(5 + 1) := by omega
6  _ = 12 := by rfl

Equivalence Steps

lean

1example (P Q R : Prop) (h1 : P ↔ Q) (h2 : Q ↔ R) : P ↔ R := calc
2  P ↔ Q := h1
3  _ ↔ R := h2

Exercise: Short calc Chain

Write a short calc proof that uses one lemma and finishes with rfl.

lean

1example (a b : Nat) : a + b = b + a := calc
2  a + b = b + a := by rw [Nat.add_comm]

aesop Next: conv