coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] tactics for Z

From: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] tactics for Z
Date: Wed, 15 Jun 2011 10:30:27 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=P02lERQwG3qukuNG80P+/0ME8qvnOjaeaw/L+EYnGDjtOSy1VCCULsHKEsk3Cibtcr 5XbWu21WjzDgzDpRgQCGFotaopMDr+a9sQO3e0w3uUQ7YpUyo8v2nkIWrxPwtN3V+CYj 5nGg3Y7IFStpuwg+V6elJT69rkiha6cwniWJY=

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

[Coq-Club] tactics for Z, Jianzhou Zhao
- Re: [Coq-Club] tactics for Z, Fr�d�ric Besson
  - Re: [Coq-Club] tactics for Z, Jianzhou Zhao
    - Re: [Coq-Club] tactics for Z, Evgeny Makarov