Module 6 · Lesson 1

calc — Calculational Proofs

calc writes a proof as a chain of equalities or inequalities, one step per line, each with its own justification.

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

Try it

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

Try it

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

Try it

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

Try it

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

ℹ

Use calc when the intermediate steps matter to the reader. Each line states where the proof is and why the step holds.

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

Try it

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

Try it

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

Try it

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

aesop Next: conv