Proof Techniques

Why Engineers Prove Things

A proof is a chain of reasoning that takes you from things you already accept to a conclusion that, by the rules of logic, must therefore hold. It looks like a math exercise. It functions, for working software engineers, like a debugger that runs over every possible input at once. When Donald Knuth quipped, "beware of bugs in the above code; I have only proved it correct, not tried it," he wasn't belittling proofs — he was pointing out that the only thing better than testing on a million inputs is reasoning that closes the door on the other infinity.

The skills in this section are not optional ornaments. They show up directly as code:

The bridge: a loop invariant is mathematical induction in disguise. A termination argument is well-founded recursion in disguise. A type checker is a tiny automated theorem prover. Whenever you write code that must be correct on inputs you have not seen, you are doing proof work whether or not you call it that.

Direct Proof

A direct proof of $P \Rightarrow Q$ assumes $P$ and uses definitions and previously established facts to derive $Q$. There is no rhetorical trick — you simply walk forward.

Worked example: if $n$ is odd, then $n^2$ is odd

Definition. An integer $n$ is odd iff there exists an integer $k$ with $n = 2k + 1$.

Proof. Assume $n$ is odd. Then $n = 2k + 1$ for some integer $k$. Squaring, $n^2 = (2k+1)^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$. Let $m = 2k^2 + 2k$; $m$ is an integer because integers are closed under addition and multiplication. Therefore $n^2 = 2m + 1$, which is the definition of odd. $\blacksquare$

Proof by Contrapositive

The contrapositive of $P \Rightarrow Q$ is $\neg Q \Rightarrow \neg P$. The two are logically equivalent — proving one proves the other. Sometimes the contrapositive is dramatically easier because $\neg Q$ gives you a concrete object to manipulate.

Worked example: if $n^2$ is even, then $n$ is even

Trying to prove this directly is awkward (square roots are not friendly over the integers). Contrapositive: if $n$ is odd, then $n^2$ is odd — which is exactly what we just proved. Done. $\blacksquare$

Proof by Contradiction

Assume the conclusion is false, derive a contradiction, conclude the conclusion is true. The technique is so old it has a Latin name: reductio ad absurdum.

Worked example 1: $\sqrt{2}$ is irrational

Suppose, for contradiction, that $\sqrt{2} = p/q$ with $p, q$ integers having no common factor (we may always reduce to lowest terms). Then $2q^2 = p^2$, so $p^2$ is even, so $p$ is even (by contrapositive above), so $p = 2r$ for some integer $r$. Substituting, $2q^2 = 4r^2$, so $q^2 = 2r^2$, so $q$ is also even. But then $p$ and $q$ share the factor 2 — contradicting our choice of lowest terms. $\blacksquare$

Worked example 2: there are infinitely many primes (Euclid)

Suppose, for contradiction, that the primes are exactly $p_1, p_2, \ldots, p_n$. Form $N = p_1 p_2 \cdots p_n + 1$. $N$ is greater than every $p_i$, so it is not in our list. Yet every integer $> 1$ has a prime factor. That factor divides $N$, but each $p_i$ divides $p_1 \cdots p_n$ and hence leaves remainder 1 when dividing $N$. So $N$ has a prime factor not on the list — contradiction. $\blacksquare$

Sketch: the halting problem is undecidable

Suppose, for contradiction, a program $H(P, x)$ exists that returns true iff program $P$ halts on input $x$. Build the diagonal program D(P): if H(P, P) returns true, loop forever; else halt. Now ask: does D(D) halt? If yes, $H(D, D)$ said yes, so D loops — contradiction. If no, $H(D, D)$ said no, so D halts — contradiction. The assumption was wrong; $H$ cannot exist. $\blacksquare$

Mathematical Induction

Induction is the workhorse of algorithm correctness. To prove $P(n)$ for every integer $n \ge n_0$:

1. Base case. Show $P(n_0)$ directly.
2. Inductive hypothesis. Assume $P(k)$ for an arbitrary $k \ge n_0$.
3. Inductive step. Using only the hypothesis and definitions, prove $P(k+1)$.

Picture an infinite line of dominoes: the base case knocks the first one over; the inductive step says each domino topples its neighbor; together every domino falls.

Worked example 1: Gauss's sum, $\sum_{i=1}^{n} i = \frac{n(n+1)}{2}$

Base. For $n = 1$, the LHS is 1 and the RHS is $\frac{1 \cdot 2}{2} = 1$. Match.

Hypothesis. Assume $\sum_{i=1}^{k} i = \frac{k(k+1)}{2}$.

