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
で場合分けすると、
expr
にTrue
とFalse
を設定することができる。
(今回はdecideLTE
を使っても良かったけど)
それと、fusion則を一般化した形で書きたかったけどな~
.
.