package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

exception InvalidProof

InvalidProof is raised if the operation is invalid.

val compare : t -> t -> int
val annot : string -> t -> t
val of_cstr : (cstr * ProofFormat.prf_rule) -> t
val output : out_channel -> t -> unit

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

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

zero represents the tautology (0=0)

val const : NumCompat.Q.t -> t

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

val 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

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 : (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 * (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.

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

val subst1 : t list -> t list

subst1 sys performs a single substitution

val saturate_subst : bool -> t list -> t list
val is_substitution : bool -> t -> var option