Leanパズル【解答編】スターリンソート

この記事は以下の記事の解答編です。

https://zenn.dev/seasawher/articles/555c0c37301da6

回答例

こんな感じでやればできます。

variable [IsPreorder α]

@[grind ->]
theorem stalinSort_cons_mem (x y : α) (xs : List α) :
    y ∈ stalinSort (x :: xs) → x ≤ y := by
  induction xs generalizing x with grind

theorem stalinSort_sorted (l : List α) : (stalinSort l).Pairwise (· ≤ ·) := by
  fun_induction stalinSort l with simp_all <;> grind [List.pairwise_cons]

この補題 stalinSort_cons_mem を思いつくかどうかが結構大事かもしれません。スターリンソートでは「入力リストの先頭の要素」は絶対に出力リストの中に生き残るので、したがって「入力リストの先頭の要素」は最小要素であるはずなんですよね。