vanilla Coq で整礎帰納法を使うには、 整礎帰納法のための induction principle (Wf_nat.lt_wf_ind とか) を使う
Require Import Wf_nat. Section S. Variable P : nat -> Prop. Goal forall n, P n. intro n. induction n using lt_wf_ind. (* n : nat H : forall m : nat, m < n -> P m ______________________________________(1/1) P n *)
SSReflect でも Coq の induction principle を使うことができる
From mathcomp Require Import all_ssreflect. Section S. Variable P : nat -> Prop. Goal forall n, P n. elim/Wf_nat.lt_wf_ind. (* forall n : nat, (forall m : nat, (m < n)%coq_nat -> P m) -> P n *)
しかしこれだと、(m < n)%coq_nat というように、 vanilla Coq の比較が出てくるので、SSReflect のスタイルじゃなくてちょっと扱いづらい
SSReflect のスタイルに直すには以下のようにすればよい
move=> n IH'. have IH : forall m : nat, m < n -> P m. move=> m mn. by apply/IH'/ltP. clear IH'. (* IH : forall m : nat, m < n -> P m *)
vanilla Coq の比較がはじめから出てこない、SSReflect 流の整礎帰納法のやりかたはないのか探してみると、 An Ssreflect Tutorial (2009) に elim: n {-2}n (leqnn n) というやり方が載っていた (strong induction で探すと出てくる。 載っているのは、elim: m {-2}m 0 (leqnn m) という形で、変数が m で、さらに命題の中にある 0 を一般化している。)
これだけだとなにをやっているのかわからないけれど、説明を読むと、 P n を forall m, m <= n -> P m に一般化してから普通の自然数の帰納法 (nat_ind) を使うという流れのようだ
From mathcomp Require Import all_ssreflect.
Section S.
Variable P : nat -> Prop.
Goal forall n, P n.
move=> n.
elim: n {-2}n (leqnn n).
(*
______________________________________(1/2)
forall n : nat, n <= 0 -> P n
______________________________________(2/2)
forall n : nat,
(forall n0 : nat, n0 <= n -> P n0) -> forall n0 : nat, n0 <= n.+1 -> P n0
*)
うぅむ、lt_wf_ind を使った場合よりも複雑になっている
まず lt_wf_ind ではゴールがひとつだったが、こちらはゴールがふたつになる (普通の帰納法なので、0 の場合と 1以上の場合のふたつになるのはそうならざるを得ない)
ひとつめは P 0 の場合で、 ふたつめは n 以下の場合について成り立つなら n+1 以下について成り立つ、というやつ
ひとつめは P の中身がわからないとこれ以上はどうしようもない
ふたつめは、n+1 以下の場合のなかで、n 以下の場合は前提から証明できるので、 n+1 の場合だけにできる
そのように変形するには以下のようにすればよい
move=> n.
elim: n {-2}n (leqnn n) => [[] // _|n IH m].
admit. (* P 0 *)
rewrite leq_eqVlt => /orP []; last by rewrite ltnS; apply IH.
move/eqP => -> {m}.
(* IH : forall n0 : nat, n0 <= n -> P n0 *)
admit. (* P n.+1 *)
しかし... これが本当にお勧めの方法なのだろうか?
さらに調べると、 mathcomp の本 (2021) には この方向でちょっと進んだやつが載っていてどうも本気らしいと感じる (こっちだと -2 という場所の指定をしなくていいという点が進歩している)
move=> n. case: (ubnPgeq n) => m. elim: n m => [[] // _|n IH m]. admit. (* P 0 *) rewrite leq_eqVlt => /orP []; last by rewrite ltnS; apply IH. move/eqP => ->. (* IH : forall m : nat, m <= n -> P m *) admit. (* P n.+1 *)
うぅむ、あらかじめ整礎帰納法の induction principle を用意しておかなくていいという利点は理解できるが、 正直、Wf_nat.lt_wf_ind を使った方が簡単だと感じられる
SSReflect のやりかたのほうがいい場合はどういう場合だろう? 0 とそれ以外の場合わけが必要になるとき? 一般化のところをいじりたいとき?
2023-11-06 Parameter じゃなくて Variable を使うようにした
命題 P n を forall j i : nat, i < j -> P i という形に一般化すれば、 Wf_nat.lt_wf_ind みたいにできるのではないかと思いついた (i=n, j=n+1 と特殊化すると i<j は簡単に証明できるので、P n が出てくる)
試したところ、move: n.+1 {-2}n (ltnSn n) とすればそのように一般化できるようだ
そうした後で、m について帰納法を行うと、m = 0 の場合には n < m が偽になるので P に関係なく証明でき、 P の中身について考えなければならないゴールはひとつで済み、Wf_nat.lt_wf_ind と同じになる
From mathcomp Require Import all_ssreflect.
Section S.
Variable P : nat -> Prop.
Goal forall n, P n.
move=> n.
elim: n.+1 {-2}n (ltnSn n) => {n} [|n IH m]; first by [].
(* IH : forall n0 : nat, n0 < n -> P n0 *)
rewrite ltnS leq_eqVlt => /orP [/eqP -> {m}|]; last by apply IH.
admit. (* P n *)
2023-11-06 Parameter じゃなくて Variable を使うようにした
さて、どっちがマシかな
Goal forall n, P n.
move=> n.
elim: n.+1 {-2}n (ltnSn n) => {n} [|n IH m]; first by [].
rewrite ltnS leq_eqVlt => /orP [/eqP -> {m}|]; last by apply IH.
admit. (* P n *)
Restart.
elim/Wf_nat.lt_wf_ind => n IH'.
have IH m : m < n -> P m. by move/ltP; apply IH'.
clear IH'.
admit. (* P n *)
行数はだいたい同じだけど、lt_wf_ind を使った方が簡単に感じられる
(もちろん、lt_wf_ind の中身は別にあるわけなので、それを使わずにここまで行数を近づけられる、ともいえる)
mathcomp だと elim: n {-2}n (leqnn n) を簡単にするために ubnPgeq が使えたように、 elim: n.+1 {-2}n (ltnSn n) を簡単にするのが用意されてないかな、と思って調べたところ、 ssrnat.v のコメントに書いてあった
あまりよくわかってないが、ubnP というのがあって、以下のように使えるようだ
From mathcomp Require Import all_ssreflect.
Section S.
Variable P : nat -> Prop.
Goal forall n, P n.
move=> m.
have [n] := ubnP m.
elim: n m => // n IH m => /ltnSE.
(* IH : forall m : nat, m < n -> P m *)
rewrite leq_eqVlt => /orP [/eqP -> {m}|]; last by apply IH.
admit. (* P n *)
2023-11-06 Parameter じゃなくて Variable を使うようにした
[latest]