The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Balazs Vegvari wrote:
> one thing came into my mind after reading documentation of the omega
> tactic: what if omega could not solve a similar system, for example
> adding a nonlinear product to the example? How would I prove this
> manually in that case?
>
> thanks,
> Balazs
>   
Non linear integer arithmetic is undecidable: there is no algorithm that 
is guaranteed
to prove all true formulas. Thus, Coq provides a few decision procedures
that are able to cope with non-linear formulas, for instance the 
micromega package
provides one such tactic (psatz Z).  If you look at the sources of  
Coq-8.2beta4, in the
sub-directory test-suite/micromega, you will see a few examples using 
this tactic.  Here is
an example that works (to run this example, you need to install both 
Coq-8.2beta4
and an extra piece of software called csdp  
https://projects.coin-or.org/Csdp/,
If you want to work with Coq 8.1, you can download the package that was 
later
included in Coq at Frédéric Besson's page 
http://www.irisa.fr/lande/fbesson/micromega.tar.gz).


Require Import ZArith Psatz.
Open Scope Z_scope.

Lemma ex1 : forall x, (x-2)*(x-1) <= 0 -> x <= 3.
intros; psatz Z.
Qed.

I believe the following is an example where psatz fail, but Frédéric Besson
may know ways to parameterize the tactic that make it succeed.

Lemma ex2 : forall x, 0 < (3 * x - 4) * (3 * x - 5).
intros; psatz Z.  (* here the program seems to compute for ever. *)

Now we can prove ex2, because the formula is a product of two monomials 
that
are either both positive (when 2 <= x) or both negative (when x < 2).  
Here is
a proof.

intros x.
case (Z_le_dec 2 x); intros x2.
apply Zmult_lt_0_compat; omega.
replace ((3*x-4)*(3*x-5)) with ((4-3*x)*(5-3*x)) by ring.
apply Zmult_lt_0_compat; omega.
Qed.

The line "intros x H1" means, "let's assume that x is an integer".
The line "case (Z_le_dec 2 x); intros x2." means "let's consider two cases,
either 2 <= x, or ~2<=x in both cases, let's name this fact x2."
The line "apply Zmult_lt_0_compat; omega." means "according to the theorem
Zmult_lt_0_compat, it suffices to prove  0 < 3*x-4 and 0 < 3*x-5, both 
formulas
are consequences of known facts (in particular x2) in linear integer 
arithmetic",
At this point, the case where "2 <= x" is solved, and we switch our 
attention to
the other case where ~x <= 2 (this fact is still called x2).
the line "replace ((3*x-4)*(3*x-5)) with ((4-3*x)*(5-3*x)) by ring." means
"according to the ring properties of integers, the formula ((3*x-4...)) 
can be
replaced with ((4-3*x...))."
The second line "apply Zmult_lt_0_compat; omega" means "it suffices to 
prove
0 < 4 - 3*x and 0 < 5 - 3*x, both formulas are consequences of known 
facts in
linear integer arithmetics."

psatz works by extracting from the goal a polynomial that is always 
positive on
the real line.  Here the most natural polynomial is (3*x-4)*(3*x-5) but 
although
this polynomial is positive on all integers, there are real numbers for 
which it
is negative (3/2, for instance), I relied on this and hoped that it 
would provide
an example of a provable goal that cannot be proved using psatz.  It 
worked!

Nevertheless, I was suprised by the behavior of the tactic on the 
following two examples:

forall x, (x+10)*(3*x-4) <= 0 -> x < 2  (success)
forall x, (x + 10) * (3 * x - 4) * (3 * x - 5) * (3 * x - 7) <= 0 -> x < 
3 (failure, but this goal is
provable, using the same technique as above)

Frédéric may be able to add some information and documentation.

Yves