package coq

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

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)

type 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.

module MonT : sig ... end
val linpol_of_pol : Poly.t -> t

linpol_of_pol p linearise the polynomial p

val var : var -> t

var x

  • returns

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

val 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.

val of_monomial : Monomial.t -> t

of_monomial m

  • returns

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

val 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

val variables : t -> Mutils.ISet.t

variables p

  • returns

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

val is_variable : t -> var option

is_variable p

  • returns

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

val is_linear : t -> bool

is_linear p

  • returns

    whether the multi-variate polynomial is linear.

val 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

val 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

val search_linear : (NumCompat.Q.t -> bool) -> t -> var option
val 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

val product : t -> t -> t

product p q

  • returns

    the product of the polynomial p*q

val factorise : var -> t -> t * t

factorise x p

  • returns

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

val 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

val monomials : t -> Mutils.ISet.t

monomials p

  • returns

    the set of monomials.

val degree : t -> int

degree p

  • returns

    return the maximum degree

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

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

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

pp o p pretty-prints a polynomial.

val 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.

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