Step. Then $\sum_{i=1}^{k+1} i = \sum_{i=1}^{k} i + (k+1) = \frac{k(k+1)}{2} + (k+1) = \frac{k(k+1) + 2(k+1)}{2} = \frac{(k+1)(k+2)}{2}$, which is the $n = k+1$ case. $\blacksquare$

Worked example 2: $2^n > n$ for all $n \ge 1$

Base. $2^1 = 2 > 1$. Holds.

Hypothesis. Assume $2^k > k$.

Step. $2^{k+1} = 2 \cdot 2^k > 2k = k + k \ge k + 1$, where the last inequality uses $k \ge 1$. So $2^{k+1} > k+1$. $\blacksquare$

Strong Induction

Sometimes "$P(k) \Rightarrow P(k+1)$" is too narrow a step — you need to lean on multiple smaller cases. Strong induction lets you assume $P(j)$ for every $n_0 \le j \le k$ when proving $P(k+1)$. Logically it is equivalent to ordinary induction; tactically it is much more powerful.

Worked example: every integer $n \ge 2$ has a prime factorization

Base. $n = 2$ is prime; the "factorization" is just $2$.

Hypothesis. Assume every integer $j$ with $2 \le j \le k$ has a prime factorization.

Step. Consider $k+1$. If $k+1$ is prime, we are done. Otherwise $k+1 = a \cdot b$ with $2 \le a, b \le k$. By the strong hypothesis, both $a$ and $b$ have prime factorizations; concatenating them gives one for $k+1$. $\blacksquare$

Structural Induction

When the objects you reason about are not numbers but recursively-defined structures — lists, trees, expressions, programs — ordinary induction on size is awkward. Structural induction matches the structure exactly:

Worked example: a complete binary tree of $n$ nodes has height $\lfloor \log_2 n \rfloor$

Let $h(T)$ denote the height of $T$ (single-node tree has height 0). We prove the equivalent claim: a complete binary tree of height $h$ has between $2^h$ and $2^{h+1} - 1$ nodes; therefore $h = \lfloor \log_2 n \rfloor$.

Base. A single-node tree has height 0 and 1 node; $2^0 = 1 \le 1 \le 2^1 - 1 = 1$. Holds.

Step. Suppose the claim holds for all complete binary trees of height $< h$. A complete tree of height $h$ has root plus two subtrees, each of height $h-1$ (one possibly missing its last level). By the hypothesis, each subtree has between $2^{h-1}$ and $2^h - 1$ nodes, so the whole tree has between $1 + 2 \cdot 2^{h-1} = 2^h + 1$... wait — the lower bound is achieved when the last level has just one node, giving $2^h$ total. The upper bound $1 + 2(2^h - 1) = 2^{h+1} - 1$ matches. Taking logs of $2^h \le n \le 2^{h+1} - 1$ gives $h = \lfloor \log_2 n \rfloor$. $\blacksquare$

Loop Invariants: Induction in Code

A loop invariant is a statement about the program state that is true every time control reaches the loop test. Tony Hoare turned this idea into a method for proving programs correct. Three obligations — an exact mirror of induction:

1. Initialization (base). The invariant holds the first time we reach the loop test.
2. Maintenance (step). If the invariant holds before an iteration, it still holds after.
3. Termination (closing the deal). When the loop exits, the invariant plus the exit condition gives the post-condition we wanted.

Worked example: insertion sort

Invariant: at the start of each iteration with index $i$, the prefix $A[1..i-1]$ is a sorted permutation of the original first $i-1$ elements.

Initialization. Before the first iteration $i = 2$; $A[1..1]$ is a single element, trivially sorted, and trivially a permutation of itself.

Maintenance. The body shifts elements of $A[1..i-1]$ larger than $A[i]$ one position right and inserts $A[i]$ in the gap. The result is a sorted permutation of the original first $i$ elements — the invariant for the next iteration with $i+1$.

Termination. The loop exits at $i = n+1$. The invariant says $A[1..n]$ is a sorted permutation of the original array — precisely the post-condition. $\blacksquare$

Worked example: binary search invariant

Invariant: if the target exists anywhere in the original array, then it lies in the slice $A[\text{lo}..\text{hi}]$.

Initialization. $\text{lo} = 0, \text{hi} = n - 1$ covers the whole array; trivially the target, if present, is in the slice.

Maintenance. We compute $m = \lfloor (\text{lo} + \text{hi})/2 \rfloor$ and compare. If $A[m] = t$ we're done. If $A[m] < t$, the array is sorted, so every index $\le m$ has value $\le A[m] < t$; the target cannot be there, so it must lie in $A[m+1..\text{hi}]$ — updating $\text{lo} \leftarrow m+1$ preserves the invariant. Symmetric argument for $A[m] > t$.

