if 式で定義された関数の性質を Lean Prover でどう証明するか

はじめに

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

以前の記事で，フィボナッチ数列を Lean4 で定義し，その性質を証明しました．このときはフィボナッチ数列という再帰的に定義されたシンプルな関数を扱っていましたが，しかしすべての関数がわかりやすく再帰的に定義されているとは限りません．一見して帰納法が使えなさそうな定義であったとき，証明はどのように行えばいいのでしょうか？

コード

今回実装するのは，「リストの最小値を先頭に持ってくる関数」と，その関数が「リストの置換を返すこと」です．関数が再帰呼び出しではなくて if ... else 式で定義されているので，帰納法を使うのは自然な方法ではありません．代わりにどうするかですが，if ... else がゴールにあるときのためのタクティクがあるので，それを使います．

以下にコードスニペットを示します．意図的に冗長な証明にしてあることに注意してください．もし知らないタクティクがあれば，タクティクリストなどで調べてみてください．