Coq中的双重感应

Question

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

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

Answer 1

实际上,有一个更简单的解决方案.A fix允许在任何子项上进行递归(也称为归纳),同时nat_rect仅允许对a的直接子项进行递归nat.nat_rect本身是用a定义的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.