Termination. Each iteration shrinks $\text{hi} - \text{lo}$ by at least 1 (since either $\text{lo}$ jumps past $m$ or $\text{hi}$ falls below $m$). When $\text{lo} > \text{hi}$, the slice is empty; combined with the invariant, the target is not in the array. $\blacksquare$

Interactive: Invariant Inspector

Step through binary search on a sorted array. At every step the cyan band shows the surviving range $A[\text{lo}..\text{hi}]$. The invariant promises that if the target is in the array at all, it is somewhere in cyan. Watch the band shrink; the green panel reaffirms why the invariant still holds.

Try a target that isn't in the array (drag the target slider to a value between two cells). The invariant still holds at every step — right up to the final step where the range becomes empty. That empty range is exactly the proof: the contrapositive form of the invariant says if the target isn't in $A[\text{lo}..\text{hi}]$, then it isn't in the original array. The algorithm correctly returns "not found."

Termination Proofs

Correctness has two parts: partial correctness (if the algorithm halts, the answer is right) and total correctness (it actually halts). Loop invariants buy you the first; you prove the second with a variant: a quantity that

1. takes values in a well-founded set (one with no infinite descending chain — e.g. $\mathbb{N}$),
2. strictly decreases on every iteration / recursive call.

Because the values are bounded below and strictly drop, the process must reach the floor — the loop exits, the recursion bottoms out.

Worked example: Euclid's GCD terminates

Recall the recurrence $\gcd(a, b) = \gcd(b, a \bmod b)$ with base $\gcd(a, 0) = a$. Take the variant $V(a, b) = b$. By definition of $\bmod$, $0 \le a \bmod b < b$, so the second argument strictly decreases. It is a non-negative integer. The recursion must reach $b = 0$ in at most $b_0$ steps. $\blacksquare$

Disproof by Counterexample

Universal claims ("for all $n$...") are disproved by exhibiting a single $n$ for which the claim fails. Existential claims ("there exists $n$...") cannot be disproved this way.

In algorithm design, counterexamples are how you reject a plausible-looking approach before you waste a week implementing it. Whenever your gut says "greedy should work here," try to break it on small inputs first. A counterexample on an array of length 4 saves you a debugging session at scale.

Pigeonhole Principle

Pigeonhole. If $n+1$ objects go into $n$ boxes, some box gets at least two.

Generalized. If $m$ objects go into $n$ boxes, some box gets at least $\lceil m/n \rceil$.

It looks trivial; it is devastatingly powerful. A few algorithmic uses:

• Hash collisions are inevitable. Any hash function from an unbounded key space into a finite table has, by pigeonhole, infinitely many collisions. There is no "perfect" general-purpose hash.
• Floyd's cycle detection. A function $f$ on a finite set, iterated, must eventually revisit a value — the iterates are pigeons, the set is the boxes. This is why the "tortoise and hare" algorithm works.
• Finite-state machines repeat. A DFA with $k$ states reading a string of length $> k$ must visit some state twice — the foundation of the pumping lemma.
• Birthday bound. Among 23 random people, two probably share a birthday. The "$\sqrt{n}$-collision" bound for hashing is the same calculation.

Mini-proof: any 5 points in a unit square include two within distance $\frac{\sqrt{2}}{2}$

Partition the unit square into four $\frac{1}{2} \times \frac{1}{2}$ sub-squares. Five points into four sub-squares — by pigeonhole, some sub-square holds at least two. Any two points in a sub-square are within its diagonal $\frac{\sqrt{2}}{2}$. $\blacksquare$

Adversary Arguments

How do you prove that no algorithm can do better than X? You play the adversary: you imagine an opponent who answers each query the algorithm makes in the worst possible (but consistent) way. If the adversary can force the algorithm into $f(n)$ work, then $f(n)$ is a lower bound for the problem.

Sketch: comparison-based sorting requires $\Omega(n \log n)$ comparisons

Any deterministic comparison sort can be drawn as a decision tree: each internal node is a comparison $a_i \lessgtr a_j$, each leaf is one of the $n!$ possible permutations. To distinguish all permutations, the tree must have at least $n!$ leaves. A binary tree with $L$ leaves has height at least $\log_2 L$. Therefore the worst-case number of comparisons is at least $\log_2(n!) = \sum_{k=1}^{n} \log_2 k = \Theta(n \log n)$ by Stirling's approximation. $\blacksquare$

