The Coq mailing list

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

Ok, I will try native-coq since the efficiency seems much better.

Thanks a lot for your explanations and kind answers!

Victor

2013/8/7 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@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.