Как изменить условия в Coq, используя плюс коммутируемость и ассоциативность?

Question

У меня есть общий вопрос о том, как переставить термины в Coq. Например, если у нас есть термин m + p + n + p, люди могут быстро перестроить термины примерно на m + n + p + p (неявно используя plus_comm и plus_assoc). Как мы делаем это эффективно в 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.

Любые предложения по эффективному переписыванию также приветствуются.

Спасибо.

Answer 1

Как Артур говорит, иногда omega не хватает, но я иногда использую его для простых шагов, подобных этому.

Require Import Omega. 
Theorem test: forall a b c:nat, a + b + 2 * c = c + b + a + c. 
    intros. 
    replace (c + b + a) with (a + b + c) by omega. 
    replace (a + b + c + c) with (a + b + (c + c)) by omega. 
    replace (c + c) with (2 * c) by omega. 
    reflexivity. 
Qed. 

Это глупый пример, потому что omega решили бы все это на одном дыхании, но иногда вы хотите переписать вещи внутри функций, которые omega не могут достичь в без небольшой помощи ...

Answer 2

В данном конкретном случае (линейная арифметической над целыми числами), вы можете просто использовать omega тактику:

Require Import Omega. 

Theorem plus_comm_test: forall n m p: nat, 
    m + p + (n + p) = m + n + 2 * p. 
Proof. intros; omega. Qed. 

Однако бывают ситуации, когда omega недостаточно. В таких случаях стандартная тактика rewrite не очень удобна. В библиотеке Ssreflect есть своя версия тактики rewrite, которая работает намного лучше для таких задач, как переписывание на суб-терминах вашей цели. Например:

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool. 
Require Import Ssreflect.ssrnat. 

Theorem plus_comm_test: forall n m p: nat, 
    m + p + (n + p) = m + n + 2 * p. 
Proof. 
move=> n m p. 
by rewrite -addnA [p + _]addnC -[_ + p]addnA addnn -mul2n addnA. 
Qed. 

аннотациям в квадратных скобках, например, [p + _], обеспечивают модели, которые помогают rewrite тактический рисунок, где действовать. Лиммы и друзья addn* - это собственная версия Ssreflect стандартных арифметических результатов над натуральными числами.