Lean4

45. Insertion sort is correct

HardChallengeVerified programAcademy Pass80 points

Problem 19 proved that isort returns a sorted list. That is only half of correctness: a function that always returns [] is sorted too. Prove the full specification, SortSpec isort: the result is sorted and it is a permutation of the input.

This is a challenge and it is Mathlib-free. Perm is defined above the editor, from scratch, by four rules: the empty lists are permutations of each other, a common head can be added, two neighbours can be swapped, and permutations compose.

What the judge checks

isort_correct : SortSpec isort

The definitions these names refer to are the read-only lines above the editor. Write any helper lemmas you need before the final theorem.

sortinginductive predicatespermutations

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Learn the ideas

Similar problems

Solution.lean
Loading…
1def ins (x : Nat) : List Nat → List Nat
2 | [] => [x]
3 | y :: ys => if x ≤ y then x :: y :: ys else y :: ins x ys
4
5def isort : List Nat → List Nat
6 | [] => []
7 | x :: xs => ins x (isort xs)
8
9inductive Sorted : List Nat → Prop
10 | nil : Sorted []
11 | single (x : Nat) : Sorted [x]
12 | cons (x y : Nat) (ys : List Nat) : x ≤ y → Sorted (y :: ys) → Sorted (x :: y :: ys)
13
14inductive Perm : List Nat → List Nat → Prop
15 | nil : Perm [] []
16 | cons (x : Nat) {l₁ l₂ : List Nat} : Perm l₁ l₂ → Perm (x :: l₁) (x :: l₂)
17 | swap (x y : Nat) (l : List Nat) : Perm (y :: x :: l) (x :: y :: l)
18 | trans {l₁ l₂ l₃ : List Nat} : Perm l₁ l₂ → Perm l₂ l₃ → Perm l₁ l₃
19
20def SortSpec (f : List Nat → List Nat) : Prop := ∀ xs, Sorted (f xs) ∧ Perm (f xs) xs
given
Loading editor…

Run checks your code against the examples and your custom inputs and records nothing. Submit also runs the hidden tests, confirms the axioms your proof uses and records the result. Each uses one compiler check.

ReadyLn 1, Col 1Lean 4
Draft saved in this browser