実例：ソートの正しさ

計算する関数と、その仕様を、別々に理解します。

18.1 何を証明したいのか

ソート関数に期待する性質は、「出力が昇順である」ことだけではありません。すべての要素が、消えず、増えず、並べ替えられただけであることも必要です。

ソートの仕様 ＝ 出力は整列済み ∧ 出力は入力の並べ替えである

Tauto では、計算する関数 sort と、その性質を述べる定理を、分けて書けます。sort は第 6 章で書いた挿入ソートです（insert で、整列済みのリストに一つの要素を正しい位置へ入れます）。

18.2 完成する定理の形

この証明は、リポジトリの examples/sort/ にあります（proof/sort.taut）。整列済みであることを表す sorted は、各要素が次の要素以下であることを述べる命題を返す関数で、Perm は、順列を表す帰納的な命題です。

inductive Perm(A: Type): (List(A)) -> (List(A)) -> Prop {
  perm_nil(): Perm(A, Nil, Nil)
  perm_skip<x: A, l: List(A), m: List(A)>(h: Perm(A, l, m)): Perm(A, Cons(x, l), Cons(x, m))
  perm_swap<x: A, y: A, l: List(A)>(): Perm(A, Cons(x, Cons(y, l)), Cons(y, Cons(x, l)))
  perm_trans<l: List(A), m: List(A), n: List(A)>(a: Perm(A, l, m), b: Perm(A, m, n)): Perm(A, l, n)
}

二つの定理を別々に証明します。

theorem sort_perm<A>(l: List(A)): Perm(A, l, sort(l)) where Ord(A) { ... }
theorem sort_sorted<A>(l: List(A)): sorted(sort(l)) where Ord(A) { ... }

そして、AndIntro で合成すると、sort_correct が完成します。

theorem sort_correct<A>(l: List(A)): sorted(sort(l)) ∧ Perm(A, l, sort(l)) where Ord(A) {
  AndIntro(sort_sorted(l), sort_perm(l))
}

実際に検査します。

tauto check examples/sort/proof/sort.taut

ok      sort_perm
ok      insert_after
ok      insert_sorted
ok      sort_sorted
ok      sort_correct

（ほかの補題も並びます。）

重要なのは、sort_correct という名前の定理を、宣言しただけでは意味がないことです。補題が実際に検査され、仮定が何なのかを追跡できて初めて、根拠のある保証になります。この例は、公理を一つも使っていません。

18.3 使える範囲を考える

このソートは、Ord(A) を満たす型に対して成り立ちます。証明が使う A の性質は、Ord の法則だけです。比較の法則が成り立たない「順序」に対しては、証明の前提が崩れます。一般的な定理ほど、前提条件を正確に理解することが大切です。

演習 18.1：出力が昇順でも、要素を一つ消してしまう実装が「ソート」として不正なのは、どの仕様を破っているからでしょうか。