доказывая сильную индукцию в coq с нуля

Я занимаюсь доказательством эквивалентности слабой и сильной индукции.

У меня есть такое определение:

Definition strong_induct (nP : nat->Prop) : Prop :=
  nP 0 /\
  (forall n : nat,
    (forall k : nat, k <= n -> nP k) ->
    nP (S n))
.

И я хотел доказать следующее и написал:

Lemma n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m
.

Lemma strong_induct_nP__nP_n__nP_k : forall (nP : nat->Prop)(n : nat),
  strong_induct nP -> nP n ->
  (forall k, k < n -> nP k)
.
Proof.
  intros nP n [Hl Hr].
  induction n as [|n' IHn].
  - intros H k H'. inversion H'.
  - intros H k H'.
    inversion H'.
    + destruct n' as [|n''] eqn : En'.
      * apply Hl.
      * apply Hr.
        unfold lt in IHn.
        assert(H'' : nP (S n'') -> forall k : nat, k <= n'' -> nP k). {
          intros Hx kx Hxx.
          apply n_le_m__Sn_le_Sm in Hxx.
          apply IHn.
          - apply Hx.
          - apply Hxx.
        }

Однако я не могу продолжать доказательство дальше. Как мне доказать лемму в этой ситуации?


induction coq
person user5876164    schedule 07.12.2019    source источник
comment
В утверждении, которое вы пытаетесь доказать, есть проблема. strong_induct nP всегда верно, независимо от nP. Таким образом, лемма действительно говорит nP n -> forall k, k < n -> nP k, что неверно.   -  person Li-yao Xia    schedule 07.12.2019
comment
Я не понимаю, какое отношение лемма, которую вы пытаетесь доказать, к доказательству эквивалентности слабой и сильной индукции. У вас возникли проблемы с тем, чтобы показать, что сильная индукция подразумевает слабую индукцию или наоборот?   -  person Ifaz Kabir    schedule 11.12.2019

Ответы (1)


arrow_upward
0
arrow_downward

Замена forall в основной лемме значительно упрощает доказательство. Я написал это следующим образом:

Lemma strong_induct_is_correct : forall (nP : nat->Prop),
  strong_induct nP -> (forall n k, k <= n -> nP k).

(Также обратите внимание, что в определении strong_induct вы использовали <=, поэтому лучше использовать то же отношение в лемме, что и я.)

Поэтому я мог бы использовать следующую лемму:

Lemma leq_implies_le_or_eq: forall m n : nat,
  m <= S n -> m <= n \/ m = S n.

чтобы доказать основную лемму следующим образом:

Proof.
  intros nP [Hl Hr] n.
  induction n as [|n' IHn].
  - intros k Hk. inversion Hk. apply Hl.
  - intros k Hk. apply leq_implies_le_or_eq in Hk.
    destruct Hk as [Hkle | Hkeq].
    + apply IHn. apply Hkle.
    + rewrite Hkeq. apply Hr in IHn. apply IHn.
Qed.

Это гораздо более простое доказательство, и вы также можете доказать более красивую лемму, используя лемму выше.

Lemma strong_induct_is_correct_prettier : forall (nP : nat->Prop),
  strong_induct nP -> (forall n, nP n).
Proof.
  intros nP H n.
  apply (strong_induct_is_correct nP H n n).
  auto.
Qed.

Примечание. Обычно после однократного использования destruct или induction тактики повторное использование одной из них не очень помогает. Поэтому я думаю, что использование destruct n' после induction n ни к чему не приведет.

person Kamyar Mirzavaziri    schedule 15.03.2020