Introduce AbstractIdealCertificate

[tweisser]

A polynomial equality p == q over an ideal generated by polynomials h[1],...,h[k] can be expressed in different ways. Currently, a groebner basis of the ideal is computed and p - q is reduced with respect to this groebner basis. The remaining coefficients are equated to zero.
Alternatively, one can introduce auxiliary variables and directly write the representation in the ideal

deg = [maxdegree(p-q) - maxdegree(hi) for hi in h]
idx = findall(i -> i>=0, deg)
@variable model aux[i in idx] Poly(maxdegree_basis(BT, variables(p - q), deg[i])
@constraint model coefficients(p-q -sum(h[i]*aux[i] for i in idx), BT) .== 0

The choice of deg is not backed up theoretically, the degree of the multipliers might actually be higher. I have not thought about an example for this though.

In order to be able to use sparsity efficiently, one should probably not use maxdegree_basis but generate a more sophisticated basis.