calc — Calculational Proofs

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]

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

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

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

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

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

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

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

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