Module `Polynomial.WithProof`Source

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

Sourcetype t = (LinPoly.t * op) * ProofFormat.prf_rule

Sourceexception InvalidProof

InvalidProof is raised if the operation is invalid.

Sourceval compare : t -> t -> int

Sourceval annot : string -> t -> t

Sourceval of_cstr : (cstr * ProofFormat.prf_rule) -> t

Sourceval output : Stdlib.out_channel -> t -> unit

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

Sourceval output_sys : Stdlib.out_channel -> t list -> unit

Sourceval zero : t

zero represents the tautology (0=0)

Sourceval const : NumCompat.Q.t -> t

const n represents the tautology (n>=0)

Sourceval product : t -> t -> t

product p q

returns
the polynomial p*q with its sign and proof

Sourceval addition : t -> t -> t

addition p q

returns
the polynomial p+q with its sign and proof

Sourceval neg : t -> t

neg p

returns
the polynomial -p with its sign and proof

raises an
error if this not an equality

Sourceval mult : LinPoly.t -> t -> t

mult p q

returns
the polynomial p*q with its sign and proof.

raises InvalidProof
if p is not a constant and p is not an equality

Sourceval cutting_plane : t -> t option

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

Sourceval 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

Sourceval simple_pivot : (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

Sourceval sort : t list -> ((int * (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 Coq. 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.

Sourceval subst : t list -> t list

Sourceval subst_constant : bool -> t list -> t list

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

Sourceval subst1 : t list -> t list

subst1 sys performs a single substitution

Sourceval saturate_subst : bool -> t list -> t list

Sourceval is_substitution : bool -> t -> var option

Install

Dune Dependency

Authors

Maintainers

Sources

doc/micromega_plugin/Micromega_plugin/Polynomial/WithProof/index.html

Module `Polynomial.WithProof`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/micromega_plugin/Micromega_plugin/Polynomial/WithProof/index.html

Module Polynomial.WithProofSource

Module `Polynomial.WithProof`Source