From dbee715e231a1aabcf105557e52855a23a964207 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Wed, 6 Dec 2023 19:20:03 +0100
Subject: Day5, part 1

---
 Common/List.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'Common/List.lean')

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
-- 
cgit v1.2.3

