package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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

Module Polynomial.WithProofSource

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 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)

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

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
Sourceval 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

Sourceval 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