The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello Victor!

Indeed for this kind of applications, you can try the native-coq branch: 
https://github.com/maximedenes/native-coq

Be warn though that you can experience bugs since this branch is very 
unstable at the moment. I advise you to checkout the commit whose hash 
is e3004efeb229878b0de1ed0b3c29d3e4fad306ea since arithmetic with the VM 
is broken in more recent revisions, and the ring tactic calls the VM.

I tried your example and it is almost instantly solved (less than a second).

Cheers,

Maxime.

On 07/08/2013 17:33, Arnaud Spiwack wrote:
> Le me first remark that bigQ is not related to ZArith, it using 
> machine integers. Which is good, since in this case bigQ performs much 
> better than Q (from QArith).
>
> Considering that this polynomial is not extremely large, I may venture 
> a guess that ring spends most of its time reifying the term. Machine 
> integers are pretty efficient during computations, but they are not 
> very compact. Plus the reification of ring is done in Ltac, which is 
> not terribly efficient, and involves quite a bit of typechecking. So 
> that would be my guess.
>
> It was to solve this sort of problem with machine integers that 
> Benjamin Grégoire started working on a new implementation where 
> machine integers are directly in Term.constr. You may want to try his 
> branch for comparison.
>
>
> Arnaud
>
>
> On 7 August 2013 16:23, Victor Magron <magron AT lix.polytechnique.fr 
> <mailto:magron AT lix.polytechnique.fr>> wrote:
>
>     Hi,
>
>     I would like to check polynomial equalities in Coq with the ring
>     tactic of the following form (see the full example attached below):
>
>     pol - obj_min_norm  ==  sos_certif + (eps_pol - eps_pol_bound)
>
>     These polynomials come from an OCaml program, in which polynomials
>     are implemented with a sparse horner representation, and whose
>     coefficients lie in ZArith rationals. eps_pol and eps_pol_bound
>     are obtained in OCaml by subtracting sos_certif to pol. This
>     operation is quite efficient in OCaml but the equality checking
>     seems a bit long (4 seconds on my laptop) and the computation time
>     blows up for harder instances (I can provide it if someone is
>     interested).
>
>     Did I miss anything important to get a more efficient checking?
>
>     Thanks,
>
>     Victor
>
>     Require Export BigQ.
>     Local Open Scope bigQ_scope.
>     Section Ring_sos.
>     Variables x1 x2 x3 x4 x5 x6 : bigQ.
>     Definition pol := x1 * x1 - x1 * x2 - x1 * x3 + (2#1) * x1 * x4 -
>     x1 * x5 - x1 * x6 + x2 * x3 - x2 * x5 - x3 * x6 + x5 * x6.
>     Definition sos_certif := (0 + ((78842557#625000000) * ( -
>     (1591550007#2000000000) * x1 + (478671257#10000000000) * x2 +
>     (478671589#10000000000) * x3 + (5952045449#10000000000) * x4 +
>     (47867119#1000000000) * x5 + (47867163#1000000000) * x6 +
>     (575207831#10000000000)) * ( - (1591550007#2000000000) * x1 +
>     (478671257#10000000000) * x2 + (478671589#10000000000) * x3 +
>     (5952045449#10000000000) * x4 + (47867119#1000000000) * x5 +
>     (47867163#1000000000) * x6 + (575207831#10000000000)) +
>     ((32395219#40000000) * ( - (3#100000000) * x1 +
>     (4999999923#10000000000) * x2 - (4999999827#10000000000) * x3 +
>     (21#1000000000) * x4 + (2500000149#5000000000) * x5 -
>     (312499997#625000000) * x6 + (1#625000000)) * ( - (3#100000000) *
>     x1 + (4999999923#10000000000) * x2 - (4999999827#10000000000) * x3
>     + (21#1000000000) * x4 + (2500000149#5000000000) * x5 -
>     (312499997#625000000) * x6 + (1#625000000)) + ((72395219#40000000)
>     * ((111#10000000000) * x1 + (625000029#1250000000) * x2 -
>     (2500000009#5000000000) * x3 + (63#10000000000) * x4 -
>     (2500000009#5000000000) * x5 + (1249999933#2500000000) * x6 +
>     (1#1250000000)) * ((111#10000000000) * x1 + (625000029#1250000000)
>     * x2 - (2500000009#5000000000) * x3 + (63#10000000000) * x4 -
>     (2500000009#5000000000) * x5 + (1249999933#2500000000) * x6 +
>     (1#1250000000)) + ((112395219#40000000) * ( - (119#10000000000) *
>     x1 - (4999999901#10000000000) * x2 - (2500000013#5000000000) * x3
>     - (37#2500000000) * x4 + (4999999849#10000000000) * x5 +
>     (156250007#312500000) * x6 - (3#2500000000)) * ( -
>     (119#10000000000) * x1 - (4999999901#10000000000) * x2 -
>     (2500000013#5000000000) * x3 - (37#2500000000) * x4 +
>     (4999999849#10000000000) * x5 + (156250007#312500000) * x6 -
>     (3#2500000000)) + ((18657170729#5000000000) * ( -
>     (2240378883#5000000000) * x1 + (2853181119#10000000000) * x2 +
>     (8916191#31250000) * x3 - (6870831991#10000000000) * x4 +
>     (2853180807#10000000000) * x5 + (2853181037#10000000000) * x6 -
>     (24359759#625000000)) * ( - (2240378883#5000000000) * x1 +
>     (2853181119#10000000000) * x2 + (8916191#31250000) * x3 -
>     (6870831991#10000000000) * x4 + (2853180807#10000000000) * x5 +
>     (2853181037#10000000000) * x6 - (24359759#625000000)) +
>     ((4657899054193#10000000000) * ( - (10916327#5000000000) * x1 +
>     (178504357#10000000000) * x2 + (178504363#10000000000) * x3 +
>     (875460347#10000000000) * x4 + (3570087#200000000) * x5 +
>     (35700873#2000000000) * x6 - (9955181429#10000000000)) * ( -
>     (10916327#5000000000) * x1 + (178504357#10000000000) * x2 +
>     (178504363#10000000000) * x3 + (875460347#10000000000) * x4 +
>     (3570087#200000000) * x5 + (35700873#2000000000) * x6 -
>     (9955181429#10000000000))))))))) * ((1#1)) + ((0 +
>     ((29669230517#10000000000) * ((1555625319#10000000000) * x1 -
>     (2469565117#2500000000)) * ((1555625319#10000000000) * x1 -
>     (2469565117#2500000000)))) * (x1 - (4#1)) + ((0 +
>     ((29674285353#10000000000) * ((1555315053#10000000000) * x1 -
>     (9878309323#10000000000)) * ((1555315053#10000000000) * x1 -
>     (9878309323#10000000000)))) * ( - x1 + (3969#625)) + ((0 +
>     ((814626130139#10000000000) * ((1555535797#10000000000) * x2 -
>     (1975654913#2000000000)) * ((1555535797#10000000000) * x2 -
>     (1975654913#2000000000)))) * (x2 - (4#1)) +
>     (((114150119#2500000000) * ( - (195843101#200000000) * x2 -
>     (2028225697#10000000000)) * ( - (195843101#200000000) * x2 -
>     (2028225697#10000000000)) + ((117130722631#2500000000) *
>     ((2028225697#10000000000) * x2 - (195843101#200000000)) *
>     ((2028225697#10000000000) * x2 - (195843101#200000000)))) * ( - x2
>     + (3969#625)) + ((0 + ((814626068469#10000000000) *
>     ((1555535789#10000000000) * x3 - (4939137283#5000000000)) *
>     ((1555535789#10000000000) * x3 - (4939137283#5000000000)))) * (x3
>     - (4#1)) + (((456599693#10000000000) * ( - (1958431009#2000000000)
>     * x3 - (50705643#250000000)) * ( - (1958431009#2000000000) * x3 -
>     (50705643#250000000)) + ((468522849307#10000000000) *
>     ((50705643#250000000) * x3 - (1958431009#2000000000)) *
>     ((50705643#250000000) * x3 - (1958431009#2000000000)))) * ( - x3 +
>     (3969#625)) + (((403673831#10000000000) * ( -
>     (495715909#500000000) * x4 - (653126143#5000000000)) * ( -
>     (495715909#500000000) * x4 - (653126143#5000000000)) +
>     ((4208674618169#10000000000) * ((653126143#5000000000) * x4 -
>     (495715909#500000000)) * ((653126143#5000000000) * x4 -
>     (495715909#500000000)))) * (x4 - (3969#625)) + ((0 +
>     ((14921155953#50000000) * ((1555535783#10000000000) * x4 -
>     (9878274567#10000000000)) * ((1555535783#10000000000) * x4 -
>     (9878274567#10000000000)))) * ( - x4 + (8#1)) + ((0 +
>     ((814626182027#10000000000) * ((1555535821#10000000000) * x5 -
>     (9878274561#10000000000)) * ((1555535821#10000000000) * x5 -
>     (9878274561#10000000000)))) * (x5 - (4#1)) +
>     (((28537493#625000000) * ( - (9792155047#10000000000) * x5 -
>     (2028225711#10000000000)) * ( - (9792155047#10000000000) * x5 -
>     (2028225711#10000000000)) + ((3660335329#78125000) *
>     ((2028225711#10000000000) * x5 - (9792155047#10000000000)) *
>     ((2028225711#10000000000) * x5 - (9792155047#10000000000)))) * ( -
>     x5 + (3969#625)) + ((0 + ((814626048953#10000000000) *
>     ((1555535827#10000000000) * x6 - (3858701#3906250)) *
>     ((1555535827#10000000000) * x6 - (3858701#3906250)))) * (x6 -
>     (4#1)) + (((456600459#10000000000) * ( - (2448038761#2500000000) *
>     x6 - (1014112863#5000000000)) * ( - (2448038761#2500000000) * x6 -
>     (1014112863#5000000000)) + ((468522828541#10000000000) *
>     ((1014112863#5000000000) * x6 - (2448038761#2500000000)) *
>     ((1014112863#5000000000) * x6 - (2448038761#2500000000)))) * ( -
>     x6 + (3969#625)))))))))))))).
>     Definition eps_pol :=  -
>     (820481632091241172808193#50000000000000000000000000000) * x1 * x1
>     * x1 +
>     (61896591623813080558471919637#625000000000000000000000000000000)
>     * x1 * x1 - (620291295589380028253#62500000000000000000000000000)
>     * x1 * x2 -
>     (2529454905290470625087#250000000000000000000000000000) * x1 * x3
>     - (272116981506221298699#31250000000000000000000000000) * x1 * x4
>     - (2492418835250797609777#250000000000000000000000000000) * x1 *
>     x5 - (2486673428068127959867#250000000000000000000000000000) * x1
>     * x6 +
>     (20287639038035263743100640691#625000000000000000000000000000000)
>     * x1 + (16711994651716976017973#200000000000000000000000000000) *
>     x2 * x2 * x2 -
>     (440177966542069171149375729#625000000000000000000000000000000) *
>     x2 * x2 - (5285773773749486754229#500000000000000000000000000000)
>     * x2 * x3 -
>     (5935760426960501166081#500000000000000000000000000000) * x2 * x4
>     - (2558877948455574420587#250000000000000000000000000000) * x2 *
>     x5 - (5135160463433038060359#500000000000000000000000000000) * x2
>     * x6 +
>     (17199416807259531188107931#25000000000000000000000000000000) * x2
>     + (6511452965571496527097#125000000000000000000000000000) * x3 *
>     x3 * x3 -
>     (902474983587847187508307#1250000000000000000000000000000) * x3 *
>     x3 - (845853026703404600109#100000000000000000000000000000) * x3 *
>     x4 - (472203181642218717429#50000000000000000000000000000) * x3 *
>     x5 - (947887260576589754979#100000000000000000000000000000) * x3 *
>     x6 + (60376042466684254444854597#25000000000000000000000000000000)
>     * x3 - (34661261460045123332131#250000000000000000000000000000) *
>     x4 * x4 * x4 +
>     (793047140235409866382585731#625000000000000000000000000000000) *
>     x4 * x4 - (972579562890585443381#125000000000000000000000000000) *
>     x4 * x5 - (3788322857889158248369#500000000000000000000000000000)
>     * x4 * x6 +
>     (407373926408822049438960913#62500000000000000000000000000000) *
>     x4 - (2674500399545806658163#1000000000000000000000000000000) * x5
>     * x5 * x5 +
>     (23886350554674110429569507#312500000000000000000000000000000) *
>     x5 * x5 - (1142854599772644349143#125000000000000000000000000000)
>     * x5 * x6 -
>     (592730160494268315445733671#625000000000000000000000000000000) *
>     x5 + (2426764882571030478403#1000000000000000000000000000000) * x6
>     * x6 * x6 +
>     (34641879820406960223114513#125000000000000000000000000000000) *
>     x6 * x6 -
>     (773418241689763265383222273#312500000000000000000000000000000) *
>     x6 -
>     (96342236722586521345305323057689#2560000000000000000000000000000000000).
>     Definition eps_pol_bound :=
>     (-30298985907618546382650873207301#512000000000000000000000000000000000).
>     Definition obj_min_norm :=
>     (-2520477499429974704598122245460053#62500000000000000000000000000000).
>
>     Lemma test_ring_sos : pol - obj_min_norm  ==  sos_certif +
>     (eps_pol - eps_pol_bound).
>
>     unfold pol; unfold eps_pol; unfold obj_min_norm; unfold
>     eps_pol_bound; unfold sos_certif.
>
>     Time ring.
>
>     Qed.
>
>     End Ring_sos.