package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

doc/micromega_plugin/Micromega_plugin/Vect/index.html

Module Micromega_plugin.VectSource

Sourcetype var = int

Variables are simply (positive) integers.

Sourcetype t

The type of vectors or equivalently linear expressions. The current implementation is using association lists. A list (0,c),(x1,ai),...,(xn,an) represents the linear expression c + a1.xn + ... an.xn where ai are rational constants and xi are variables.

Note that the variable 0 has a special meaning and represent a constant. Moreover, the representation is spare and variables with a zero coefficient are not represented.

Sourcetype vector = t

Generic functions

hash equal and compare so that Vect.t can be used as keys for Set Map and Hashtbl

Sourceval hash : t -> int
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int

Basic accessors and utility functions

Sourceval pp_gen : (Stdlib.out_channel -> var -> unit) -> Stdlib.out_channel -> t -> unit

pp_gen pp_var o v prints the representation of the vector v over the channel o

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

pp o v prints the representation of the vector v over the channel o

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

pp_smt o v prints the representation of the vector v over the channel o using SMTLIB conventions

Sourceval variables : t -> Mutils.ISet.t

variables v returns the set of variables with non-zero coefficients

Sourceval get_cst : t -> NumCompat.Q.t

get_cst v returns c i.e. the coefficient of the variable zero

Sourceval decomp_cst : t -> NumCompat.Q.t * t

decomp_cst v returns the pair (c,a1.x1+...+an.xn)

Sourceval decomp_at : var -> t -> NumCompat.Q.t * t

decomp_at xi v returns the pair (ai, ai+1.xi+...+an.xn)

Sourceval decomp_fst : t -> (var * NumCompat.Q.t) * t
Sourceval cst : NumCompat.Q.t -> t

cst c returns the vector v=c+0.x1+...+0.xn

Sourceval is_constant : t -> bool

is_constant v holds if v is a constant vector i.e. v=c+0.x1+...+0.xn

Sourceval null : t

null is the empty vector i.e. 0+0.x1+...+0.xn

Sourceval is_null : t -> bool

is_null v returns whether v is the null vector i.e equal v null

Sourceval get : var -> t -> NumCompat.Q.t

get xi v returns the coefficient ai of the variable xi. get is also defined for the variable 0

Sourceval set : var -> NumCompat.Q.t -> t -> t

set xi ai' v returns the vector c+a1.x1+...ai'.xi+...+an.xn i.e. the coefficient of the variable xi is set to ai'

Sourceval mkvar : var -> t

mkvar xi returns 1.xi

Sourceval update : var -> (NumCompat.Q.t -> NumCompat.Q.t) -> t -> t

update xi f v returns c+a1.x1+...+f(ai).xi+...+an.xn

Sourceval fresh : t -> int

fresh v return the fresh variable with index 1+ max (variables v)

Sourceval choose : t -> (var * NumCompat.Q.t * t) option

choose v decomposes a vector v depending on whether it is null or not.

  • returns

    None if v is null

  • returns

    Some(x,n,r) where v = r + n.x x is the smallest variable with non-zero coefficient n <> 0.

Sourceval from_list : NumCompat.Q.t list -> t

from_list l returns the vector c+a1.x1...an.xn from the list of coefficient l=c;a1;...;an

Sourceval to_list : t -> NumCompat.Q.t list

to_list v returns the list of all coefficient of the vector v i.e. c;a1;...;an The list representation is (obviously) not sparsed and therefore certain ai may be 0

Sourceval decr_var : int -> t -> t

decr_var i v decrements the variables of the vector v by the amount i. Beware, it is only defined if all the variables of v are greater than i

Sourceval incr_var : int -> t -> t

incr_var i v increments the variables of the vector v by the amount i.

Sourceval gcd : t -> NumCompat.Z.t

gcd v returns gcd(num(c),num(a1),...,num(an)) where num extracts the numerator of a rational value.

Sourceval normalise : t -> t

normalise v returns a vector with only integer coefficients

Linear arithmetics

Sourceval add : t -> t -> t

add v1 v2 is vector addition.

  • parameter v1

    is of the form c +a1.x1 +...+an.xn

  • parameter v2

    is of the form c'+a1'.x1 +...+an'.xn

  • returns

    c1+c1'+ (a1+a1').x1 + ... + (an+an').xn

Sourceval mul : NumCompat.Q.t -> t -> t

mul a v is vector multiplication of vector v by a scalar a.

  • returns

    a.v = a.c+a.a1.x1+...+a.an.xn

Sourceval mul_add : NumCompat.Q.t -> t -> NumCompat.Q.t -> t -> t

mul_add c1 v1 c2 v2 returns the linear combination c1.v1+c2.v2

Sourceval subst : int -> t -> t -> t

subst x v v' replaces x by v in vector v'

Sourceval div : NumCompat.Q.t -> t -> t

div c1 v1 returns the mutiplication by the inverse of c1 i.e (1/c1).v1

Sourceval uminus : t -> t

uminus v

  • returns

    -v the opposite vector of v i.e. (-1).v

Iterators

Sourceval fold : ('acc -> var -> NumCompat.Q.t -> 'acc) -> 'acc -> t -> 'acc

fold f acc v returns f (f (f acc 0 c ) x1 a1 ) ... xn an

Sourceval fold_error : ('acc -> var -> NumCompat.Q.t -> 'acc option) -> 'acc -> t -> 'acc option

fold_error f acc v is the same as fold (fun acc x i -> match acc with None -> None | Some acc' -> f acc' x i) (Some acc) v but with early exit...

Sourceval find : (var -> NumCompat.Q.t -> 'c option) -> t -> 'c option

find f v returns the first f xi ai such that f xi ai <> None. If no such xi ai exists, it returns None

Sourceval for_all : (var -> NumCompat.Q.t -> bool) -> t -> bool

for_all p v returns /\_>=0 (f xi ai)

Sourceval exists2 : (NumCompat.Q.t -> NumCompat.Q.t -> bool) -> t -> t -> (var * NumCompat.Q.t * NumCompat.Q.t) option

exists2 p v v' returns Some(xi,ai,ai') if p(xi,ai,ai') holds and ai,ai' <> 0. It returns None if no such pair of coefficient exists.

Sourceval dotproduct : t -> t -> NumCompat.Q.t

dotproduct v1 v2 is the dot product of v1 and v2.

Sourceval map : (var -> NumCompat.Q.t -> 'a) -> t -> 'a list
Sourceval abs_min_elt : t -> (var * NumCompat.Q.t) option
Sourceval partition : (var -> NumCompat.Q.t -> bool) -> t -> t * t
Sourcemodule Bound : sig ... end