The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 09/12/2014 22:04, Daniel Galvez wrote:

> Can anyone describe to me how to add parenthese in an expression (such as
> turning the first expression into the second expression)? The larger program I
> need this statement in makes it such that I cannot simply insert parantheses
> manually where I need this proof.

You can either do it by hand by applying the corresponding rewriting rules:

unfold Qminus.
rewrite <- Qplus_assoc.

or you can let a tactic like ring or field do the proof for you 
automatically:

setoid_replace (a - b + c - d) with ((a - b) + (c - d)) by ring.

Whichever solution is better depends on how many rewriting steps you 
need to achieve the desired result.

Best regards,

Guillaume