From d09a6869fea6f0d79c57e4ff756e21e03d395d52 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 3 Dec 2023 00:29:59 +0100
Subject: Quicksort. Might be useful later.

---
 Common/List.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 Common/List.lean

(limited to 'Common/List.lean')

diff --git a/Common/List.lean b/Common/List.lean
new file mode 100644
index 0000000..4076c87
--- /dev/null
+++ b/Common/List.lean
@@ -0,0 +1,24 @@
+theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length ≥ (l.filter p).length := by
+  induction l with
+  | nil => simp[List.filter]
+  | cons a as hi =>
+    simp[List.length, List.filter]
+    cases (p a) with
+    | false =>
+      simp
+      constructor
+      assumption
+    | true => simp_arith[hi]
+
+
+def quicksort {α : Type} [Ord α] : List α → List α
+| [] => []
+| a :: as =>
+  let smallerPred := λ b ↦ Ord.compare b a == Ordering.lt
+  let largerEqualPred := λ b ↦ Ord.compare b a != Ordering.lt
+  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
-- 
cgit v1.2.3

