はじめに

この記事の方法はあまり良くないとの指摘があったので、最新
版の記事をご覧ください。

Coqにおける拡張ライブラリSSRelfectを導入した状態で完全帰納法を使いたいとき、完全帰納法自体の証明をやらずに、たった1行のコマンドで済む方法を紹介します。

使い方

Proof modeにおけるゴールが以下のようだったとします。¹

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

このときnに関する完全帰納法を使うときに以下のコマンドを実行します。

elim : n {-2}n (leqnn n).

すると以下のようなゴールに書き換わります。

P : nat -> Prop
n : nat
============================
forall n : nat, n <= 0, P n

subgoal 2 is:
forall n : nat,
  (forall n0 : nat, n0 <= n -> P n0) -> forall n0 : nat, n0 <= n.+1 -> P n0

1つ目のサブゴールは、実質P 0を示せと言っていて、これは完全帰納法が使えるなら示せる命題です。
2つ目のサブゴールに関して、P n0はn0 < n.+1のときは仮定からすぐ示せるため、実質P n.+1を示せと言っていることになります。今、n.+1未満の任意のn0に対してP n0が成り立つという仮定があるので、これはまさに完全帰納法の仮定そのものです。

1つ目のP 0の証明を書かないといけないのが若干冗長なものの、この方法を使えば完全帰納法そのものを証明するよりも簡単に完全帰納法が適用できます。

解説

どうしてこうなるかというと、まずleqnn nすなわちn <= nをスタックに追加し、{-2}nを実行することによって、2番目以外のnをスタックに追加します。
つまりゴールはforall n0 : nat, n0 <= n -> P n0なります。そこで残った2番目のnに関して通常の帰納法を使うと上記のようなゴールに書き換わるというわけです。

実際に使用してみる

次に実際に使用した様子を見てみます。

自然数に関する完全帰納法

まず、完全帰納法自体を証明してみます。

Lemma complete_ind (P:nat -> Prop) :
  (forall n, (forall m, m < n -> P m) -> P n) ->
  forall n, P n.
Proof.
  move => H n.
    by elim : n {-2}n (leqnn n) =>[[_|//]|n IHn m Hm];
       apply : H => l Hl //; exact : IHn (leq_trans Hl Hm).
Qed.

冗長だった1つ目のゴールは2つ目を示すのと同じ証明が使えるので、そんなに記述量が増えることはないです。

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

例として、クイックソートにおける帰納原理を示していきます。²

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

Lemma 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.
  elim : s {-2}s (leqnn (size s)) =>[|xs s IHs][]//= xl l Hsize.
    by apply : Hcons; exact : IHs (leq_trans (filter_size _ _) Hsize).
Qed.

elim : s {-2}s (leqnn (size s))もしくはelim : (size s) {-2}s (leqnn (size s))のように記述します。1つ目はリストに対する帰納法、2つ目はリストの長さに対する帰納法を使っていますが、変数sは、ゴールの仮定size s0 <= size sの部分1ヶ所にしか登場しないため、どちらを使用しても大丈夫です。

ちなみにリストの長さに対して帰納法を使ったときの証明は以下の通りです。

Proof.
  move => Hnil Hcons s.
  elim : (size s) {-2}s (leqnn (size s)) =>[|n IHn][]//= xl l Hsize.
    by apply : Hcons; exact : IHn (leq_trans (filter_size _ _) Hsize).
Qed.

どちらを使用したとしても、証明もほぼ同じで、記述する量もあまり変わらないことがわかります。

また、冗長だったゴールは仮定のP [::]ですぐに示せるので、証明2行目//=で消えているはずです。

まとめ

Coq/SSReflectで完全帰納法を使用する方法を解説しました。完全帰納法を直接使用するよりも若干冗長なゴールが増えますが、使用例で見たようにそれが大きな手間になるわけではないため、実用上ではそんなに問題になることはないと思います。