-
Notifications
You must be signed in to change notification settings - Fork 0
/
Quicksort.lean
71 lines (56 loc) · 2.52 KB
/
Quicksort.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
import algebra.order.group
import tactic
private def only_those {T : Type} (cond : T → T → Prop) [∀ n, ∀ m, decidable (cond n m)] : T → list T → list T
| p [] := []
| p (x :: xs) := if (cond x p) then x :: only_those p xs else only_those p xs
private lemma size_cap {T : Type} {cond : T → T → Prop} [∀ n, ∀ m, decidable (cond n m)] {pivot : T} {lizt : list T} :
(only_those cond pivot lizt).sizeof < (pivot :: lizt).sizeof :=
begin
induction lizt with head tail ih,
unfold only_those,
unfold list.sizeof,
linarith,
unfold list.sizeof,
by_cases cond head pivot,
-- here `cond` holds
have unwrap_yes : only_those cond pivot (head :: tail) = head :: only_those cond pivot tail,
{
unfold only_those,
simp,
contrapose!,
intro _,
exact h,
},
calc (only_those cond pivot (head :: tail)).sizeof
= (head :: only_those cond pivot tail).sizeof : by rw unwrap_yes
... = 1 + (sizeof head) + (only_those cond pivot tail).sizeof : by unfold list.sizeof
... < 1 + (sizeof head) + (pivot :: tail).sizeof : by linarith -- uses `ih` and `add_le_add` afaik
... = 1 + (sizeof head) + (1 + (sizeof pivot) + tail.sizeof) : by unfold list.sizeof,
-- here `cond` does not hold
have unwrap_no : only_those cond pivot (head :: tail) = only_those cond pivot tail,
{
unfold only_those,
simp,
contrapose,
intro _,
exact h,
},
calc (only_those cond pivot (head :: tail)).sizeof
= (only_those cond pivot tail).sizeof : by rw unwrap_no
... < (pivot :: tail).sizeof : ih
... = (1 + (sizeof pivot) + tail.sizeof) : by unfold list.sizeof
... ≤ 1 + (sizeof head) + (1 + (sizeof pivot) + tail.sizeof) : le_add_self
end
variable {L : Type}
variable [linear_order L]
private def only_le : L → list L → list L :=
only_those (≤)
private def only_gt : L → list L → list L :=
only_those (>)
def kviksort : list L → list L
| [] := []
| (x :: xs) := have (only_le x xs).sizeof < (x :: xs).sizeof, from size_cap,
have (only_gt x xs).sizeof < (x :: xs).sizeof, from size_cap,
kviksort (only_le x xs) ++ [x] ++ kviksort (only_gt x xs)
#eval kviksort [14, 8, 2, 20, 15, 0, 11, 18, 7, 6, 3, 13, 10, 17, 1, 4, 5, 9, 19, 12, 16, 10]
-- Result should be a sequence of integers 0..20 where 10 is twice.