Interval scheduling

DefinitionCompatible activities#✓fully proved

Let each activity \(a\) have a start time \(s(a)\) and a finish time \(f(a)\) in a linearly ordered type, thought of as the closed-open interval \([s(a), f(a))\). Two activities \(a\) and \(b\) are compatible when \(f(a) \le s(b)\) or \(f(b) \le s(a)\); in particular, activities whose intervals only touch at an endpoint are compatible.

def IntervalCompatible (start finish : ι → τ) (a b : ι) : Prop :=
  finish a ≤ start b ∨ finish b ≤ start a

Used by 2

Used byCorrectness and optimality of earliest-finish interval scheduling · Symmetry of interval compatibility

TheoremSymmetry of interval compatibility#✓fully proved

For any start and finish times and any activities \(a\) and \(b\), if \(a\) is compatible with \(b\), then \(b\) is compatible with \(a\).

theorem IntervalCompatible.symm {start finish : ι → τ} {a b : ι}
    (h : IntervalCompatible start finish a b) : IntervalCompatible start finish b a

Uses 1 · Used by 1

Statement usesCompatible activities

Used byCorrectness and optimality of earliest-finish interval scheduling

DefinitionEarliest-finish greedy interval scheduling#✓fully proved

Given start and finish times \(s\) and \(f\) in a linear order and a list \(L\) of activities, sort \(L\) by finish time with merge sort, then scan the sorted list: the first activity is selected, and each later activity \(a\) is selected exactly when \(s(a)\) is at least the finish time of the last selected activity. The result is the list of selected activities in sorted order, together with a cost that counts one for each finish-time comparison made by the merge sort and one for each scanned activity after the first.

Cslib.Algorithms.Lean.TimeM.intervalSchedule · 19 lines

def intervalSchedule (start finish : ι → τ) (xs : List ι) : TimeM Nat (List ι) :=
  let rec scan (lastFinish : τ) : List ι → TimeM Nat (List ι)
    | [] => pure []
    | a :: rest => do
      ✓ if lastFinish ≤ start a then
        return a :: (← scan (finish a) rest)
      else
        scan lastFinish rest
  let values := xs.toArray
  let indices : TimeM Nat (List (Fin values.size)) :=
    List.mergeSortM (List.finRange values.size) (fun a b =>
      (⟨decide (finish values[a] ≤ finish values[b]), 1⟩ : TimeM Nat Bool))
  -- CSLib's monadic sort is universe-zero; sort array indices, then recover their payloads.
  let sorted := indices.ret.map fun i => values[i]
  let selection : TimeM Nat (List ι) :=
    match sorted with
    | [] => pure []
    | a :: rest => do return a :: (← scan (finish a) rest)
  ⟨selection.ret, indices.time + selection.time⟩

Used by 2

Used byCorrectness and optimality of earliest-finish interval scheduling · Comparison bound for earliest-finish interval scheduling

TheoremCorrectness and optimality of earliest-finish interval scheduling#✓fully proved

Let \(s\) and \(f\) assign start and finish times in a linear order to activities, and let \(L\) be a list of activities with \(s(a) < f(a)\) for every \(a\) in \(L\). Let \(S\) be the list returned by the earliest-finish schedule of \(L\). Then \(S\) is a subpermutation of \(L\) (each activity occurs in \(S\) at most as often as in \(L\)), any two entries of \(S\) at distinct positions are compatible, and every subpermutation \(M\) of \(L\) whose entries at distinct positions are pairwise compatible has length at most the length of \(S\).

theorem intervalSchedule_correct (start finish : ι → τ) (xs : List ι)
    (hproper : ∀ a ∈ xs, start a < finish a) :
    (intervalSchedule start finish xs).ret.Subperm xs ∧
      List.Pairwise (IntervalCompatible start finish) (intervalSchedule start finish xs).ret ∧
      ∀ ys, ys.Subperm xs → List.Pairwise (IntervalCompatible start finish) ys →
        ys.length ≤ (intervalSchedule start finish xs).ret.length

Uses 3

Statement usesCompatible activities · Earliest-finish greedy interval scheduling

Proof usesSymmetry of interval compatibility

TheoremComparison bound for earliest-finish interval scheduling#✓fully proved

For any start and finish times and any list of \(n\) activities, the earliest-finish schedule charges at most \(n \lceil \log_2 n \rceil + (n - 1)\) comparisons when \(n \ge 1\), and none when \(n = 0\).

theorem intervalSchedule_time (start finish : ι → τ) (xs : List ι) :
    (intervalSchedule start finish xs).time ≤
      xs.length * Nat.clog 2 xs.length + (xs.length - 1)

Uses 1

Statement usesEarliest-finish greedy interval scheduling

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.