Coq 中的双重归纳

基本上，我想证明以下结果:

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

这就是所谓的双重归纳的递归方案。

我试图用归纳法证明它两次，但我不确定我会以这种方式到达任何地方。确实，我当时陷入了困境:

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

最佳答案

实际上，有一个更简单的解决方案。 fix 允许对任何子项进行递归(也称为归纳)，而 nat_rect 只允许对 nat 的直接子项进行递归。 nat_rect 本身是用 fix 定义的，而 nat_ind 只是 nat_rect 的一个特例。

Definition nat_rect_2 (P : nat -> Type) (f1 : P 0) (f2 : P 1)
  (f3 : forall n, P n -> P (S (S n))) : forall n, P n :=
  fix nat_rect_2 n :=
  match n with
  | 0 => f1
  | 1 => f2
  | S (S m) => f3 m (nat_rect_2 m)
  end.

关于Coq 中的双重归纳，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/19200136/