К каким терминам мы можем применить лемму?

Question

Предположим, у нас есть цель

a + b + c + d = a + c + b + d

, где a, b, c, d: nat и лемма plus_comm из Arith:

plus_comm
     : forall n m : nat, n + m = m + n

Можно сделать

• rewrite plus_comm. для получения d + (a + b + c) = a + c + b + d и
• rewrite (plus_comm a b). для получения b + a + c + d = a + c + b + d.

Но выполнение rewrite (plus_comm b c) или rewrite (plus_comm c d) приведет кошибка, аналогичная

Found no subterm matching "b + c" in the current goal.

Вопрос. Почему это так, и что мы можем сделать, чтобы переписать b + c как c + b в цели?

---

Редактировать. Переписать b + c как c + b мы можем сделать

rewrite (plus_assoc_reverse a).
rewrite (plus_comm b c).
rewrite plus_assoc.

Для доказательства леммы с помощью reflexivity. Есть ли более элегантный способ?

Answer 1

В этом случае, если вы хотите избежать необходимости знать все теоремы наизусть, вы часто можете написать:

ring

Эта команда (также называемая тактикой),доступно, как только вы загрузите библиотеку Arith.Он специализируется на доказательстве равенств, в которых два члена имеют одинаковую ассоциативность по модулю, коммутативность сложения и умножения и дистрибутивность умножения над сложением.Если вы используете тип целых чисел Z, вы также можете включить вычитание.

Тактика omega, предложенная в другом ответе, сработает, но только для формул, которые содержат ограниченные формыумножение.Как примечание: omega будет удален в будущих версиях Coq, его заменит тактика с именем lia (что означает линейную целочисленную арифметику).

Answer 2

Оператор + в Coq является ассоциативным слева, поэтому такие термины, как a + b + c + d, фактически скрыты ((a + b) + c) + d.Это должно ответить, почему plus_comm не делает то, что вы ожидаете.

Чтобы решить эти типы целей, вам нужно применить серию лемм, как вы узнали.Это часто может быть утомительным, поэтому есть некоторые тактики для их решения, такие как omega (см. этот вопрос).