#はじめに

前回の記事で完全帰納法を適用する方法について記述しましたが、{-2}のように適用する場所を指定するのはあまり良くない¹ため、今は用いられないとの指摘がありました。

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

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

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

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

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

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

 elim /ltn_ind : n =>[n IHn]

これにより、ゴールが

  P : nat -> Prop
  n : nat
  IHn : forall m : nat, m < n -> P m
=============================
 P n

に書き変わります。

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

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

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

  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に関する完全帰納法は、前回の記事と同様にforall n, n < m -> P nをmに関する帰納法を使って示します。²
この形を作るのが、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を一般化してから帰納法を回します。

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

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

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

##失敗例

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

  (* 失敗例 *)
  elim /ltn_ind : (size s).

  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に関して完全帰納法を使用します。

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

  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)を使うと、以下のように帰納法の仮定がスッキリします。

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

  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)

###具体例

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

  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.

ただし

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を用いた方法を使用するのがいいことがわかりました。

{n}表記は内部でNotationを分解したときに現れる回数で数えるため、表記通りの個数とは限らず、混同しやすい点が一因として挙げられる。 ↩
前回記事ではn <= m -> P nでしたが、n = mの場合の証明が冗長になるので、 n < mにしています。 ↩