From f0abc13487398457fbf352b0863ef44caaa66bfd Mon Sep 17 00:00:00 2001 From: Curly-Howard-Chungus Correspondence | Lamport-Cabot-Codd-Backus-Naur Form Date: Mon, 23 Feb 2026 11:26:00 +0000 Subject: [PATCH 1/4] feat(algorithms): add InsertionSort and Sorting definitions * Introduced InsertionSort algorithm. * Added shared sorting definitions for ascending and descending orders. * Updated MergeSort to reflect changes in sorting definitions. --- Cslib.lean | 2 + .../Lean/InsertionSort/InsertionSort.lean | 367 ++++++++++++++++++ .../Algorithms/Lean/MergeSort/MergeSort.lean | 51 ++- Cslib/Algorithms/Lean/Sorting.lean | 107 +++++ 4 files changed, 500 insertions(+), 27 deletions(-) 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 8905be5f..71a6ab4b 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 00000000..19186dd0 --- /dev/null +++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean @@ -0,0 +1,367 @@ +/- +Copyright (c) 2026 Trong-Nghia Be. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Trong-Nghia Be +-/ + +module + +public import Cslib.Algorithms.Lean.Sorting +public import Mathlib.Data.Nat.Cast.Order.Ring + +@[expose] public section + +/-! +# InsertionSort on a list + +In this file we introduce `insert` and `insertionSort` algorithms that return a time monad +over the list `TimeM ℕ (List α)`. The time complexity of `insertionSort` is the number of +comparisons. + +-- +## Main results + +- `insertionSort_correct`: `insertionSort` permutes the list into a sorted one. +- `insertionSort_time`: The number of comparisons of `insertionSort` is at most `(n * (n - 1)) / 2`. + +-/ + +set_option autoImplicit false + +namespace Cslib.Algorithms.Lean.TimeM + +variable {α : Type} [LinearOrder α] + +/-- Inserts an element `x` into a sorted list, counting comparisons as time cost. +Returns a `TimeM ℕ (List α)` where the time represents the number of comparisons performed. +-/ +def insert (x : α) : List α → TimeM ℕ (List α) + -- Base case: Inserting into an empty list just returns a singleton list with no comparisons. + | [] => return [x] + -- Recursive case: Compare `x` with the head `y` of the list, + -- then recursively insert into the tail. + | y :: ys => do + -- Each comparison of `x` with `y` costs 1 unit of time. + -- Define `c` as the result of the comparison, and charge for it. + ✓ let c := (x ≤ y : Bool) + -- If `x` is less than or equal to `y`, we can place `x` before `y` without further comparisons. + if c then + return (x :: y :: ys) + -- Otherwise, we need to insert `x` into the tail `ys`, which may involve more comparisons. + else + let rest ← insert x ys + return (y :: rest) + +/-- Sorts a list using the `insertionSort` algorithm, counting comparisons as time cost. +Returns a `TimeM ℕ (List α)` where the time represents the total number of comparisons. +-/ +def insertionSort : List α → TimeM ℕ (List α) + -- Base case: An empty list is already sorted, so we return it with no time cost. + | [] => return [] + -- Recursive case: Sort the tail of the list, then insert the head into the sorted tail. + | x :: xs => do + let sorted ← insertionSort xs + insert x sorted + +section Correctness + +open List + +/-- If `z` is in the result of inserting `x` into `ys`, then `z` is either `x` +or an element of `ys`. +-/ +@[grind →] +theorem mem_insert_ret (x : α) (ys : List α) (z : α) (hz : z ∈ ⟪insert x ys⟫) : + z = x ∨ z ∈ ys := by + -- The proof proceeds by induction on the structure of the function `insert`. + fun_induction insert x ys with + -- Case 1: Inserting into an empty list. + | case1 => + simp only [ret_pure] at hz + exact Or.inl (List.mem_singleton.mp hz) + -- Case 2: Inserting into a non-empty list `y :: ys`. + | case2 => + grind + +/-- If `ys` is a sorted list and `x` is inserted into `ys`, then the result is also sorted. +-/ +theorem sorted_insert (x : α) (ys : List α) (hys : IsSortedAscending ys) : + IsSortedAscending ⟪insert x ys⟫ := by + -- The proof proceeds by induction on the structure of the function `insert`. + fun_induction insert x ys with + -- Case 1: Inserting into an empty list. + | case1 => + simp [IsSortedAscending] + -- Case 2: Inserting into a non-empty list `y :: ys`. + | case2 => + grind [pairwise_cons] + +/-- If `x` is inserted into a list `ys`, then the result is a permutation of `x :: ys`. +-/ +theorem insert_perm (x : α) (ys : List α) : + ⟪insert x ys⟫ ~ x :: ys := by + -- The proof proceeds by induction on the structure of the function `insert`. + fun_induction insert x ys with + -- Case 1: Inserting into an empty list. + | case1 => + simp [Perm.refl] + -- Case 2: Inserting into a non-empty list `y :: ys`. + | case2 => + simp only [ret_bind] + grind + +/-- If `insertionSort` is applied to a list `xs`, then the result is a sorted list. +-/ +theorem insertionSort_sorted (xs : List α) : + IsSortedAscending ⟪insertionSort xs⟫ := by + -- The proof proceeds by induction on the structure of the function `insertionSort`. + fun_induction insertionSort xs with + -- Case 1: Sorting an empty list. + | case1 => + simp [IsSortedAscending] + -- Case 2: Sorting a non-empty list `x :: xs`. + | case2 x xs ih => + simp only [ret_bind] + exact sorted_insert _ _ ih + +/-- If `insertionSort` is applied to a list `xs`, then the result is a permutation of `xs`. +-/ +theorem insertionSort_perm (xs : List α) : + ⟪insertionSort xs⟫ ~ xs := by + -- The proof proceeds by induction on the structure of the function `insertionSort`. + fun_induction insertionSort xs with + -- Case 1: Sorting an empty list. + | case1 => + simp + -- Case 2: Sorting a non-empty list `x :: xs`. + | case2 x xs ih => + simp only [ret_bind] + exact (insert_perm _ _).trans (Perm.cons _ ih) + +/-- Functional correctness of `insertionSort`. + +If `insertionSort` is applied to a list `xs`, then the result is: +(1) a sorted list, and +(2) a permutation of `xs`. +-/ +theorem insertionSort_correct (xs : List α) : + let sorted_xs := ⟪insertionSort xs⟫ + IsSortedAscending sorted_xs ∧ sorted_xs ~ xs := + -- Combine the results of `insertionSort_sorted` and `insertionSort_perm` to conclude correctness. + ⟨insertionSort_sorted xs, insertionSort_perm xs⟩ + +end Correctness + +section TimeComplexity + +open List + +/-- Recurrence relation for the time complexity of `insertionSort`. + +For a list of length `n`, this counts the worst-case total number of comparisons: +- Base case: 0 comparisons for an empty list. +- Recursive case: Sort the tail (cost `timeInsertionSortRec (n-1)`), + then insert into the sorted tail (worst-case `n-1` comparisons). +-/ +def timeInsertionSortRec : ℕ → ℕ + | 0 => 0 + | n + 1 => timeInsertionSortRec n + n + +/-- The recurrence solves to exactly `n*(n-1)/2`, stated without division. -/ +theorem timeInsertionSortRec_eq (n : ℕ) : + 2 * timeInsertionSortRec n = n * (n - 1) := by + -- The proof proceeds by induction on `n`. + induction n with + -- Base case: `n = 0`. + | zero => + rfl + -- Inductive case: Assume the statement holds for `n`, and prove it for `n + 1`. + | succ n ih => + unfold timeInsertionSortRec + cases n with + | zero => + simp [timeInsertionSortRec] + | succ m => + simp only [Nat.succ_sub_one] at ih ⊢ + rw [mul_add, ih, mul_comm 2 (m + 1), ← mul_add] + exact mul_comm _ _ + +/-- Inserting an element `x` into a list `ys` results in a list with length +equal to `ys.length + 1`. +-/ +@[simp] +theorem insert_ret_length (x : α) (ys : List α) : + ⟪insert x ys⟫.length = ys.length + 1 := by + -- The proof proceeds by induction on the structure of the function `insert`. + fun_induction insert x ys with + -- Case 1: Inserting into an empty list. + | case1 => + simp + -- Case 2: Inserting into a non-empty list `y :: ys`. + | case2 => + grind + +/-- If `x ≤ y`, inserting `x` into a list `ys` with head `y` results in a list +starting with `x`, followed by `y` and the rest of `ys`. +-/ +@[simp] +theorem insert_ret_of_le (x y : α) (ys : List α) (h : x ≤ y) : + ⟪insert x (y :: ys)⟫ = x :: y :: ys := by + unfold insert + simp [h] + +/-- Applying `insertionSort` to a list `xs` results in a list with the same length as `xs`. +-/ +@[simp] +theorem insertionSort_same_length (xs : List α) : + ⟪insertionSort xs⟫.length = xs.length := by + -- The proof proceeds by induction on the structure of the function `insertionSort`. + fun_induction insertionSort with + -- Case 1: Sorting an empty list. + | case1 => + simp + -- Case 2: Sorting a non-empty list `x :: xs`. + | case2 => + grind [insert_ret_length] + +/-- `insertionSort` acts as an identity function on already-sorted lists. -/ +@[simp] +theorem insertionSort_eq_of_sorted (xs : List α) (h : IsSortedAscending xs) : + ⟪insertionSort xs⟫ = xs := by + induction xs with + | nil => + simp [insertionSort] + | cons x xs ih => + rw [IsSortedAscending, List.pairwise_cons] at h + have h_head : ∀ y ∈ xs, x ≤ y := h.left + have h_tail : IsSortedAscending xs := h.right + unfold insertionSort + simp only [ret_bind, ih h_tail] + cases xs with + | nil => + simp [insert] + | cons y ys => + have h_x_le_y : x ≤ y := h_head y List.mem_cons_self + simp [h_x_le_y] + +/-- If two lists are permutations of each other, any element-wise property +that holds for all elements of the first list also holds for the second. -/ +theorem forall_mem_of_perm {P : α → Prop} {l1 l2 : List α} -- TODO: Fix linter warning. + (h_perm : l1 ~ l2) (h_forall : ∀ a ∈ l1, P a) : + ∀ a ∈ l2, P a := by + intro a ha + have ha_in_l1 : a ∈ l1 := h_perm.mem_iff.mpr ha + exact h_forall a ha_in_l1 + +/-- If `x` is inserted into a list `ys`, then the time taken is at most the length of `ys`. +-/ +@[simp] +theorem insert_time (x : α) (ys : List α) : + (insert x ys).time ≤ ys.length := by + -- The proof proceeds by induction on the structure of the function `insert`. + fun_induction insert x ys with + -- Case 1: Inserting into an empty list. + | case1 => + simp + -- Case 2: Inserting into a non-empty list `y :: ys`. + | case2 => + simp only [time_bind] + grind + +/-- If an element `x` is less than or equal to the head `y`, insertion takes exactly 1 comparison. +-/ +@[simp] +theorem insert_time_of_le (x y : α) (ys : List α) (h : x ≤ y) : + (insert x (y :: ys)).time = 1 := by + unfold insert + simp [h] + +/-- If an element `x` is strictly greater than every element in `ys`, +insertion takes exactly `ys.length` comparisons. +-/ +@[simp] +theorem insert_time_of_gt_all (x : α) (ys : List α) (h : ∀ y ∈ ys, x > y) : + (insert x ys).time = ys.length := by + induction ys with + | nil => + simp [insert] + | cons y ys ih => + have h_head : y < x := h y List.mem_cons_self + have h_not_le : ¬(x ≤ y) := not_le_of_gt h_head + have h_tail : ∀ y' ∈ ys, x > y' := fun y' hy' => h y' (List.mem_cons_of_mem _ hy') + unfold insert + simp [h_not_le, ih h_tail, add_comm] + +/-- If `insertionSort` is applied to a list `xs`, +then the time taken is at most `timeInsertionSortRec xs.length`. +-/ +theorem insertionSort_time_le (xs : List α) : + (insertionSort xs).time ≤ timeInsertionSortRec xs.length := by + -- The proof proceeds by induction on the structure of the function `insertionSort`. + fun_induction insertionSort with + -- Case 1: Sorting an empty list. + | case1 => + grind + -- Case 2: Sorting a non-empty list `x :: xs`. + | case2 _ _ ih => + simp only [time_bind] + grw [insert_time] + simp only [insertionSort_same_length] + unfold timeInsertionSortRec + grind + +/-- Time complexity of `insertionSort`. + +If `insertionSort` is applied to a list `xs` of length `n`, +then the time taken is at most `(n * (n - 1)) / 2` (the worst-case number of comparisons). +-/ +theorem insertionSort_time (xs : List α) : + let n := xs.length + (insertionSort xs).time ≤ (n * (n - 1)) / 2 := by + grind [insertionSort_time_le, timeInsertionSortRec_eq] + +/-- Time complexity of `insertionSort` - Worst-case scenario. + +In the worst case, the input list is strictly sorted in descending order, +so each insertion requires comparing with every element in the sorted tail. + +Thus, the total time is `n * (n - 1) / 2` comparisons for a list of length `n`. +-/ +theorem insertionSort_time_worst_case (xs : List α) (h_sorted : IsStrictlySortedDescending xs) : + let n := xs.length + (insertionSort xs).time = n * (n - 1) / 2 := by + induction xs with + | nil => + -- Base case: n = 0. Time is 0. + simp [insertionSort] + | cons x xs ih => + rw [IsStrictlySortedDescending, List.pairwise_cons] at h_sorted + have h_head : ∀ y ∈ xs, x > y := h_sorted.left + have h_tail : IsStrictlySortedDescending xs := h_sorted.right + have ih_tail := ih h_tail + have h_perm : xs ~ ⟪insertionSort xs⟫ := (insertionSort_perm xs).symm + have h_gt_sorted : ∀ y ∈ ⟪insertionSort xs⟫, x > y := + forall_mem_of_perm h_perm h_head + unfold insertionSort + simp only [time_bind] + have h_insert_time : (insert x ⟪insertionSort xs⟫).time = ⟪insertionSort xs⟫.length := + insert_time_of_gt_all x ⟪insertionSort xs⟫ h_gt_sorted + rw [h_insert_time, ih_tail, insertionSort_same_length] + simp_all + sorry + +/-- Time complexity of `insertionSort` - Best-case scenario. + +In the best case, the input list is already sorted in ascending order, +so each insertion takes only 1 comparison. + +Thus, the total time is `n - 1` comparisons for a list of length `n`. +-/ +theorem insertionSort_time_best_case (xs : List α) (h_sorted : IsSortedAscending xs) : + let n := xs.length + (insertionSort xs).time = n - 1 := by + sorry + +end TimeComplexity + +end Cslib.Algorithms.Lean.TimeM diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean index 31f05103..2fd0ddb9 100644 --- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean +++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean @@ -1,12 +1,12 @@ /- -Copyright (c) 2025 Sorrachai Yingchareonthawornhcai. All rights reserved. +Copyright (c) 2026 Sorrachai Yingchareonthawornhcai. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sorrachai Yingchareonthawornhcai -/ module -public import Cslib.Algorithms.Lean.TimeM +public import Cslib.Algorithms.Lean.Sorting public import Mathlib.Data.Nat.Cast.Order.Ring public import Mathlib.Data.Nat.Lattice public import Mathlib.Data.Nat.Log @@ -34,6 +34,7 @@ namespace Cslib.Algorithms.Lean.TimeM variable {α : Type} [LinearOrder α] /-- Merges two lists into a single list, counting comparisons as time cost. + Returns a `TimeM ℕ (List α)` where the time represents the number of comparisons performed. -/ def merge : List α → List α → TimeM ℕ (List α) | [], ys => return ys @@ -47,7 +48,8 @@ def merge : List α → List α → TimeM ℕ (List α) let rest ← merge (x::xs') ys' return (y :: rest) -/-- Sorts a list using the merge sort algorithm, counting comparisons as time cost. +/-- Sorts a list using the `mergeSort` algorithm, counting comparisons as time cost. + Returns a `TimeM ℕ (List α)` where the time represents the total number of comparisons. -/ def mergeSort (xs : List α) : TimeM ℕ (List α) := do if xs.length < 2 then return xs @@ -63,12 +65,6 @@ section Correctness open List -/-- A list is sorted if it satisfies the `Pairwise (· ≤ ·)` predicate. -/ -abbrev IsSorted (l : List α) : Prop := List.Pairwise (· ≤ ·) l - -/-- `x` is a minimum element of list `l` if `x ≤ b` for all `b ∈ l`. -/ -abbrev MinOfList (x : α) (l : List α) : Prop := ∀ b ∈ l, x ≤ b - @[grind →] theorem mem_either_merge (xs ys : List α) (z : α) (hz : z ∈ ⟪merge xs ys⟫) : z ∈ xs ∨ z ∈ ys := by fun_induction merge @@ -81,14 +77,14 @@ theorem min_all_merge (x : α) (xs ys : List α) (hxs : MinOfList x xs) (hys : M MinOfList x ⟪merge xs ys⟫ := by grind -theorem sorted_merge {l1 l2 : List α} (hxs : IsSorted l1) (hys : IsSorted l2) : - IsSorted ⟪merge l1 l2⟫ := by +theorem sorted_merge {l1 l2 : List α} (hxs : IsSortedAscending l1) (hys : IsSortedAscending l2) : + IsSortedAscending ⟪merge l1 l2⟫ := by fun_induction merge l1 l2 with | case3 => grind [pairwise_cons] | _ => simpa -theorem mergeSort_sorted (xs : List α) : IsSorted ⟪mergeSort xs⟫ := by +theorem mergeSort_sorted (xs : List α) : IsSortedAscending ⟪mergeSort xs⟫ := by fun_induction mergeSort xs with | case1 x => rcases x with _ | ⟨a, _ | ⟨b, rest⟩⟩ <;> grind @@ -112,19 +108,20 @@ theorem mergeSort_perm (xs : List α) : ⟪mergeSort xs⟫ ~ xs := by _ ~ left++right := Perm.append ih2 ih1 _ ~ x := by simp only [take_append_drop, Perm.refl, left, right] -/-- MergeSort is functionally correct. -/ -theorem mergeSort_correct (xs : List α) : IsSorted ⟪mergeSort xs⟫ ∧ ⟪mergeSort xs⟫ ~ xs := +/-- `mergeSort` is functionally correct. -/ +theorem mergeSort_correct (xs : List α) : IsSortedAscending ⟪mergeSort xs⟫ ∧ ⟪mergeSort xs⟫ ~ xs := ⟨mergeSort_sorted xs, mergeSort_perm xs⟩ end Correctness section TimeComplexity -/-- Recurrence relation for the time complexity of merge sort. +/-- Recurrence relation for the time complexity of `mergeSort`. + For a list of length `n`, this counts the total number of comparisons: -- Base cases: 0 comparisons for lists of length 0 or 1 -- Recursive case: split the list, sort both halves, - then merge (which takes at most `n` comparisons) -/ +- Base cases: 0 comparisons for lists of length `0` or `1`. +- Recursive case: Split the list, sort both halves, + then merge (which takes at most `n` comparisons). -/ def timeMergeSortRec : ℕ → ℕ | 0 => 0 | 1 => 0 @@ -132,13 +129,13 @@ def timeMergeSortRec : ℕ → ℕ open Nat (clog) -/-- Key Lemma: ⌈log2 ⌈n/2⌉⌉ ≤ ⌈log2 n⌉ - 1 for n > 1 -/ +/-- Key Lemma: `⌈log2 ⌈n/2⌉⌉ ≤ ⌈log2 n⌉ - 1` for `n > 1`. -/ @[grind →] lemma clog2_half_le (n : ℕ) (h : n > 1) : clog 2 ((n + 1) / 2) ≤ clog 2 n - 1 := by rw [Nat.clog_of_one_lt one_lt_two h] grind -/-- Same logic for the floor half: ⌈log2 ⌊n/2⌋⌉ ≤ ⌈log2 n⌉ - 1 -/ +/-- Same logic for the floor half: `⌈log2 ⌊n/2⌋⌉ ≤ ⌈log2 n⌉ - 1`. -/ @[grind →] lemma clog2_floor_half_le (n : ℕ) (h : n > 1) : clog 2 (n / 2) ≤ clog 2 n - 1 := by apply Nat.le_trans _ (clog2_half_le n h) @@ -148,10 +145,10 @@ lemma clog2_floor_half_le (n : ℕ) (h : n > 1) : clog 2 (n / 2) ≤ clog 2 n - private lemma some_algebra (n : ℕ) : (n / 2 + 1) * clog 2 (n / 2 + 1) + ((n + 1) / 2 + 1) * clog 2 ((n + 1) / 2 + 1) + (n + 2) ≤ (n + 2) * clog 2 (n + 2) := by - -- 1. Substitution: Let N = n_1 + 2 to clean up the expression + -- 1. Substitution: Let `N = n + 2` to clean up the expression. let N := n + 2 have hN : N ≥ 2 := by omega - -- 2. Rewrite the terms using N + -- 2. Rewrite the terms using `N`. have t1 : n / 2 + 1 = N / 2 := by omega have t2 : (n + 1) / 2 + 1 = (N + 1) / 2 := by omega have t3 : n + 1 + 1 = N := by omega @@ -159,19 +156,19 @@ private lemma some_algebra (n : ℕ) : have h_bound_l : clog 2 (N / 2) ≤ k - 1 := clog2_floor_half_le N hN have h_bound_r : clog 2 ((N + 1) / 2) ≤ k - 1 := clog2_half_le N hN have h_split : N / 2 + (N + 1) / 2 = N := by omega - grw [t1, t2, t3, h_bound_l, h_bound_r, ←Nat.add_mul, h_split] + grw [t1, t2, t3, h_bound_l, h_bound_r, ← Nat.add_mul, h_split] exact Nat.le_refl (N * (k - 1) + N) -/-- Upper bound function for merge sort time complexity: `T(n) = n * ⌈log₂ n⌉` -/ +/-- Upper bound function for `mergeSort` time complexity: `T(n) = n * ⌈log₂ n⌉`. -/ abbrev T (n : ℕ) : ℕ := n * clog 2 n -/-- Solve the recurrence -/ +/-- Solve the recurrence. -/ theorem timeMergeSortRec_le (n : ℕ) : timeMergeSortRec n ≤ T n := by fun_induction timeMergeSortRec with | case1 => grind | case2 => grind | case3 n ih2 ih1 => - grw [ih1,ih2] + grw [ih1, ih2] have := some_algebra n grind [Nat.add_div_right] @@ -206,7 +203,7 @@ theorem mergeSort_time_le (xs : List α) : unfold timeMergeSortRec grind -/-- Time complexity of mergeSort -/ +/-- Time complexity of `mergeSort`. -/ theorem mergeSort_time (xs : List α) : let n := xs.length (mergeSort xs).time ≤ n * clog 2 n := by diff --git a/Cslib/Algorithms/Lean/Sorting.lean b/Cslib/Algorithms/Lean/Sorting.lean new file mode 100644 index 00000000..b2457620 --- /dev/null +++ b/Cslib/Algorithms/Lean/Sorting.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2026 Sorrachai Yingchareonthawornhcai. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Trong-Nghia Be, Sorrachai Yingchareonthawornhcai +-/ + +module + +public import Cslib.Algorithms.Lean.TimeM +public import Mathlib.Order.Defs.LinearOrder + +@[expose] public section + +/-! +# Shared Sorting Definitions + +Common definitions used by sorting algorithm files. + +## Main definitions + +- `IsSortedAscending`: A list is sorted in ascending order if each element is less than or equal +to the next. +- `IsSortedDescending`: A list is sorted in descending order if each element is greater than or +equal to the next. +- `IsSorted`: A list is sorted if it is either sorted in ascending or descending order. +- `MinOfList`: `x` is a minimum element of a list if `x ≤ b` for all `b` in the list. +- `MaxOfList`: `x` is a maximum element of a list if `x ≥ b` for all `b` in the list. +-/ + +set_option autoImplicit false + +namespace Cslib.Algorithms.Lean.TimeM + +variable {α : Type} [LinearOrder α] + +section Sortedness + +/-- A list is sorted (ascending/increasing) if it satisfies the `Pairwise (· ≤ ·)` predicate. +-/ +abbrev IsSortedAscending (l : List α) : Prop := List.Pairwise (· ≤ ·) l + +/-- A list is sorted (descending/decreasing) if it satisfies the `Pairwise (· ≥ ·)` predicate. +-/ +abbrev IsSortedDescending (l : List α) : Prop := List.Pairwise (· ≥ ·) l + +/-- A list is strictly sorted (ascending/increasing) +if it satisfies the `Pairwise (· < ·)` predicate. +-/ +abbrev IsStrictlySortedAscending (l : List α) : Prop := List.Pairwise (· < ·) l + +/-- A list is strictly sorted (descending/decreasing) +if it satisfies the `Pairwise (· > ·)` predicate. +-/ +abbrev IsStrictlySortedDescending (l : List α) : Prop := List.Pairwise (· > ·) l + +/-- A list is sorted if it is either sorted in ascending or descending order. +-/ +abbrev IsSorted (l : List α) : Prop := IsSortedAscending l ∨ IsSortedDescending l + +/-- If a list is strictly sorted in ascending order, then it is also sorted in ascending order. +-/ +theorem StrictlySortedAscendingImpliesSortedAscending (l : List α) : + IsStrictlySortedAscending l → IsSortedAscending l := by + intro h + unfold IsStrictlySortedAscending at h + unfold IsSortedAscending + apply List.Pairwise.imp _ h + intro a b hab + exact le_of_lt hab + +/-- If a list is strictly sorted in descending order, then it is also sorted in descending order. +-/ +theorem StrictlySortedDescendingImpliesSortedDescending (l : List α) : + IsStrictlySortedDescending l → IsSortedDescending l := by + intro h + unfold IsStrictlySortedDescending at h + unfold IsSortedDescending + apply List.Pairwise.imp _ h + intro a b hab + apply le_of_lt hab + +/-- If a list is strictly sorted in either ascending or descending order, then it is also sorted. +-/ +theorem StrictlySortedImpliesSorted (l : List α) : + IsStrictlySortedAscending l ∨ IsStrictlySortedDescending l → IsSorted l := by + intro h + cases h with + | inl hAsc => + exact Or.inl (StrictlySortedAscendingImpliesSortedAscending l hAsc) + | inr hDesc => + exact Or.inr (StrictlySortedDescendingImpliesSortedDescending l hDesc) + +end Sortedness + +section Extrema + +/-- `x` is a minimum element of list `l` if `x ≤ b` for all `b ∈ l`. +-/ +abbrev MinOfList (x : α) (l : List α) : Prop := ∀ b ∈ l, x ≤ b + +/-- `x` is a maximum element of list `l` if `x ≥ b` for all `b ∈ l`. +-/ +abbrev MaxOfList (x : α) (l : List α) : Prop := ∀ b ∈ l, x ≥ b + +end Extrema + +end Cslib.Algorithms.Lean.TimeM From 94ba740d51e87c0cc0abbfccee7f5158c4617a95 Mon Sep 17 00:00:00 2001 From: Curly-Howard-Chungus Correspondence | Lamport-Cabot-Codd-Backus-Naur Form Date: Mon, 23 Feb 2026 15:32:42 +0000 Subject: [PATCH 2/4] feat(InsertionSort): add worst-case and best-case time complexity proofs for insertionSort --- .../Lean/InsertionSort/InsertionSort.lean | 64 +++++++++++++++++-- 1 file changed, 58 insertions(+), 6 deletions(-) diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean index 19186dd0..53a02fac 100644 --- a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean +++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean @@ -320,6 +320,21 @@ theorem insertionSort_time (xs : List α) : (insertionSort xs).time ≤ (n * (n - 1)) / 2 := by grind [insertionSort_time_le, timeInsertionSortRec_eq] +/-- Auxiliary lemma to show that the closed-form solution of the recurrence matches +the expected formula. +-/ +private lemma worst_case_math (n : ℕ) : n * (n - 1) / 2 + n = (n + 1) * n / 2 := by + have h1 : timeInsertionSortRec n = n * (n - 1) / 2 := by + have h := timeInsertionSortRec_eq n + omega + have h2 : timeInsertionSortRec (n + 1) = (n + 1) * n / 2 := by + have h := timeInsertionSortRec_eq (n + 1) + have h_sub : (n + 1) - 1 = n := rfl + rw [h_sub] at h + omega + have h3 : timeInsertionSortRec (n + 1) = timeInsertionSortRec n + n := rfl + omega + /-- Time complexity of `insertionSort` - Worst-case scenario. In the worst case, the input list is strictly sorted in descending order, @@ -330,10 +345,12 @@ Thus, the total time is `n * (n - 1) / 2` comparisons for a list of length `n`. theorem insertionSort_time_worst_case (xs : List α) (h_sorted : IsStrictlySortedDescending xs) : let n := xs.length (insertionSort xs).time = n * (n - 1) / 2 := by + -- The proof proceeds by induction on the structure of the list `xs`. induction xs with + -- Base case: n = 0. | nil => - -- Base case: n = 0. Time is 0. simp [insertionSort] + -- Inductive case: Assume the statement holds for lists of length `n`, and prove it for `n + 1`. | cons x xs ih => rw [IsStrictlySortedDescending, List.pairwise_cons] at h_sorted have h_head : ∀ y ∈ xs, x > y := h_sorted.left @@ -347,20 +364,55 @@ theorem insertionSort_time_worst_case (xs : List α) (h_sorted : IsStrictlySorte have h_insert_time : (insert x ⟪insertionSort xs⟫).time = ⟪insertionSort xs⟫.length := insert_time_of_gt_all x ⟪insertionSort xs⟫ h_gt_sorted rw [h_insert_time, ih_tail, insertionSort_same_length] - simp_all - sorry + simp + have h_math := worst_case_math xs.length + simp [h_math] /-- Time complexity of `insertionSort` - Best-case scenario. In the best case, the input list is already sorted in ascending order, so each insertion takes only 1 comparison. -Thus, the total time is `n - 1` comparisons for a list of length `n`. +Thus, if `xs` is a non-empty sorted list of length `n > 0`, the total time is `n - 1` comparisons +for a list of length `n`. +If `xs` is empty, the time is 0 comparisons. -/ theorem insertionSort_time_best_case (xs : List α) (h_sorted : IsSortedAscending xs) : let n := xs.length - (insertionSort xs).time = n - 1 := by - sorry + if n = 0 + then (insertionSort xs).time = 0 + else (insertionSort xs).time = n - 1 := by + -- Remove the `let n := xs.length` to avoid issues with the `if` statement + -- and make the proof more straightforward. + change + if xs.length = 0 + then (insertionSort xs).time = 0 + else (insertionSort xs).time = xs.length - 1 + -- The proof proceeds by induction on the structure of the list `xs`. + induction xs with + -- Base case: n = 0. + | nil => + simp [insertionSort] + -- Inductive case: Assume the statement holds for lists of length `n`, and prove it for `n + 1`. + | cons x xs ih => + split + · contradiction + · rw [IsSortedAscending, List.pairwise_cons] at h_sorted + have h_head : ∀ y ∈ xs, x ≤ y := h_sorted.left + have h_tail : IsSortedAscending xs := h_sorted.right + unfold insertionSort + simp only [time_bind] + rw [insertionSort_eq_of_sorted xs h_tail] + cases xs with + | nil => + simp [insert, insertionSort] + | cons y ys => + have h_x_le_y : x ≤ y := h_head y List.mem_cons_self + rw [insert_time_of_le x y ys h_x_le_y] + have ih_tail := ih h_tail + split at ih_tail + · contradiction + · simp_all end TimeComplexity From c8f69328b51068392e5220f022e49605999515e1 Mon Sep 17 00:00:00 2001 From: Curly-Howard-Chungus Correspondence | Lamport-Cabot-Codd-Backus-Naur Form Date: Mon, 23 Feb 2026 15:59:44 +0000 Subject: [PATCH 3/4] style(InsertionSort): fix linter warning by `set_option linter.unusedSectionVars false` --- Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean index 53a02fac..a9708da4 100644 --- a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean +++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean @@ -27,6 +27,7 @@ comparisons. -/ set_option autoImplicit false +set_option linter.unusedSectionVars false namespace Cslib.Algorithms.Lean.TimeM @@ -246,7 +247,7 @@ theorem insertionSort_eq_of_sorted (xs : List α) (h : IsSortedAscending xs) : /-- If two lists are permutations of each other, any element-wise property that holds for all elements of the first list also holds for the second. -/ -theorem forall_mem_of_perm {P : α → Prop} {l1 l2 : List α} -- TODO: Fix linter warning. +theorem forall_mem_of_perm {P : α → Prop} {l1 l2 : List α} (h_perm : l1 ~ l2) (h_forall : ∀ a ∈ l1, P a) : ∀ a ∈ l2, P a := by intro a ha From a9c6cf107374daa307ace777b62f5f00d8e7362d Mon Sep 17 00:00:00 2001 From: Curly-Howard-Chungus Correspondence | Lamport-Cabot-Codd-Backus-Naur Form Date: Mon, 23 Feb 2026 16:03:24 +0000 Subject: [PATCH 4/4] docs(InsertionSort): add docstring for best and worst cases time complexity --- Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean index a9708da4..dc86a6f1 100644 --- a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean +++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean @@ -23,7 +23,10 @@ comparisons. - `insertionSort_correct`: `insertionSort` permutes the list into a sorted one. - `insertionSort_time`: The number of comparisons of `insertionSort` is at most `(n * (n - 1)) / 2`. - +- `insertionSort_time_worst_case`: In the worst case, the number of comparisons +is exactly `(n * (n - 1)) / 2`. +- `insertionSort_time_best_case`: In the best case, the number of comparisons +is `n - 1` for a non-empty list, and `0` for an empty list. -/ set_option autoImplicit false