雙誘導勒柯克

基本上，我想證明以下結果：雙誘導勒柯克

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

雙誘導勒柯克

回答

相關問題