Coqで累積的帰納法/course of values induction

# 概要
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` の出力が必ず偶数になることを証明しましょう。証明の手順は明らかで「一つ前と二つ前が偶数なんだから足しても偶数だから全部偶数」となります。ここでは、一つ前だけでなく二つ前についての性質を利用しているので、通常の帰納法では詰まってしまいます

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

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

```coq
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](https://coq.inria.fr/library/Coq.Init.Wf.html) において一般的な帰納の枠組みである整礎帰納法を扱えます。特に自然数の場合には累積帰納法となり、[Arith.Wf_nat](https://coq.inria.fr/distrib/current/stdlib/Coq.Arith.Wf_nat.html)に必要な道具立てが揃っています。つまり順序関係 `lt`がwell foundedであるという事実から累積帰納法の正しさの根拠である typed object が得られます:

```coq
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 とやってもよいです):

```coq
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である証明をしてみました。一応メモとして置いておきます:

```coq
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が自動生成してくれます。一番シンプルなタイプの帰納法であり、数学的にはペアノ算術に含まれる公理図式でもあります。本稿でも触れたように機能不足である場合がありえます:

```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`を渡したときの帰納原理は、あと一歩というところです:

```coq
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 であることを利用した整礎帰納法です

```coq
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でありそこで性質が成立すると読めます:

```coq
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).
```