package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
doc/micromega_plugin/Micromega_plugin/Polynomial/WithProof/index.html
Module Polynomial.WithProof
Source
module WithProof
constructs polynomials packed with the proof that their sign is correct.
InvalidProof
is raised if the operation is invalid.
out_channel chan c
pretty-prints the constraint c
over the channel chan
const n
represents the tautology (n>=0)
cutting_plane p
does integer reasoning and adjust the constant to be integral
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
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.
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