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.
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...
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.
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.