Coq
定理証明
Coq-8.7
余帰納法

Coqの余帰納法でハマってしまった

帰納的構造に従った再帰では、帰納的な型の値を引数にとり、再帰呼び出しにはより小さい値を与えます。
一方で余帰納的構造に従った余再帰では、余帰納的な型の値を返り値として返し、余再帰呼び出しの結果よりも大きい値を返します。

Inductive List := Nil : List | Cons : nat -> List -> List.
Fixpoint length l :=
  match l with
  | Nil => O
  | Cons n l' => S (length l') (* l' は l より "小さい" *)
  end.

CoInductive Stream := SCons : nat -> Stream -> Stream.
CoFixpoint countup (n : nat) : Stream :=
  SCons n (countup (S n)). 
(*SCons n (countup (S n)) は (countup (S n)) より大きい*)

ただしこの「大きい」は、ただ余再帰呼び出しの結果をコンストラクタで包めばいいというわけではなく、下に示すfooのような定義は受け入れられません。

CoFixpoint bad: Stream :=
  match bad with
  | SCons x y => SCons x bad
  end.

確かにこの関数の返り値SCons x badbadよりも「大きい」ですが、badの最初の要素を決めようとすると無限再帰に陥ります。

Coqのcofix/CoFixpointには、余再帰呼び出しで得られた値について

  • matchで分解してはならない
  • コンストラクタによって「大きく」して返さなければならない

という制約があり、これらを満たしているときGuardedであるとよばれます。

当然ながらこのGuarded制約は、余帰納的な証明にも適用されます。
そのため余帰納的証明では、余帰納法の仮定をdestructやinversionで分解することはできません。
証明中にうっかりこれをやっていないかは、Guardedコマンドで確認することができます。

さて、自分がハマったのはここからです。
簡単のため、ごく単純な余帰納的述語を考えます。

CoInductive X : nat -> Prop :=
| X_intro : forall n, X (S n) ->X n.

これがすべての自然数に対して成り立つことは容易に示せます。

Lemma X_All : forall n, X n.
Proof.
  cofix CIH. (* CIH: ∀n. X n |- ∀n. X n *)
  intro n.   (* CIH: ∀n. X n, n: nat |- X n *)
  constructor. (* CIH : ∀ n. X n, n: nat |- X (S n) *)
  apply CIH.
Qed.

ですが説明のために、同じ命題に対して少しひねくれた証明を考えます。

Lemma X_All' : forall n, X n.
Proof.
  enough (forall n, X (S (S n)) -> X n) as H.
  - cofix CIH.
    intro n.
    apply H.
    apply CIH.
  - intros n H.
    constructor.
    constructor.
    assumption.
Qed.

Xのコンストラクタである x_intro : forall n, X (S n) -> X nをわざわざforall n, X (S (S n)) -> X nに変形して使っています。余計な事をしてはいますが、Guard条件は満たされているので証明は成立します。
問題がおきるのは、この変形を定理として外に出した場合です。


Lemma X_SSn_n : forall n, X (S (S n)) -> X n.
Proof.
  intros n H.
  constructor.
  constructor.
  assumption.
Qed.

Lemma X_All'' : forall n, X n.
Proof.
  cofix CIH.
  intro n.
  apply X_SSn_n.
  apply CIH.
  (*Qed. -> Error *)
Abort.

やっていることは同じですが、X_All''Qedしようとすると、Guard条件のチェックに失敗します。
証明は同じなのに、なぜ失敗するのでしょうか。 X_All''に相当するプログラムを直接CoFixpointを使って書くとどうなるかをみてみます。

CoFixpoint X_All'' n : X n :=
  X_SSn_n n (X_All'' (S (S n))).

この余再帰がGuard条件を満たしているかどうかはX_SSn_nの中身を見ないとわかりません。ところがX_SSn_nQedコマンドによって中身が隠蔽されているために、チェックができないというわけです。そのため、X_SSn_nの末尾をQedではなくDefinedに変えると、上記の証明はチェックを通ります。

そもそも余帰納的証明においては、余帰納法の仮定を他の定理に渡すこと自体が筋が悪いので、この仕様も仕方がないことなのだろうと思います。
どうしても使いたい場合は、補題をQedではなくDefinedで締めておけばチェックは通るようです。