Если вы хотите применить индукцию к двум переменным одновременно, вам нужно использовать запятую, или 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.
который минимален и изящен.