はじめに
前回の記事で完全帰納法を適用する方法について記述しましたが、{-2}のように適用する場所を指定するのはあまり良くない1ため、今は用いられないとの指摘がありました。
そこで、本記事では、{}を使わずに完全帰納法を適用する方法について記述します。
自然数に対する完全帰納法
実は、完全帰納法自体は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に関する帰納法を使って示します。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を一般化してから帰納法を回します。
リストの長さに関する完全帰納法
以下のようにリスト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を用いた方法を使用するのがいいことがわかりました。