Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> sec:abstractAs of version 2.7, the ACL2 theorem prover has been extended to automatically verify sets of polynomial inequalities that include nonlinear relationships. In this paper we describe our mechanization of linear and nonlinear arithmetic in ACL2. The nonlinear arithmetic procedure operates in cooperation with the pre-existing ACL2 linear arithmetic decision procedure. It extends what can be automatically verified with ACL2, thereby eliminating the need for certain types of rules in ACL2’s database while simultaneously increasing the performance of the ACL2 system when verifying arithmetic conjectures. The resulting system lessens the human effort required to construct a large arithmetic proof by reducing the number of intermediate lemmas that must be proven to verify a desired theorem. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge, this is the first generally useful proof-producing implementation of such an algorithm. While many problems within the domain are intractable, we demonstrate convincing examples of its value in interactive theorem proving. <s> BIB002 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination procedures: for Presburger arithmitics and for linear real arithmetics. <s> BIB003 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> When goals fall in decidable logic fragments, users of proof-assistants expect automation. However, despite the availability of decision procedures, automation does not come for free. The reason is that decision procedures do not generate proof terms. In this paper, we show how to design efficient and lightweight reflexive tactics for a hierarchy of quantifier-free fragments of integer arithmetics. The tactics can cope with a wide class of linear and non-linear goals. For each logic fragment, off-the-shelf algorithms generate certificates of infeasibility that are then validated by straightforward reflexive checkers proved correct inside the proof-assistant. This approach has been prototyped using the Coq proofassistant. Preliminary experiments are promising as the tactics run fast and produce small proof terms. <s> BIB004 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> Techniques based on sums of squares appear promising as a general approach to the universal theory of reals with addition and multiplication, i.e. verifying Boolean combinations of equations and inequalities. A particularly attractive feature is that suitable 'sum of squares' certificates can be found by sophisticated numerical methods such as semidefinite programming, yet the actual verification of the resulting proof is straightforward even in a highly foundational theorem prover. We will describe our experience with an implementation in HOL Light, noting some successes as well as difficulties. We also describe a new approach to the univariate case that can handle some otherwise difficult examples. <s> BIB005 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and Taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction. <s> BIB006 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> One can reduce the problem of proving that a polynomial is nonnegative, or more generally of proving that a system of polynomial inequalities has no solutions, to finding polynomials that are sums of squares of polynomials and satisfy some linear equality (Positivstellensatz). This produces a witness for the desired property, from which it is reasonably easy to obtain a formal proof of the property suitable for a proof assistant such as Coq. The problem of finding a witness reduces to a feasibility problem in semidefinite programming, for which there exist numerical solvers. Unfortunately, this problem is in general not strictly feasible, meaning the solution can be a convex set with empty interior, in which case the numerical optimization method fails. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty. We implemented our method and illustrate its use with examples, including extractions of proofs to Coq. <s> BIB007 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Linear inequalities <s> This paper presents a formalization in higher-order logic of a practical representation of multivariate Bernstein polynomials. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies for formally and automatically solving polynomial global optimization problems. <s> BIB008
Taking into account the fact that the field of real numbers is ordered requires more complicated procedures. So, before tackling polynomial inequalities, we first consider only procedures dedicated to linear inequalities, e.g. 2x + 3y < 3z ⇒ y ≥ z ⇒ 5x < 0. Coq provides the fourier tactic (superseded by lra in recent versions) based on Fourier-Motzkin quantifier elimination for solving universally-quantified systems of linear inequalities. HOL Light provides a similar algorithm with REAL ARITH. This procedure is also able to perform some algebraic manipulations and to handle functions like maximum and absolute value though. Isabelle/HOL provides a ferrack tactic that provides a quantifier elimination inspired by Ferrante and Rackoff's algorithm (Chaieb 2008) . While it only tackles linear inequalities, the actual coefficients can be polynomials. Another provided procedure is mir; it is designed to solve linear systems that combine both real arithmetic and a floor function BIB003 . For ACL2(r), the decision procedures of ACL2 for linear arithmetic over rational numbers are available BIB001 . As for PVS, the SIMPLIFY command has a decision procedure for linear inequalities, and thus, so do commands built upon it, e.g. GRIND. 5.1.3. Other inequalities Finally, let us have a look at polynomial and transcendental inequalities. HOL Light comes with a quantifier-elimination procedure for real arithmetic named REAL ELIM CONV BIB002 . Such procedures are known to have a high complexity (doubly exponential time), which may prevent their use in practice. In some cases, especially univariate, a decision procedure based on Positivstellensatz refutations and sums of squares may be more efficient to prove systems of polynomial inequalities. HOL Light was the first system to come with such a procedure BIB005 ; the REAL SOS function has not been integrated to the core system though. This implementation was later ported to Coq (psatz, BIB004 ) and Isabelle/HOL (sos). All of these decision procedures rely on csdp, an external solver for semi-definite program-ming problems. Due to the approximated computations of this solver, these procedures might fail to deduce a correct sum of squares and thus to prove valid goals. There exist improvements to this approach but they have not yet made their way into the procedures above BIB007 . PVS provides some strategies based on numerical computations: numerical performs interval arithmetic to verify inequalities involving transcendental functions BIB006 ); bernstein performs global optimization based on Bernstein polynomials to verify systems of polynomial inequalities BIB008 . The computational power of C-CoRN allows one to prove polynomial and transcendental inequalities just by computing the values with enough precision as long as there are no indeterminates. This feature may even be used in a proof based on the standard library by using the equivalence lemma proved in  . Such computations are also available for the other formalizations based on Cauchy sequences, though they may be less efficient