CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 15. Greedy Algorithms
15.2. Greedy-Choice Property and Optimal Substructure (Meta-Theorems)

Imports

import Mathlib

15.2. Greedy-Choice Property and Optimal Substructure (Meta-Theorems)

This section formalizes the two structural properties that CLRS §15.2 identifies as the reusable core of every greedy algorithm:

Greedy-choice property: making a locally optimal (greedy) choice never prevents a globally optimal solution.
Optimal substructure: an optimal solution to a problem contains within it optimal solutions to its subproblems.

We define an abstract GreedyProblem structure that bundles the data and axioms needed to prove greedy optimality, and prove the meta-theorem gsolve_optimal: if a problem satisfies both properties (with a well-founded size measure), then the recursive greedy algorithm returns an optimal solution for every instance.

The instantiation with the activity-selection problem from §15.1 is provided in a separate companion file and recovers the existing greedySelect_maxCardinality theorem as a corollary of the generic meta-theorem.

Activity-selection instance

Main results:

Structure GreedyProblem : bundles the greedy-choice property and optimal substructure.
Definition gsolve : the generic recursive greedy solver.
Theorem gsolve_optimal : gsolve returns optimal solutions for every instance of a GreedyProblem.
Predicate GreedyChoiceProperty : the abstract greedy-choice property.
Predicate OptimalSubstructure : the abstract, solver-independent optimal-substructure property.

Notation conventions:

P : problem type
Sol : solution type
Elem : type of individual elements
optimal p s : s is an optimal solution for p
greedyElt p : the greedy element for p
sub p : the subproblem after making the greedy choice
combine e s : assemble a solution from the greedy element and tail solution
size p : a Nat well-founded measure

namespace CLRSnamespace GreedyMeta

The abstract `GreedyProblem` structure

A GreedyProblem formalizes the CLRS §15.2 pattern. It bundles:

Data:

optimal p s : s is an optimal solution for p
greedyElt p : the locally optimal (greedy) element
sub p : the residual subproblem after removing the greedy choice and incompatible elements
combine e s : construct a solution from the greedy element and a subproblem solution
base : the base (empty) solution
size p : a Nat measure for termination and induction

Axioms:

greedy_choice: a non-base problem has an optimal solution beginning with the greedy choice.
optimal_substructure: the tail of such an optimal solution is optimal for the residual subproblem.
replace_optimal_tail: any other optimal residual solution can replace that tail. This is the small compositional bridge needed by the generic solver.
sub_lt and base_opt: well-foundedness and base-case optimality.

structure GreedyProblem (Elem Sol P : Type) where
  optimal : P → Sol → Prop
  greedyElt : P → Elem
  sub : P → P
  combine : Elem → Sol → Sol
  base : Sol
  size : P → ℕ

  -- The greedy choice occurs in some optimal solution.
  greedy_choice : ∀ (p : P), size p > 0 →
    ∃ tail, optimal p (combine (greedyElt p) tail)

  -- The tail of an optimal greedy-shaped solution is optimal for the subproblem.
  optimal_substructure : ∀ (p : P) (tail : Sol), size p > 0 →
    optimal p (combine (greedyElt p) tail) → optimal (sub p) tail

  -- Optimal tails are interchangeable under the fixed greedy choice.
  replace_optimal_tail : ∀ (p : P) (oldTail newTail : Sol), size p > 0 →
    optimal (sub p) oldTail → optimal (sub p) newTail →
    optimal p (combine (greedyElt p) oldTail) →
    optimal p (combine (greedyElt p) newTail)

  -- The subproblem is strictly smaller (well-foundedness)
  sub_lt : ∀ (p : P), size p > 0 → size (sub p) < size p

  -- Base-case optimality
  base_opt : ∀ (p : P), size p = 0 → optimal p base

Generic recursive greedy solver

The recursive greedy solver for a GreedyProblem. Defined by well-founded recursion on the size measure.

