概要

Coqの帰納的定義で自動生成される帰納法は機能が貧弱です。例えば自然数natに対する nat_ind は、「n=kについて成立を仮定すればn=k+1で成立する」という形式の帰納法の正しさの根拠である typed objectです。一方より強力な帰納法「n≤kについて成立を仮定すればn=k+1で成立する」という形式――累積的帰納法/course of values induction――が存在します。そちらを使わなければ証明できない数学的言明も多々あります。

そこで本稿では累積的帰納法を使った証明を実践してみます。

解きたい課題

$f(0)=2, f(1)=2, f(n+2)=f(n)+f(n+1)$で定義される関数 myfunc の出力が必ず偶数になることを証明しましょう。証明の手順は明らかで「一つ前と二つ前が偶数なんだから足しても偶数だから全部偶数」となります。ここでは、一つ前だけでなく二つ前についての性質を利用しているので、通常の帰納法では詰まってしまいます

Fixpoint myfunc n :=
match n with
| O => 2
| S O => 2
| S (S n'' as n') =>  myfunc n'' + myfunc n'
end.

例えばこんな感じで詰まります:

Require Import Even.
Theorem alleven_fail: forall n, even(myfunc n).
Proof. induction n.
- repeat(constructor).
- simpl. destruct n. repeat(constructor). apply even_even_plus; try assumption.
Admitted.

Coqでの解決法

Init.Wf において一般的な帰納の枠組みである整礎帰納法を扱えます。特に自然数の場合には累積帰納法となり、Arith.Wf_natに必要な道具立てが揃っています。つまり順序関係 ltがwell foundedであるという事実から累積帰納法の正しさの根拠である typed object が得られます:

Require Import Wf_nat.
Check lt_wf_ind.
(* lt_wf_ind
     : forall (n : nat) (P : nat -> Prop),
       (forall n0 : nat, (forall m : nat, m < n0 -> P m) -> P n0) -> P n
*)

というわけで、これを使うと上記例題を証明できます。inductionタクティックにusingをつけてこの帰納法を使うよう指示します(恰好をつけなくても apply lt_wf_ind とやってもよいです):

Require Import Even.
Require Import Wf_nat.

Theorem alleven: forall n, even (myfunc n).
Proof.
  induction n using lt_wf_ind.
  destruct n as [|[|n'']].
  - repeat(constructor).
  - repeat(constructor).
  - simpl. apply even_even_plus.
   + apply H. auto.
   + destruct n''.
       * repeat(constructor).
       * apply even_even_plus. apply H. auto. apply H. auto.
Qed.

おまけ

勉強のため自分でも lt がwell foundedである証明をしてみました。一応メモとして置いておきます:

Require Import Compare_dec.

Lemma xyz: forall n m:nat, n < m -> m < S n -> False.
Proof. induction n; intros.
- destruct m.
 + inversion H.
 + apply Lt.lt_S_n in H0. inversion H0.
- destruct m.
 + inversion H.
 + apply Lt.lt_S_n in H0. apply Lt.lt_S_n in H.
    eapply IHn; eassumption.
Qed.

Theorem wf_lt: well_founded lt.
Proof.
 intros n. induction n.
 - split. intros m H. inversion H.
 - split. intros m H2.
   destruct(lt_eq_lt_dec m n) as [[]|].
   + apply IHn. assumption.
   + subst. assumption.
   + exfalso. eapply xyz; eassumption.
Qed.

おまけ２

関係しそうな帰納原理を列挙します

まずは nat_ind です。自然数を帰納的に定義した時にCoqが自動生成してくれます。一番シンプルなタイプの帰納法であり、数学的にはペアノ算術に含まれる公理図式でもあります。本稿でも触れたように機能不足である場合がありえます:

nat_ind: forall P:nat->Prop,
    P O ->
    (forall k:nat, P k -> P (S k)) ->
    forall n:nat, P n

続いて le_ind です。順序関係 le すなわち ≤ はCoqでは帰納的に定義されるので、Coqが自動的にその帰納原理を生成してくれます。特にOを渡したときの帰納原理は、あと一歩というところです:

le_ind: forall (n:nat) (P:nat->Prop),
    P n ->
    (forall k:nat, n <= k -> P k -> P (S k)) ->
    forall m:nat, n <= m -> P m

次は本稿で主に説明した lt_wf_ind です。これは Wf_nat をインポートするとアクセスできる帰納原理です。 lt が well founded であることを利用した整礎帰納法です

lt_wf_ind: forall (n:nat) (P:nat->Prop),
    (forall k:nat, (forall m:nat, m < k -> P m) -> P k)->
    P n.

コメントで指摘のあったfunctional inductionで使う帰納原理です。Functionで関数定義すると自動生成される myfunc の構造を反映した帰納原理です。P a bは関数入力がaの時の出力がbでありそこで性質が成立すると読めます:

myfunc_ind: forall P: nat->nat->Prop,
    (forall n:nat, n = 0 -> P 0 2) ->
    (forall n:nat, n = 1 -> P 1 2) ->
    (forall n n'':nat,
        n = S (S n'') ->
        P n'' (myfunc n'') ->
        P (S n'') (myfunc (S n'')) ->
        P (S (S n'')) (myfunc n''+ myfunc (S n''))) ->
    forall n:nat, P n (myfunc n).