real_ideal_cofactors : term list -> term -> term list

SYNOPSIS

Produces cofactors proving that one real polynomial is in the ideal generated by others.

DESCRIPTION

The call real_ideal_cofactors [`p1`; ...; `pn`] `p`, where all the terms have type :real and can be considered as polynomials, will test whether p is in the ideal generated by the p1,...,pn. If so, it will return a corresponding list [`q1`; ...; `qn`] of `cofactors' such that the following is an algebraic identity (provable by REAL_RING or a slight elaboration of REAL_POLY_CONV, for example):

  p = p1 * q1 + ... + pn * qn

hence providing an explicit certificate for the ideal membership. If ideal membership does not hold, real_ideal_cofactors fails. The test is performed using a Gr\"obner basis procedure.

FAILURE CONDITIONS

Fails if the terms are ill-typed, or if ideal membership fails.

EXAMPLE

Here is a fairly simple example:

 # prioritize_real();;
 val it : unit = ()

 # real_ideal_cofactors
   [`y1 * y3 + x1 * x3`;
    `y3 * (y2 - y3) + (x2 - x3) * x3`]
   `x3 * y3 * (y1 * (x2 - x3) - x1 * (y2 - y3))`;;
 ...
val it : term list = [`&1 * y3 pow 2 + -- &1 * y2 * y3`; `&1 * y1 * y3`]

and we can confirm the identity as follows (note that REAL_IDEAL_CONV already does this directly):

  # REAL_RING `(&1 * y3 pow 2 + -- &1 * y2 * y3) * (y1 * y3 + x1 * x3) +
               (&1 * y1 * y3) * (y3 * (y2 - y3) + (x2 - x3) * x3) =
               x3 * y3 * (y1 * (x2 - x3) - x1 * (y2 - y3))`;;

COMMENTS

When we say that terms can be `considered as polynomials', we mean that initial normalization, essentially in the style of REAL_POLY_CONV, will be applied, but some complex constructs such as conditional expressions will be treated as atomic.