選択ソートと，それがソートアルゴリズムであることの証明を Lean Prover で実装する

はじめに

Lean4 は純粋関数型言語であり，定理証明支援系でもあります．プログラミング言語として使ってアルゴリズムを書き，書き終わったら定理証明支援系として使ってその性質を証明する…というハイブリッドな使い方が可能です．

以前の記事で，「リストの最小値を先頭に持ってくる関数」を定義し，それが置換であることを証明しました．ここで「置換である」とは，与えられたリストと返り値として返すリストが要素の順番だけしか異ならないという意味です．それを発展させ，今回は選択ソートを Lean で実装し, それがソートアルゴリズムであることを証明します．

コード

ソートアルゴリズムであるとは，

• 返すリストが元のリストと順番だけしか異ならず，
• かつ返されるリストが昇順にソートされている

ということで表現できます．この両方を示すことで，ソートであることを証明します．

以下に注意事項を書いておきます：

• リストが置換で等しいことは ~ で表現します．
• 定義した関数が有限時間で停止することを保証するために，termination_by を使用します．
• 証明に「リスト l の長さに対する帰納法」を用いるのですが，lean4 で実現するには induction' タクティクを用います．
• 選択ソートの定義の中で mem : μ ∈ l を証明していますが，後に続く置換であることの証明やソート済みであることの証明でも再度示しています．これは，関数の中で補題として示した命題にスコープ外からアクセスすることができないためです．