👻

Lean4で挿入ソートを定義して正当性を示す

に公開
ソート
Lean
Lean 4
tech

今回の方針

Batteries や Mathlib などの外部のライブラリは使用しないことにします。標準ライブラリのみで頑張ります。

挿入ソートの定義

まずは定義からです。挿入ソートは以下のように定義できます。

variable {α : Type} [LE α] [DecidableLE α]

namespace List

/-- リストに要素を挿入する。
引数のリストがそもそもソート済みであれば、
挿入後のリストもソート済みになることが期待される。 -/
@[grind]
def orderedInsert (a : α) (as : List α) : List α :=
  match as with
  | [] => [a]
  | b :: bs =>
    if a ≤ b then
      a :: b :: bs
    else
      b :: orderedInsert a bs

/-- 挿入ソート -/
def insertionSort (as : List α) : List α :=
  match as with
  | [] => []
  | a :: bs => orderedInsert a (insertionSort bs)

end List

-- 簡単なテスト
#guard [3, 1, 4, 15, 9, 2].insertionSort = [1, 2, 3, 4, 9, 15]

性質の証明

挿入ソートの性質というと、いろんな性質が知られています。たとえば以下のようなものがありますね。

  • 最悪時の実行時間が引数のリストの長さ n について、n² のオーダーになる。
  • in-place で動作する。つまり追加のメモリを必要としない。

しかし、ここでは上記の性質については証明せず、単に「ソートである」ことだけ示すことにします。ソートであることを示すには、以下の二点を示せば十分です。

  • 出力されるリストが元のリストの並び替えであること
  • 出力されるリストがソート済みであること

並び替えであること

並び替えであることは Perm という述語で表現でき、これは ~ で表現されます。

namespace List

attribute [grind] Perm

@[grind ·]
theorem perm_orderedInsert (a : α) (as : List α) :
    (orderedInsert a as) ~ (a :: as) := by
  fun_induction orderedInsert a as with
  | case1 => grind [perm_singleton]
  | case2 => grind [Perm.refl]
  | case3 b bs hif ih => calc
    _ ~ b :: orderedInsert a bs := by rfl
    _ ~ b :: a :: bs := by grind
    _ ~ a :: b :: bs := by grind

theorem perm_insertionSort (as : List α) : insertionSort as ~ as := by
  fun_induction insertionSort as with
  | case1 => grind [Perm.refl]
  | case2 b bs ih => calc
    _ ~ orderedInsert b bs.insertionSort := by rfl
    _ ~ b :: bs.insertionSort := by grind
    _ ~ b :: bs := by grind

end List

ソート済みであること

まず「ソート済みである」ことを表現する必要があります。そこで IsChain という述語を用意します。

namespace List

/-- 二項関係Rがリストの隣接要素に対して成立する。
たとえば、`[a, b, c].IsChain R` は `R a b ∧ R b c` と等しい。-/
@[grind]
inductive IsChain (R : α → α → Prop) : List α → Prop
  | nil : IsChain R []
  | single (a : α) : IsChain R [a]
  | cons {a b : α} {bs : List α} (h₁ : R a b) (h₂ : IsChain R (b :: bs)) :
    IsChain R (a :: b :: bs)

abbrev Sorted := @IsChain α (· ≤ ·)

そうすると、証明することができます。

-- この仮定が必要
variable [Std.IsLinearOrder α]

@[grind =>]
theorem sorted_orderedInsert (a : α) (as : List α) (h : Sorted as) :
    Sorted (orderedInsert a as) := by
  induction as with grind

theorem sorted_insertionSort (as : List α) : Sorted (insertionSort as) := by
  fun_induction insertionSort as with grind

end List

感想

「ソート済みであること」の証明には普通は List.Pairwise を使うのですが、順序関係が推移的であれば IsChain と同じになります。

Discussion