Last active
December 1, 2025 20:22
-
-
Save tchaumeny/8015dff25ff03794c8138ecfb0f874c0 to your computer and use it in GitHub Desktop.
Quicksort implemented and certified in Lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| open List | |
| def quicksort : List Nat → List Nat | |
| | nil => nil | |
| | pivot :: rest => | |
| quicksort (rest.filter (· < pivot)) | |
| ++ [pivot] | |
| ++ quicksort (rest.filter (· ≥ pivot)) | |
| termination_by l => l.length decreasing_by | |
| all_goals | |
| simp only [length_unattach, length_cons, gt_iff_lt] | |
| apply Nat.lt_succ_of_le | |
| rw [←length_attach (l := rest)] | |
| apply length_filter_le | |
| #eval quicksort [42, 12, 23, 54, 4, 12, 18, 16, 25] | |
| theorem quicksort_is_permutation : (quicksort l) ~ l := by | |
| fun_induction quicksort l with | |
| | case1 => exact Perm.refl nil | |
| | case2 pivot rest hs hl => | |
| rw [unattach_filter] at hs hl | |
| simp only [unattach_attach] at hs hl | |
| have h₀ : rest ~ rest.filter (· < pivot) ++ rest.filter (· ≥ pivot) := by | |
| simp only [ge_iff_le, ← Nat.not_lt, decide_not, (filter_append_perm (· < pivot) rest).symm] | |
| have h₁ : quicksort (rest.filter (· < pivot)) ++ quicksort (rest.filter (· ≥ pivot)) | |
| ~ rest.filter (· < pivot) ++ rest.filter (· ≥ pivot) := Perm.append hs hl | |
| all_goals grind | |
| #print quicksort_is_permutation | |
| theorem quicksort_is_sorted : (quicksort l).Pairwise (· ≤ ·) := by | |
| fun_induction quicksort l with | |
| | case1 => exact Pairwise.nil | |
| | case2 pivot rest hs hl => | |
| rw [unattach_filter] at hs hl | |
| simp only [unattach_attach] at hs hl | |
| simp only [ge_iff_le, append_assoc, cons_append, nil_append, pairwise_append, pairwise_cons, | |
| mem_cons, forall_eq_or_imp] | |
| have hp(p) : ∀ x ∈ quicksort (rest.filter p), p x := by | |
| simp only [Perm.mem_iff quicksort_is_permutation, mem_filter, and_imp, imp_self, implies_true] | |
| and_intros | |
| exact hs | |
| intro x hx | |
| exact of_decide_eq_true (hp (· ≥ pivot) x hx) | |
| exact hl | |
| intro x hx | |
| and_intros | |
| exact Nat.le_of_lt (of_decide_eq_true (hp (· < pivot) x hx)) | |
| all_goals grind only | |
| #print quicksort_is_sorted |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment