feat(Algorithms): Prove insertion sort is stable

Cslib.lean

@@ -1,7 +1,15 @@
 module  -- shake: keep-all
 
-public import Cslib.Algorithms.Lean.MergeSort.MergeSort
-public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.AlgorithmsTheory.Algorithms.ListInsertionSort
+public import Cslib.AlgorithmsTheory.Algorithms.ListLinearSearch
+public import Cslib.AlgorithmsTheory.Algorithms.ListOrderedInsert
+public import Cslib.AlgorithmsTheory.Algorithms.MergeSort
+public import Cslib.AlgorithmsTheory.Lean.MergeSort.MergeSort
+public import Cslib.AlgorithmsTheory.Lean.TimeM
+public import Cslib.AlgorithmsTheory.LowerBounds.ComparisonSort
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSearch
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSort
+public import Cslib.AlgorithmsTheory.QueryModel
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic

Cslib/AlgorithmsTheory/Algorithms/ListInsertionSort.lean

@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shreyas Srinivas, Eric Wieser
+-/
+module
+
+public import Cslib.AlgorithmsTheory.Algorithms.ListOrderedInsert
+public import Mathlib.Tactic.NormNum
+
+@[expose] public section
+
+/-!
+# Insertion sort in a list
+
+In this file we state and prove the correctness and complexity of insertion sort in lists under
+the `SortOpsInsertHead` model. This insertionSort evaluates identically to the upstream version of
+`List.insertionSort`
+--
+
+## Main Definitions
+
+- `insertionSort` : Insertion sort algorithm in the `SortOpsInsertHead` query model
+
+## Main results
+
+- `insertionSort_eval`: `insertionSort` evaluates identically to `List.insertionSort`.
+- `insertionSort_permutation` :  `insertionSort` outputs a permutation of the input list.
+- `insertionSort_sorted` : `insertionSort` outputs a sorted list.
+- `insertionSort_complexity` : `insertionSort` takes at most n * (n + 1) comparisons and
+  (n + 1) * (n + 2) list head-insertions.
+- `insertionSort_stable` : `insertionSort` is a stable sorting algorithm.
+-/
+
+namespace Cslib
+
+namespace Algorithms
+
+open Prog
+
+/-- The insertionSort algorithms on lists with the `SortOps` query. -/
+def insertionSort (l : List α) : Prog (SortOpsInsertHead α) (List α) :=
+  match l with
+  | [] => return []
+  | x :: xs => do
+      let rest ← insertionSort xs
+      insertOrd x rest
+
+@[simp]
+theorem insertionSort_eval (l : List α) (le : α → α → Bool) :
+    (insertionSort l).eval (sortModel le) = l.insertionSort (fun x y => le x y = true) := by
+  induction l with simp_all [insertionSort]
+
+theorem insertionSort_permutation (l : List α) (le : α → α → Bool) :
+    ((insertionSort l).eval (sortModel le)).Perm l := by
+    simp [insertionSort_eval, List.perm_insertionSort]
+
+theorem insertionSort_sorted
+    (l : List α) (le : α → α → Bool)
+    [Std.Total (fun x y => le x y = true)] [IsTrans α (fun x y => le x y = true)] :
+    ((insertionSort l).eval (sortModel le)).Pairwise (fun x y => le x y = true) := by
+  simpa using List.pairwise_insertionSort _ _
+
+lemma insertionSort_length (l : List α) (le : α → α → Bool) :
+    ((insertionSort l).eval (sortModel le)).length = l.length := by
+  simp
+
+lemma insertionSort_time_compares (head : α) (tail : List α) (le : α → α → Bool) :
+    ((insertionSort (head :: tail)).time (sortModel le)).compares =
+      ((insertionSort tail).time (sortModel le)).compares +
+        ((insertOrd head (tail.insertionSort (fun x y => le x y = true))).time
+          (sortModel le)).compares := by
+  simp [insertionSort]
+
+lemma insertionSort_time_inserts (head : α) (tail : List α) (le : α → α → Bool) :
+    ((insertionSort (head :: tail)).time (sortModel le)).inserts =
+      ((insertionSort tail).time (sortModel le)).inserts +
+        ((insertOrd head (tail.insertionSort (fun x y => le x y = true))).time
+          (sortModel le)).inserts := by
+  simp [insertionSort]
+
+theorem insertionSort_complexity (l : List α) (le : α → α → Bool) :
+    ((insertionSort l).time (sortModel le))
+      ≤ ⟨l.length * (l.length + 1), (l.length + 1) * (l.length + 2)⟩ := by
+  induction l with
+  | nil =>
+    simp [insertionSort]
+  | cons head tail ih =>
+    grind [insertOrd_complexity_upper_bound, List.length_insertionSort, SortOpsCost.le_def,
+      insertionSort_time_compares, insertionSort_time_inserts]
+
+section Stability
+
+private lemma filter_orderedInsert_of_neg {r : α → α → Prop} [DecidableRel r]
+    (a : α) (l : List α) (p : α → Bool) (ha : p a = false) :
+    (l.orderedInsert r a).filter p = l.filter p := by
+  induction l with
+  | nil => rw [List.orderedInsert_nil]; simp [ha]
+  | cons b l ih =>
+    rw [List.orderedInsert_cons]
+    split
+    · simp [List.filter, ha]
+    · simp only [List.filter]; split <;> simp [ih]
+
+private lemma filter_orderedInsert_of_pos {r : α → α → Prop} [DecidableRel r]
+    (a : α) (l : List α) (p : α → Bool)
+    (ha : p a = true)
+    (hcompat : ∀ b, p b = true → r a b)
+    (hsorted : l.Pairwise r) :
+    (l.orderedInsert r a).filter p = a :: l.filter p := by
+  induction l with
+  | nil => rw [List.orderedInsert_nil]; simp [ha]
+  | cons b l ih =>
+    rw [List.orderedInsert_cons]
+    rw [List.pairwise_cons] at hsorted
+    split
+    · simp [List.filter, ha]
+    · rename_i hnr
+      have hnpb : p b = false := by
+        by_contra h; push_neg at h
+        cases hpb : p b with
+        | false => simp [hpb] at h
+        | true => exact hnr (hcompat b hpb)
+      simp only [List.filter, hnpb]
+      exact ih hsorted.2
+
+theorem insertionSort_stable
+    (xs : List α)
+    (le : α → α → Bool)
+    [Std.Total (fun x y => le x y = true)]
+    [IsTrans α (fun x y => le x y = true)] :
+    IsStableSort (fun xs => (insertionSort xs).eval (sortModel le)) xs le := by
+  simp only [insertionSort_eval]
+  intro k
+  induction xs with
+  | nil => simp
+  | cons a rest ih =>
+    change List.filter (fun x => le x k && le k x)
+      (List.insertionSort (fun x y => le x y = true) (a :: rest)) =
+      List.filter (fun x => le x k && le k x) (a :: rest)
+    rw [List.insertionSort_cons]
+    have hsorted : (rest.insertionSort (fun x y => le x y = true)).Pairwise
+        (fun x y => le x y = true) :=
+      List.pairwise_insertionSort _ rest
+    rcases hab : (le a k && le k a) with _ | _
+    · rw [filter_orderedInsert_of_neg a _ (fun x => le x k && le k x) hab]
+      simp [hab, ih]
+    · rw [filter_orderedInsert_of_pos a _ (fun x => le x k && le k x) hab _ hsorted]
+      · simp [hab, ih]
+      · intro b hb
+        simp only [Bool.and_eq_true] at hab hb
+        exact IsTrans.trans (r := fun x y => le x y = true) a k b hab.1 hb.2
+
+end Stability
+
+end Algorithms
+
+end Cslib

