diff options
| -rw-r--r-- | Common.lean | 1 | ||||
| -rw-r--r-- | Common/List.lean | 24 |
2 files changed, 25 insertions, 0 deletions
diff --git a/Common.lean b/Common.lean index aa53152..b74da23 100644 --- a/Common.lean +++ b/Common.lean @@ -2,3 +2,4 @@ import Common.Helpers import Common.Option import Common.DayPart import Common.String +import Common.List 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 |