noncomputable def gsolve (gp : GreedyProblem Elem Sol P) : P → Sol :=
  fun p =>
    if Variable name `h` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`h : gp.size p > 0 then
      gp.combine (gp.greedyElt p) (gsolve gp (gp.sub p))
    else
      gp.base
termination_by p => gp.size p
decreasing_by
  exact gp.sub_lt _ h

Recursion equation for non-base problems: gsolve makes the greedy choice and recurses on the subproblem.


theorem gsolve_eq (gp : GreedyProblem Elem Sol P) {p : P} (h : gp.size p > 0) :
    gsolve gp p = gp.combine (gp.greedyElt p) (gsolve gp (gp.sub p)) := by
  rw [gsolve.eq_def]
  simp [h]

Base-case equation: when size p = 0, gsolve returns base.


theorem gsolve_base (gp : GreedyProblem Elem Sol P) {p : P} (h : gp.size p = 0) :
    gsolve gp p = gp.base := by
  rw [gsolve.eq_def]
  simp [h]

Meta-theorem (CLRS §15.2)

Meta-theorem. If a problem class satisfies the greedy-choice property and optimal substructure (formalized as a GreedyProblem), then the recursive greedy algorithm gsolve returns an optimal solution for every problem instance.

Proof by strong induction on the size measure.


theorem gsolve_optimal (gp : GreedyProblem Elem Sol P) (p : P) :
    gp.optimal p (gsolve gp p) := by
  induction hsize : gp.size p using Nat.strong_induction_on generalizing p with
  | h n ih =>
    by_cases hzero : gp.size p = 0
    · rw [gsolve_base gp hzero]
      exact gp.base_opt p hzero
    · have hpos : gp.size p > 0 := Nat.pos_of_ne_zero hzero
      rw [gsolve_eq gp hpos]
      have hsub_lt : gp.size (gp.sub p) < gp.size p := gp.sub_lt p hpos
      have h_eq : gp.size (gp.sub p) < n := by
        rw [← hsize]
        exact hsub_lt
      have h_ih : gp.optimal (gp.sub p) (gsolve gp (gp.sub p)) :=
        ih (gp.size (gp.sub p)) h_eq (gp.sub p) rfl
      rcases gp.greedy_choice p hpos with ⟨oldTail, hwhole⟩
      have hold_opt : gp.optimal (gp.sub p) oldTail :=
        gp.optimal_substructure p oldTail hpos hwhole
      exact gp.replace_optimal_tail p oldTail (gsolve gp (gp.sub p)) hpos
        hold_opt h_ih hwhole

Predicate form of the greedy properties

GreedyChoiceProperty says that every active problem has an optimal solution that begins with its locally greedy element. It is an existence property and does not mention a particular solver.

def GreedyChoiceProperty (P Elem Sol : Type) (optimal : P → Sol → Prop)
    (active : P → Prop) (greedyElt : P → Elem)
    (combine : Elem → Sol → Sol) : Prop :=
  ∀ p, active p → ∃ tail, optimal p (combine (greedyElt p) tail)

OptimalSubstructure says that whenever an optimal solution is decomposed into the greedy choice and a tail, that tail is optimal for the residual subproblem. Unlike the former formulation, this is a property of the problem decomposition and is independent of any solver.

def OptimalSubstructure (P Elem Sol : Type) (optimal : P → Sol → Prop)
    (active : P → Prop) (greedyElt : P → Elem) (subproblem : P → P)
    (combine : Elem → Sol → Sol) : Prop :=
  ∀ p tail, active p →
    optimal p (combine (greedyElt p) tail) → optimal (subproblem p) tail

              theorem GreedyProblem.greedyChoiceProperty (gp : GreedyProblem Elem Sol P) :
    GreedyChoiceProperty P Elem Sol gp.optimal (fun p => gp.size p > 0)
      gp.greedyElt gp.combine :=
  gp.greedy_choicetheorem GreedyProblem.hasOptimalSubstructure (gp : GreedyProblem Elem Sol P) :
    OptimalSubstructure P Elem Sol gp.optimal (fun p => gp.size p > 0)
      gp.greedyElt gp.sub gp.combine :=
  gp.optimal_substructureend GreedyMetaend CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_15.Section_15_2_Greedy_Meta.ActivitySelection

Activity selection as a `GreedyProblem`

This companion connects the concrete §15.1 exchange proof to the abstract §15.2 framework. Problem instances carry the finish-sortedness invariant, so the generic solver's axioms are proved rather than assumed by callers.

namespace CLRS.GreedyMetaopen CLRS.ActivitySelection

A finish-time-sorted activity-selection subproblem.

abbrev SortedActivityProblem :=
  {xs : List Activity // FinishSorted xs}

              def activityGreedyElt : SortedActivityProblem → Option Activity
  | ⟨[], _⟩ => none
  | ⟨a :: _, _⟩ => some adef activitySubproblem : SortedActivityProblem → SortedActivityProblem
  | ⟨[], _⟩ => ⟨[], by simp [FinishSorted]⟩
  | ⟨a :: rest, hsorted⟩ =>
      ⟨activitiesAfter a rest,
        finishSorted_activitiesAfter (List.pairwise_cons.mp hsorted).2⟩def activityCombine : Option Activity → List Activity → List Activity
  | none, selected => selected
  | some a, selected => a :: selecteddef activityOptimal (p : SortedActivityProblem) (selected : List Activity) : Prop :=
  MaxCardinality p.1 selecteddef activitySize (p : SortedActivityProblem) : Nat :=
  p.1.length

The §15.1 activity-selection problem satisfies the separated greedy-choice and optimal-substructure interface from §15.2.


noncomputable def activityGreedyProblem :
    GreedyProblem (Option Activity) (List Activity) SortedActivityProblem where
  optimal := activityOptimal
  greedyElt := activityGreedyElt
  sub := activitySubproblem
  combine := activityCombine
  base := []
  size := activitySize
  greedy_choice := by
    rintro ⟨xs, hsorted⟩ hpos
    cases xs with
    | nil => simp [activitySize] at hpos
    | cons a rest =>
        refine ⟨greedySelect (activitiesAfter a rest), ?_⟩
        exact greedySelect_cons_maxCardinality hsorted
  optimal_substructure := by
    rintro ⟨xs, hsorted⟩ tail hpos hwhole
    cases xs with
    | nil => simp [activitySize] at hpos
    | cons a rest =>
        change MaxCardinality (activitiesAfter a rest) tail
        change MaxCardinality (a :: rest) (a :: tail) at hwhole
        have htailSub : tail.Sublist (activitiesAfter a rest) :=
          feasible_competitor_tail_sublist_after
            (finishSorted_head_minFinish hsorted) hwhole.sublist hwhole.feasible.2
        refine ⟨htailSub, hwhole.feasible.1, ?_⟩
        intro other hotherSub hotherFeasible
        have hotherBefore : ∀ b ∈ other, Before a b := by
          intro b hb
          exact (mem_activitiesAfter.mp (hotherSub.subset hb)).2
        have hbound := hwhole.maximum (a :: other)
          (List.Sublist.cons_cons a
            (hotherSub.trans (activitiesAfter_sublist a rest)))
          (feasible_cons hotherFeasible hotherBefore)
        simpa using hbound
  replace_optimal_tail := by
    rintro ⟨xs, hsorted⟩ oldTail newTail hpos hold hnew hwhole
    cases xs with
    | nil => simp [activitySize] at hpos
    | cons a rest =>
        change MaxCardinality (activitiesAfter a rest) newTail at hnew
        change MaxCardinality (a :: rest) (a :: newTail)
        exact greedy_choice_optimal_from_certificate hnew
          (finishSorted_greedyChoiceCertificate hsorted hnew.sublist)
  sub_lt := by
    rintro ⟨xs, _hsorted⟩ hpos
    cases xs with
    | nil => simp [activitySize] at hpos
    | cons a rest =>
        have hle := (activitiesAfter_sublist a rest).length_le
        change (activitiesAfter a rest).length < (a :: rest).length
        simpa using Nat.lt_succ_of_le hle
  base_opt := by
    rintro ⟨xs, hsorted⟩ hzero
    cases xs with
    | nil =>
        exact ⟨by simp, by simp [Feasible], by
          intro other hsub _
          simpa using hsub.length_le⟩
    | cons a rest => simp [activitySize] at hzero

Generic §15.2 optimality specialized to activity selection.

theorem activityGsolve_maxCardinality (p : SortedActivityProblem) :
    MaxCardinality p.1 (gsolve activityGreedyProblem p) :=
  gsolve_optimal activityGreedyProblem p

The generic solver computes the same recursive selector formalized in §15.1.


theorem activityGsolve_eq_greedySelect (p : SortedActivityProblem) :
    gsolve activityGreedyProblem p = greedySelect p.1 := by
  induction hsize : activitySize p using Nat.strong_induction_on generalizing p with
  | h n ih =>
      rcases p with ⟨xs, hsorted⟩
      cases xs with
      | nil =>
          rw [gsolve_base activityGreedyProblem (by rfl)]
          simp [activityGreedyProblem, greedySelect]
      | cons a rest =>
          have hpos : activityGreedyProblem.size ⟨a :: rest, hsorted⟩ > 0 := by
            simp [activityGreedyProblem, activitySize]
          rw [gsolve_eq activityGreedyProblem hpos, greedySelect_cons_eq]
          change a :: gsolve activityGreedyProblem
              (activitySubproblem ⟨a :: rest, hsorted⟩) =
            a :: greedySelect (activitiesAfter a rest)
          apply congrArg (a :: ·)
          have hlt := activityGreedyProblem.sub_lt ⟨a :: rest, hsorted⟩ hpos
          have hltN : activitySize (activitySubproblem ⟨a :: rest, hsorted⟩) < n := by
            rw [← hsize]
            exact hlt
          simpa [activitySubproblem] using
            ih (activitySize (activitySubproblem ⟨a :: rest, hsorted⟩)) hltN
              (activitySubproblem ⟨a :: rest, hsorted⟩) rfl

The concrete §15.1 optimum theorem is recovered from the §15.2 instance.


theorem greedySelect_maxCardinality_via_meta {xs : List Activity}
    (hsorted : FinishSorted xs) :
    MaxCardinality xs (greedySelect xs) := by
  let p : SortedActivityProblem := ⟨xs, hsorted⟩
  rw [← activityGsolve_eq_greedySelect p]
  exact activityGsolve_maxCardinality p

The abstract instance exposes the two textbook properties separately.

theorem activityGreedyChoiceProperty :
    GreedyChoiceProperty SortedActivityProblem (Option Activity) (List Activity)
      activityOptimal (fun p => activitySize p > 0)
      activityGreedyElt activityCombine :=
  activityGreedyProblem.greedyChoiceProperty

theorem activityOptimalSubstructure :
    OptimalSubstructure SortedActivityProblem (Option Activity) (List Activity)
      activityOptimal (fun p => activitySize p > 0)
      activityGreedyElt activitySubproblem activityCombine :=
  activityGreedyProblem.hasOptimalSubstructure

end CLRS.GreedyMeta