Day5, part 1

1 files changed, 7 insertions, 5 deletions

diff --git a/Common/List.lean b/Common/List.lean
index 1a76c3e..1d770a8 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -12,17 +12,19 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length
       assumption
     | true => simp_arith[hi]
 
-def quicksort {α : Type} [Ord α] : List α → List α
+def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α
 | [] => []
 | a :: as =>
-  let smallerPred := λ b ↦ Ord.compare b a == Ordering.lt
-  let largerEqualPred := λ b ↦ Ord.compare b a != Ordering.lt
+  let smallerPred := λ b ↦ pred b a
+  let largerEqualPred := not ∘ smallerPred
   have : List.length (List.filter smallerPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList]
   have : List.length (List.filter largerEqualPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList]
   let smallers := as.filter smallerPred
   let biggers := as.filter largerEqualPred
-  (quicksort smallers) ++ [a] ++ (quicksort biggers)
-  termination_by quicksort l => l.length
+  (quicksortBy pred smallers) ++ [a] ++ (quicksortBy pred biggers)
+  termination_by quicksortBy pred l => l.length
+
+def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt
 
 /-- Maps a List to another list, but keeps state.
     The output list is a list of the state, and **has** the initial state