The Coq mailing list

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

2011/6/15 Frédéric Besson 
<frederic.besson AT inria.fr>:
> Hello,
>
> The psatz tactic does the job (Chapter 20 of the refman).
> Note that it requires an external tool csdp.

Thanks. It solves the goal after I installed csdp.

> In the trunk, there is also an alternative experimental tactic nlia.

Does nlia reply on any external tools? I think it is not included in
the 8.3 release. Where can I access the tactic?

> Require Import ZArith.
> Require Import Psatz.
> Open Scope Z_scope.
>
> Goal forall a b, a > 0 -> b < 0 -> a * b < 0.
> Proof.
>  intros.
>  psatz Z. (* nlia. *)
> Qed.
>
> Best,
> --
> Frédéric
>
> On 15 juin 2011, at 16:30, Jianzhou Zhao wrote:
>
>> Hi,
>>
>> I am trying to solve a goal for Z arithmetic, for example
>>   a > 0 -> b < 0 -> a * b < 0
>>
>> The Zhint db works for many cases, but does not solve the goal. I
>> looked into the tactics lia, psatzl at
>>  http://coq.inria.fr/stdlib/Coq.micromega.Psatz.html
>> They still cannot solve the goal.
>>
>> Do we have any other tactics in the stdlib for Z, rather than proving
>> the lemma manually?
>>
>> Thanks.
>> --
>> Jianzhou
>
>
>



-- 
Jianzhou