У меня есть общий вопрос о том, как переставить термины в Coq. Например, если у нас есть термин m + p + n + p
, люди могут быстро перестроить термины примерно на m + n + p + p
(неявно используя plus_comm и plus_assoc). Как мы делаем это эффективно в Coq?Как изменить условия в Coq, используя плюс коммутируемость и ассоциативность?
Для (глупый), например,
Require Import Coq.Arith.Plus.
Require Import Coq.Setoids.Setoid.
Theorem plus_comm_test: forall n m p: nat,
m + p + (n + p) = m + n + 2 * p.
Proof. intros. rewrite plus_assoc. simpl. rewrite <- plus_n_O.
Теперь мы имеем
1 subgoals
...
______________________________________(1/1)
m + p + n + p = m + n + (p + p)
Мой вопрос:
Как переписать LHS в m + n + p + p
эффективно?
Я пытался использовать rewrite plus_comm at 2
, но он дает ошибку Nothing to rewrite.
Просто с помощью переписывания plus_comm
изменяет LHS в p + m + n + p
.
Любые предложения по эффективному переписыванию также приветствуются.
Спасибо.
Спасибо за ответ. Но то, что я показал, является частью большего доказательства «нат». Часть 'm + p + n + p' заключена в нечто другое. Кроме того, я пытаюсь узнать, как работает Coq. Знаете ли вы о более примитивном методе Coq для этого, не привлекая внешние библиотеки? – tinlyx
Хотел бы я, чтобы я ... Я лично никогда не мог понять, как узнать синтаксис для всех функций 'rewrite' в стандартном Coq. Я полагаю, что может быть ошибка, из-за которой возникновение выбора ведет себя некорректно, когда используется библиотека 'Setoid', но я не уверен. В любом случае вы всегда можете явно указывать параметры в своих леммах, что помогает избежать неоднозначностей в некоторых случаях, например. 'rewrite <- (plus_assoc m p)'. –
Вы также можете использовать 'assert', чтобы доказать уравнение, которое вы хотите отдельно, используя' omega', а затем переписать с ним напрямую. –