separate definition of stability into ListComparisonSort.lean

Author: Arleee1

Cslib/AlgorithmsTheory/Algorithms/MergeSort.lean

@@ -265,12 +265,13 @@ private lemma mergeSortNaive_stable_equiv
     rw [List.take_append_drop]
 
 theorem mergeSort_stable
-    (xs : List α) (le : α → α → Bool)
+    (xs : List α)
+    (le : α → α → Bool)
     [Std.Total (fun x y => le x y = true)]
     [IsTrans _ (fun x y => le x y = true)] :
-    let ys := (mergeSort xs).eval (sortModelNat le)
-    ∀ k : α, ys.filter (fun x => le x k && le k x) = xs.filter (fun x => le x k && le k x) := by
-  simpa [mergeSort_eval] using (mergeSortNaive_stable_equiv xs le)
+    IsStableSort (fun xs => (mergeSort xs).eval (sortModelNat le)) xs le := by
+  intro k
+  simpa [mergeSort_eval] using (mergeSortNaive_stable_equiv xs le k)
 
 end Stability
 

Cslib/AlgorithmsTheory/Models/ListComparisonSort.lean

@@ -20,7 +20,8 @@ public import Mathlib.Tactic.FastInstance
 In this file we define two query types `SortOps` which is suitable for insertion sort, and
 `SortOps`for comparison based searching in Lists. We define a model `sortModel` for `SortOps`
 which uses a custom cost structure `SortOpsCost`. We define a model `sortModelCmp` for `SortOpsCmp`
-which defines a `ℕ` based cost structure.
+which defines a `ℕ` based cost structure. We also define a notion of stability for sorting
+algorithms in lists.
 --
 ## Definitions
 
@@ -30,6 +31,7 @@ which defines a `ℕ` based cost structure.
 - `SortOpsCmp`:  A query type for comparison based sorting that only includes a comparison query.
    This is more suitable for comparison based sorts for which it is only desirable to count
    comparisons
+- `IsStableSort`: A definition of stability for sorting algorithms in lists.
 
 -/
 namespace Cslib
@@ -145,6 +147,18 @@ def sortModelNat {α : Type*}
 
 end NatModel
 
+section SortStability
+
+/-- Definition of a stable sorting algorithm. -/
+def IsStableSort
+    (sortAlg : List α → List α)
+    (xs : List α)
+    (le : α → α → Bool) : Prop :=
+  let ys := sortAlg xs
+  ∀ (k : α), ys.filter (fun x => le x k && le k x) = xs.filter (fun x => le x k && le k x)
+
+end SortStability
+
 end Algorithms
 
 end Cslib