Geek Answers Handbook

Double induction in Coq

Basically, I would like to prove that the following result:

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

which is a recurrence scheme of the so-called double induction.

I tried to prove that he uses induction twice, but I'm not sure that I will get to the end. In fact, I am stuck at this point:

Proof.
  intros. elim n.
    exact H.
    intros. elim n0.
      exact H0.
      intros. apply (H1 n1).
+4
source share
3 answers

In fact, there is a much simpler solution. A fixadmits recursion (aka induction) on any subterm, and nat_rectadmits recursion on a direct subtopic of a nat. nat_rectit is determined by itself fix, but nat_indis only a special case 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.
+8

@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 - , .

+4

, .

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.
+1

More articles:


All Articles