The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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> 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.