The Coq mailing list

[Victor Magron <magron AT lix.polytechnique.fr>]

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.