クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する

#はじめに
[前回の記事](https://qiita.com/nekonibox/items/c1c7f4d1ad1695967e39)で、全順序が仮定されているからこそうまくいくソートアルゴリズムを半順序で使用するとどうなるかを見ました。結果としてクイックソートなら半順序でもうまくソートできることを見ましたが、本記事では、これを定理証明支援系Coqを用いて、形式的に証明していきます。

定理証明支援系Coqに関して軽く説明しておくと、プログラムが正しく動くことを、数学的に検証できるツールとして使えるものです。

#クイックソートを定義
SSReflectのpathライブラリには、標準のソート関数`sort`が定義されていますが、このアルゴリズムはマージソートなので、前回の記事で検証したように半順序では使えません。
そこでCoqでクイックソートを定義します。
まず定義の前に、ソートを行う要素の集合`T`と、半順序関係`R`を宣言しておきます。実際には`T`は型で、`R`はただの`T`上の二項関係`T -> T -> bool`として定義しています。`R`が半順序関係であることは証明する時に仮定します。

```coq
Section qsort.
  Variable (T:Type).
  Variable (R:Rel T).
```

クイックソート`qsort`を定義するために`Function`コマンドを使います。

```coq
  Function qsort (s:seq T) {measure size s} :=
    if s is x :: s'
    then qsort [seq y <- s' | R y x] ++ x :: qsort [seq y <- s' | ~~ R y x]
    else [::].
  Proof.
    - move => _ x s _/=. apply /ltP. by rewrite ltnS size_filter count_size.
    - move => _ x s _/=. apply /ltP. by rewrite ltnS size_filter count_size.
  Defined.
```

ここで`{measure size s}`と記述するのは、`qsort`の停止性を保証するためです。
Coqでプログラムを定義するには、プログラムの停止性を保証しなくてはいけません。具体的には、メジャー関数と呼ばれる、以下のような性質を満たす関数を示してやる必要があります。

- プログラムの引数から自然数への関数であり、プログラムが再帰呼び出しされるたびに呼び出される関数の引数が狭義短調減少するもの。

今回、メジャーとして列の長さを返す関数`size`を与えています。`Proof`以降では、この関数の再帰呼び出しを行った際の引数がこのメジャーで狭義減少していることを証明しています。

##帰納原理
`Function`コマンドで関数を定義すると、その関数の帰納原理など、定義した関数に関する基本的な定理も自動生成されます。しかし、今回定義したクイックソートの場合、自動生成される帰納原理`qsort_ind`の使い勝手が悪いです。

```coq
qsort_ind
     : forall P : seq T -> seq T -> Prop,
       (forall (s : seq T) (x : T) (s' : seq T),
        s = x :: s' ->
        P [seq y <- s' | R y x] (qsort [seq y <- s' | R y x]) ->
        P [seq y <- s' | ~~ R y x] (qsort [seq y <- s' | ~~ R y x]) ->
        P (x :: s')
          (qsort [seq y <- s' | R y x] ++ x :: qsort [seq y <- s' | ~~ R y x])) ->
       (forall s _x : seq T,
        s = _x ->
        match _x with
        | [::] => True
        | _ :: _ => False
        end -> P _x [::]) -> forall s : seq T, P s (qsort s)
```
本当は以下のようなシンプルなもので十分です。

```coq
  Lemma my_qsort_ind (P:seq T -> Prop) :
    P [::] ->
    (forall x s, P [seq y <- s | R y x] ->
                 P [seq y <- s | ~~ R y x] ->
                 P (x :: s)) ->
    forall s, P s.
```
この補題の証明は[こちらの記事]
(https://qiita.com/nekonibox/items/8147291e9fd483e3d579)を参照してください。


クイックソートにおいて、引数が`[::]`の場合とそうでない場合で場合分けをするので、この帰納原理にもそれぞれの場合に対応した2つの仮定があります。

なぜ、自動生成された帰納原理よりシンプルに記述できるかというと、`my_qsort_ind`は`qsort`が再帰呼び出しをする引数のみに着目した補題であり、その計算には触れていないからです。その証拠に、自動生成された`qsort_ind`の定義には`qsort`が表れていますが、`my_qsort_ind`内に`qsort`は表れません。
関数の停止性を示すときにも、内部の計算には触れず、再帰呼び出しする引数のみに着目しますが、同様に帰納原理も引数だけに着目したもので十分です。

実際に`my_qsort_ind`を使用した証明を見ていきます。

###クイックソートに関する補題
後の半順序でのソートに関する証明に使う補題を示しておきます。

```coq
  Lemma all_qsort p s : all p (qsort s) = all p s.
  Proof.
    elim /my_qsort_ind : s =>[|x s]//=.
    rewrite [qsort (_ :: _)]qsort_equation all_cat /==>->->.
    case : (p x) =>/=; last exact : andbF. elim : s =>[|y s]//=.
    case : ifP =>_/=<-; case : (p y)=>//=. exact : andbF.
  Qed.
```

この補題はクイックソートしたリスト`qsort s`の各要素で`p`が成り立つことと、元のリスト`s`の各要素で`p`が成り立つことが同値であることを示しており、`my_qsort_ind`を使った帰納法で示すことができます。
証明中に`qsort_equation`という補題が使われていますが、これは`qsort`を定義したときに自動生成される補題で、`qsort s`を定義式の右辺に書き換えるものになっています。

次に半順序におけるソートされている状態を定義します。

#半順序におけるソートされている状態とは
以下に定義するのが半順序に関するソートされている状態を表す述語になります。

```coq
  Fixpoint mysorted (s:seq T) :=
    if s is x :: s'
    then all (fun y => ~~ R y x || R x y) s' && mysorted s'
    else true.
```

`~~ R y x || R x y`は`R y x ==> R x y`の言い換えとなっており、[前回の記事](https://qiita.com/nekonibox/items/c1c7f4d1ad1695967e39)と同様の定義になっていることがわかります。
ここで名前が`mysorted`なのは、もともとpathライブラリに全順序におけるソートされた状態を表す述語`sorted`があるからです。実際に、`R`が全順序のときは`mysorted`と`sorted`は同値になります。

また、`mysorted`に関する補題を1つ示しておきます。

```coq
  Lemma mysorted_cat s1 s2 :
    mysorted s1 -> mysorted s2 ->
    all (fun x => all (fun y => ~~ R y x || R x y) s2) s1 ->
    mysorted (s1 ++ s2).
  Proof.
    elim : s1 =>[|x s1 IHs1]//=.
    rewrite all_cat => /andP [->] Hs1 Hs2 /andP [->]/=. exact : IHs1.
  Qed.
```
これは、リスト`s1`、`s2`を結合したときに`mysorted`であることの十分条件を表しています。クイックソートでは再帰呼び出しを行った後に結合するので、この補題があると便利です。


#ソート可能であることの証明

ここからが本題です。まず半順序を仮定します。

```coq
  Hypothesis (Htrans:transitive R).
```

あれ？と思うかも知れませんが、これでいいのです。
半順序は反射性、反対称性、推移性を満たす二項関係で定義されますが、ここでは推移性のみを仮定しています。
実はクイックソートでソート可能であることを示すには推移性だけしか使わないです。
実際の証明は以下の通りです。

```coq
  Lemma qsort_sorted s : mysorted (qsort s).
  Proof.
    elim /my_qsort_ind : s =>[|x s IHs1 IHs2]//.
    rewrite qsort_equation. apply : mysorted_cat =>//=.
    - rewrite IHs2 andbT all_qsort.
        by apply : (sub_all _ (filter_all _ _)) => y ->.
    - rewrite all_qsort.
      apply : (sub_all _ (filter_all _ _)) => y Hyx.
      rewrite Hyx orbT all_qsort /=.
      apply : (sub_all _ (filter_all _ _)) => z.
      case Hzy : (R z y)=>//. by rewrite (Htrans Hzy Hyx).
  Qed.
```

証明の流れとしては、まず`my_qsort_ind`を使い、`qsort`が再帰呼び出しする場合としない場合で場合分けをします。引数が`[::]`の場合は`//`ですぐ示せるので、引数が`x :: s`の場合だけを考えればいいです。
引数が`x :: s`の場合は`mysorted (qsort [seq y <- s | R y x] ++ x :: qsort [seq y <- s | ~~ R y x])`を示すわけですが、ここで先程示した`mysorted_cat`を使います。
`mysorted_cat`の1つ目と2つ目の仮定は帰納法の仮定からすぐわかるので、最後の仮定だけを示せばいいです。そこから先は流れで示せます。

#まとめ
クイックソートが半順序でもソートできることをCoq/SSReflectを使って形式的に証明しました。実は半順序を仮定しなくても、推移性を満たす任意の二項関係で成り立つことがわかりました。