Correctness and Proof Writing

Loop invariants, induction, exchange arguments, cut property, contradiction, recurrence reasoning, and proof sketches suitable for interviews and contest editorials.

Shape of the argument holds initially, preserved by each iteration, implies the result at exit (Module 1) base case correct; if all smaller inputs are correct, so is this one transform any optimal solution step by step into the greedy one without getting worse (Modules 21, 52) Cut / cycle property MST and graph greedy lightest edge across a cut is safe; heaviest edge on a cycle is not needed (Module 32) lower bounds, impossibility assume a better solution exists and derive an impossibility Potential / amortized each operation's actual cost plus change in potential is bounded (Module 2)

Interview-length proof sketch (binary search on the answer): “The predicate feasible(c) is monotone: if capacity c ships everything in d days, any larger capacity does too, because the same day-by-day split still fits. So the feasible values form a suffix of the range, and binary search finds its first element. Each check is O(n), so the total is O(n log S) where S is the search range.”

A good sketch states the claim, the key property (monotonicity, invariant, exchange step), and why it implies the result — in three or four sentences.

Quiz

? Which technique proves a DP recurrence correct?
+ Induction over subproblem size or evaluation order :: Assume smaller states are correct.
- Exchange argument :: For greedy.
- Cut property :: For MSTs.
- Stress testing :: Evidence, not proof.

? What are the three parts of a loop-invariant proof?
+ Initialisation, maintenance, termination :: Module 1.
- Base, step, conclusion only for recursion :: That is induction.
- Lemma, theorem, corollary :: Not specific.
- Input, output, complexity :: No.

? Which statements belong in an interview proof sketch? (select all that apply)
+ The claim being proved :: State it.
+ The key property used :: Monotonicity, invariant, exchange.
+ Why the property implies correctness :: Connect them.
- Every line of the code :: Too detailed.