Probabilistic Arguments

The probabilistic method proves that an object with property $X$ exists by showing that a randomly drawn object has property $X$ with positive probability. Strange — you never construct the object. But if it would exist with probability $> 0$, then by the definition of probability there must be at least one in the sample space.

For algorithm analysis, the friendlier cousin is expected-value reasoning. Randomized quicksort, with a uniformly random pivot, runs in expected time $E[T(n)] = O(n \log n)$ even though its worst case is $O(n^2)$. The proof shows that any pair of elements is compared at most once and computes the expected number of comparisons by linearity of expectation:

$E[\text{comparisons}] = \sum_{i < j} \Pr[a_i \text{ and } a_j \text{ are compared}] = \sum_{i < j} \frac{2}{j - i + 1} = O(n \log n)$.

Case Study: Verifying Binary Search

We now write the algorithm out and annotate every meaningful line with its role in the proof. Python first; TypeScript second with explicit invariant assertions.

For A = [1, 4, 7, 9, 12], lo = 0 and hi = 4.

lo = 0, hi = 4 → mid = 2.

A[2] = 7, target = 9 → narrow to A[3..4].

1def binary_search(A, target):
2    """Return an index i with A[i] == target, or -1 if not found.
3       Pre:  A is sorted in non-decreasing order.
4       Post: Returns -1 iff target not in A.
5    """
6    lo, hi = 0, len(A) - 1
7
8    # INVARIANT: if target is in A, then it is in A[lo..hi].
9    while lo <= hi:
10        mid = (lo + hi) // 2          # midpoint of surviving range
11        if A[mid] == target:
12            return mid                # post-condition trivially holds
13        elif A[mid] < target:
14            lo = mid + 1              # invariant preserved (sorted ⇒ left half ruled out)
15        else:
16            hi = mid - 1              # invariant preserved (sorted ⇒ right half ruled out)
17        # VARIANT (hi - lo) strictly decreased; well-founded in N.
18
19    return -1                         # range empty + invariant ⇒ target absent

The same algorithm in TypeScript, with the invariants written as runtime assertions you can keep in development builds:

Catches bugs like binarySearch([3, 1, 4]) early.

1function binarySearch(A: readonly number[], target: number): number {
2  // Pre-condition: A is sorted non-decreasing.
3  for (let i = 1; i < A.length; i++) {
4    console.assert(A[i - 1] <= A[i], "pre: A must be sorted");
5  }
6
7  let lo = 0;
8  let hi = A.length - 1;
9
10  while (lo <= hi) {
11    // Invariant: target ∈ A ⇒ target ∈ A[lo..hi].
12    const containsTarget =
13      A.slice(lo, hi + 1).includes(target) || !A.includes(target);
14    console.assert(containsTarget, "invariant violated");
15
16    const mid = lo + ((hi - lo) >> 1);   // overflow-safe midpoint
17    if (A[mid] === target) return mid;
18    if (A[mid] < target) lo = mid + 1;
19    else hi = mid - 1;
20  }
21  return -1;
22}

Case Study: Euclid's GCD

Two proof obligations: the algorithm computes the right thing (partial correctness via the recurrence $\gcd(a, b) = \gcd(b, a \bmod b)$), and it terminates (well-founded variant $b$).

gcd(48, 18) → 6.

(48, 18) → (18, 12) → (12, 6) → (6, 0).

1def gcd(a: int, b: int) -> int:
2    """Greatest common divisor of a, b ≥ 0, not both zero.
3       Recurrence: gcd(a, 0) = a; gcd(a, b) = gcd(b, a % b).
4    """
5    # Pre: a ≥ 0, b ≥ 0, (a, b) ≠ (0, 0).
6    while b != 0:
7        # Variant: b is a non-negative integer; we prove it strictly decreases.
8        a, b = b, a % b              # 0 ≤ a % b < b ⇒ new b strictly less than old b
9    return a                         # b == 0 ⇒ result is a (base case of the recurrence)

The TypeScript version is essentially the same; the proof obligations transfer verbatim. We use BigInt here because the algorithm is most useful for cryptographic-sized integers, where ordinary 64-bit arithmetic would overflow.

gcd(48n, 18n) iterations: (48, 18) → (18, 12) → (12, 6) → (6, 0).

1function gcd(a: bigint, b: bigint): bigint {
2  if (a < 0n || b < 0n) throw new Error("gcd requires non-negative inputs");
3  if (a === 0n && b === 0n) throw new Error("gcd(0, 0) is undefined");
4
5  while (b !== 0n) {
6    const r = a % b;        // 0 ≤ r < b — this is the variant decrease
7    a = b;
8    b = r;                  // new b strictly less than old b
9  }
10  return a;
11}

