Chapter 16 - Greedy Algorithms

The current Chapter 16 site contains two proved greedy-algorithm tracks. Section 16.1 proves the finite sorted-list activity-selection theorem for the executable greedy selector; Section 16.3 is the project's strongest completed greedy-algorithm case study.

Sections

• 16.1 Activity selection: proved for finite sorted lists. Main results: CLRS.­ActivitySelection.­finishSorted_head_minFinish, CLRS.­ActivitySelection.­finishSorted_greedyChoiceCertificate, CLRS.­ActivitySelection.­activitySelection, CLRS.­ActivitySelection.­activitySelection_cons_eq, CLRS.­ActivitySelection.­greedySelect_cons_eq, CLRS.­ActivitySelection.­greedySelect_sublist, CLRS.­ActivitySelection.­greedySelect_feasible, CLRS.­ActivitySelection.­greedySelect_after_maxCardinality, CLRS.­ActivitySelection.­greedySelect_cons_maxCardinality, CLRS.­ActivitySelection.­greedySelect_maxCardinality, CLRS.­ActivitySelection.­activitySelection_cons_maxCardinality, CLRS.­ActivitySelection.­activitySelection_maxCardinality, CLRS.­ActivitySelection.­greedySelect_optimal_length, CLRS.­ActivitySelection.­greedySelect_cons_recursive_correct, CLRS.­ActivitySelection.­activitySelection_cons_recursive_correct, CLRS.­ActivitySelection.­activitySelection_cons_correct, and CLRS.­ActivitySelection.­activitySelection_correct.

• 16.3 Huffman codes: proved. Main results: CLRS.­HuffmanV2.­optimum_huffman_freqs, CLRS.­HuffmanV2.­huffmanOfFreqs_correct, and CLRS.­HuffmanV2.­huffmanOfFreqs_cost_le.

Proof Theme

Both sections expose the same high-level CLRS pattern: make a greedy choice, turn the textbook exchange argument into a reusable certificate, then compose it with the recursive subproblem.

For Huffman, the key move is a split-leaf transformation:

1. Merge the two least frequent symbols.

2. Use the inductive optimum for the merged instance.

3. Split the merged leaf back into the two original leaves.

4. Compare costs against every competing tree.

The final public theorems are stated over a frequency table. Readers can use CLRS.­HuffmanV2.­huffmanOfFreqs_correct for the bundled correctness statement or CLRS.­HuffmanV2.­huffmanOfFreqs_cost_le for the direct minimum-cost comparison against any consistent tree with the same frequencies.

Why This Page Matters

Huffman is a useful benchmark for CLRS-Lean because it proves true optimality, not only functional correctness. Activity selection is the lighter companion: it proves the sorted-list greedy recursion directly. The proof first builds the exchange certificate from sorted order, then composes it with the recursive tail optimum to obtain maximum cardinality for CLRS.­ActivitySelection.­greedySelect. The theorem CLRS.­ActivitySelection.­greedySelect_cons_recursive_correct exposes the nonempty recursive step itself: choose the first finish-sorted activity, solve the filtered compatible tail, and bundle the exact recursion equation with tail optimality, full optimality, feasibility, sublist membership, and the optimal-length inequality. The public wrapper CLRS.­ActivitySelection.­activitySelection carries the same recursion equation and maximum-cardinality certificates under the CLRS-facing algorithm name. The theorem CLRS.­ActivitySelection.­activitySelection_correct exposes the reader-facing theorem bundle: the greedy output is a feasible sublist and no feasible sublist is longer. The theorem CLRS.­ActivitySelection.­activitySelection_cons_correct gives the same bundle for the nonempty recursive step.