Module Polynomial.WithProof

module WithProof constructs polynomials packed with the proof that their sign is correct.

type t
exception InvalidProof

InvalidProof is raised if the operation is invalid.

val repr : t -> (LinPoly.t * op) * ProofFormat.prf_rule
val proof : t -> ProofFormat.prf_rule
val polynomial : t -> LinPoly.t
val compare : t -> t -> int
val annot : string -> t -> t
val of_cstr : (cstr * ProofFormat.prf_rule) -> t
val output : Stdlib.out_channel -> t -> unit

out_channel chan c pretty-prints the constraint c over the channel chan

val output_sys : Stdlib.out_channel -> t list -> unit
val zero : t

zero represents the tautology (0=0)

const n represents the tautology (n>=0)

val product : t -> t -> t

product p q

  • returns

    the polynomial p*q with its sign and proof

val addition : t -> t -> t

addition p q

  • returns

    the polynomial p+q with its sign and proof

val neg : t -> t

neg p

  • returns

    the polynomial -p with its sign and proof

  • raises an

    error if this not an equality

mul_cst c q

  • returns

    the polynomial c * q with its sign and proof.

val def : LinPoly.t -> op -> int -> t

def p op i creates an alias with the variable index i

val square : LinPoly.t -> LinPoly.t -> t

square p q is q = p^2 >= 0

val mkhyp : LinPoly.t -> op -> int -> t

mkhyp p op i binds p to hypothesis i

val cutting_plane : t -> t option

cutting_plane p does integer reasoning and adjust the constant to be integral

val linear_pivot : t list -> t -> Vect.var -> t -> t option

linear_pivot sys p x q

  • returns

    the polynomial q where x is eliminated using the polynomial p The pivoting operation is only defined if

    • p is linear in x i.e p = a.x+b and x neither occurs in a and b
    • The pivoting also requires some sign conditions for a
val simple_pivot : (Micromega_core_plugin.NumCompat.Q.t * var) -> t -> t -> t option

simple_pivot (c,x) p q performs a pivoting over the variable x where p = c+a1.x1+....+c.x+...an.xn and c <> 0

val sort : t list -> ((int * (Micromega_core_plugin.NumCompat.Q.t * var)) * t) list

sort sys sorts constraints according to the lexicographic order (number of variables, size of the smallest coefficient

subst sys performs the equivalent of the 'subst' tactic of Rocq. For every p=0 \in sys such that p is linear in x with coefficient +/- 1 i.e. p = 0 <-> x = e and x \notin e. Replace x by e in sys

NB: performing this transformation may hinders the non-linear prover to find a proof. elim_simple_linear_equality is much more careful.

val subst : t list -> t list
val subst_constant : bool -> t list -> t list

subst_constant b sys performs the equivalent of the 'subst' tactic of Rocq only if there is an equation a.x = c for a,c a constant and a divides c if b= true

val saturate_subst : bool -> t list -> t list