双诱导勒柯克

基本上，我想证明以下结果：双诱导勒柯克

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

来源

2013-10-05 Matteo Zanchi

其实，有一个更简单的解决方案。 A 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.

来源

2013-10-05 21:47:52

我认为有理有据的感应是必要的。

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-05 17:35:05

@瑞的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-19 22:42:11 NonNumeric

双诱导勒柯克

回答

相关问题