Двойная индукция в Coq

По сути, я хотел бы доказать это следующим результатом:

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

recurrence double induction coq
person Matteo Zanchi    schedule 05.10.2013    source источник

Ответы (3)


arrow_upward
8
arrow_downward

На самом деле есть гораздо более простое решение. 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.
person Community    schedule 05.10.2013

arrow_upward
3
arrow_downward

fix Решение @Rui является довольно общим. Вот альтернативное решение, использующее следующее наблюдение: при мысленном доказательстве этой леммы вы используете несколько более сильный принцип индукции. Например, если 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 доказывает что-то лишнее, но вызов тактики индукции дает достаточный контекст для почти тривиального доказательства.

person NonNumeric    schedule 19.11.2013

arrow_upward
1
arrow_downward

Я считаю, что для этого необходима хорошо обоснованная индукция.

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.
person Community    schedule 05.10.2013