Вернемся к проверке Coq для проверки через 5-8 лет: как доказать, что (в общем случае n, m: N, (n - (S m)) = pred (n - m))?

Question

Где-то между 5 и 8 годами go (вероятно, 6 или 7) я написал полную формализацию Bubble Sort в Coq. Одной из самых ранних проверенных лемм была та, которая в названии, которую я назвал «sub_succ_r» (или, может быть, это стандартное имя?):

forall n m : nat, (n - (S m))%nat = pred(n - m)

Теперь, тогда это было очень простое доказательство что лемма:

intros n m.
induction n m using n_double_ind.
simpl.
auto.
apply sub_0_r.
Qed.

"sub_0_r" - это лемма, утверждающая, что

forall n : nat, (n - 0)%nat = n

Теперь внимательные читатели, которые также знакомы с современным Coq, возможно, уже обнаружили проблему со старым доказательство: эта вторая строка.

induction n m

, то есть одновременная индукция по 2 терминам, больше не работает, даже когда указывается, что используется «n_double_ind». Я ломал голову над тем, как доказать это, используя сначала индукцию по n, а затем индукцию по m, но я просто не могу понять это.

Любая помощь, большая или маленькая, будет высоко цениться .

Answer 1

Если вы хотите применить индукцию к двум переменным одновременно, вам нужно использовать запятую, или Coq распознает f t как f, примененный к t, поэтому, когда вы пишете n m, это фактически означает n это функция, и вы хотите применить ее к m. Вместо этого используйте запятую, как это:

induction n, m.

это генерирует четыре подцели. Два из них могут быть доказаны с помощью auto, поэтому вы можете попросить Coq использовать auto tacti c для каждой подцели, сгенерированной индукцией, используя точку с запятой следующим образом:

induction n, m; auto.

, а остальные подцели легко доказать, используя упомянутая вами лемма и гипотезы индукции. поэтому весь сценарий выглядит следующим образом:

Lemma sub_0_r : forall n : nat, (n - 0) = n.
Admitted.

Theorem sub_succ_r: forall n m : nat, (n - (S m)) = pred(n - m).
Proof.
  induction n, m; auto.
  - apply sub_0_r.
  - apply IHn.
Qed.

Также обратите внимание, что использование %nat необязательно.

Но, как вы видели, мы использовали только IHn, что означает, что мы не t использовать гипотезу индукции для m, поэтому нам не нужно использовать induction на m, только destruct tacti c будет работать, лучшее доказательство:

induction n; destruct m; auto.
- apply sub_0_r.
- apply IHn.

который минимален и изящен.