package coq-core

  1. Overview
  2. No Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

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 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 saturate_subst : bool -> t list -> t list