The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

Hi Thomas and Viktor.

Thanks!

zify transforms positive to Z. And then omega solves the rest.
Actually my original goal to solve was wrong, it should be

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


On Wed, May 30, 2012 at 5:46 PM, Thomas Braibant
<thomas.braibant AT gmail.com>
 wrote:
> 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



-- 
Jianzhou