The Coq mailing list

[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.
In the trunk, there is also an alternative experimental tactic nlia.

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