Arith

The Arith tactic  is used to justify conclusions which follow from hypotheses by a restricted form of arithmetic reasoning. It is described fully in the appendix to written by Chan[2]. Roughly speaking, Arith knows about the ring axioms  for integer multiplication and addition, the total order axioms of <, the reflexivity, symmetry and transitivity of equality, and a limited form of substitutivity of equality. We will describe the class of problems decidable by Arith by giving an informal account of the procedure which Arith uses to decide whether or not C follows from H.

Arith understands standard arithmetic relations over the integers; namely terms of the form s < t, , s > t, , and . It also recognizes negations of these terms. As the only equalities Arith concerns itself with are those of the form , we will drop the and write only s = t in the rest of this description. The arith rule may be used to justify goals of the form

where each is a term denoting an arithmetic relation. If Arith can justify the goal it will produce subgoals requiring the user to show that the left- and right-hand sides of each denote integer terms. As a convenience Arith will attempt to prove goals in which not all of the are arithmetic relations; it simply ignores such disjuncts. If it is successful on such a goal, it will produce subgoals requiring the user to prove that each such disjunct is a well-formed proposition.

Arith analyzes the hypotheses of the goal to find relevant assumptions. In particular, it will maximally decompose each hypothesis into a term of the form (), and will use as an assumption any of the which are arithmetic relations of the form describe above. It also extracts assumptions from declarations of variables in types that are subsets of . For example from the declaration it extracts the assumption that .

Arith begins by normalizing  the relevant formulas of the goal according to the following conventions:

1. Rewrite each relation of the form as the equivalent . A conclusion C follows from such an assumption if it follows from either s<t or t<s; hence arith tries both cases. Henceforth, we assume that all negations of equalities have been eliminated from consideration.
2. Replace all occurrences of terms which are not addition, subtraction or multiplication by a new variable. Multiple occurrences of the same term are replaced by the same variable. Arith uses only facts about addition, subtraction and multiplication, so it treats all other terms as atomic. At this point all terms are built from integer constants and integer variables using +, - and .
3. Rewrite all terms as polynomials in canonical form  . The exact nature of the canonical form is irrelevant (the reader may think of it as the form used in high school algebra texts) but has the important property that any two equal terms are identical. Each term now has the form , where p and are nonconstant polynomials in canonical form, c and are constants, and is one of <, = or ( is equivalent to ).
4. Replace each nonconstant polynomial p by a new variable, with each occurrence of p being replaced by the same variable. This amounts to treating each nonconstant polynomial as an atom. Now each formula is of the form . Arith now decides whether or not the conclusion follows from the hypotheses by using the total order axioms of <, the reflexivity, symmetry, transitivity and substitutivity of =, and the following so-called trivial  monotonicity axioms (c and d are constants).
   • 
   • 
   These rules capture all of the acceptable forms of reasoning which may be applied to formulas in canonical form.