4

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

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

4 回答 4

8

实际上，有一个更简单的解决方案。Afix允许对任何子项进行递归（也称为归纳），而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.
于 2013-10-05T21:47:52.613 回答
3

@Rui 的fix解决方案很笼统。这是使用以下观察的替代解决方案：在心理上证明这个引理时，您使用了更强的归纳原理。例如，如果 P 为两个连续的数字成立，则很容易让它为下一对成立：

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 回答
1

我认为有充分根据的归纳是必要的。

Require Import Arith.

Theorem nat_rect_3 : forall P,
  (forall n1, (forall n2, n2 < n1 -> P n2) -> P n1) ->
  forall n, P n.
Proof.
intros P H1 n1.
apply Acc_rect with (R := lt).
  info_eauto.
  induction n1 as [| n1 H2].
    apply Acc_intro. intros n2 H3. Check lt_n_0. Check (lt_n_0 _). Check (lt_n_0 _ H3). destruct (lt_n_0 _ H3).
    destruct H2 as [H2]. apply Acc_intro. intros n2 H3. apply Acc_intro. intros n3 H4. apply H2. info_eauto with *.
Defined.

Theorem nat_rect_2 : forall P,
  P 0 ->
  P 1 ->
  (forall n, P n -> P (S (S n))) ->
  forall n, P n.
Proof.
intros ? H1 H2 H3.
induction n as [n H4] using nat_rect_3.
destruct n as [| [| n]].
info_eauto with *.
info_eauto with *.
info_eauto with *.
Defined.
于 2013-10-05T17:35:05.833 回答
1

一个有趣的观察：Rui 的答案是 NonNumeric 答案的定点翻译，它是 user1861759 对任何 n 答案的概括，而不仅仅是 n = 2。

换句话说，这些答案都很好，并且实际上通过终止固定点和广义归纳之间的对应关系彼此密切相关。

于 2021-12-24T02:34:50.683 回答