Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Real Arithmetic <s> Abstract. We provide a package of strategies for automation of non-linear arithmetic in PVS. Inparticular, we describe a simplification procedure for the field of real numbers and a strategy for cancellationof common terms.Key words, non-linear arithmetic, PVS strategies, real number automationSubject classification. Computer Science1. Introduction. While conducting research on the formal safety analysis of Air Traffic Management(ATM) systems at the NASA Langley Research Center [2, 3, 6], we have found the verification system PVS[7] very well suited for specifying avionics systems. Avionics systems are hybrid systems, that is, they aredigital systems that interact with the continuous physical environment where they are deployed. These twolevels of dynamics, discrete and continuous, can be easily modeled using PVS higher-order logic. Despitethat, deductive methods, such as theorem proving, are not usually the first approach for modeling andverification of hybrid systems. Most of the literature on verification of hybrid systems concerns variationsof algorithmic methods, such as model checking, on restricted sub-classes of the general problem. This canbe explained by the fact that although theorem provers based on higher-order logic, e.g., PVS [7], Coq [1],Isabelle-HOL [8], integrate expressive specification languages with powerful theorem provers, they lack ofadequate support for continuous mathematics.The PVS system, for instance, incorporates a rich type system supporting predicate sub-typing anddependent types. It also comes with a set of decision procedures that solve problems in a broad range ofdecidable fields. Moreover, it includes in the prelude library a large collection of properties for real numbers(for example, real_props and real_axioms) that are applied automatically by the decision procedures.This is true except for non-linear ones, i.e., those involving multiplication or division of non-numeric terms.Indeed, the PVS command (GRIND :theories "real_props"), although useful in several cases, fails todischarge a simple non-linear formula such as(1.1) aa+_+ 1 - b -- 1 <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Real Arithmetic <s> We present a new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system. The efficiency is improved to a point that we can now prove equalities that were previously beyond reach. A special care has been taken to implement efficient algorithms while keeping the complexity of the correctness proofs low. This leads to a single tool, with a single implementation, which can be addressed for a ring or for a semi-ring, abstract or not, using the Leibniz equality or a setoid equality. This example shows that such reflective methods can be effectively used in symbolic computation. <s> BIB002
First, let us have a look at methods dedicated to proving properties on rational and real numbers. This section is not meant to be exhaustive, especially as systems like HOL Light and Isabelle/HOL are generous when it comes to decision procedures. Instead, it is meant to give an overview about the capabilities of various systems. Note that systems may also provide some help in manipulating expressions. For instance, in PVS, the Manip arithmetic package  does not aim at automatically solving goals but at an easy handling of both equalities and inequalities. This set of algebraic manipulation strategies allows one, for example, to easily move terms from one side to the other or to cancel terms. There is no heavy automation here, but a practical handling of equalities and inequalities that comes close to pen-and-paper manipulations. 5.1.1. Algebraic equalities Presumably, the feature the most sought of when it comes to real numbers is the ability to perform algebraic rearrangements to prove universal equalities over real numbers. The Coq proof assistant comes with a tactic ring that makes it possible to automatically prove equalities between two polynomials, e.g. a 2 − b 2 = (a + b)(a − b). This tactic behaves by first normalizing each side of the equality and then comparing them BIB002 . The field variant of the tactic can cope with divisions; it normalizes the goal to rational functions instead of polynomials  . The ring tactic is quite generic and has been instantiated on the real numbers from the MathClasses library. PVS provides a FIELD strategy similar to Coq's field, but adapted to PVS specificities BIB001 . The basic GRIND strategy is extended with additional theories reals props and extra reals props as GRIND-REALS. It is very efficient, but as GRIND, it may not terminate. The REAL RING and REAL FIELD decision procedures of HOL Light, the algebra strategy of Isabelle/HOL, and the nsatz tactic of Coq play a similar role. They are slightly more powerful though, as they do not normalize terms in isolation. Instead they use Gröbner bases and thus can handle the equational theories of integral domains and fields Wenzel 2007, Pottier 2008) .