1\chapter{The arith Library} 2 3This document describes the facilities provided by the \ml{arith} library 4for the HOL system~\cite{description}. The main function is a partial decision 5procedure for a subset of linear natural number 6arithmetic\index{linear arithmetic}. There are also some associated functions, 7and some more general tools for normalisation and for increasing the power of 8proof procedures. 9 10The main function, \ml{ARITH\_CONV}, is a partial decision procedure for 11Presburger natural arithmetic\index{Presburger arithmetic}. Presburger natural 12arithmetic is the subset of arithmetic formulae made up from natural number 13constants, numeric variables, addition, multiplication by a constant, the 14relations on the natural numbers ($<$, $\leq$, $=$, $\geq$, $>$) and the 15logical connectives ($\neg$, $\wedge$, $\vee$, $\Rightarrow$, 16$\Leftrightarrow$, $\forall$, $\exists$). 17Products\index{products}\index{multiplication} of two expressions which both 18contain variables are not included in the subset, but the function 19{\small\verb%SUC%} which is not normally included in a specification of 20Presburger arithmetic are allowed in this \HOL\ implementation. 21 22\ml{ARITH\_CONV} further restricts the subset as follows: when the formula has 23been put in prenex normal form\index{prenex normal form} it must contain only 24one kind of quantifier, that is the quantifiers must either all be 25universal\index{quantifiers!universal} (`forall') or all 26existential\index{quantifiers!existential}. Variables may appear 27free\index{free variables} (unquantified) provided any quantifiers that do 28appear in the prenex normal form are universal; free variables are taken as 29being implicitly universally quantified so mixing them with existential 30quantifiers would violate the above restriction. 31 32\index{normalisation} 33The function makes use of a number of preprocessors\index{preprocessors} which 34extend the coverage beyond the subset specified above and which are also 35available as separate functions. Natural number subtraction\index{subtraction}, 36the predecessor function {\small\verb%PRE%}, and conditional 37statements\index{conditional statements} can be eliminated using the function 38\ml{SUB\_AND\_COND\_ELIM\_CONV}. Another preprocessor, \ml{INSTANCE\_T\_CONV}, 39permits substitution instances\index{instances}\index{substitution instances} 40of universally quantified formulae to be accepted. There is also a function 41for putting a formula into prenex normal form\index{prenex normal form}: 42\ml{PRENEX\_CONV}. 43 44 45\section{The method of proof} 46 47The main function, \ml{ARITH\_CONV}, is constructed from two separate 48procedures, one for universally quantified formulae (\ml{FORALL\_ARITH\_CONV}) 49and one for existentially quantified formulae (\ml{EXISTS\_ARITH\_CONV}). 50\ml{FORALL\_ARITH\_CONV}\index{quantifiers!universal} uses a variable 51elimination\index{variable elimination} technique similar to the one described 52by Hodes~\cite{VarElimHodes}\index{Hodes}. This procedure is 53incomplete\index{completeness} for the natural numbers\index{natural numbers}. 54In particular, it does not prove formulae which depend on the integral 55properties\index{integral properties} of natural numbers. 56 57\ml{EXISTS\_ARITH\_CONV}\index{quantifiers!existential} uses a technique of 58Shostak's~\cite{SUPINFShostak}\index{Shostak} based on the 59{\small SUP-INF}\index{SUP-INF method} method due to 60Bledsoe~\cite{SUPINFBledsoe}\index{Bledsoe}. This technique is able to find 61witnesses\index{witnesses} for the existentially quantified variables, that is 62values which satisfy\index{satisfaction of formulae} the formula. 63Unfortunately this method too is incomplete\index{completeness} for the 64natural numbers. The implementation used by \ml{EXISTS\_ARITH\_CONV} does not 65have a very good coverage. It could be improved but only at the expense of 66increased computation times. Despite the incompleteness, the procedure should 67be of some use. 68 69Both of the proof methods are described more fully in a 70report~\cite{EfficFullyExpTP} which also discusses techniques for writing 71efficient\index{efficient proof procedures} proof procedures in the \HOL\ 72system. 73 74 75\section{Using the library} 76 77The \ml{arith} library can be loaded into a user's \HOL\ session using the 78function \ml{load\_library}\index{load\_library@{\ptt load\_library}} (see the 79\HOL\ manual for a general description of library loading). The first action 80in the load sequence initiated by \ml{load\_library} is to update the \HOL\ 81help\index{help!updating search path} search path. The help search path is 82updated with a pathname to online help files for the \ML\ functions in the 83library. After updating the help search path, the \ml{reduce} 84library~\cite{reduce} is loaded. The \ml{arith} library makes use of some of 85the functions in the \ml{reduce} library. Finally, the \ML\ functions in the 86\ml{arith} library are loaded into \HOL. 87 88The following session shows how the \ml{arith} library may be loaded using 89\ml{load\_library}: 90 91\setcounter{sessioncount}{1} 92\begin{session}\begin{verbatim} 93#load_library `arith`;; 94Loading library `arith` ... 95Updating help search path 96.Loading library `reduce` ... 97Extending help search path. 98Loading boolean conversions........ 99Loading arithmetic conversions.................. 100Loading general conversions, rule and tactic..... 101Library `reduce` loaded. 102............................................................................. 103............................................................................. 104............................................................................. 105............................................................................. 106............................................................................. 107................................ 108Library `arith` loaded. 109() : void 110 111# 112\end{verbatim}\end{session} 113 114\noindent 115The arithmetic proof procedure can be called by applying the conversion 116\ml{ARITH\_CONV}: 117 118\begin{session}\begin{verbatim} 119#ARITH_CONV "!m n p. m < n /\ n < p ==> m < p";; 120|- (!m n p. m < n /\ n < p ==> m < p) = T 121\end{verbatim}\end{session} 122 123\noindent 124It is easy to define a function which returns a theorem directly corresponding 125to the arithmetic formula: 126 127\begin{session}\begin{verbatim} 128#let ARITH_PROVE = EQT_ELIM o ARITH_CONV;; 129ARITH_PROVE = - : conv 130 131#ARITH_PROVE "!m n p. m < n /\ n < p ==> m < p";; 132|- !m n p. m < n /\ n < p ==> m < p 133\end{verbatim}\end{session} 134 135 136\section{Using the procedure to prove a formula false} 137 138Continuing the session from the previous section, here is an example of how 139to use the proof procedure to prove that a formula is 140false\index{false!proof of}\index{proving false}: 141 142\begin{session}\begin{verbatim} 143#NEGATE_CONV ARITH_CONV "!m n. m < n";; 144|- (!m n. m < n) = F 145 146#NEGATE_CONV ARITH_CONV "?m n. (m + n) < 0";; 147|- (?m n. (m + n) < 0) = F 148\end{verbatim}\end{session} 149 150\noindent 151\ml{NEGATE\_CONV} works by applying the proof procedure to the 152negation\index{negation} of the formula. This means that when proving a 153universally quantified formula false, the main procedure is actually trying to 154prove that an existentially quantified formula is true. One could define a 155function that proves formulae either true or false, but this would be 156inefficient as for certain examples it would apply \ml{ARITH\_CONV} twice. The 157author anticipates that in most circumstances the user will know whether the 158formula is true or false and can therefore apply either \ml{ARITH\_CONV} or 159\ml{NEGATE\_CONV ARITH\_CONV} as appropriate. A combined function is 160illustrated below: 161 162\begin{session}\begin{verbatim} 163#let TF_ARITH_CONV = ARITH_CONV ORELSEC NEGATE_CONV ARITH_CONV;; 164TF_ARITH_CONV = - : conv 165 166#TF_ARITH_CONV "!m n p. m < n /\ n < p ==> m < p";; 167|- (!m n p. m < n /\ n < p ==> m < p) = T 168 169#TF_ARITH_CONV "!m n. m < n";; 170|- (!m n. m < n) = F 171\end{verbatim}\end{session} 172 173 174\section{Constructing a tactic} 175 176Consider the following goal\index{goals}: 177 178\begin{session}\begin{verbatim} 179#g "!x y t. x /\ ((~(t + 3 = 0)) => F | y) = y /\ x";; 180"!x y t. x /\ ((~(t + 3 = 0)) => F | y) = y /\ x" 181 182() : void 183\end{verbatim}\end{session} 184 185\noindent 186\ml{ARITH\_CONV} can be used as a tactic\index{tactics} as illustrated below: 187 188\begin{session}\begin{verbatim} 189#expand (CONV_TAC ARITH_CONV);; 190OK.. 191evaluation failed ARITH_CONV -- formula not in the allowed subset 192\end{verbatim}\end{session} 193 194\noindent 195This fails because the arithmetic conversion is only being applied to the 196whole goal. To simplify the goal it is necessary to apply the conversion 197deep\index{depth conversion} within the goal: 198 199\begin{session}\begin{verbatim} 200#let DEPTH_ARITH_TAC = CONV_TAC (ONCE_DEPTH_CONV ARITH_CONV);; 201DEPTH_ARITH_TAC = - : tactic 202 203#expand DEPTH_ARITH_TAC;; 204OK.. 205"!x y t. x /\ (T => F | y) = y /\ x" 206 207() : void 208\end{verbatim}\end{session} 209