package coq

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

Module Polynomial.WithProofSource

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

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct