Proof Techniques

Every algorithm in this course comes with four deliverables, and the third — proof of correctness — is the one students skip and regret. An algorithm you cannot argue for is a conjecture: it might be right, but you have no way to know, and it passed my tests is not a proof, since one untested instance can sink it.

The arguments you need are few. A small kit of techniques proves nearly everything in algorithms, and the same shapes recur from sorting to intractability. This lesson is that kit. None of it is deep; the skill is recognizing which tool fits a given claim, and writing the argument cleanly enough that a skeptical reader is forced to agree.

Direct proof

The default. To prove if $P$ then $Q$, assume $P$ and walk a chain of valid steps to $Q$. Most everyday claims yield to it.

The whole move is to unfold the definitions (odd means $2k+1$), do the algebra, then fold the definition back (an expression of the form $2m+1$ is odd). Many direct proofs follow this shape: translate the hypothesis into symbols, manipulate, translate back.

Proof by contrapositive

The statements if $P$ then $Q$ and if not $Q$ then not $P$ are logically equivalent:

So when the forward direction is awkward, prove the contrapositive instead — it is the same theorem in an easier form. We used exactly this to prove a search routine sound in the previous lesson: rather than reason about the whole array (if $k\notin A$ it returns not found), we reasoned about one line of code (if it returns found then $k\in A$).

Proving $n^2$ even $\Rightarrow n$ even directly is clumsy (you would factor $n^2$); the contrapositive reduces it to a one-line consequence of work already done.

In algorithm design, contrapositives are most useful when they turn a claim about absence into a claim about presence. Here is the argument that lets a trial-division primality test stop at $\sqrt{n}$ instead of scanning all the way to $n-1$:

The forward statement quantifies over every candidate divisor and asserts a negative, which gives you nothing to compute with. The contrapositive supplies a concrete object ($a$, the smaller factor) and one inequality. The algorithmic payoff is real: testing a twelve-digit number now takes about $10^6$ trial divisions instead of $10^{12}$.

Proof by contradiction

To prove $P$, assume $\neg P$ and derive an impossibility. Since valid reasoning from a true premise cannot reach a falsehood, the premise $\neg P$ must have been false, so $P$ holds. It is the proof of last resort, and often the shortest.

The classic is the irrationality of $\sqrt{2}$, the proof the Pythagoreans reputedly found unsettling.

Contradiction also proves things do not exist or cannot be improved. The $\Omega (n\log n)$ lower bound for comparison sorting and the proof that no greedy coin system is always optimal are both suppose a better object existed, derive absurdity arguments. Here is the smallest specimen of that genre, a genuine lower bound proved in four sentences:

The move deserves a name, because it recurs: the contradiction is manufactured by an adversary who watches what the algorithm does and then plants the bad case precisely in the spot it never looked. Every you cannot do better than $X$ claim in this course, from sorting to searching, has this shape: assume a faster algorithm exists, then exhibit an input it must get wrong.

from math import isqrt

def integer_sqrt(number: int) -> int:
  """
    The floor of the square root of a non-negative integer.\n
  """
  if number < 0:
    raise ValueError("integer_sqrt is undefined for negative integers")
  return isqrt(number)

def is_perfect_square(number: int) -> bool:
  """
    Whether `number` is a perfect square — equivalently, whether sqrt(number)\n
    is rational for a non-negative integer.\n
  """
  if number < 0:
    return False

  # a number is a perfect square iff floor(sqrt) squared recovers it.
  root: int = isqrt(number)
  return root * root == number

def has_rational_sqrt(number: int) -> bool:
  """
    Whether the square root of a non-negative integer is rational. By the\n
    contradiction argument, this holds exactly for perfect squares; sqrt(2),\n
    not a square, is therefore irrational.\n
  """
  return is_perfect_square(number)

def square_is_even_implies_even(number: int) -> bool:
  """
    A checkable instance of the contrapositive lemma used in the proof:\n
    if number^2 is even then number is even. Returns whether the\n
    implication holds for this `number` (always True).\n
  """
  # the contrapositive: whenever the square is even, the number is too.
  square_is_even: bool = (number * number) % 2 == 0
  number_is_even: bool = number % 2 == 0
  return (not square_is_even) or number_is_even

Induction

Induction is the main tool for proving algorithm correctness, because algorithms repeat: loops and recursion both do the same thing on ever-smaller (or ever-larger) instances.¹ To prove a statement $P(n)$ for all $n\ge n_0$, you show two things:

• Base case. $P(n_0)$ holds outright.
• Inductive step. Assuming $P(k)$ (the induction hypothesis), prove $P(k+1)$.

Together these are a falling chain of dominoes: the base case tips the first, the step guarantees each tips the next, so all of them fall.

The textbook example is the sum of the first $n$ integers, the same closed form the analysis lessons lean on.

Equalities are the gentlest case, because the inductive step is forced: substitute the hypothesis, simplify, done. Inequalities require slightly more judgment: after substituting you must still bridge from what the hypothesis gives you to what the claim demands. Here is the inequality that explains why halving reaches $1$ in logarithmically many steps, the fact behind binary search and every divide-and-conquer depth bound:

Read the step closely: the hypothesis delivered $2(k+1)$, the claim wanted $k+2$, and the bridge was the observation that the surplus $k$ is nonnegative. Most failed induction attempts on inequalities die exactly at that bridge, and the usual repair is to prove a stronger claim whose surplus is bigger.

The art is choosing the hypothesis. Too weak and the step cannot go through; the fix is often to prove a stronger statement, whose hypothesis gives the step more to work with (this is strengthening the induction hypothesis, and it powers the substitution method for recurrences).

def gauss_sum_closed(count: int) -> int:
  """
    The closed form 1 + 2 + ... + count = count*(count+1)/2.\n
    Defined as 0 for count <= 0 (an empty sum).\n
  """
  if count <= 0:
    return 0
  return count * (count + 1) // 2

def gauss_sum_iterative(count: int) -> int:
  """
    The same total accumulated in a loop, maintaining the invariant that\n
    after visiting integer `current`, `running_total` equals the closed\n
    form for `current`. Termination at count yields the claim.\n
  """
  running_total: int = 0
  for current in range(1, count + 1):
    running_total += current

    # invariant: the partial sum equals the closed form so far.
    assert running_total == gauss_sum_closed(current)
  return running_total

Strong induction

Sometimes $P(k+1)$ needs more than its immediate predecessor — it needs several smaller cases, or one you cannot predict in advance. Strong induction grants the entire history: to prove $P(n)$, assume $P(j)$ for all $n_0\le j<n$.

It is the natural argument whenever a problem splits into smaller subproblems of sizes you do not know ahead of time — which is to say, most of divide & conquer and dynamic programming.

Ordinary induction would be stuck here: $n$'s factorization has nothing to do with $(n-1)$'s. Knowing that $12=2^2\cdot 3$ tells you nothing useful about $13$, and knowing about $13$ tells you nothing about $14=2\cdot 7$. We needed the freedom to reach back to $a$ and $b$, wherever they landed. For $n=91$ that means $a=7$ and $b=13$, neither of which is $90$.

def is_prime(number: int) -> bool:
  """
    Whether `number` is prime by trial division up to its square root.\n
  """
  if number < 2:
    return False

  # trial-divide by every candidate up to sqrt(number).
  divisor: int = 2
  while divisor * divisor <= number:
    if number % divisor == 0:
      return False
    divisor += 1
  return True

def smallest_factor(number: int) -> int:
  """
    The smallest divisor of `number` that is at least 2 — `number` itself\n
    when it is prime. Requires number >= 2.\n
  """
  # the first divisor found below sqrt is prime; none means number is prime.
  candidate: int = 2
  while candidate * candidate <= number:
    if number % candidate == 0:
      return candidate
    candidate += 1
  return number

def prime_factors(number: int) -> list[int]:
  """
    The non-decreasing list of prime factors of `number` (with multiplicity),\n
    whose product is `number`. Requires number >= 2.\n
    Follows the strong-induction structure: peel off the smallest prime\n
    factor, then factor the strictly smaller quotient.\n
  """
  if number < 2:
    raise ValueError("prime factorization is defined for integers >= 2")

  # peel off the smallest prime factor, then recurse on the quotient.
  factors: list[int] = []
  remaining: int = number
  while remaining > 1:
    factor: int = smallest_factor(remaining)
    factors.append(factor)
    remaining //= factor

  return factors

Strong induction proves recursion correct

The payoff of strong induction is that it certifies recursive algorithms almost mechanically: assume every recursive call returns the right answer (each call is on a smaller instance, so the strong hypothesis covers it), then check that the combining logic is sound.¹ Here is the standard fast exponentiation routine, which computes $x^n$ in $O(\log n)$ multiplications by squaring:

Notice which induction was required. The call from input $n$ is on $\lfloor n/2\rfloor$, not on $n-1$: for $n=100$ the proof for $100$ leans on the case $50$, skipping the forty-nine cases between. Weak induction's hypothesis covers only the immediate predecessor and cannot reach that far back. Every recursive correctness proof in this course follows this template: base case = the non-recursive branch, hypothesis = the recursive calls are correct, step = the combine logic preserves correctness. The only obligation that varies is checking the combine.

Structural induction: trees

Induction is not confined to $1,2,3,\dots$: any collection of objects built from smaller objects of the same kind supports it. Trees are the canonical case: a binary tree is either a single leaf or a root with two smaller binary trees hanging off it, so a claim about all binary trees can be proved by inducting on the tree's size, with the subtrees playing the role of smaller cases. This is structural induction, and it is strong induction in disguise: a root's subtrees can be any smaller sizes, so the step needs the full history, exactly as prime factorization did.

The proof never mentions the tree's shape: balanced, degenerate, or lopsided, the count comes out the same, which is why the figure shows a deliberately skewed tree. Facts of this kind recur throughout the course: this one bounds the size of merge trees and decision trees in the sorting lower bound, and its siblings (a binary tree of height $h$ has at most $2^h$ leaves) are proved by the same template.²

Where inductions go wrong

Induction fails in stereotyped ways, and each failure mode has a classic specimen. Knowing them keeps your own proofs honest.

A valid step cannot rescue a false base. Consider the claim $n^2\ge 2n+1$ for all $n\ge 1$. The inductive step is airtight: if $k^2\ge 2k+1$, then

since $2k\ge 1$ for $k\ge 1$. Yet the claim is false: at $n=1$ we would need $1\ge 3$, and at $n=2$ we would need $4\ge 5$. The first domino never falls. The statement only becomes true at $n=3$ ($9\ge 7$), so the honest theorem is for all $n\ge 3$, with base case $n=3$. Checking where the base actually starts is not pedantry: an algorithm proved correct for all $n\ge 3$ still needs separate handling for $n=1$ and $2$, and a recursive implementation hits those inputs last and crashes on them first.

Count how far back the step reaches. A step that uses $P(k)$ and $P(k-1)$ together (the shape of every Fibonacci-flavored claim) needs two base cases, because the step for $n=2$ reaches down to $P(0)$, which one base case at $n=1$ never established. In general, a step that reaches back $r$ positions needs $r$ consecutive base cases, and a strong-induction step that recurses to $\lfloor n/2\rfloor$ needs the base to cover everything its smallest instances bottom out on. Erickson's advice is to write the step first, see which smaller cases it consumed, and only then decide what the base must be.¹

Flawed maintenance: all horses are the same color. The most famous broken induction proves that any $n$ horses are identically colored. Base case ($n=1$): one horse has one color. ✓ Inductive step: given $n+1$ horses, remove the first; the remaining $n$ are same-colored by hypothesis. Remove the last instead; the first $n$ are also same-colored. The two groups overlap, so all $n+1$ share one color. $\square$?

The flaw is quantifier-shaped: the overlap argument silently assumes the two groups share at least one horse, which requires $n+1\ge 3$. At the very first application of the step (from $n=1$ to $n=2$) the groups are $\{1\}$ and $\{2\}$ with empty intersection, and nothing links their colors. One broken link, at exactly one value of $n$, and every later domino stands: the proof is valid for any $n$ horses of which some two share a color, a theorem nobody needs. The lesson is to test the inductive step at its smallest instance, where degenerate geometry (empty overlaps, single elements, zero-length ranges) lives.

Assuming what you are proving. The inductive hypothesis is $P(k)$; the obligation is $P(k+1)$. Writing assume $P(k+1)$ and simplifying it into a true statement proves nothing, because false premises can yield true conclusions: from $1=2$, multiplying both sides by $0$ gives the perfectly true $0=0$. This mistake usually appears disguised as start with the equation for $k+1$ and manipulate both sides until they match. The repair is directional discipline: start from the left side of the $k+1$ claim (or from the hypothesis), and transform it by known-valid steps until the right side appears, never touching the target equation as if it were already true.

Proof by construction

To prove something exists, the most convincing move is to build it — exhibit the object and check it works. A constructive existence proof produces a witness, not merely a guarantee.

This is the proof style closest to our subject, because an algorithm is a constructive proof: a correct algorithm for a problem is a witness that a solution exists and a recipe for producing it. When the greedy method proves its choice is safe by an exchange argument — take any optimal solution, transform it into the greedy one without making it worse — that, too, is construction: it builds the optimum it claims exists.

from math import factorial

def composite_run(length: int) -> list[int]:
  """
    A run of `length` consecutive composite integers — the constructed\n
    witness. Term i (for offset 2..length+1) is (length+1)! + offset, which\n
    `offset` divides, so each term is composite. Requires length >= 1.\n
  """
  if length < 1:
    raise ValueError("a composite run must have length >= 1")
  base: int = factorial(length + 1)
  return [base + offset for offset in range(2, length + 2)]

def witness_divisor(length: int, position: int) -> int:
  """
    For the `position`-th term of `composite_run(length)` (0-indexed), a\n
    proper divisor that certifies it composite — namely position + 2.\n
  """
  if not 0 <= position < length:
    raise IndexError("position out of range for the constructed run")
  return position + 2

Disproof by counterexample

The arguments above confirm universal claims (for all $n$…). To refute one, you need just a single instance where it fails. One counterexample is fatal; no amount of confirming examples can rescue a false for all.

This is why correctness must hold on every input, and why a plausible heuristic needs a proof rather than a few passing trials. Hunting for a small counterexample is also the fastest way to test a conjecture before investing in a proof³ — a conjecture that survives honest attempts to break it is worth the cost of a proof.

from typing import NamedTuple, Optional, Sequence

class Counterexample(NamedTuple):
  """
    A witness that greedy change is suboptimal: the amount, the coin count\n
    greedy uses, and the true minimum.\n
  """
  amount: int
  greedy_coins: int
  optimal_coins: int

def greedy_coin_count(denominations: Sequence[int], amount: int) -> Optional[int]:
  """
    Coins used by the greedy rule (largest coin that fits, repeatedly), or\n
    None if greedy gets stuck before reaching exactly `amount`.\n
  """
  remaining: int = amount
  coins_used: int = 0

  # repeatedly take as many of the largest fitting coin as possible.
  for coin in sorted(denominations, reverse=True):
    if coin <= 0:
      continue
    coins_used += remaining // coin
    remaining %= coin

  # success only when greedy lands exactly on the amount.
  return coins_used if remaining == 0 else None

def optimal_coin_count(denominations: Sequence[int], amount: int) -> Optional[int]:
  """
    The true minimum number of coins making exactly `amount`, by dynamic\n
    programming, or None if no combination works.\n
  """
  # best[t] is the fewest coins for amount t; unreachable marks "no way yet".
  unreachable: int = amount + 1
  best: list[int] = [0] + [unreachable for _ in range(amount)]

  # relax every target against each coin it can end with.
  for target in range(1, amount + 1):
    for coin in denominations:
      if 0 < coin <= target and best[target - coin] + 1 < best[target]:
        best[target] = best[target - coin] + 1

  return None if best[amount] == unreachable else best[amount]

def find_counterexample(
  denominations: Sequence[int], max_amount: int
) -> Optional[Counterexample]:
  """
    The smallest amount in 1..max_amount where greedy uses strictly more\n
    coins than the optimum, or None if greedy is optimal throughout that\n
    range. Hunting a small counterexample is the fast first attack on a\n
    conjectured "this always works."\n
  """
  # scan amounts upward; the first where greedy beats optimal is the witness.
  for amount in range(1, max_amount + 1):
    greedy: Optional[int] = greedy_coin_count(denominations, amount)
    optimal: Optional[int] = optimal_coin_count(denominations, amount)
    if greedy is not None and optimal is not None and greedy > optimal:
      return Counterexample(amount, greedy, optimal)

  return None

Loop invariants are induction

The reason induction matters so much here is that loop invariants are induction applied to time. A loop invariant is a statement true before and after every iteration; proving it amounts to an induction over the iteration count, and its three-part rubric⁴ maps one-to-one onto the parts of an inductive proof:

We proved Find-Max correct exactly this way, and the pattern returns for every loop in the course. To see the rubric run end-to-end once more, here is the simplest loop that computes anything:

• Initialization. Before the first iteration, $i=1$ and the invariant reads $s=$ (sum of no elements) $=0$. The seed line set $s\leftarrow 0$, and the empty sum is $0$ by convention. ✓
• Maintenance. Assume the invariant entering the iteration with cursor $i$: $s=A[1]+\cdots +A[i-1]$. The body executes $s\leftarrow s+A[i]$, after which $s=A[1]+\cdots +A[i-1]+A[i]$ — the invariant with cursor value $i+1$, the state in which the next iteration begins. ✓
• Termination. The loop exits when the cursor passes $n$, i.e. with the invariant holding for $i=n+1$: $s=A[1]+\cdots +A[n]$. That is the specified output, and the last line returns it. ✓

Each bullet is short because the invariant was chosen well: it names the one quantity the loop maintains, at one fixed instant (the start of an iteration), and it mentions the cursor so that termination instantiates it at a known value. A vaguer statement ($s$ holds a partial sum) passes initialization and maintenance trivially and then gives you nothing at termination. The rubric only pays off if the invariant is strong enough that its $i=n+1$ instance is the correctness claim.⁴

Recursion is even more direct: a recursive algorithm is correct by (usually strong) induction on the size of its input, with the base case the non-recursive branch and the inductive step the assumption that the recursive calls are themselves correct, exactly the $\text{Power}$ proof above.

from typing import Sequence, TypeVar

from comparable import Comparable

Element = TypeVar("Element", bound=Comparable)

def find_max(values: Sequence[Element]) -> Element:
  """
    The largest element of a non-empty sequence, found by a single scan that\n
    checks its loop invariant after every iteration. Raises ValueError on an\n
    empty sequence.\n
  """
  if not values:
    raise ValueError("find_max is undefined for an empty sequence")

  current_max: Element = values[0]
  scanned: int = 1

  # initialization: current_max is the max of the length-1 prefix.
  assert current_max == max(values[:scanned])

  for index in range(1, len(values)):
    if values[index] > current_max:
      current_max = values[index]
    scanned = index + 1

    # maintenance: current_max is the max of the prefix values[:scanned].
    assert current_max == max(values[:scanned])

  # termination: the whole sequence was scanned, so this is the maximum.
  return current_max

from typing import Any, Protocol, TypeVar


class Comparable(Protocol):
  """
    Anything orderable with `<` (int, float, str, tuple, date, …).\n
  """

  # `other` is position-only so built-ins (int, str, …), whose dunder
  # operands are position-only, structurally satisfy the protocol.
  def __lt__(self, other: Any, /) -> bool: ...
  def __gt__(self, other: Any, /) -> bool: ...
  def __le__(self, other: Any, /) -> bool: ...
  def __ge__(self, other: Any, /) -> bool: ...

A note on yes/no algorithms

For procedures that decide rather than compute — does a path exist, is this formula satisfiable, is $k$ in the array — correctness has two halves with standard names, introduced earlier: soundness (every yes is true — no false positives) and completeness (every true case is caught — no false negatives). The two are proved separately and often with different tools: soundness frequently falls to a direct or contrapositive argument about a single accepting step, while completeness usually wants induction over the algorithm's progress. Keeping them apart keeps the proof honest.

Machine-checked proof, and its limits

Every technique here is a paper-and-pencil proof, checked by a human reader. Two developments push past that. The first is machine-checked proof: an a proof assistant like Coq, Lean, or Isabelle can check an inductive argument mechanically, invariant by invariant, with no gap left to clearly. The four-color theorem (1976) was the first famous result whose proof had to be completed by computer, and modern formalizations — Gonthier's fully machine-checked four-color and Feit–Thompson proofs — show the same induction and case analysis we do by hand, scaled to sizes no referee could audit.⁵ When a correctness proof matters enough that a subtle error would be costly, this is where the discipline of state the invariant precisely pays off.

The second is a caution about what a proof of correctness does and does not buy. A verified algorithm is correct relative to its specification; if the specification is wrong, the proof certifies the wrong thing. And correctness is separate from feasibility: proving that a procedure eventually halts with the right answer says nothing about whether it halts before the sun burns out — the running-time analysis of the next lessons is a distinct obligation. Skiena's running advice, to attack a conjecture with small counterexamples before attempting a proof, is the cheap filter that saves the expensive one: most false conjectures die to an instance with three or four elements.⁶

Takeaways

• Match the tool to the claim. If $P$ then $Q$ → direct, or contrapositive if the reverse is easier. A for all $n$ about a repeated process → induction (strong induction when a step needs many smaller cases). There exists → construction. This always works that you doubt → hunt a counterexample.
• Induction is the spine of correctness proofs, because loops and recursion repeat. Loop invariants are induction over iterations; recursive correctness is induction over input size.
• Strengthen the hypothesis when an inductive step won't close — proving a stronger statement can be easier, because the step gets more to work with.
• Audit the base and the smallest step. A valid inductive step cannot rescue a false base case, a step that reaches back $r$ positions needs $r$ base cases, and flawed maintenance hides at the smallest instance (the horses proof breaks only at $n+1=2$).
• One counterexample refutes a universal claim; no finite pile of examples proves one. This is why it passed the tests is evidence, not proof.
• An algorithm is a constructive existence proof — which is why getting the proof right and getting the algorithm right are the same task, not two.