Lean4で選択ソートを定義して正当性を示す

以前、挿入ソートをLean4で実装してソートであることを証明する記事を投稿しました。

https://zenn.dev/seasawher/articles/77d8bdd31aeafc

今回は選択ソートを実装してみましょう。

方針

MathlibやBatteriesのような外部ライブラリは一切使用しない方針でやります。

選択ソートの定義

選択ソートは、以下のように定義できます。minFirst関数の定義がごちゃごちゃしていますが、これは後で証明で使うべく補題を示しているためです。

variable {α : Type} [LE α] [DecidableEq α] [DecidableLE α] [Std.IsLinearOrder α]

instance : Min α := minOfLe

open List

/-- リストの最小値を先頭に持ってくる -/
@[grind]
def minFirst (xs : List α) : List α :=
  match h : xs with
  | [] => []
  | x :: xs =>
    let μ := List.min (x :: xs) (h := by simp)
    have mem : μ ∈ x :: xs := by grind [min_mem]
    have min : ∀ y ∈ x :: xs, μ ≤ y := by grind [min_le_of_mem]

    let rest := List.erase (x :: xs) μ
    have len_eq : (μ :: rest).length = (x :: xs).length := by grind
    μ :: rest

-- 簡単な動作確認
#guard minFirst [3, 1, 4, 15, 9] = [1, 3, 4, 15, 9]

@[grind =]
theorem minFirst_length (xs : List α) :
    (minFirst xs).length = xs.length := by
  fun_cases minFirst xs with grind

/-- 選択ソート -/
@[grind]
def selectionSort (xs : List α) : List α :=
  let ys := minFirst xs
  have : ys.length = xs.length := by grind
  match hy : ys with
  | [] => []
  | z :: zs =>
    have : zs.length < ys.length := by grind
    z :: selectionSort zs
termination_by xs.length

-- 簡単な動作確認
#guard selectionSort [3, 1, 4, 15, 9] = [1, 3, 4, 9, 15]

証明

さて、それでは性質を証明していきます。

並び替えであること

並び替えであることは、grindで適当にしばいていれば示せます。

@[grind! ·]
theorem minFirst_perm (xs : List α) :
    minFirst xs ~ xs := by
  cases xs with grind

@[grind! ·]
theorem selectionSort_perm (xs : List α) :
    selectionSort xs ~ xs := by
  fun_induction selectionSort xs with grind

（昇順の）ソートであること

次にソートであることですが、これもgrindでしばけば通ります。終わりです。

attribute [grind] List.Pairwise

@[grind ->]
theorem minFirst_spec (x : α) (xs ys : List α) (h : x :: xs = minFirst ys) :
    ∀ y ∈ xs, x ≤ y := by
  fun_cases minFirst ys with grind

theorem selectionSort_sorted (xs : List α) :
    (selectionSort xs).Pairwise (· ≤ ·) := by
  fun_induction selectionSort xs with grind [= minFirst.eq_def]

感想

選択ソートは私が初めてLeanで正当性を証明したアルゴリズムで、懐かしい気持ちになりました。当時はMathlibを使う必要があり、証明ももっと長かったと記憶していますが、いまやりなおしてみると証明は全部grindの一撃で終わってしまい、MathlibどころかBatteriesすら不要でした。Lean4の進歩を感じますね。

なお当時のコードはこちらです:
https://github.com/Seasawher/SelectionSort.lean