概要
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.
おまけ2
関係しそうな帰納原理を列挙します
まずは 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).