コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

Idrisで挿入ソート

挿入ソート - Wikipedia

foldrで挿入ソートを実装できることを知った。

insert : Nat -> List Nat -> List Nat
insert x []      = [x]
insert x (y::ys) = if lte x y then x :: y :: ys
                              else y :: insert x ys
-- 挿入ソート
isort : List Nat -> List Nat
isort = foldr insert []

*Isort> isort [9, 3, 7, 1, 4, 1]
[1, 1, 3, 4, 7, 9] : List Nat

.
.
よし、この挿入ソートの正当性を証明しよう。
ソートの正当性を言う為には、ソートされている事の他に、
要素が変わっていない事(元リストのPermutationであること)
も言わないといけないですが、スキップします。
.
.

sorted (foldr insert [] zs) = True

foldrに関数をかぶせているので、何か定理がないかな~と探したら、
『foldrのfusion則』
というのがあるらしい。
.
.
これは、

f undefined = undefined(今回は手で確認する)
f a = b
∀x,y f (g x y) = h x (f y)

の3条件の元で、

f . foldr g a = foldr h b

が成立するというもの。

参考記事:

.
.
『foldrのfusion則』を使ってsortedを証明したものがこちら。

Idrisのテクとして、if (expr) then a else bを証明したい時、
with (expr) proof pで場合分けすると、
exprTrueFalseを設定することができる。
(今回はdecideLTEを使っても良かったけど)

それと、fusion則を一般化した形で書きたかったけどな~
.
.