4

基本的に、次の結果を証明したいと思います。

Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) ->
    forall n, P n.

それは、いわゆる二重誘導の再発スキームです。

帰納法を 2 回適用して証明しようとしましたが、この方法でどこにでも到達できるかどうかはわかりません。確かに、私はその時点で立ち往生しました：

Proof.
  intros. elim n.
    exact H.
    intros. elim n0.
      exact H0.
      intros. apply (H1 n1).
4

4 に答える 4

3

@Ruiのfix解決策は非常に一般的です。これは、次の観察を使用する別の解決策です。この補題を精神的に証明するときは、やや強力な帰納法を使用します。たとえば、P が 2 つの連続する数字で成り立つ場合、次のペアで成り立つようにするのは簡単になります。

Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) ->
    forall n, P n.
Proof.
  intros P0 P1 H.
  assert (G: forall n, P n /\ P (S n)).
    induction n as [ | n [Pn PSn]]; auto.
    split; try apply H; auto.
  apply G.
Qed.

ここで G は冗長なものを証明しますが、それに対して帰納法を呼び出すことで、自明に近い証明に十分なコンテキストがもたらされます。

于 2013-11-19T22:42:11.963 に答える