Module `Polynomial.WithProof`Source

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

Sourcetype t

Sourceexception InvalidProof

InvalidProof is raised if the operation is invalid.

Sourceval repr : t -> (LinPoly.t * op) * ProofFormat.prf_rule

Sourceval proof : t -> ProofFormat.prf_rule

Sourceval polynomial : t -> LinPoly.t

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 : Micromega_core_plugin.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 mul_cst : Micromega_core_plugin.NumCompat.Q.t -> t -> t

mul_cst c q

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

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

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

Sourceval square : LinPoly.t -> LinPoly.t -> t

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

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

mkhyp p op i binds p to hypothesis i

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

Source

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

Source

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.

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 Rocq only if there is an equation a.x = c for a,c a constant and a divides c if b= true

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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Polynomial.WithProof`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Polynomial.WithProofSource

Module `Polynomial.WithProof`Source