blob: 4076c870c881a334ce8b6a0690cade8b570cb8e4 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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
|