Proofs in Industry

These techniques are not academic decoration. They underpin real systems whose failure would be catastrophic.

The throughline: where the cost of failure is high enough, machine-checked proof is cheaper than testing. Even when full proof is overkill, the local techniques — an invariant comment, a termination argument, a sketch of why your greedy is optimal — are the difference between code that almost works and code you can ship.

Common Pitfalls

1. The base case is wrong (or trivially picked)

The horse-color paradox above is the canonical example: a base case that doesn't actually let the inductive step take its first non-trivial bite. Always test the step at $n = n_0 + 1$ manually, not just at $n_0$.

2. Confusing weak and strong induction

If your inductive step needs facts about cases much smaller than $k$ (recursing on halves, factors, sub-trees), you need strong induction. Trying to force the argument into ordinary induction will leave a hole.

3. "Proof" by example

Verifying an identity for $n = 1, 2, 3, 4, 5$ proves nothing about $n = 6$. Polya's prime-counting conjecture $L(n) \le 0$ held for the first $10^{14}$ integers and turned out to be false. Examples build intuition; only a proof closes the gap.

4. Off-by-one in the inductive step

The most common bug: assuming $P(k)$ and accidentally proving $P(k)$ again, not $P(k+1)$. Annotate which index you are reasoning about at every line.

5. Forgetting termination

Every loop and every recursive call needs some argument for why it ends. "The variable seems to get smaller" isn't enough — identify the variant explicitly. Real-world example: the 2003 Northeast blackout was triggered partly by an alarm system stuck in an infinite race-condition loop.

6. Confusing necessary and sufficient

$P \Rightarrow Q$ is not the same as $Q \Rightarrow P$. "If it's a square, it's a rectangle" doesn't mean "rectangles are squares." Half the bad correctness arguments collapse on this point.

7. Universal vs. existential mix-up

To disprove "$\forall n, P(n)$" one counterexample suffices. To disprove "$\exists n, P(n)$" you must prove the universal negation — one counterexample is not enough.

Exercises

Warm-up

1. Prove by induction that $\sum_{i=1}^{n} (2i - 1) = n^2$.
2. Prove by contradiction that $\sqrt{3}$ is irrational.
3. Disprove: "every quadratic $ax^2 + bx + c$ with integer coefficients is reducible over the integers." (Give a counterexample.)
4. Identify the variant for the loop while n > 1: n = n // 2. Why does it terminate?

Loop invariants

1. Linear search for an element in an unsorted array. State the invariant. Prove initialization, maintenance, and termination.
2. Selection sort. State an invariant strong enough to prove the post-condition ("A is sorted"). Prove all three obligations.
3. The two-pointer algorithm for "does a sorted array $A$ contain two elements summing to $s$?" State and prove an invariant relating the pointers $i, j$ to the search space.

Termination

1. Find a variant for the recursion f(n) = f(n // 2) + f(n // 2) with base f(0) = 1. Why does the well-founded relation work even though we make two recursive calls?
2. The recursion ack(m, n) for the Ackermann function calls itself with smaller pairs in the lexicographic order on $\mathbb{N}^2$. State the variant precisely and explain why $\mathbb{N}^2$ with this order is well-founded.

Structural induction

1. Prove by structural induction on binary trees that for every tree, $\#\text{leaves} = \#\text{internal nodes} + 1$ (assuming every internal node has exactly two children).
2. Prove that the in-order traversal of a binary search tree visits keys in non-decreasing order. (Hint: induction on tree structure; carefully state what you assume about the left and right subtrees.)

Pigeonhole and adversary

1. Prove: any sequence of 11 distinct integers contains either an increasing subsequence of length 4 or a decreasing subsequence of length 4. (Generalization of Erdős–Szekeres.)
2. Adversary lower bound: prove that finding the maximum of $n$ elements requires at least $n - 1$ comparisons. Sketch the adversary's strategy.

Challenge

1. State and prove the loop invariant for the in-place partition step of quicksort (the Lomuto scheme). Use it to prove that, after partition, the pivot ends up in its final sorted position.
2. Prove that any reachable state of the readers-writers concurrent algorithm (with at most one writer or any number of readers) satisfies the safety invariant. (You will need to enumerate the program states and show every transition preserves the invariant.)

With proof techniques in hand, every algorithm we meet from now on comes with a built-in question: what is the invariant, and why does it terminate? Answer those two and you have understood the algorithm at the level a senior engineer is expected to.