Imports
import Mathlib.Tactic4.1. The Maximum-Subarray Problem
This file gives the first Lean model for CLRS Section 4.1. The textbook problem asks for a nonempty contiguous subarray of maximum sum. We model the input as a list of integer daily changes, enumerate all nonempty contiguous subarrays, and choose a candidate with maximum sum.
The first executable selector is an exhaustive finite search, which gives a clean specification. The file then builds the CLRS divide-and-conquer proof layers on top of that specification: the crossing helper, the executable combine step, and a structurally recursive selector over explicit split trees.
Main results:
-
Theorem
mem_nonemptySubarrays_iff: the candidate enumerator contains exactly the nonempty contiguous subarrays. -
Theorem
mem_crossingSubarrays_iff: the crossing-candidate enumerator contains exactly the nonempty suffix/prefix candidates that cross a split. -
Theorem
bestCandidate_correct: the generic finite argmax selector returns a member whose sum is at least every listed candidate. -
Theorem
maxCrossingSubarray_correct: the crossing helper returns a maximum-sum candidate among all candidates crossing a split. -
Theorem
maxCrossingSubarray_isNonemptySubarray_append: the crossing helper returns a valid nonempty subarray of the concatenated input. -
Theorem
subarray_append_left_or_right_or_crossing: every nonempty subarray ofleft ++ rightis left-only, right-only, or crossing. -
Theorem
subarray_append_optimal_of_cases: a candidate that dominates the left-only, right-only, and crossing cases dominates every subarray of the concatenated input. -
Theorem
maxSubarrayDivideStep_correct: an executable combine step for the CLRS divide-and-conquer proof returns a globally optimal candidate forleft ++ right. -
Theorem
maxSubarrayDivideTree_correct: a structurally recursive split-tree selector returns a globally optimal maximum subarray. -
Theorem
maxSubarrayDivideFuel_correct: a fuelled midpoint splitter gives an executable divide-and-conquer selector with the same correctness contract. -
Theorem
maxSubarray_exists_of_ne_nil: nonempty inputs have a selected maximum-subarray candidate. -
Theorem
maxSubarray_correct: the executable maximum-subarray selector returns a nonempty contiguous subarray whose sum is maximal among all nonempty contiguous subarrays.
Current gaps:
-
The recursive divide-and-conquer correctness theorem is proved for an explicit/fuelled split model. Runtime and RAM-cost analysis are future strengthening targets.
namespace CLRSnamespace Chapter04Contiguous subarrays
The sum of a candidate subarray.
def subarraySum (xs : List Int) : Int := xs.sum
pre is a nonempty prefix of xs.
This is a specification predicate; the executable enumerator below is proved equivalent to it.
def IsNonemptyPrefix (pre xs : List Int) : Prop :=
pre ≠ [] ∧ ∃ rest, xs = pre ++ rest
sub is a nonempty contiguous subarray of xs.
The witnesses are the elements before and after the contiguous segment.
def IsNonemptySubarray (sub xs : List Int) : Prop :=
sub ≠ [] ∧ ∃ before after, xs = before ++ sub ++ after
suf is a nonempty suffix of xs.
This is the right half of the CLRS crossing-subarray helper: a crossing subarray uses a nonempty suffix of the left half and a nonempty prefix of the right half.
def IsNonemptySuffix (suf xs : List Int) : Prop :=
suf ≠ [] ∧ ∃ before, xs = before ++ suf
sub crosses the split between left and right when it is a
nonempty suffix of the left side followed by a nonempty prefix of the right
side.
def IsCrossingSubarray (sub left right : List Int) : Prop :=
∃ suf pre,
IsNonemptySuffix suf left ∧ IsNonemptyPrefix pre right ∧ sub = suf ++ preEnumerate all nonempty prefixes of a list.
def nonemptyPrefixes : List Int → List (List Int)
| [] => []
| x :: xs => [x] :: (nonemptyPrefixes xs).map (fun pre => x :: pre)Enumerate all nonempty suffixes of a list.
def nonemptySuffixes : List Int → List (List Int)
| [] => []
| x :: xs => (x :: xs) :: nonemptySuffixes xsEnumerate all subarrays crossing a fixed split.
def crossingSubarrays (left right : List Int) : List (List Int) :=
(nonemptySuffixes left).flatMap
(fun suf => (nonemptyPrefixes right).map (fun pre => suf ++ pre))private theorem flatMap_nil {α β : Type} (xs : List α) :
xs.flatMap (fun _ => ([] : List β)) = [] :=
induction xs with
Enumerate all nonempty contiguous subarrays of a list.
def nonemptySubarrays : List Int → List (List Int)
| [] => []
| x :: xs => nonemptyPrefixes (x :: xs) ++ nonemptySubarrays xsThe prefix enumerator is exact.
The suffix enumerator is exact.
The crossing-subarray enumerator is exact for a fixed split.
theorem mem_crossingSubarrays_iff {sub left right : List Int} :
sub ∈ crossingSubarrays left right ↔
IsCrossingSubarray sub left right :=
Every crossing candidate is a nonempty contiguous subarray of the concatenated input.
theorem crossingSubarray_isNonemptySubarray_append {sub left right : List Int}
(hcross : IsCrossingSubarray sub left right) :
IsNonemptySubarray sub (left ++ right) :=
cases suf with
exact ⟨before, after, ⟩Lifting subarrays across an append
A left-half subarray is also a subarray after appending a right half.
theorem isNonemptySubarray_append_left {sub left right : List Int}
(hsub : IsNonemptySubarray sub left) :
IsNonemptySubarray sub (left ++ right) :=
exact ⟨hsubNonempty, before, after ++ right,
⟩A right-half subarray is also a subarray after prepending a left half.
theorem isNonemptySubarray_append_right {sub left right : List Int}
(hsub : IsNonemptySubarray sub right) :
IsNonemptySubarray sub (left ++ right) :=
exact ⟨hsubNonempty, left ++ before, after,
⟩The contiguous-subarray enumerator is exact.
theorem mem_nonemptySubarrays_iff {sub xs : List Int} :
sub ∈ nonemptySubarrays xs ↔ IsNonemptySubarray sub xs :=
induction xs generalizing sub with
exact ⟨hsubNonempty, ⟨[], rest, ⟩⟩
exact ⟨hsubNonempty, ⟨x :: before, after, ⟩⟩
cases before with
exact mem_nonemptyPrefixes_iff.mpr
⟨hsubNonempty, ⟨after, ⟩⟩
exact ih.mpr
⟨hsubNonempty, ⟨beforeTail, after,
⟩⟩Split classification
Every nonempty subarray of a concatenation is either fully in the left half, fully in the right half, or crosses the split.
This is the structural lemma needed by the CLRS divide-and-conquer proof after the recursive calls and the crossing helper have produced their local winners.
exact ⟨hsubNonempty, ⟨beforeRight, after,
⟩⟩
exact ⟨hsubNonempty, ⟨before, leftAfter,
⟩⟩
cases leftRest with
exact ⟨hsubNonempty, ⟨[], after, ⟩⟩
cases rightPrefix with
exact ⟨hsubNonempty, ⟨before, [],
⟩⟩
exact ⟨x :: xs, y :: ys,
⟨ , ⟨before, hleft⟩⟩,
⟨ , ⟨after, hright⟩⟩,
hsubEq⟩If a candidate dominates every left-only, right-only, and crossing subarray, then it dominates every nonempty subarray of the concatenated input.
theorem subarray_append_optimal_of_cases {best left right : List Int}
(hleft :
∀ cand, IsNonemptySubarray cand left →
subarraySum cand ≤ subarraySum best)
(hright :
∀ cand, IsNonemptySubarray cand right →
subarraySum cand ≤ subarraySum best)
(hcross :
∀ cand, IsCrossingSubarray cand left right →
subarraySum cand ≤ subarraySum best) :
∀ cand, IsNonemptySubarray cand (left ++ right) →
subarraySum cand ≤ subarraySum best :=
Finite argmax
Choose the candidate with greater sum, breaking ties toward the first one.
def betterCandidate (a b : List Int) : List Int :=
if subarraySum a < subarraySum b then b else aA finite maximum-by-sum selector for a list of candidates.
def bestCandidate : List (List Int) → Option (List Int)
| [] => none
| cand :: rest =>
match bestCandidate rest with
| none => some cand
| some best => some (betterCandidate cand best)The finite selector returns an element of the candidate list whose sum is at least every candidate sum.
Every nonempty candidate list has a selected best candidate.
theorem bestCandidate_exists_of_ne_nil {candidates : List (List Int)}
(hcandidates : candidates ≠ []) :
∃ best, bestCandidate candidates = some best :=
cases candidates with
cases hrest : bestCandidate rest with
If the finite argmax selector returns no candidate, the list was empty.
Crossing-subarray helper
Choose a maximum-sum subarray that crosses the split between left and
right. If either side is empty there is no crossing candidate.
def maxCrossingSubarray (left right : List Int) : Option (List Int) :=
bestCandidate (crossingSubarrays left right)Empty left sides have no crossing candidate.
theorem maxCrossingSubarray_nil_left (right : List Int) :
maxCrossingSubarray [] right = none :=
Empty right sides have no crossing candidate.
theorem maxCrossingSubarray_nil_right (left : List Int) :
maxCrossingSubarray left [] = none :=
Nonempty left and right sides have at least one crossing candidate.
theorem maxCrossingSubarray_exists_of_ne_nil {left right : List Int}
(hleft : left ≠ []) (hright : right ≠ []) :
∃ best, maxCrossingSubarray left right = some best :=
cases left with
cases right with
Correctness of the CLRS crossing helper: whenever it returns a candidate, that candidate crosses the split and has maximum sum among all crossing candidates.
theorem maxCrossingSubarray_correct {left right best : List Int}
(hbest : maxCrossingSubarray left right = some best) :
IsCrossingSubarray best left right ∧
∀ cand, IsCrossingSubarray cand left right →
subarraySum cand ≤ subarraySum best :=
If the crossing helper returns no candidate, no crossing candidate exists.
The crossing helper returns an ordinary nonempty contiguous subarray of the concatenated input.
theorem maxCrossingSubarray_isNonemptySubarray_append {left right best : List Int}
(hbest : maxCrossingSubarray left right = some best) :
IsNonemptySubarray best (left ++ right) :=
Maximum-subarray selector
Exhaustively choose a maximum-sum nonempty contiguous subarray. Empty inputs
have no nonempty candidate and therefore return none.
def maxSubarray (xs : List Int) : Option (List Int) :=
bestCandidate (nonemptySubarrays xs)
The selector returns none on the empty input.
theorem maxSubarray_nil :
maxSubarray [] = none :=
Nonempty inputs have at least one nonempty contiguous-subarray candidate.
theorem maxSubarray_exists_of_ne_nil {xs : List Int} (hxs : xs ≠ []) :
∃ best, maxSubarray xs = some best :=
cases xs with
Correctness of the maximum-subarray selector: whenever it returns a candidate, that candidate is a nonempty contiguous subarray and has maximum sum among all nonempty contiguous subarrays of the input.
theorem maxSubarray_correct {xs best : List Int}
(hbest : maxSubarray xs = some best) :
IsNonemptySubarray best xs ∧
∀ cand, IsNonemptySubarray cand xs →
subarraySum cand ≤ subarraySum best :=
If the exhaustive selector returns no candidate, no nonempty subarray exists.
Unified result specification for maximum-subarray selectors.
Returning none means that there is no nonempty contiguous subarray.
Returning some best means that best is a valid candidate whose
sum dominates every valid candidate.
def IsMaxSubarrayResult (xs : List Int) : Option (List Int) → Prop
| none => ∀ cand, ¬ IsNonemptySubarray cand xs
| some best =>
IsNonemptySubarray best xs ∧
∀ cand, IsNonemptySubarray cand xs →
subarraySum cand ≤ subarraySum bestThe exhaustive selector satisfies the unified result specification.
theorem maxSubarray_result_correct (xs : List Int) :
IsMaxSubarrayResult xs (maxSubarray xs) :=
cases hbest : maxSubarray xs with
Executable divide-and-conquer combine step
Combine already-computed left and right winners with the crossing winner.
This is the local executable step used both by maxSubarrayDivideStep and
by the recursive split-tree selector below.
def maxSubarrayCombineOptions (left right : List Int)
(leftBest rightBest : Option (List Int)) : Option (List Int) :=
bestCandidate
(leftBest.toList ++ rightBest.toList ++
(maxCrossingSubarray left right).toList)The local combine step preserves the maximum-subarray result contract.
One executable CLRS divide-and-conquer combine step.
The left and right subproblems are solved by the already-proved exact selector,
and the crossing case is solved by maxCrossingSubarray. The step then
selects the best among the available local winners.
def maxSubarrayDivideStep (left right : List Int) : Option (List Int) :=
maxSubarrayCombineOptions left right (maxSubarray left) (maxSubarray right)Correctness of the executable divide-and-conquer combine step: whenever it returns a candidate, that candidate is a nonempty subarray of the concatenated input and dominates every nonempty subarray of that input.
Recursive divide-and-conquer selector
An explicit split tree for divide-and-conquer maximum-subarray selection.
Leaves are solved directly by the exact selector. Internal nodes combine the recursive winners from the left and right children with the crossing helper.
inductive SubarraySplitTree where
| leaf (xs : List Int)
| split (left right : SubarraySplitTree)namespace SubarraySplitTreeThe input list represented by a split tree.
def input : SubarraySplitTree → List Int
| leaf xs => xs
| split left right => input left ++ input rightend SubarraySplitTreeRecursive divide-and-conquer selector over an explicit split tree.
def maxSubarrayDivideTree : SubarraySplitTree → Option (List Int)
| .leaf xs => maxSubarray xs
| .split left right =>
maxSubarrayCombineOptions left.input right.input
(maxSubarrayDivideTree left) (maxSubarrayDivideTree right)The recursive split-tree selector satisfies the maximum-subarray contract.
theorem maxSubarrayDivideTree_result_correct (tree : SubarraySplitTree) :
IsMaxSubarrayResult tree.input (maxSubarrayDivideTree tree) :=
induction tree with
Correctness of the recursive split-tree selector: whenever it returns a candidate, that candidate is globally optimal for the input represented by the tree.
Build a split tree by repeatedly splitting at the midpoint, for at most
fuel recursive levels. When fuel runs out, the remaining chunk becomes a
leaf and is solved by the exact selector.
def midpointSplitTree : Nat → List Int → SubarraySplitTree
| 0, xs => .leaf xs
| _fuel + 1, [] => .leaf []
| _fuel + 1, [x] => .leaf [x]
| fuel + 1, xs =>
let mid := xs.length / 2
.split (midpointSplitTree fuel (xs.take mid))
(midpointSplitTree fuel (xs.drop mid))The fuelled midpoint split tree represents exactly the original input.
theorem midpointSplitTree_input (fuel : Nat) (xs : List Int) :
(midpointSplitTree fuel xs).input = xs :=
induction fuel generalizing xs with
cases xs with
cases xs with
A fuelled executable divide-and-conquer selector. Correctness holds for every fuel value; larger fuel simply refines more leaves before falling back to the exact selector.
def maxSubarrayDivideFuel (fuel : Nat) (xs : List Int) : Option (List Int) :=
maxSubarrayDivideTree (midpointSplitTree fuel xs)Correctness of the fuelled midpoint divide-and-conquer selector for the original list input.
theorem maxSubarrayDivideFuel_correct {fuel : Nat} {xs best : List Int}
(hbest : maxSubarrayDivideFuel fuel xs = some best) :
IsNonemptySubarray best xs ∧
∀ cand, IsNonemptySubarray cand xs →
subarraySum cand ≤ subarraySum best :=
end Chapter04end CLRS