Выполнение двойной индукции в Coq правильно - PullRequest
Новая
       113

Выполнение двойной индукции в Coq правильно

0 голосов
/ 04 июня 2018

Я пытаюсь доказать теорему plus_n_Sm из главы Индукция в Основах программного обеспечения 

Theorem succ_is_plus_1: forall n: nat, S n = n + 1.
Proof.
  induction n as [| n' ind_hyp].
  - simpl. reflexivity.
  - simpl. rewrite <- ind_hyp. reflexivity.
Qed.

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  induction n as [| n' ind_hyp ].
  - induction m as [| m' ind_m ].
    + simpl. reflexivity.
    + simpl. reflexivity.
  - induction m as [| m' ind_m2 ].
    + rewrite -> succ_is_plus_1 . rewrite <- plus_n_O. reflexivity.
    + rewrite -> succ_is_plus_1. rewrite <- ind_m2.

Выход в этот момент 

1 subgoal
n' : nat
ind_hyp : forall m : nat, S (n' + m) = n' + S m
m' : nat
ind_m2 : S (S n' + m') = S n' + S m'
______________________________________(1/1)
S (S n' + m') + 1 = S n' + S (S m')

I 'Я застрял здесь.Что я делаю неправильно?Как правильно мыслить для доказательства индукции по двум переменным?

1 Ответ

0 голосов
/ 04 июня 2018

Как говорилось в первом комментарии, ключ в том, что индукции по n достаточно, m может быть константой.Тогда доказательство просто.

...