Предположим, что у меня есть сумма как a + (b + (c + d)), которую я хочу преобразовать в a + b + c + d, чтобы применить лемму.Coq: удалить все (вложенные) круглые скобки из суммы
Выполнение этого вручную с помощью Nat.add_assoc крайне утомительно. Есть ли более разумный способ?
«легко, но не хороший» способ, которым я хотел бы использовать это replace (a + (b + (c + d)))) with (a + b + c + d) by now omega
Вы можете использовать repeat тактический, который повторяет некоторые тактику до тех пор, пока не может быть применено больше:
repeat rewrite Nat.add_assoc.
или более кратким версия:
rewrite !Nat.add_assoc.
Он работает так же, как и в варианте с repeat.
Недостатком этого подхода является то, что он переписывается повсюду в цели. Таким образом, вы можете захотеть выбрать часть своей формулы для перезаписи только на ней.
Почему это не приятно? Кроме того, вы также можете использовать 'auto с *'. –
Если вы когда-либо рассматривали выходной термин, созданный 'omega', вы поймете. В большинстве случаев это слишком сложно, а небольшое доказательство с использованием переписывания будет меньше. Но это вопрос личного мнения;) – Vinz
'by omega' будет работать; и 'by ring' также решает проблему. Первый модуль «Omega» должен быть импортирован; последний - «Арит». –