Imports
import MathlibCLRS Section 2.1 - Insertion sort
This file is the first Chapter 2 workflow slice. It formalizes a functional version of insertion sort and proves the two correctness facts that correspond to the textbook argument:
-
the result is ordered;
-
the result is a permutation of the input.
The CLRS pseudocode is array-based and is usually justified by a loop invariant. Here we use a recursive list algorithm, because it exposes the same invariant as small structural lemmas: inserting into an ordered list keeps it ordered, and it does not change the multiset of elements.
namespace CLRSnamespace Chapter02
Every element of xs is at least lower.
def AllLe (lower : Nat) (xs : List Nat) : Prop :=
∀ x ∈ xs, lower ≤ xA compact sortedness predicate for lists of natural numbers.
def Ordered : List Nat → Prop
| [] => True
| [_] => True
| x :: y :: ys => x ≤ y ∧ Ordered (y :: ys)Insert an element into an already ordered list.
def insertSorted (x : Nat) : List Nat → List Nat
| [] => [x]
| y :: ys =>
if x ≤ y then
x :: y :: ys
else
y :: insertSorted x ysFunctional insertion sort over lists.
def insertionSort : List Nat → List Nat
| [] => []
| x :: xs => insertSorted x (insertionSort xs)theorem ordered_tail {x : Nat} {xs : List Nat}
(h : Ordered (x :: xs)) : Ordered xs :=
cases xs with
theorem ordered_allLe_tail {x : Nat} {xs : List Nat}
(h : Ordered (x :: xs)) : AllLe x xs :=
induction xs generalizing x with
theorem ordered_cons_of_allLe {x : Nat} {xs : List Nat}
(hxs : Ordered xs) (hall : AllLe x xs) : Ordered (x :: xs) :=
cases xs with
exact ⟨hall y ( ), hxs⟩theorem allLe_insertSorted {lower x : Nat} {xs : List Nat}
(hx : lower ≤ x) (hxs : AllLe lower xs) :
AllLe lower (insertSorted x xs) :=
induction xs with
Inserting into an ordered list keeps it ordered.
theorem insertSorted_ordered {x : Nat} {xs : List Nat}
(hxs : Ordered xs) : Ordered (insertSorted x xs) :=
induction xs with
Inserting into a list preserves the input elements up to permutation.
theorem insertSorted_perm (x : Nat) (xs : List Nat) :
(insertSorted x xs).Perm (x :: xs) :=
induction xs with
Insertion sort returns an ordered list.
theorem insertionSort_sorted (xs : List Nat) : Ordered (insertionSort xs) :=
induction xs with
Insertion sort preserves the input elements up to permutation.
theorem insertionSort_perm (xs : List Nat) :
(insertionSort xs).Perm xs :=
induction xs with
end Chapter02end CLRS