Cslib/AlgorithmsTheory/Algorithms/ListLinearSearch.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shreyas Srinivas, Eric Wieser
+-/
+
+module
+
+public import Cslib.AlgorithmsTheory.QueryModel
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSearch
+public import Batteries.Data.List
+public import Mathlib.Algebra.Order.Group.Nat
+public import Mathlib.Tactic.Set
+
+@[expose] public section
+
+/-!
+# Linear search in a list
+
+In this file we state and prove the correctness and complexity of linear search in lists under
+the `ListSearch` model.
+--
+
+## Main Definitions
+
+- `listLinearSearch` : Linear search algorithm in the `ListSearch` query model
+
+## Main results
+
+- `listLinearSearch_eval`: `listLinearSearch` evaluates identically to `List.contains`.
+- `listLinearSearchM_time_complexity_upper_bound` : `linearSearch` takes at most `n`
+  comparison operations
+- `listLinearSearchM_time_complexity_lower_bound` : There exist lists on which `linearSearch` needs
+  `n` comparisons
+-/
+namespace Cslib
+
+namespace Algorithms
+
+open Prog
+
+open ListSearch in
+/-- Linear Search in Lists on top of the `ListSearch` query model. -/
+def listLinearSearch (l : List α) (x : α) : Prog (ListSearch α) Bool := do
+  match l with
+  | [] => return false
+  | l :: ls =>
+    let cmp : Bool ← compare (l :: ls) x
+    if cmp then
+      return true
+    else
+      listLinearSearch ls x
+
+@[simp, grind =]
+lemma listLinearSearch_eval [BEq α] (l : List α) (x : α) :
+    (listLinearSearch l x).eval ListSearch.natCost = l.contains x := by
+  fun_induction l.elem x with simp_all [listLinearSearch]
+
+lemma listLinearSearchM_correct_true [BEq α] [LawfulBEq α] (l : List α)
+    {x : α} (x_mem_l : x ∈ l) : (listLinearSearch l x).eval ListSearch.natCost = true := by
+  simp [x_mem_l]
+
+lemma listLinearSearchM_correct_false [BEq α] [LawfulBEq α] (l : List α)
+    {x : α} (x_mem_l : x ∉ l) : (listLinearSearch l x).eval ListSearch.natCost = false := by
+  simp [x_mem_l]
+
+lemma listLinearSearchM_time_complexity_upper_bound [BEq α] (l : List α) (x : α) :
+    (listLinearSearch l x).time ListSearch.natCost ≤ l.length := by
+  fun_induction l.elem x with
+  | case1 => simp [listLinearSearch]
+  | case2 => simp_all [listLinearSearch]
+  | case3 =>
+    simp [listLinearSearch]
+    lia
+
+lemma listLinearSearchM_time_complexity_lower_bound [DecidableEq α] [Nontrivial α] (n : ℕ) :
+    ∃ (l : List α) (x : α), l.length = n
+      ∧ (listLinearSearch l x).time ListSearch.natCost = l.length := by
+  obtain ⟨x, y, hneq⟩ := exists_pair_ne α
+  use List.replicate n y, x
+  split_ands
+  · simp
+  · induction n <;> simp [listLinearSearch, List.replicate]
+    grind [ListSearch.natCost_cost, ListSearch.natCost_evalQuery]
+
+end Algorithms
+
+end Cslib

Cslib/AlgorithmsTheory/Algorithms/ListOrderedInsert.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shreyas Srinivas, Eric Wieser
+-/
+
+module
+
+public import Cslib.AlgorithmsTheory.QueryModel
+public import Cslib.AlgorithmsTheory.Models.ListComparisonSort
+public import Mathlib.Algebra.Order.Group.Nat
+public import Mathlib.Data.Int.ConditionallyCompleteOrder
+public import Mathlib.Data.List.Sort
+public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+@[expose] public section
+
+/-!
+# Ordered insertion in a list
+
+In this file we state and prove the correctness and complexity of ordered insertions in lists under
+the `SortOps` model. This ordered insert is later used in `insertionSort` mirroring the structure
+in upstream libraries for the pure lean code versions of these declarations.
+
+--
+
+## Main Definitions
+
+- `insertOrd` : ordered insert algorithm in the `SortOps` query model
+
+## Main results
+
+- `insertOrd_eval`: `insertOrd` evaluates identically to `List.orderedInsert`.
+- `insertOrd_complexity_upper_bound` : Shows that `insertOrd` takes at most `n` comparisons,
+   and `n + 1` list head-insertion operations.
+- `insertOrd_sorted` : Applying `insertOrd` to a sorted list yields a sorted list.
+-/
+
+namespace Cslib
+namespace Algorithms
+
+open Prog
+
+open SortOpsInsertHead
+
+/--
+Performs ordered insertion of `x` into a list `l` in the `SortOps` query model.
+If `l` is sorted, then `x` is inserted into `l` such that the resultant list is also sorted.
+-/
+def insertOrd (x : α) (l : List α) : Prog (SortOpsInsertHead α) (List α) := do
+  match l with
+  | [] => insertHead x l
+  | a :: as =>
+      if (← cmpLE x a : Bool) then
+        insertHead x (a :: as)
+      else
+        let res ← insertOrd x as
+        insertHead a res
+
+@[simp]
+lemma insertOrd_eval (x : α) (l : List α) (le : α → α → Bool) :
+    (insertOrd x l).eval (sortModel le) = l.orderedInsert (fun x y => le x y = true) x := by
+  induction l with
+  | nil =>
+    simp [insertOrd, sortModel]
+  | cons head tail ih =>
+    by_cases h_head : le x head
+    · simp [insertOrd, h_head]
+    · simp [insertOrd, h_head, ih]
+
+-- TODO : to upstream
+@[simp]
+lemma _root_.List.length_orderedInsert (x : α) (l : List α) [DecidableRel r] :
+    (l.orderedInsert r x).length = l.length + 1 := by
+  induction l <;> grind
+
+theorem insertOrd_complexity_upper_bound
+    (l : List α) (x : α) (le : α → α → Bool) :
+    (insertOrd x l).time (sortModel le) ≤ ⟨l.length, l.length + 1⟩ := by
+  induction l with
+  | nil =>
+    simp [insertOrd, sortModel]
+  | cons head tail ih =>
+    obtain ⟨ih_compares, ih_inserts⟩ := ih
+    rw [insertOrd]
+    by_cases h_head : le x head
+    · simp [h_head]
+    · simp [h_head]
+      grind
+
+lemma insertOrd_sorted
+    (l : List α) (x : α) (le : α → α → Bool)
+    [Std.Total (fun x y => le x y)]
+    [IsTrans _ (fun x y => le x y)] :
+    l.Pairwise (fun x y => le x y)
+      → ((insertOrd x l).eval (sortModel le)).Pairwise (fun x y => le x y = true) := by
+  rw [insertOrd_eval]
+  exact List.Pairwise.orderedInsert _ _
+
+end Algorithms
+
+end Cslib