The Coq mailing list

[Fr�d�ric Besson <fbesson AT irisa.fr>]

Hello,

> 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. *)
Indeed, it will!
As you explain below, psatz is only reasoning over R:
If the goal is provable over Z but not over R, the tactic is very  
very likely to fail
(the only bit of Z reasoning is the  removal of strict comparisons: x  
> y --> x -1 >= y)

> 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.
Here, you could still get a bit more of automation using psatz.
intros x.
case (Z_le_dec 2 x) ; psatz Z.
Qed.

> 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.
Humm, I do not really know what is going on -- it is fairly difficult  
the understand the limits of csdp.
BTW, the csdp driver is taken from J. Harrison Hol Light sos module  
-- it can prove amazing  things!

What is for sure is that:
- the tactic normalises  polynomials.
    Your goal is boils down to this nasty one
     forall x, 27 * x ^ 4 + 126 * x ^ 3 - 1191 * x ^ 2 + 2350 * x -  
1400 <= 0 ->   x < 3.
- the degree of polynomials has a strong impact on csdp
- csdp is using numeric methods and might therefore miss a proof.

I tried to solve your goal by hand and  it appears that psatz fails  
on embarrassingly simpler sub-goals.
I will investigate that...

BTW, if Coq users stumble on non linear polynomial goals that cannot  
be solved automatically, I am client -- drop me a mail !

--
Frédéric