Insertion sort

AbbreviationCharged comparison#✓fully proved

For elements \(x\) and \(y\) of a linearly ordered type, this computation returns the truth value of \(x \le y\) and charges one unit of time.

abbrev compareLE (x y : α) : TimeM Nat Bool := do
  ✓ return decide (x ≤ y)

Used by 11

Used byBucket sort permutes its input · Exact cost of bucket sort · Lower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · The running time of bucket sort is integrable · The running time of bucket sort is measurable · Agreement with CSLib's monadic insertion sort · Costed insertion into a list · Cost of a single insertion · Costed insertion returns the ordered insertion

DefinitionCosted insertion into a list#✓fully proved

Let \(a\) be an element of a linearly ordered type. Inserting \(a\) into the empty list returns \([a]\) at no cost. Inserting \(a\) into a list with head \(b\) and tail \(l\) first charges one unit for comparing \(a \le b\); if \(a \le b\) it returns \(a\) followed by \(b\) and \(l\), and otherwise it inserts \(a\) into \(l\), adding that cost, and returns \(b\) followed by the result.

def insertionSortInsert (a : α) : List α → TimeM Nat (List α)
  | [] => pure [a]
  | b :: xs => TimeM.bind (compareLE a b) fun before =>
      if before then pure (a :: b :: xs)
      else TimeM.bind (insertionSortInsert a xs) fun tail => pure (b :: tail)

Uses 1 · Used by 6

Statement usesCharged comparison

Used byInsertion sort with comparison cost · Agreement with CSLib's monadic insertion sort · Cost of a single insertion · Comparison bound for insertion sort · Cost-annotated insertion sort returns the standard insertion sort · Costed insertion returns the ordered insertion

DefinitionInsertion sort with comparison cost#✓fully proved

On a list over a linearly ordered type, insertion sort returns the empty list at no cost when the input is empty. On a list with head \(a\) and tail \(l\), it sorts \(l\) and then inserts \(a\) into the result by costed insertion; its cost is the cost of sorting \(l\) plus the cost of that insertion. Exactly one unit is charged for each order comparison.

def insertionSort : List α → TimeM Nat (List α)
  | [] => pure []
  | a :: xs => TimeM.bind (insertionSort xs) (insertionSortInsert a)

Uses 1 · Used by 22

Statement usesCosted insertion into a list

Used byBucket sort · Bucket sort on the empty array · Bucket sort permutes its input · Bucket sort sorts · Exact cost of bucket sort · Lower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · The running time of bucket sort is integrable · Bound on the cost of bucket sort via squared bucket sizes · Linear lower bound on the cost of bucket sort · The running time of bucket sort is measurable · Correctness of insertion sort · Agreement with CSLib's monadic insertion sort · Insertion sort permutes its input · Insertion sort returns a sorted list · Comparison bound for insertion sort · Cost-annotated insertion sort returns the standard insertion sort · Group medians for median-of-medians selection · Group medians are lower medians of their blocks · Group medians come from the input · Comparison cost of the group medians

TheoremCosted insertion returns the ordered insertion#✓fully proved

For an element \(a\) and a list \(l\) over a linearly ordered type, the list returned by costed insertion of \(a\) into \(l\) is the ordered insertion of \(a\) into \(l\) with respect to \(\le\): \(a\) is placed immediately before the first element \(b\) of \(l\) with \(a \le b\), or at the end of \(l\) if there is no such element.

theorem ret_insertionSortInsert (a : α) (xs : List α) :
    (insertionSortInsert a xs).ret = List.orderedInsert (fun x y => x ≤ y) a xs

Uses 2 · Used by 1

Statement usesCosted insertion into a list

Proof usesCharged comparison

Used byCost-annotated insertion sort returns the standard insertion sort

TheoremCost-annotated insertion sort returns the standard insertion sort#✓fully proved

For every list \(xs\) over a linearly ordered type, the list returned by insertion sort with comparison costs equals the standard insertion sort of \(xs\) with respect to \(\le\), which inserts the head into the sorted tail.

@[simp]
theorem ret_insertionSort (xs : List α) :
    (insertionSort xs).ret = List.insertionSort (fun x y => x ≤ y) xs

Uses 3 · Used by 3

Statement usesInsertion sort with comparison cost

Proof usesCosted insertion into a list · Costed insertion returns the ordered insertion

Used byInsertion sort permutes its input · Insertion sort returns a sorted list · Group medians are lower medians of their blocks

TheoremAgreement with CSLib's monadic insertion sort#✓fully proved

For a list \(l\) over a linearly ordered type in the lowest universe, the costed insertion sort of \(l\) equals CSLib's generic monadic insertion sort run in the time-counting monad with the charged comparison: the returned lists agree and the numbers of charged comparisons agree.

@[simp]
theorem insertionSort_eq_insertionSortM {β : Type} [LinearOrder β] (xs : List β) :
    insertionSort xs = List.insertionSortM compareLE xs

Uses 3 · Used by 7

Statement usesCharged comparison · Insertion sort with comparison cost

Proof usesCosted insertion into a list

Used byBucket sort permutes its input · Exact cost of bucket sort · Lower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · The running time of bucket sort is integrable · The running time of bucket sort is measurable

TheoremInsertion sort returns a sorted list#✓fully proved

For every list \(l\) over a linearly ordered type, the list returned by insertion sort on \(l\) is nondecreasing.

theorem insertionSort_sorted (xs : List α) :
    List.Pairwise (fun x y => x ≤ y) (insertionSort xs).ret

Uses 2 · Used by 2

Statement usesInsertion sort with comparison cost

Proof usesCost-annotated insertion sort returns the standard insertion sort

Used byBucket sort sorts · Correctness of insertion sort

TheoremInsertion sort permutes its input#✓fully proved

For every list \(l\) over a linearly ordered type, the list returned by insertion sort is a permutation of \(l\); in particular every element occurs in it exactly as often as in \(l\).

theorem insertionSort_perm (xs : List α) : List.Perm (insertionSort xs).ret xs

Uses 2 · Used by 12

Statement usesInsertion sort with comparison cost

Proof usesCost-annotated insertion sort returns the standard insertion sort

Used byBucket sort permutes its input · Bucket sort sorts · Exact cost of bucket sort · Lower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · The running time of bucket sort is integrable · The running time of bucket sort is measurable · Correctness of insertion sort · Comparison bound for insertion sort · Group medians are lower medians of their blocks · Group medians come from the input

TheoremCorrectness of insertion sort#✓fully proved

For every list \(l\) over a linearly ordered type, the list returned by insertion sort is nondecreasing and is a permutation of \(l\).

theorem insertionSort_correct (xs : List α) :
    List.Pairwise (fun x y => x ≤ y) (insertionSort xs).ret ∧
      List.Perm (insertionSort xs).ret xs

Uses 3

Statement usesInsertion sort with comparison cost

Proof usesInsertion sort permutes its input · Insertion sort returns a sorted list

TheoremCost of a single insertion#✓fully proved

For an element \(a\) and a list \(l\) over a linearly ordered type, costed insertion of \(a\) into \(l\) charges at most \(n\) comparisons, where \(n\) is the length of \(l\).

theorem insertionSortInsert_time_le (a : α) (xs : List α) :
    (insertionSortInsert a xs).time ≤ xs.length

Uses 2 · Used by 1

Statement usesCosted insertion into a list

Proof usesCharged comparison

Used byComparison bound for insertion sort

TheoremComparison bound for insertion sort#✓fully proved

On a list of length \(n\) over a linearly ordered type, insertion sort charges at most \(n(n-1)/2\) comparisons.

theorem insertionSort_time (xs : List α) :
    (insertionSort xs).time ≤ xs.length * (xs.length - 1) / 2

Uses 4 · Used by 6

Statement usesInsertion sort with comparison cost

Proof usesCosted insertion into a list · Cost of a single insertion · Insertion sort permutes its input

Used byLower bound on the expected time of bucket sort · Expected time of bucket sort on one input · Upper bound on the expected time of bucket sort · The running time of bucket sort is integrable · Bound on the cost of bucket sort via squared bucket sizes · Comparison cost of the group medians

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.