From 34f3bae71e05a2981e881004a1d841f0c607bbb7 Mon Sep 17 00:00:00 2001 From: robert Date: Tue, 19 May 2026 19:16:40 +0000 Subject: [PATCH 1/2] feat(algorithms): add stable insertion sort --- Cslib.lean | 2 + .../Lean/InsertionSort/InsertionSort.lean | 156 ++++++++++++++++++ Cslib/Algorithms/Lean/Sorting.lean | 28 ++++ 3 files changed, 186 insertions(+) create mode 100644 Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean create mode 100644 Cslib/Algorithms/Lean/Sorting.lean diff --git a/Cslib.lean b/Cslib.lean index 1b7b4c4b1..bb6a31a56 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,6 +1,8 @@ module -- shake: keep-all +public import Cslib.Algorithms.Lean.InsertionSort.InsertionSort public import Cslib.Algorithms.Lean.MergeSort.MergeSort +public import Cslib.Algorithms.Lean.Sorting public import Cslib.Algorithms.Lean.TimeM public import Cslib.Computability.Automata.Acceptors.Acceptor public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean new file mode 100644 index 000000000..25aa13e85 --- /dev/null +++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean @@ -0,0 +1,156 @@ +/- +Copyright (c) 2026 Robert Joseph George. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robert Joseph George +-/ + +module + +public import Cslib.Algorithms.Lean.Sorting +public import Cslib.Algorithms.Lean.TimeM +public import Mathlib.Data.List.Sort +public import Mathlib.Data.Nat.Basic + +/-! +# Stable insertion sort on lists + +`insertionSort` returns a `TimeM ℕ (List α)`: the return value is the sorted list, and the time +component counts comparisons. + +Equal values are inserted before equal values already in the sorted tail. Since the sort processes +the input from right to left, this preserves the original order of equal values. + +The cost model charges exactly one tick for each comparison made while searching for the insertion +point. +-/ + +@[expose] public section + +set_option autoImplicit false + +namespace Cslib.Algorithms.Lean.TimeM + +variable {α : Type} [LinearOrder α] + +/-- +Inserts one value into a sorted list, counting comparisons as time cost. The test is `x ≤ y`, so +the new value is placed before equal values in the already-sorted tail. +-/ +def insert (x : α) : List α → TimeM ℕ (List α) + | [] => return [x] + | y :: ys => do + ✓ let inFront := x ≤ y + if inFront then + return x :: y :: ys + else + let rest ← insert x ys + return y :: rest + +/-- Sorts a list using stable insertion sort, counting comparisons as time cost. -/ +def insertionSort : List α → TimeM ℕ (List α) + | [] => return [] + | x :: xs => do + let sortedTail ← insertionSort xs + insert x sortedTail + +section Correctness + +/-- Timed `insert` computes mathlib's ordered insertion. -/ +@[simp, grind =] +theorem ret_insert (x : α) (xs : List α) : + ⟪insert x xs⟫ = xs.orderedInsert (· ≤ ·) x := by + induction xs with + | nil => simp [insert] + | cons y ys ih => + by_cases h : x ≤ y <;> simp [insert, h, ih] + +/-- Timed insertion sort computes mathlib's insertion sort. -/ +@[simp, grind =] +theorem ret_insertionSort (xs : List α) : + ⟪insertionSort xs⟫ = xs.insertionSort (· ≤ ·) := by + induction xs with + | nil => simp [insertionSort] + | cons x xs ih => simp [insertionSort, ih] + +/-- Inserting one value keeps exactly the original values. -/ +private theorem insert_perm (x : α) (xs : List α) : (⟪insert x xs⟫).Perm (x :: xs) := by + simpa using List.perm_orderedInsert (· ≤ ·) x xs + +/-- Insertion sort returns a permutation of its input. -/ +theorem insertionSort_perm (xs : List α) : (⟪insertionSort xs⟫).Perm xs := by + simpa using List.perm_insertionSort (· ≤ ·) xs + +/-- Inserting one value is stable with respect to filtering by any fixed value. -/ +private theorem insert_stable (x : α) (xs : List α) : StableByValue (x :: xs) ⟪insert x xs⟫ := by + induction xs with + | nil => simp [StableByValue, insert] + | cons y ys ih => + intro z + by_cases h : x ≤ y + · simp [insert, h] + · have ihz := ih z + by_cases hyz : y = z <;> by_cases hxz : x = z <;> grind [insert] + +/-- +Insertion sort is stable. The induction uses stability of the recursive tail and then stability of +one insertion step. +-/ +theorem insertionSort_stable (xs : List α) : StableByValue xs ⟪insertionSort xs⟫ := by + induction xs with + | nil => simp [StableByValue, insertionSort] + | cons x xs ih => + intro z + simp only [insertionSort, ret_bind] + rw [insert_stable x ⟪insertionSort xs⟫ z] + simp only [List.filter_cons] + rw [ih z] + +/-- Insertion sort returns a sorted list. -/ +theorem insertionSort_sorted (xs : List α) : List.Pairwise (· ≤ ·) ⟪insertionSort xs⟫ := by + simpa using List.pairwise_insertionSort (· ≤ ·) xs + +/-- Insertion sort is functionally correct. -/ +theorem insertionSort_correct (xs : List α) : List.Pairwise (· ≤ ·) ⟪insertionSort xs⟫ ∧ + (⟪insertionSort xs⟫).Perm xs ∧ StableByValue xs ⟪insertionSort xs⟫ := by + exact ⟨insertionSort_sorted xs, insertionSort_perm xs, insertionSort_stable xs⟩ + +end Correctness + +section TimeComplexity + +/-- Inserting into a list performs at most one comparison per possible insertion point. -/ +private theorem insert_time_le (x : α) (xs : List α) : (insert x xs).time ≤ xs.length + 1 := by + induction xs with + | nil => simp [insert] + | cons y ys ih => + by_cases h : x ≤ y + · simp [insert, h] + · simp [insert, h] + omega + +/-- Insertion sort preserves length. -/ +private theorem insertionSort_length (xs : List α) : ⟪insertionSort xs⟫.length = xs.length := by + simp + +/-- Time complexity of insertion sort. -/ +theorem insertionSort_time (xs : List α) : + let n := xs.length + (insertionSort xs).time ≤ n * n := by + induction xs with + | nil => simp [insertionSort] + | cons x xs ih => + simp only [List.length_cons] + simp only [insertionSort, time_bind] + have hinsert := insert_time_le x ⟪insertionSort xs⟫ + have hlen : ⟪insertionSort xs⟫.length = xs.length := by simp + have hsquare : xs.length * xs.length + (xs.length + 1) ≤ + (xs.length + 1) * (xs.length + 1) := by + exact Nat.le_trans + (Nat.add_le_add_right + (Nat.mul_le_mul_right xs.length (Nat.le_succ xs.length)) (xs.length + 1)) + (by rw [Nat.mul_succ]) + omega + +end TimeComplexity + +end Cslib.Algorithms.Lean.TimeM diff --git a/Cslib/Algorithms/Lean/Sorting.lean b/Cslib/Algorithms/Lean/Sorting.lean new file mode 100644 index 000000000..e20257d9d --- /dev/null +++ b/Cslib/Algorithms/Lean/Sorting.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2026 Robert Joseph George. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robert Joseph George +-/ + +module + +public import Cslib.Init + +/-! +# Sorting utilities + +For stable list sorts, filtering the input and output by any value records the relative order of +the copies of that value. +-/ + +@[expose] public section + +set_option autoImplicit false + +namespace Cslib.Algorithms.Lean + +/-- `ys` preserves the order of equal values from `xs`. -/ +abbrev StableByValue {α : Type*} [DecidableEq α] (xs ys : List α) : Prop := + ∀ value, ys.filter (fun x => x = value) = xs.filter (fun x => x = value) + +end Cslib.Algorithms.Lean From ef927a28af6948c6eb467c8fa5a5a982a034e121 Mon Sep 17 00:00:00 2001 From: robert Date: Tue, 19 May 2026 19:50:28 +0000 Subject: [PATCH 2/2] Address insertion sort review comments --- .../Lean/InsertionSort/InsertionSort.lean | 19 +++++++++++++++---- Cslib/Algorithms/Lean/Sorting.lean | 8 +++++--- 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean index 25aa13e85..3e35a6b3b 100644 --- a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean +++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean @@ -30,7 +30,7 @@ set_option autoImplicit false namespace Cslib.Algorithms.Lean.TimeM -variable {α : Type} [LinearOrder α] +variable {α : Type*} [LinearOrder α] /-- Inserts one value into a sorted list, counting comparisons as time cost. The test is `x ≤ y`, so @@ -89,7 +89,18 @@ private theorem insert_stable (x : α) (xs : List α) : StableByValue (x :: xs) by_cases h : x ≤ y · simp [insert, h] · have ihz := ih z - by_cases hyz : y = z <;> by_cases hxz : x = z <;> grind [insert] + by_cases hyz : y = z + · by_cases hxz : x = z + · subst x + subst y + exact (h le_rfl).elim + · have hxlez : ¬x ≤ z := by simpa [hyz] using h + simpa [insert, hxlez, hxz, hyz] using ihz + · by_cases hxz : x = z + · subst x + have hzley : ¬z ≤ y := by simpa using h + simpa [insert, hzley, hyz] using ihz + · simpa [insert, h, hyz, hxz] using ihz /-- Insertion sort is stable. The induction uses stability of the recursive tail and then stability of @@ -142,14 +153,14 @@ theorem insertionSort_time (xs : List α) : simp only [List.length_cons] simp only [insertionSort, time_bind] have hinsert := insert_time_le x ⟪insertionSort xs⟫ - have hlen : ⟪insertionSort xs⟫.length = xs.length := by simp + rw [insertionSort_length xs] at hinsert have hsquare : xs.length * xs.length + (xs.length + 1) ≤ (xs.length + 1) * (xs.length + 1) := by exact Nat.le_trans (Nat.add_le_add_right (Nat.mul_le_mul_right xs.length (Nat.le_succ xs.length)) (xs.length + 1)) (by rw [Nat.mul_succ]) - omega + exact (Nat.add_le_add ih hinsert).trans hsquare end TimeComplexity diff --git a/Cslib/Algorithms/Lean/Sorting.lean b/Cslib/Algorithms/Lean/Sorting.lean index e20257d9d..332b64e94 100644 --- a/Cslib/Algorithms/Lean/Sorting.lean +++ b/Cslib/Algorithms/Lean/Sorting.lean @@ -11,8 +11,10 @@ public import Cslib.Init /-! # Sorting utilities -For stable list sorts, filtering the input and output by any value records the relative order of -the copies of that value. +For stable list sorts, filtering the input and output by any value gives a compact way to state that +the output keeps the same per-value subsequence as the input. For plain values this is equivalent to +preserving the number of copies of each value; for richer element types it can express a stronger +order-preservation property. -/ @[expose] public section @@ -23,6 +25,6 @@ namespace Cslib.Algorithms.Lean /-- `ys` preserves the order of equal values from `xs`. -/ abbrev StableByValue {α : Type*} [DecidableEq α] (xs ys : List α) : Prop := - ∀ value, ys.filter (fun x => x = value) = xs.filter (fun x => x = value) + ∀ value, ys.filter (fun x => decide (x = value)) = xs.filter (fun x => decide (x = value)) end Cslib.Algorithms.Lean