Coq/SSReflectで{}を使わずに完全帰納法を適用する

#はじめに

[前回の記事](https://qiita.com/nekonibox/items/514da8edfc6107b57254)で完全帰納法を適用する方法について記述しましたが、`{-2}`のように適用する場所を指定するのはあまり良くない[^1]ため、今は用いられないとの指摘がありました。

[^1]: `{n}`表記は内部で`Notation`を分解したときに現れる回数で数えるため、表記通りの個数とは限らず、混同しやすい点が一因として挙げられる。

そこで、本記事では、`{}`を使わずに完全帰納法を適用する方法について記述します。


#自然数に対する完全帰納法

実は、完全帰納法自体は`ssrnat`にて`ltn_ind`という名前で証明されています。

つまり、完全帰納法で示したい命題`P:nat -> Prop`があった場合

```coq
  P : nat -> Prop
  n : nat
=============================
 P n
```

以下のコマンドで完全帰納法を使うことができます。

```coq
 elim /ltn_ind : n =>[n IHn]
```

これにより、ゴールが

```coq
  P : nat -> Prop
  n : nat
  IHn : forall m : nat, m < n -> P m
=============================
 P n
```
に書き変わります。


##完全帰納法自体の証明

完全帰納法`ltn_ind`を`{}`を使わずに証明していきます。

ここでは元の証明を少し見やすい形にして`myltn_ind`として証明を解説していきます。

```coq
  Lemma myltn_ind (P:nat -> Prop) :
    (forall n, (forall m, m < n -> P m) -> P n) -> forall n, P n.
  Proof.
    move => accP n.
    have [m] := ubnP n.
    elim : m =>[|m IHm]// in n *=> lenm.
      by apply : accP => l /leq_trans /(_ lenm) /IHm.
  Qed.
```

`n`に関する完全帰納法は、[前回の記事](https://qiita.com/nekonibox/items/514da8edfc6107b57254)と同様に`forall n, n < m -> P n`を`m`に関する帰納法を使って示します。[^2]
この形を作るのが、`have [m] := ubnP n.`です。
これは`move : (ubnP n) =>[m]`と同じで、仮定に`{ m | n < m }`を持ってきて、これを`case`すると`forall m, n < m -> P n`が出てきます。
また、`elim : m =>[|m IHm]// in n *`は`elim : m n =>[|m IHm]// n`と同じで、`n`を一般化してから帰納法を回します。

[^2]: 前回記事では`n <= m -> P n`でしたが、`n = m`の場合の証明が冗長になるので、` n < m`にしています。



#リストの長さに関する完全帰納法

以下のようにリスト`s`に関する命題を示すのに、リストの長さ`size s`に関する完全帰納法を使いたいとします。

```coq
  T : Type
  P : seq T -> Prop
  n : seq T
=============================
 P s
```

##失敗例

このとき、単に`elim /ltn_ind : (size s)`としてしまうと、それがリスト`s`の長さであるという情報を失い、以下のように勝手な自然数に関する帰納法になってしまいます。

```coq
  (* 失敗例 *)
  elim /ltn_ind : (size s).
```
```coq
  T : Type
  P : seq T -> Prop
  n : seq T
=============================
 forall n : nat, (forall m : nat, m < n -> P s) -> P s
```


##`ltn_ind`を使う
そこで、`ltn_ind`を使う場合は、以下のように`size s = n`としてから`n`に関して完全帰納法を使用します。

```coq
  move eqs : (size s) => n.
  elim /ltn_ind : n s eqs =>[n IHn][|xs s]//=.
```

```coq
  T : Type
  P : seq T -> Prop
  n : seq T
  IHn : forall m : nat, m < n -> forall s : seq T, size s = m -> P s
=============================
 0 = n -> P [::]

subgoal 2
 (size s).+1 = n -> P (xs :: s)
```

しかしながら、帰納法の仮定に`size s = m`があり、証明が冗長になります。

##`ubnP`を使う
リストの長さに関する完全帰納法を使う場合は、完全帰納法の自体を示したように、`ubnP (size s)`を使うと、以下のように帰納法の仮定がスッキリします。

```coq
  have [n] := ubnP (size s).
  elim : n s =>[|n IHn][|xs s]//=; rewrite ltnS.
```

```coq
  T : Type
  P : seq T -> Prop
  n : seq T
  IHn : forall s : seq T, size s < n -> P s
=============================
 0 <= n -> P [::]

subgoal 2
 size s < n -> P (xs :: s)
```


###具体例

前回同様、例として、クイックソートに関する帰納原理を証明してみます。

```coq
  Variable (T:Type).
  Variable (R : rel T).

  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.
  Proof.
    move => Hnil Hcons s.
    have [n] := ubnP (size s).
    elim : n s =>[|n IHn][|xs s]//= Hsize.
      by apply : Hcons; exact : IHn (leq_ltn_trans (filter_size _ _) Hsize).
  Qed.
```

ただし

```coq
Lemma filter_size T p (s:seq T) : size (filter p s) <= size s.
Proof. by rewrite size_filter count_size. Qed.
```

#まとめ

Coq/SSReflectにおいて、完全帰納法を`{}`を使わずに適用する方法を示しました。
自然数の変数に対しては`ltn_ind`を使い、それ以外の値の場合は`ubnP`を用いた方法を使用するのがいいことがわかりました。