package coq-core

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

Install 

dune-project
 Dependency

coq.inria.fr Readme 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.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

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

Module Polynomial.LinPolySource

Linear(ised) polynomials represented as a Vect.t i.e a sorted association list. The constant is the coefficient of the variable 0

Each linear polynomial can be interpreted as a multi-variate polynomial. There is a bijection mapping between a linear variable and a monomial (see module MonT)

Sourcetype t = Vect.t

Each variable of a linear polynomial is mapped to a monomial. This is done using the monomial tables of the module MonT.

Sourcemodule MonT : sig ... end
Sourceval linpol_of_pol : Poly.t -> t

linpol_of_pol p linearise the polynomial p

Sourceval var : var -> t

var x

  • returns

    1.y where y is the variable index of the monomial x^1.

Sourceval coq_poly_of_linpol : (NumCompat.Q.t -> 'a) -> t -> 'a Mc.pExpr

coq_poly_of_linpol c p

  • parameter p

    is a multi-variate polynomial.

  • parameter c

    maps a rational to a Coq polynomial coefficient.

  • returns

    the coq expression corresponding to polynomial p.

Sourceval of_monomial : Monomial.t -> t

of_monomial m

  • returns

    1.x where x is the variable (index) for monomial m

Sourceval of_vect : Vect.t -> t

of_vect v

  • returns

    a1.x1 + ... + an.xn This is not the identity because xi is the variable index of xi^1

Sourceval variables : t -> Mutils.ISet.t

variables p

  • returns

    the set of variables of the polynomial p interpreted as a multi-variate polynomial

Sourceval is_variable : t -> var option

is_variable p

  • returns

    Some x if p = a.x for a >= 0

Sourceval is_linear : t -> bool

is_linear p

  • returns

    whether the multi-variate polynomial is linear.

Sourceval is_linear_for : var -> t -> bool

is_linear_for x p

  • returns

    true if the polynomial is linear in x i.e can be written c*x+r where c is a constant and r is independent from x

Sourceval constant : NumCompat.Q.t -> t

constant c

  • returns

    the constant polynomial c

search_linear pred p

  • returns

    a variable x such p = a.x + b such that p is linear in x i.e x does not occur in b and a is a constant such that pred a

Sourceval search_linear : (NumCompat.Q.t -> bool) -> t -> var option
Sourceval search_all_linear : (NumCompat.Q.t -> bool) -> t -> var list

search_all_linear pred p

  • returns

    all the variables x such p = a.x + b such that p is linear in x i.e x does not occur in b and a is a constant such that pred a

Sourceval product : t -> t -> t

product p q

  • returns

    the product of the polynomial p*q

Sourceval factorise : var -> t -> t * t

factorise x p

  • returns

    a,b such that p = a.x + b and x does not occur in b

Sourceval collect_square : t -> Monomial.t MonMap.t

collect_square p

  • returns

    a mapping m such that ms = s^2 for every s^2 that is a monomial of p

Sourceval monomials : t -> Mutils.ISet.t

monomials p

  • returns

    the set of monomials.

Sourceval degree : t -> int

degree p

  • returns

    return the maximum degree

Sourceval pp_var : Stdlib.out_channel -> var -> unit

pp_var o v pretty-prints a monomial indexed by v.

Sourceval pp : Stdlib.out_channel -> t -> unit

pp o p pretty-prints a polynomial.

Sourceval pp_goal : string -> Stdlib.out_channel -> (t * op) list -> unit

pp_goal typ o l pretty-prints the list of constraints as a Coq goal.