Imports
import MathlibCLRS Section 2.2 - Analyzing algorithms
This file records the first lightweight cost model used in the Chapter 2 workflow. It does not try to formalize a full RAM model yet. Instead it captures the standard insertion-sort worst-case comparison count as a triangular sum and proves a quadratic upper bound.
namespace CLRSnamespace Chapter02
The triangular sum 1 + 2 + ... + n.
def triangular : Nat → Nat
| 0 => 0
| n + 1 => triangular n + (n + 1)A small eventual upper-bound predicate for chapter-level runtime claims.
def EventuallyBoundedBy (f g : Nat → Nat) : Prop :=
∃ c n₀, 0 < c ∧ ∀ n, n₀ ≤ n → f n ≤ c * g n
The usual worst-case comparison count for insertion sort on n elements.
def insertionSortWorstComparisons (n : Nat) : Nat :=
triangular (n - 1)theorem triangular_le_square (n : Nat) : triangular n ≤ n * n :=
induction n with
theorem insertionSortWorstComparisons_quadratic (n : Nat) :
insertionSortWorstComparisons n ≤ n * n :=
exact (triangular_le_square (n - 1)).trans ( )theorem insertionSortWorstComparisons_eventually_quadratic :
EventuallyBoundedBy insertionSortWorstComparisons (fun n => n * n) :=
refine ⟨1, 0, , ?_⟩
end Chapter02end CLRS