how to rearrange terms in Coq using plus communtat

Question

I have a general question about how to rearrange terms in Coq. For example, if we have a term m + p + n + p, humans can quickly re-arrange the terms to something like m + n + p + p (implicitly using plus_comm and plus_assoc). How do we do this efficiently in Coq?

For a (silly) example,

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.

Now, we have

1 subgoals
...
______________________________________(1/1)
m + p + n + p = m + n + (p + p)

My question is:

How do I rewrite the LHS to m + n + p + p effectively?

I tried to use rewrite plus_comm at 2, but it gives an error Nothing to rewrite. Simply using rewrite plus_comm changes the LHS to p + m + n + p.

Any suggestions on effective rewrites are also welcome.

Thanks.

Answer 1

In this particular case (linear arithmetic over the integers), you can just use the omega tactic:

Require Import Omega.

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

However, there are situations where omega is not enough. In those cases, the standard rewrite tactic is not very convenient. The Ssreflect library comes with its own version of the rewrite tactic, that works much better for tasks such as rewriting on sub-terms of your goal. For instance:

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.

The annotations in square brackets, such as [p + _], provide patterns that help the rewrite tactic figure out where to act. The addn* lemmas and friends are Ssreflect's own version of the standard arithmetic results over the natural numbers.

Answer 2

As Arthur says sometimes omega is not enough, but I sometimes use it for simple steps like this.

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.

This is a silly example, because omega would have solved it all in one go, but sometimes you want to rewrite things inside functions that omega can't reach into without a little help...

Answer 3

The ring tactic is able to prove equality of these rearrangements.

Using your example:

Require Import ZArith.
Open Scope Z_scope.

(* Both "ring" and "omega" can prove this. *)
Theorem plus_comm_test : forall n m p : Z,
  m + p + (n + p) = m + n + 2 * p.
Proof.
  intros.
  ring.
Qed.

ring works on the integers, but I don't think it works on the natural numbers.

However, ring is able to prove some identities that omega cannot prove. (The docs say, "Multiplication is handled by omega but only goals where at least one of the two multiplicands of products is a constant are solvable. This is the restriction meant by "Presburger arithmetic".")

For example:

(* "ring" can prove this but "omega" cannot. *)
Theorem rearrange_test : forall a b c : Z,
  a * (b + c) = c*a + b*a.
Proof.
  intros.
  ring.
Qed.