The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

I believe that [zify] if what you are looking for.

Require Import BinPos.
Goal (forall x y z: positive, x + y = z -> x + y + x + y = z + z)%positive.
intros. zify. omega.
Qed.

It works as well for N, btw, but may be slower than specially crafted
versions of zify, that are limited to the symbol you actually use.

Thomas


On Wed, May 30, 2012 at 5:35 PM, Jianzhou Zhao 
<jianzhou AT seas.upenn.edu>
 wrote:
> Hi List,
>
> I have some goals about properties of BinPos.positive. For example,
>   p1 + (p2 - p3) = p1 +  p2 - p3 when p2 >= p3 ...
> I did not find lemmas in Coq libs that can prove the goals like this 
> directly,
>
> Coq has tools to streamline proofs about real and Z. Rather than
> proving them from scratch, I was wondering if Coq lib or any Coq
> contribution already implemented tools or Tactics for reasoning about
> BinPos.positive.
>
> Thanks.
> --
> Jianzhou